Formalization of simplification for context-free grammars

TL;DR

This paper formalizes the process of simplifying context-free grammars using the Coq proof assistant, ensuring that language equivalence is preserved through various elimination operations.

Contribution

It provides a formal proof of the correctness of grammar simplification operations within a proof assistant, enhancing reliability in language processing.

Findings

Proved correctness of useless symbol elimination

Proved correctness of inaccessible symbol elimination

Proved correctness of empty and unit rule eliminations

Abstract

Context-free grammar simplification 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 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.