For posterity.
Start with undecidable Post Correspondence Problem, or PCP:
Given two lists of words $(u_1,\dots,u_n)$ and $(v_1,\dots,v_n)$ does
there exist a sequence of indices such that $u_{i_1}\dots u_{i_k} = v_{i_1}\dots v_{i_k}$?
The language will consist of PCP over $\{a,b\}$ that have a solution, coded as string $(u_1;v_1) \dots (u_n;v_n) $ with $u_i,v_i \in \{a,b\}^*$.
The grammar will generate a PCP instance, and non-deterministically an attempt for a solution. Then equality of the two strings is tested by deleting matching letters.
The equality check is more easily done when one of the strings is stored in reverse, so we will generate $u^R_{i_k} \dots u^R_{i_1} X v_{i_1}\dots v_{i_k}$.
Generate an instance of PCP.
- $ I \to (W;W) I \mid (W;W) $ (add a pair of words)
- $ W \to a W \mid b W \mid \varepsilon $ (generate a word)
Copy one of the pairs of PCP and move it to the pair of words around $X$ that should be equal.
- $ D \tau \to \tau D$ for $\tau = a,b,(,),;$
- $ D ( \to ( L $ (pair selected)
- $ L ; \to ; R $
- $ R ) \to ) $
- $ L \sigma \to \sigma L_\sigma L $ for $\sigma = a,b$ (make a copy)
$ R \sigma \to \sigma R_\sigma R $ for $\sigma = a,b$
$ L_\sigma \tau = \tau L_\sigma $ for $\sigma = a,b$ and $\tau = a,b,(,),;$ (move right)
$ R_\sigma \tau = \tau R_\sigma $ for $\sigma = a,b$ and $\tau = a,b,(,),;$
$ L_\sigma X \to \sigma X$ (drop copy to the left of $X$, it will
reverse)
- $ R_\sigma X \to X \sigma$ (drop copy to the right of $X$)
Check equality
- $ X \to Z $
- $ \sigma Z \sigma \to Z$ for $\sigma = a,b$
Start. The $\#$ marks the end of the string, or rather the end of the solution that is generated. The last rule will delete it and at the same time test whether the solution has been completely removed by the earlier rules checking equality.
- $ S \to C I X \#$
- $ C \to C D \mid D $ for generating the solution, copy several word pairs
Done
PS. Most constructions for a non-context-sensitive language use diagonalization on context-sensitive grammars to get a language that is still recursive. This one is not recursive, but recursively enumerable.
Indeed many rules are context-sensitive (or rather monotonic/non-contracting). But especially note the rules like $aZa\to Z$: they shorten the string. These are definitely type-0 and not monotonic, and they are essential. After the computation they delete the proposed solution of PCP. Like a scratch tape used by a Turing machine.
PS2. Although the intuitive meaning of each of the productions is explained above, it is not very simple to formally prove the grammar is correct. This is mostly due to the parallellism. There are many nonterminals moving around in the grammar at the same time independently (for instance, when a copy of a PCP pair $(u_i,v_i)$ is made all these letters move in a row to the right; also we can start looking for the next pair to copy even before the last one was finished). This makes it hard to formulate invariants. It takes some time to check that all nonterminals keep in a proper order, for instance. Fortunately none of the moving nonterminals can overtake one another.
For this reason analysing Turing Machines sometimes is less complicated. Only the reading/writing head is moving around.
Example (added by Andremoniy)
Consider simplest case: $(a;a)$. For this string derivation sequence will be:
$S\Rightarrow CIX\Rightarrow D(W;W)X\Rightarrow C(a;a)X\Rightarrow D(a;a)X\Rightarrow (La;a)X\Rightarrow (aL_aL;a)X\Rightarrow (aL_a;Ra)X\Rightarrow (a;L_aRa)X\Rightarrow (a;L_a aR_aR)X\Rightarrow (a;aL_aR_aR)X\Rightarrow (a;aL_aR_a)X\Rightarrow (a;aL_a)R_aX\Rightarrow (a;a)L_aR_aX\Rightarrow (a;a)L_aXa\Rightarrow (a;a)aXa\Rightarrow (a;a)aZa\Rightarrow (a;a)Z\Rightarrow (a;a)$
