Formalization of context-free language theory

TL;DR

This paper formalizes key results in context-free language theory using Coq, including closure properties, grammar simplification techniques, and Chomsky Normal Form, enhancing rigor and reproducibility in formal language research.

Contribution

It provides a comprehensive Coq formalization of fundamental context-free language results, which was previously lacking in the literature.

Findings

Formal proof of closure properties for context-free languages

Algorithms for grammar simplification implemented and verified

Proof of existence of Chomsky Normal Form for context-free grammars

Abstract

Context-free language theory is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of fundamental results related to context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols inaccessible symbols, empty rules and unit rules) and the existence of a Chomsky Normal Form for context-free grammars.