Formalization of context-free language theory

Abstract

Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different such tools are being increasingly used in order to accelerate and simplify proof checking, and the Coq proof assistant is one of the most known and used. Language and automata theory is a well-established area of mathematics, relevant to computer science foundations and information technology. In particular, context-free language theory is of fundamental importance in the analysis, design and implementation of computer programming languages. This work describes a formalization effort, using the Coq proof assistant, of fundamental results of the classical theory of 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), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. To achieve this, several steps had to be fulfilled, including (i) understanding of the characteristics, importance and benefits of mathematical formalization, specially in computer science, (ii) familiarization with the underlying mathematical theories used in proof assistants, (iii) familiarization with the Coq proof assistant, (iv) review of the strategies used in the informal proofs of the main results of the context-free language theory and finally (iv) selection and adequation of the representation and proof strategies adopted in order the achieve the desired objectives. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the remarkable result that is the formalization of the Pumping Lemma for context-free languages. The perspectives for the further development of this work are diverse and can be grouped in three different areas: inclusion of new devices and results, code extraction and general enhancements of its libraries.