Jana Hofmann: Bachelor's Thesis
Verified Algorithms for Context-Free Grammars in Coq
Advisor: Prof. Dr. Gert Smolka
Abstract:
We give a basic formalization of context-free grammars and the languages they describe in the proof assistant Coq. We show the decidability of the word and the emptiness problem of context-free languages by giving and verifying decision procedures. Furthermore, we describe four grammar transformations: The elimination of empty rules, the elimination of unit rules, the separation of characters from the rest of the grammar and the binarization of a grammar. For each transformation, we show that it preserves the language of the grammar. Together, they yield a grammar which is in Chomsky normal form.
We aim for algorithms that are easy to understand and verify. Many of our results are obtained with finite iteration on lists. By using abstractions of fixed point and closure iterations, the correctness of the algorithms is intuitive and formally obtained with short proofs.
References
-
A formalisation of the theory of context-free languages in higher order logic (2010)
Aditi Barthwal
-
Three models for the description of language (1956)
Noam Chomsky
-
Certified CYK parsing of context-free languages (2014)
Denis Firsov and Tarmo Uustalu
-
Certified normalization of context-free grammars (2015)
Denis Firsov and Tarmo Uustalu
-
Introduction to Automata Theory, Languages and Computation (1979)
John E. Hopcroft and Jeffrey D. Ullman
-
Validating LR (1) parsers (2012)
Jacques-Henri Jourdan, François Pottier, and Xavier Leroy
-
Trx: A formally verified parser interpreter (2010)
Adam Koprowski and Henri Binsztok
-
Automata and Computability (1997)
Dexter C. Kozen
-
Formalization of context-free language theory (2016)
Marcus V. M. Ramos
-
Introduction to computational logic. Lecture Notes [PDF] (2014)
Gert Smolka and Chad E. Brown
-
The coq reference manual, version 8.5 (July 2016)
The Coq Development Team
Dowloads
Legal notice, Privacy policy
