turing machines – What is appearance checking in the context of formal grammars?

Appearance checking is a concept in the theory of regulated grammars.

In an ordinary (context-free) grammar we may appay a production to a string if its right-hand side occurs in that string.
So for $pi: Ato alpha$ we write $x Rightarrow_pi y$ if $x= w_1 A w_2$ and $y = w_1alpha w_2$.

In a regulated grammar we may specify the order in which the productions should occur in the derivation.
As an example, the following context free grammar

$pi_0: Sto AC$, $pi_1: Ato aAb$, $pi_2: Cto cC$, $pi_3: Ato ab$, $pi_4: Cto c$

generates the language ${ a^nb^nc^m mid m,nge 1}$.
As a regulated grammar we can choose to restrict the sequences of chosen productions to be the (regular) language $pi_0(pi_1pi_2)^*pi_3pi_4$. Clearly with this restriction the grammar generates the non context-free language ${ a^nb^nc^n mid nge 1}$.

Appearance checking is the notion that we are allowed to skip a production if it cannot be applied. Formally for $pi: Ato alpha$ we write $x Rightarrow^{ac}_pi y$ if either (i) $x$ contains $A$ and $x Rightarrow_pi y$ or (ii) $x$ does not contain $A$ and $x=y$.

How it this useful? It can be used to check that actually all symbols in the string are rewritten before the derivation continues. Consider the productions $pi_1: Ato BB$, $pi_2: Ato X$, $pi_5: Bto a$ and the “regulator” $pi_1^*pi_2pi_5^*$, and starting with the string $A^n$. In this case the variable $X$ cannot be rewritten. So applying the production $pi_2$ has to be avoided. This is allowed in appearance checking mode when $A$ does not occur in the string. That means we have to rewrite all $A$‘s into $B$‘s, then we can skip $pi_2$, and continue rewriting the $B$‘s.
This trick can be extended into a grammar that generates ${a^{2^n} mid nge 0}$:

$pi_1: Ato BB$, $pi_2: Ato X, pi_3: Bto A$, $pi_4: Bto X, pi_5: Bto a$ and “regulator” $(pi_1^*pi_2pi_3^*pi_4)^* pi_5^*$