Document Open Access Logo

Closure Properties of General Grammars – Formally Verified

Authors Martin Dvorak , Jasmin Blanchette

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.15.pdf
  • Filesize: 0.68 MB
  • 16 pages

Document Identifiers

Author Details

Martin Dvorak
  • Institute of Science and Technology Austria, Klosterneuburg, Austria
Jasmin Blanchette
  • Ludwig-Maximilians-Universität München, Germany

Funding

  • Blanchette, Jasmin: 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).

Acknowledgements

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.

Cite AsGet BibTex

Martin Dvorak and Jasmin Blanchette. Closure Properties of General Grammars – Formally Verified. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.15

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
Keywords
  • Lean
  • type-0 grammars
  • recursively enumerable languages
  • Kleene star

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Alfred V. Aho and Jeffrey D. Ullman. The Theory of Parsing, Translation, and Compiling. Prentice Hall, 1st edition, 1972. Google Scholar
  2. Andrea Asperti and Wilmer Ricciotti. Formalizing Turing Machines. In Logic, Language, Information and Computation, volume 7456 of Lecture Notes in Computer Science, pages 1-25. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32621-9_1.
  3. Frank J. Balbach. The Cook-Levin theorem. Archive of Formal Proofs, 2023. , Formal proof development. URL: https://isa-afp.org/entries/Cook_Levin.html.
  4. Aditi Barthwal and Michael Norrish. Mechanisation of PDA and Grammar Equivalence for Context-Free Languages. In Anuj Dawar and Ruy de Queiroz, editors, WoLLIC 2010, volume 6188 of Lecture Notes in Computer Science, pages 125-135. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13824-9_11.
  5. Patricia L. Carlson, Grzegorz Bancerek, and Im Pan. Context-Free Grammar - Part 1. J. Formaliz. Math., 1992. URL: http://mizar.org/JFM/pdf/lang1.pdf.
  6. Mario Carneiro. Formalizing Computability Theory via Partial Recursive Functions. In John Harrison, John O'Leary, and Andrew Tolmach, editors, ITP 2019, volume 141 of LIPIcs, pages 12:1-12:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.12.
  7. Jing-Chao Chen and Yatsuka Nakamura. Introduction to Turing Machines. J. Formaliz. Math., 9(4), 2001. URL: https://fm.mizar.org/2001-9/pdf9-4/turing_1.pdf.
  8. Claudio Sacerdoti Coen. A Constructive Proof of the Soundness of the Encoding of Random Access Machines in a Linda Calculus with Ordered Semantics. In Carlo Blundo and Cosimo Laneve, editors, ICTCS 2003, volume 6188 of Lecture Notes in Computer Science, pages 37-57. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45208-9_5.
  9. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors, CADE-25, volume 9195 of Lecture Notes in Computer Science, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  10. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A Metaprogramming Framework for Formal Verification. Proc. ACM Program. Lang., 1(ICFP):1-29, 2017. URL: https://doi.org/10.1145/3110278.
  11. Denis Firsov and Tarmo Uustalu. Certified Normalization of Context-Free Grammars. In CPP 2015, pages 167-174. ACM, 2015. URL: https://doi.org/10.1145/2676724.2693177.
  12. Yannick Forster and Fabian Kunze. A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. In John Harrison, John O'Leary, and Andrew Tolmach, editors, ITP 2019, volume 141 of LIPIcs, pages 17:1-17:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.17.
  13. Yannick Forster, Fabian Kunze, and Marc Roth. The Weak Call-by-Value Lambda-Calculus is Reasonable for Both Time and Space. Proc. ACM Program. Lang., 4(POPL):27:1-27:23, 2019. URL: https://doi.org/10.1145/3371095.
  14. Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke. A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. In Liron Cohen and Cezary Kaliszyk, editors, ITP 2021, volume 193 of LIPIcs, pages 19:1-19:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.19.
  15. Yannick Forster, Fabian Kunze, and Maximilian Wuttke. Verified Programming of Turing Machines in Coq. In CPP 2020, pages 114-128. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373816.
  16. Yannick Forster and Gert Smolka. Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. In Mauricio Ayala-Rincón and César A. Muñoz, editors, ITP 2017, volume 10499 of Lecture Notes in Computer Science, pages 189-206. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_13.
  17. Lennard Gäher and Fabian Kunze. Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. In Liron Cohen and Cezary Kaliszyk, editors, ITP 2021, volume 193 of LIPIcs, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.20.
  18. John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Pearson/Addison Wesley, 3rd edition, 2007. Google Scholar
  19. Fulya Horozal, Florian Rabe, and Michael Kohlhase. Flexary Operators for Formalized Mathematics. In Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, and Josef Urban, editors, Intelligent Computer Mathematics, Lecture Notes in Computer Science, pages 312-327. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08434-3_23.
  20. Fabian Kunze, Gert Smolka, and Yannick Forster. Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. In Sukyoung Ryu, editor, APLAS 2018, volume 11275 of Lecture Notes in Computer Science, pages 264-283. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02768-1_15.
  21. Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. URL: https://era.ed.ac.uk/bitstream/handle/1842/12487/Luo1990.Pdf.
  22. The mathlib Community. The Lean Mathematical Library. In Jasmin Blanchette and Cătălin Hritcu, editors, CPP 2020, pages 367-381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  23. Yasuhiko Minamide. Verified Decision Procedures on Context-Free Grammars. In Klaus Schneider and Jens Brandt, editors, TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science, pages 173-188. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74591-4_14.
  24. Michael Norrish. Mechanised Computability Theory. In Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, ITP 2011, volume 6898 of Lecture Notes in Computer Science, pages 297-311. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22863-6_22.
  25. Marcus Vinícius Midena Ramos. Formalization of Context-Free Language Theory. Bull. Symbol. Log., 25(2):214-214, 2019. URL: https://doi.org/10.1017/bsl.2019.3.
  26. Jian Xu, Xingyuan Zhang, and Christian Urban. Mechanising Turing Machines and Computability Theory in Isabelle/HOL. In Interactive Theorem Proving, volume 7998, pages 147-162. Springer Berlin Heidelberg, 2013. Lecture Notes in Computer Science. URL: https://doi.org/10.1007/978-3-642-39634-2_13.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact