Greibach Normal Form

Alexander Haberl 📧, Tobias Nipkow 📧 and Akihisa Yamada 📧

August 27, 2025

Abstract

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.

License

BSD License

Topics

Session Greibach_Normal_Form

Depends on

Cite

× 
@article{Greibach_Normal_Form-AFP,
  author  = {Alexander Haberl and Tobias Nipkow and Akihisa Yamada},
  title   = {Greibach Normal Form},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/Greibach_Normal_Form.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download