2026-07-20T12:09:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5985 2024-03-06T10:37:27Z ddc:004 open_access

Formal Languages, Formally and Coinductively Traytel, Dmitriy Formal languages codatatypes corecursion coinduction interactive theorem proving Isabelle HOL 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dmitriy Traytel 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.31 urn:nbn:de:0030-drops-59853 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.31 eng https://creativecommons.org/licenses/by/3.0/legalcode