License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.31
URN: urn:nbn:de:0030-drops-59853
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5985/
Go to the corresponding LIPIcs Volume Portal

Traytel, Dmitriy

Formal Languages, Formally and Coinductively

pdf-format:
LIPIcs-FSCD-2016-31.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{traytel:LIPIcs:2016:5985,
  author =	{Dmitriy Traytel},
  title =	{{Formal Languages, Formally and Coinductively}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5985},
  URN =		{urn:nbn:de:0030-drops-59853},
  doi =		{10.4230/LIPIcs.FSCD.2016.31},
  annote =	{Keywords: Formal languages, codatatypes, corecursion, coinduction, interactive theorem proving, Isabelle HOL}
}

Keywords: Formal languages, codatatypes, corecursion, coinduction, interactive theorem proving, Isabelle HOL
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI