Email Gateway (Aug 19 2022 at 12:32): Email Gateway (Aug 19 2022 at 12:32):From: Tobias Nipkow <nipkow@in.tum.de>
As Gerwin warned you: Some new submissions for 2013-1 will become available in
the next few days. This is the first one:
Dmitriy Traytel: A Codatatype of Formal Languages
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.
http://afp.sourceforge.net/entries/Coinductive_Languages.shtml
Last updated: Apr 23 2024 at 08:19 UTC