Traytel, Dmitriy - Formal Languages, Formally and Coinductively

lmcs:3943 - Logical Methods in Computer Science, September 19, 2017, Volume 13, Issue 3
Formal Languages, Formally and Coinductively

Authors: Traytel, Dmitriy

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.


Source : oai:arXiv.org:1611.09633
DOI : 10.23638/LMCS-13(3:28)2017
Volume: Volume 13, Issue 3
Published on: September 19, 2017
Submitted on: May 31, 2017
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages


Share

Browsing statistics

This page has been seen 61 times.
This article's PDF has been downloaded 17 times.