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!

Last updated: Sep 13 2025 at 04:22 UTC