Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Greibach Normal Form


view this post on Zulip Email Gateway (Sep 12 2025 at 20:42):

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!

view this post on Zulip Email Gateway (Sep 13 2025 at 08:27):

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