Jana Hofmann: Bachelor's Thesis

Saarland University Computer Science

Verified Algorithms for Context-Free Grammars in Coq

Advisor: Prof. Dr. Gert Smolka


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.



Legal notice, Privacy policy