Greibach Normal Form

Alexander Haberl 📧, Tobias Nipkow 📧 and Akihisa Yamada 📧

August 27, 2025

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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