Document Open Access Logo

Formal Languages, Formally and Coinductively

Author Dmitriy Traytel

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.31.pdf
  • Filesize: 0.49 MB
  • 17 pages

Document Identifiers

Author Details

Dmitriy Traytel

Cite AsGet BibTex

Dmitriy Traytel. Formal Languages, Formally and Coinductively. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.31

Abstract

Traditionally, formal languages are defined as sets of words. More recently, the alternative coalgebraic or coinductive representation as infinite tries, i.e., prefix trees branching over the alphabet, has been used to obtain compact and elegant proofs of classic results in language theory. In this paper, we study this representation in the Isabelle proof assistant. We define regular operations on infinite tries and prove the axioms of Kleene algebra for those operations. Thereby, we exercise corecursion and coinduction and confirm the coinductive view being profitable in formalizations, as it improves over the set-of-words view with respect to proof automation.
Keywords
  • Formal languages
  • codatatypes
  • corecursion
  • coinduction
  • interactive theorem proving
  • Isabelle HOL

Metrics

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

References

  1. Andreas Abel and Brigitte Pientka. Wellfounded recursion with copatterns: A unified approach to termination and productivity. In G. Morrisett and T. Uustalu, editors, ICFP'13, pages 185-196. ACM, 2013. Google Scholar
  2. Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: programming infinite structures by observations. In R. Giacobazzi and R. Cousot, editors, POPL'13, pages 27-38. ACM, 2013. Google Scholar
  3. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In ITP 2014, volume 8558 of LNCS, pages 93-110. Springer, 2014. Google Scholar
  4. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Foundational extensible corecursion. In J. Reppy, editor, ICFP 2015, pages 192-204. ACM, 2015. Google Scholar
  5. Filippo Bonchi, Marcello M. Bonsangue, Jan J. M. M. Rutten, and Alexandra Silva. Brzozowski’s algorithm (co)algebraically. In R.L. Constable and A. Silva, editors, Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday, volume 7230 of LNCS, pages 12-23. Springer, 2012. Google Scholar
  6. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In R. Giacobazzi and R. Cousot, editors, POPL'13, pages 457-468. ACM, 2013. Google Scholar
  7. Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, 1964. URL: http://dx.doi.org/10.1145/321239.321249.
  8. Adam Chlipala. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013. URL: http://mitpress.mit.edu/books/certified-programming-dependent-types.
  9. Eduardo Giménez and Pierre Castéran. A tutorial on [co-]inductive types in Coq. 1998. URL: http://www.labri.fr/perso/casteran/RecTutorial.pdf.
  10. Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In M. Blume, N. Kobayashi, and G. Vidal, editors, FLOPS 2010, volume 6009 of LNCS, pages 103-117. Springer, 2010. Google Scholar
  11. Ralf Hinze. Concrete stream calculus: An extended study. J. Funct. Program., 20(5-6):463-535, 2010. Google Scholar
  12. Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222-259, 1997. Google Scholar
  13. Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput., 110(2):366-390, 1994. Google Scholar
  14. Dexter Kozen and Alexandra Silva. Practical coinduction. Technical report, Cornell University, 2012. URL: http://hdl.handle.net/1813/30510.
  15. Alexander Krauss and Tobias Nipkow. Proof pearl: Regular expression equivalence and relation algebra. J. Automated Reasoning, 49:95-106, 2012. published online March 2011. Google Scholar
  16. Andreas Lochbihler and Johannes Hölzl. Recursive functions on lazy lists via domains and topologies. In G. Klein and R. Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 341-357. Springer, 2014. Google Scholar
  17. Tobias Nipkow and Gerwin Klein. Concrete Semantics: With Isabelle/HOL. Springer, 2014. URL: http://www.in.tum.de/~nipkow/Concrete-Semantics.
  18. Lawrence C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. J. Logic Comp., 7(2):175-204, 1997. Google Scholar
  19. Lawrence C. Paulson. A formalisation of finite automata using hereditarily finite sets. In A.P. Felty and A. Middeldorp, editors, CADE-25, volume 9195 of LNCS, pages 231-245. Springer, 2015. Google Scholar
  20. Tillmann Rendel, Julia Trieflinger, and Klaus Ostermann. Automatic refunctionalization to a language with copattern matching: with applications to the expression problem. In K. Fisher and J.H. Reppy, editors, ICFP 2015, pages 269-279. ACM, 2015. Google Scholar
  21. Jurriaan Rot, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Coinductive proof techniques for language equivalence. In A. Horia Dediu, C. Martín-Vide, and B. Truthe, editors, LATA 2013, volume 7810 of LNCS, pages 480-492. Springer, 2013. Google Scholar
  22. Jurriaan Rot, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Proving language inclusion and equivalence by coinduction. Inf. Comput., 246:62-76, 2016. Google Scholar
  23. J. J. M. M. Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249:3-80, 2000. Google Scholar
  24. Jan J. M. M. Rutten. Automata and coinduction (an exercise in coalgebra). In D. Sangiorgi and R. de Simone, editors, CONCUR 1998, volume 1466 of LNCS, pages 194-218. Springer, 1998. URL: http://dx.doi.org/10.1007/BFb0055624.
  25. Anton Setzer. How to reason coinductively informally. To appear in R. Kahle, T. Strahm, and T. Studer (Eds.): Festschrift on occasion of Gerhard Jäger’s 60th birthday. Available from http://www.cs.swan.ac.uk/~csetzer/articles/jaeger60Birthdaymain.pdf, 2015.
  26. Alexandra Silva. A short introduction to the coalgebraic method. ACM SIGLOG News, 2(2):16-27, 2015. Google Scholar
  27. Dmitriy Traytel. A codatatype of formal languages. In Archive of Formal Proofs. 2013. URL: http://afp.sf.net/entries/Coinductive_Languages.shtml.
  28. Dmitriy Traytel. A coalgebraic decision procedure for WS1S. In Stephan Kreutzer, editor, CSL 2015, volume 41 of LIPIcs, pages 487-503. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  29. Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette. Foundational, compositional (co)datatypes for higher-order logic - Category theory applied to theorem proving. In LICS 2012, pages 596-605. IEEE Computer Society, 2012. Google Scholar
  30. Dmytro Traytel. Formalizing Symbolic Decision Procedures for Regular Languages. PhD thesis, TU München, 2015. URL: http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20151016-1273011-1-9.
  31. Philip Wadler. The Expression Problem. Available online at: http://tinyurl.com/wadler-ep, 1998.
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