Greibach’s Hardest Context-Free Language

Tobias Nipkow 📧

August 25, 2026

Abstract

Formalization of Greibach’s hardest context-free language theorem: There is a “hardest” context-free language $L_0$ such that every context-free language is an inverse homomorphic image of $L_0$.

License

BSD License

Note

Claude was used to produce the initial version of the theory based on Greibach's paper.

Topics

Related publications

Session Greibach_Hardest

Depends on

Cite

× 
@article{Greibach_Hardest-AFP,
  author  = {Tobias Nipkow},
  title   = {Greibach’s Hardest Context-Free Language},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/Greibach_Hardest.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download