The following exercise is inspired by an old exam question (note that this is not the question):
Let us define a single-letter alphabet $\Sigma = \{a\}$ and the language $L = \{ w \in \Sigma^*: |w| = 2^n, n \in \mathbb Z_+\}$. (In other words, $L = \{a^2, a^4, a^8, \ldots \}$.) What is an unrestricted grammar for $L$?
I thought of a solution using binary number representation. Consider the grammar:
$S \rightarrow 10TaX$
$T \rightarrow 0T | \epsilon$
$0a \rightarrow aa0$
$0X \rightarrow X$
$1a \rightarrow a1$
$1X \rightarrow \epsilon$
$\epsilon$ signifies the empty string. Using the first two production rules, we can produce a string of the type $10^naX$, for example $100aX$. One route here to get rid of the non-terminal symbols is $100aX \Rightarrow 10aa0X \Rightarrow 1aa0a0X \Rightarrow 1aaaa00X \Rightarrow 1aaaa0X$ $\Rightarrow 1aaaaX \Rightarrow \ldots \Rightarrow aaaa1X \Rightarrow aaaa = a^4$.
Assuming that this solution is correct, one interesting thing about it is that by modifying the third production rule to $0a \rightarrow a^k0$ one can get a restriction-free grammar for strings of length $k^n$ instead. But maybe there is a cleaner solution, so I am interested in seeing other examples of unrestricted grammars for the language.
However, here comes the actual question: the existence of an unrestricted grammar for $L$ only proves that it is recursively enumerable. Therefore I would like to ask for an unrestricted grammar of $\overline{L}$ (then we have one proof that $L$ is a Turing-decidable language).
Edit: In case the question here is unclear, please read the discussion in the comments.