Closure Properties of General Grammars -- Formally Verified
Martin Dvorak, Jasmin Blanchette
TL;DR
The paper reports the formalization of general grammars (type-0) in Lean 3 and uses this framework to prove closure of type-0 languages under union, reversal, concatenation, and Kleene star. It develops a grammar-based approach, including a novel construction for Kleene star, and encodes grammars, derivations, and languages within the Lean/mathlib ecosystem (~12,500 lines of code). The authors describe both a detailed proof sketch and a formalization, with explicit commentary on abstractions, lifting techniques, and the complexity of certain arguments. The work demonstrates that grammar-based formalisms can yield rigorous, constructive proofs in a proof assistant and lays groundwork for extending formal verification to broader parts of the Chomsky hierarchy, including potential equivalence with Turing machines.
Abstract
We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.