Email Gateway (May 28 2025 at 22:53): Email Gateway (May 28 2025 at 22:53):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
The AFP is climbing down the Chomsky hierarchy. Type-2 is here:
Context-Free Grammars and Languages
by Tobias Nipkow, Markus Gschoßmann, Felix Krayer, Fabian Lehr, Bruno Philipp, August Martin Stimpfle, Kaan Taskin, and Akihisa Yamada
This is a basic library of definitions and results about context-free grammars and languages. It includes context-free grammars and languages, parse trees, Chomsky normal form, pumping lemmas and the relationship of right-linear grammars to finite automata.
https://www.isa-afp.org/entries/Context_Free_Grammar.html
Enjoy! Or as Randall Munroe would interject: GRAMMAR! (https://xkcd.com/1090/).
Last updated: Jun 20 2025 at 12:44 UTC