From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
Alexander Haberl, Tobias Nipkow, and Akihisa Yamada are expanding our ever-growing collection of results on context-free grammars. And this one even has bad_grammar®!
Greibach Normal Form
This theory formalizes Hopcroft and Ullman’s algorithm to transform a set of productions into Greibach Normal Form (GNF). We concentrate on the essential property of the GNF: every production starts with a terminal; the tail of a rhs may contain further terminals. The complexity of the algorithm can be exponential.
https://www.isa-afp.org/entries/Greibach_Normal_Form.html
Enjoy!
From: Alex Shkotin <alex.shkotin@gmail.com>
Dear Dmitriy and All,
Let me add by association the GNF usage (PDF) Program structure
<https://www.researchgate.net/publication/45865036_Program_structure>
This may be enjoyable.
BR
Alex
пт, 12 сент. 2025 г. в 23:42, Dmitriy Traytel <
cl-isabelle-users@lists.cam.ac.uk>:
Dear all,
Alexander Haberl, Tobias Nipkow, and Akihisa Yamada are expanding our
ever-growing collection of results on context-free grammars. And this one
even has bad_grammar®!Greibach Normal Form
This theory formalizes Hopcroft and Ullman’s algorithm to transform a set
of productions into Greibach Normal Form (GNF). We concentrate on the
essential property of the GNF: every production starts with a terminal; the
tail of a rhs may contain further terminals. The complexity of the
algorithm can be exponential.https://www.isa-afp.org/entries/Greibach_Normal_Form.html
Enjoy!
Last updated: Oct 08 2025 at 20:22 UTC