TL;DR
This paper formalizes general (type-0) grammars in Lean 3, proving closure properties under union, reversal, concatenation, and Kleene star with novel grammar-based constructions, contrasting with traditional Turing machine approaches.
Contribution
It provides the first formal proof of closure properties of type-0 languages using a proof assistant, introducing new grammar-based methods for Kleene star closure.
Findings
Closure under union, reversal, concatenation, and Kleene star proven
Novel grammar-based construction for Kleene star closure
Formal verification using Lean 3 enhances reliability of results
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
