TL;DR
This paper explores the coinductive representation of formal languages as infinite tries within the Isabelle proof assistant, demonstrating its advantages in proof automation and formal reasoning about language operations.
Contribution
It formalizes regular operations on infinite tries and proves Kleene algebra axioms, showcasing the benefits of coinductive methods in language theory formalizations.
Findings
Coinductive representation improves proof automation.
Formalization of Kleene algebra axioms on infinite tries.
Enhanced reasoning about regular languages in Isabelle.
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 article, 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.