Closure properties of general grammars - formally verified
Dvorak M, Blanchette J. 2023. Closure properties of general grammars - formally verified. 14th International Conference on Interactive Theorem Proving. ITP: International Conference on Interactive Theorem Proving, LIPIcs, vol. 268, 15.
Download
Conference Paper
| Published
| English
Scopus indexed
Author
Dvorak, MartinISTA 
;
Blanchette, Jasmin
;
Blanchette, JasminCorresponding author has ISTA affiliation
Department
Series Title
LIPIcs
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.
Publishing Year
Date Published
2023-07-27
Proceedings Title
14th International Conference on Interactive Theorem Proving
Publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Acknowledgement
Jasmin Blanchette: This research has received funding from the Netherlands Organization
for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).
__
We thank Vladimir Kolmogorov for making this collaboration possible. We
thank Václav Končický for discussing ideas about the Kleene star construction. We thank Patrick Johnson, Floris van Doorn, and Damiano Testa for their small yet very valuable contributions to our code. We thank Eric Wieser for simplifying one of our proofs. We thank Mark Summerfield for suggesting textual improvements. We thank the anonymous reviewers for very helpful comments. Finally, we thank the Lean community for helping us with various technical issues and answering many questions.
Volume
268
Article Number
15
Conference
ITP: International Conference on Interactive Theorem Proving
Conference Location
Bialystok, Poland
Conference Date
2023-07-31 – 2023-08-04
ISBN
eISSN
IST-REx-ID
Cite this
Dvorak M, Blanchette J. Closure properties of general grammars - formally verified. In: 14th International Conference on Interactive Theorem Proving. Vol 268. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.ITP.2023.15
Dvorak, M., & Blanchette, J. (2023). Closure properties of general grammars - formally verified. In 14th International Conference on Interactive Theorem Proving (Vol. 268). Bialystok, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ITP.2023.15
Dvorak, Martin, and Jasmin Blanchette. “Closure Properties of General Grammars - Formally Verified.” In 14th International Conference on Interactive Theorem Proving, Vol. 268. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.ITP.2023.15.
M. Dvorak and J. Blanchette, “Closure properties of general grammars - formally verified,” in 14th International Conference on Interactive Theorem Proving, Bialystok, Poland, 2023, vol. 268.
Dvorak M, Blanchette J. 2023. Closure properties of general grammars - formally verified. 14th International Conference on Interactive Theorem Proving. ITP: International Conference on Interactive Theorem Proving, LIPIcs, vol. 268, 15.
Dvorak, Martin, and Jasmin Blanchette. “Closure Properties of General Grammars - Formally Verified.” 14th International Conference on Interactive Theorem Proving, vol. 268, 15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:10.4230/LIPIcs.ITP.2023.15.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
2023_LIPIcS_Dvorak.pdf
715.98 KB
Access Level
Open Access
Date Uploaded
2023-08-07
MD5 Checksum
773a0197f05b67feaa6cb1e17ec3642d
Export
Marked PublicationsOpen Data ISTA Research Explorer
Sources
arXiv 2302.06420
Google Scholar
ISBN Search