2026-07-22T21:50:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18390 2024-03-06T11:01:46Z ddc:004 open_access

Closure Properties of General Grammars – Formally Verified Dvorak, Martin Blanchette, Jasmin Lean type-0 grammars recursively enumerable languages Kleene star 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Martin Dvorak and Jasmin Blanchette 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.15 urn:nbn:de:0030-drops-183906 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15 eng https://creativecommons.org/licenses/by/4.0/legalcode