Context-Free Language Theory Formalization

TL;DR

This paper formalizes key aspects of context-free language theory within the Coq proof assistant, including closure properties and grammar simplification, to enhance formal verification in computer science and language processing.

Contribution

It introduces a formalization of context-free grammar properties and simplification techniques in Coq, advancing the use of proof assistants in formal language theory.

Findings

Formalized closure properties for context-free grammars

Proved correctness of grammar simplification operations

Enhanced formal verification methods in language processing

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 tools are being increasingly used in order to accelerate and simplify proof checking. Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This proposal aims at formalizing parts of context-free language theory in the Coq proof assistant. This report presents the underlying theory and general characteristics of proof assistants, including Coq itself, discusses its use in relevant formalization projects, presents the current status of the implementation, addresses related projects and the contributions of this work. The results obtained so far include the formalization of closure properties for context-free grammars (under union, concatenation and closure) and the formalization of grammar simplification. Grammar simplification is a subject of high importance in computer language processing technology as well as in formal language theory, and the formalization refers to the fact that general context-free grammars generate languages that can be also generated by simpler and equivalent context-free grammars. Namely, useless symbol elimination, inaccessible symbol elimination, unit rules elimination and empty rules elimination operations were described and proven correct with respect to the preservation of the language generated by the original grammar.