### Abstract

We define formal languages as a codataype of infinite trees branching over the alphabet. Each node in such a tree indicates whether the path to this node constitutes a word inside or outside of the language. This codatatype is isormorphic to the set of lists representation of languages, but caters for definitions by corecursion and proofs by coinduction.

Regular operations on languages are then defined by primitive corecursion. A difficulty arises here, since the standard definitions of concatenation and iteration from the coalgebraic literature are not primitively corecursive-they require guardedness up-to union/concatenation. Without support for up-to corecursion, these operation must be defined as a composition of primitive ones (and proved being equal to the standard definitions). As an exercise in coinduction we also prove the axioms of Kleene algebra for the defined regular operations.

Furthermore, a language for context-free grammars given by productions in Greibach normal form and an initial nonterminal is constructed by primitive corecursion, yielding an executable decision procedure for the word problem without further ado.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Session Coinductive_Languages

- Coinductive_Language
- Coinductive_Regular_Set
- Context_Free_Grammar

### Depends on

- Regular Sets and Expressions

### Used by

- Derivatives of Logical Formulas

### Auto-related entries

- Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
- Kleene Algebra with Tests and Demonic Refinement Algebras

## Cite

×

Coinductive_Languages-AFP

    @article{Coinductive_Languages-AFP,
      author  = {Dmitriy Traytel},
      title   = {A Codatatype of Formal Languages},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Coinductive_Languages.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1