Open access
Autor(in)
Datum
2017-09-19Typ
- Journal Article
ETH Bibliographie
yes
Altmetrics
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. Mehr anzeigen
Persistenter Link
https://doi.org/10.3929/ethz-b-000241647Publikationsstatus
publishedExterne Links
Zeitschrift / Serie
Logical Methods in Computer ScienceBand
Seiten / Artikelnummer
Verlag
Technische Universität BraunschweigThema
Computer Science; Logic in Computer Science,Computer Science; Programming LanguagesETH Bibliographie
yes
Altmetrics