Certified normalization of context-free grammars

Denis Firsov and Tarmo Uustalu



Every context-free grammar can be transformed into an equivalent one which is in Chomsky normal form. In our work, we divide normalization procedure into four independant transformations and prove their correctness in Agda programming language. Also, we show that if transformations are combined in the right order then Chomsky normal form is achieved and correctness is preserved. Since our work is done in the constructive setting then soundness and completeness could be used as functions for converting between parse trees in original and normalized grammars.


[pdf, code (Agda 2.4.2; standard library 0.8.1)]