Proof any CFG can be converted to GNF

Question

I studied algorithm for converting grammars to GNF and was wondering about a proof that any CFG can be converted into GNF. I found this paper - ENGELFRIET, Joost. An Elementary Proof of Double Greibach Normal Form, 1992, but I do not understand the proof at all.

Any CFG can be converted into CNF, so we try to prove that any grammar in CNF can be converted into GNF.

At first, a grammar H (not GNF, but can be easily converted into GNF by substitution and by removing rules containing empty string) is constructed from original CNF denoted G as follows:

1) for rules Y → a $$ A \rightarrow a[Y,A] $$ 2) for rules C → DQ $$ [D, A] \rightarrow Q[C, A] $$ 3) $$ [A, A] \rightarrow \epsilon $$

Than there are mentioned two statements about this new grammar. These statements are essential for the proof, because they show that the grammar H is equivalent to G. And I do not know why they are right:

$$ ([Y,A] \rightarrow^*_H w) \iff (A \rightarrow ^*_G Y w) $$ and $$ (A \rightarrow^*_H w) \iff (A \rightarrow ^*_G w) $$

There is also written that these statements can be shown by induction. I tried to prove them but it seems to me that to prove one of them, I also need to prove the second. So I am stuck at cycle.

Could somebody please explain it to me?

Answer 1

The textbook proofs of Greibach NF I have seen, contain endless substitutions. This way to construct GrNF is much crisper.

The key is to understand what the nonterminal $[Y,A]$ actually represents. It means a derivation that has a leftward "backbone" which starts from $A$ and ends just before $Y$, as in the picture below.

Now the first production in $H$ can be explained as follows. If I start with $A$ and want to produce GrNF then I must generate a terminal. We choose to generate the leftmost terminal $a$ of the subtree under $A$. So, we produce $a$, but we still must find a derivation $[Y,A]$ of the form in the picture, where $Y$ is the nonterminal that actually produces $a$ using the available production $Y\to a$.