License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.15
URN: urn:nbn:de:0030-drops-183906
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18390/
Dvorak, Martin ;
Blanchette, Jasmin
Closure Properties of General Grammars – Formally Verified
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.
BibTeX - Entry
@InProceedings{dvorak_et_al:LIPIcs.ITP.2023.15,
author = {Dvorak, Martin and Blanchette, Jasmin},
title = {{Closure Properties of General Grammars – Formally Verified}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {15:1--15:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18390},
URN = {urn:nbn:de:0030-drops-183906},
doi = {10.4230/LIPIcs.ITP.2023.15},
annote = {Keywords: Lean, type-0 grammars, recursively enumerable languages, Kleene star}
}
