text:
\section{Introduction}
\label{sec:intro}

If we ask a computer scientist what a formal language is, the answer will most
certainly be: a set of words. Here, we advocate another valid answer: an
infinite trie. This is the coalgebraic approach to
languages~\cite{Rutten98}, viewed through the lens of a lazy functional programmer.

This article shows how to formalize the coalgebraic or coinductive approach to
formal languages in the Isabelle/HOL proof assistant in the form of a gentle
introduction to corecursion and coinduction. Our interest in the coalgebraic
approach to formal languages arose in the context of a larger formalization effort of coalgebraic decision procedures for regular
languages~\cite{Traytel-CSL15,phd-traytel}. Indeed, we present here a reusable
library modeling languages, which lies at the core of those formalized decision
procedures. A lesson we have learned from this exercise and hope to convey here
is that often it is worthwhile to look at well-understood objects from a
different (in this case coinductive) perspective.

The literature is abound with tutorials on coinduction. So why bother writing
yet another one? First, because we finally can do it in Isabelle\slash HOL,
which became a coinduction-friendly proof assistant
recently~\cite{BlanchetteHLPPT-ITP14}. Earlier studies of coinduction in
Isabelle had to engage in tedious manual constructions just to define a
coinductive datatype~\cite{Paulson97}. Second, coinductive techniques are still not as
widespread as they could be (and we believe should be, since they constitute a
convenient proof tool for questions about semantics). Third, many
tutorials~\cite{Jacobs1997,KozenS12,Hinze10,Chlipala13,GimenezC98,setzer15},
with or without a theorem prover, exercise streams to the extent that one starts
to believe having seen every single stream example one can imagine.
In contrast, Rutten~\cite{Rutten98} demonstrates that it is entirely feasible to
start a tutorial with a structure slightly more complicated than streams, but
familiar to every computer scientist. Moreover, Rot, Bonsangue,
and Rutten \cite{RotBR13,RotBR16} present an accessible introduction to
coinduction up to congruence using the coinductive view of formal languages.
Our work additionally focuses on
corecursion up-to and puts Rutten's exposition in the context of a proof
assistant.

When programming with infinite structures in the total setting of a proof
assistant, productivity must be ensured. Intuitively, a corecursive function is
productive if it always eventually yields observable output, e.g., in form of a
constructor. %
Functions that output exactly one constructor before proceeding corecursively or stopping with a fixed (non-corecursive) value
are called primitively corecursive---a fragment dual to well-understood
primitively recursive functions on inductive datatypes. Primitively corecursive
functions are productive. While sophisticated methods involving domain,
measure, and category theory for handling more complex corecursive
specifications have been proposed~\cite{HoelzlL-ITP14,BlanchettePT-ICFP15} and implemented in Isabelle~\cite{BlanchetteBLPT}, we
explore here how far primitive corecursion can get us. Restricting ourselves to
this fragment is beneficial in several ways. First, our constructions become
mostly Isabelle independent, since primitive corecursion is supported by all
coinduction-friendly proof assistants. Second, when working in the restricted
setting, we quickly hit and learn to understand the limits. In fact, we will face
some non-primitively corecursive specifications on infinite tries, which we
reduce to a composition of primitively corecursive specifications. Those
reductions are insightful and hint at a general pattern for handling certain
non-primitively corecursive specifications.

Infinite data structures are often characterized in terms of observations. For
infinite tries, which we define as a coinductive datatype or short codatatype
(Section~\ref{sec:3:trie}), we can observe the root, which in our case is
labeled by a Boolean value. This label determines if the empty word is
\emph{accepted} by the trie. Moreover, we can observe the immediate subtrees of
a trie, of which we have one for each alphabet letter. This observation
corresponds to making transitions in an automaton or rather computing the left
quotient $L_a = \{w \mid \Cons{a}{w} \in L\}$ of the language $L$ by the letter
$a$. Indeed, we will see that Brzozowski's ingenious derivative
operation~\cite{Brzozowski64}, which mimics this computation recursively on the
syntax of regular expressions, arises very naturally when defining regular
operations corecursively on tries (Section~\ref{sec:3:corec}). To validate our
definitions, we formally prove by coinduction that they satisfy the axioms of
Kleene algebra. Thereby, we use two similar but different coinduction principles for equalities and inequalities (Section~\ref{sec:3:coind}). %
After having presented our formalization, we step back and connect concrete
intuitive notions (such as tries) with abstract coalgebraic terminology
(Section~\ref{sec:3:coalg}). Furthermore, we discuss our formalization and its
relation to other work on corecursion and coinduction with or without proof
assistants~(Section~\ref{sec:3:discuss}). %

This article extends the homonymous FSCD 2016 paper~\cite{Traytel-FSCD16} with the definition of the shuffle product on tries (Subsection~\ref{subsec:shuffle}), a trie construction for context-free grammars (Subsection~\ref{subsec:cfg}), the coinductive treatment of inequalities (Subsection~\ref{ssec:3:sim}) instead of reducing them to equalities, and the proof that the trie construction for context-free grammars is sound~(Subsection~\ref{ssec:3:cfg}).
The material presented here is based on the publicly available
Isabelle\slash HOL formalization~\cite{Traytel-AFP13} and is partly described in
the author's Ph.D.\ thesis~\cite{phd-traytel}.

\PARA{Preliminaries}

Isabelle/HOL is a proof assistant for higher-order logic, built around a small
trusted inference kernel. The kernel accepts only non-recursive type and
constant definitions. High-level specification mechanisms, which allow the user
to enter (co)recursive specifications, reduce this input to something equivalent
but non-recursive. The original (co)recursive specification is later derived as
a theorem. For a comprehensive introduction to Isabelle/HOL we refer to a recent
textbook~\cite[Part \Rmnum{1}]{Concrete}.

In Isabelle/HOL types $\tau$ are built from type variables $\alpha$, $\beta$,
etc., via type constructors~$\kappa$ written postfix (e.g., $\alpha\;\kappa$).
Some special types are the sum type $\alpha + \beta$, the product type $\alpha
\times \beta$, and the function type $\alpha \to \beta$, for which the type
constructors are written infix. Infix operators bind less tightly than the
postfix or prefix ones. Other important types are the type of Booleans ${\ty{bool}}$
inhabited by exactly two different values $\top$ (truth) and $\bot$ (falsity)
and the types $\listT{\alpha}$ and $\setT{\alpha}$ of lists and sets of elements
of type $\alpha$. %
For Boolean connectives and sets common mathematical notation is used. A special
constant is equality ${=} \mathrel{:\mskip-.5mu:} \alpha \to \alpha \to {\ty{bool}}$, which is
polymorphic (it exists for any type, including the function type, on which it is
extensional, i.e., $(\forall x.\; f\;x=g\;x) \longrightarrow f = g$). %
The functions ${\const{Inl}}$ and ${\const{Inr}}$ are the standard embeddings of $+$.
Lists are constructed from $\Nil\mathrel{:\mskip-.5mu:} \listT{\alpha}$ and $\mathbin{\#} \mathrel{:\mskip-.5mu:}
\alpha\to\listT{\alpha}\to\listT{\alpha}$; the latter written infix and often
omitted, i.e., we write $\Cons{a}{w}$ for $a \mathbin{\#} w$. Likewise, list concatenation $\mathbin{+\kern-4pt+}$ is written infix and may be omitted. The notation
$\length{\mathit{w}}$ stands for the length of the list $\mathit{w}$, i.e., $\length{\Nil} =
0$ and $\length{\Cons{a}{\mathit{w}}}=1+\length{\mathit{w}}$.

\section{Languages as Infinite Tries}
\label{sec:3:trie}

We define the type of formal languages as a codatatype of infinite tries, that
is, (prefix) trees of infinite depth branching over the alphabet. We represent
the alphabet by the type parameter~$\alpha$. Each node in a trie carries a
Boolean label, which indicates whether the (finite) path to this node
constitutes a word inside or outside of the language. The function type models
branching: for each letter $x \mathrel{:\mskip-.5mu:} \alpha$ there is a subtree, which we call
\emph{$x$-subtree}. %
\begin{quotex}
${\keyw{codatatype}}~\langT{\alpha} = {\const{L}}~({\omicron}: {\ty{bool}})~({\delta}: \alpha\to\langT{\alpha})$
\end{quotex}

The ${\keyw{codatatype}}$ command defines the type $\langT{\alpha}$ together with a
\emph{constructor} ${\const{L}}\mathrel{:\mskip-.5mu:}{\ty{bool}} \to (\alpha\to\langT{\alpha}) \to
\langT{\alpha}$ and two \emph{selectors} ${\omicron}\mathrel{:\mskip-.5mu:}\langT{\alpha}\to{\ty{bool}}$
and ${\delta}\mathrel{:\mskip-.5mu:}\langT{\alpha}\to\alpha\to\langT{\alpha}$. For a binary
alphabet $\alpha = \{a,\,b\}$, the trie $\mathit{even}$ shown in
Figure~\ref{fig:3:even} is an inhabitant of $\langT{\alpha}$. The label
of its root is given by $\final{\mathit{even}} = \top$ and its subtrees by another
trie $\deriv{\mathit{even}}{a} = \deriv{\mathit{even}}{b} = \mathit{odd}$. Similarly, we have
$\final{\mathit{odd}} = \bot$ and $\deriv{\mathit{odd}}{a} = \deriv{\mathit{odd}}{b} = \mathit{even}$.
Note that we could have equally written $\mathit{even} =
{\const{L}}\;\top\;(\lambda\_.\;\mathit{odd})$ and $\mathit{odd} =
{\const{L}}\;\bot\;(\lambda\_.\;\mathit{even})$ to obtain the same mutual characterization
of $\mathit{even}$ and $\mathit{odd}$.

\begin{figure}[h]
\centering
\begin{tikzpicture}[node distance=3em]
\node (eps) {$\top$};
\node[below left of=eps, xshift=-2em] (a) {$\bot$};
\node[below right of=eps, xshift=2em] (b) {$\bot$};
\node[below left of=a] (aa) {$\top$};
\node[below right of=a] (ab) {$\top$};
\node[below left of=b] (ba) {$\top$};
\node[below right of=b] (bb) {$\top$};
\node[below of=aa, yshift=2ex] (aax) {$\ldots$};
\node[below of=ab, yshift=2ex] (abx) {$\ldots$};
\node[below of=ba, yshift=2ex] (bax) {$\ldots$};
\node[below of=bb, yshift=2ex] (bbx) {$\ldots$};

\path[-latex,draw] (eps) -- node[above left,gray] {$a\vphantom{b}$} (a);
\path[-latex,draw] (eps) -- node[above right,gray] {$b$} (b);
\path[-latex,draw] (a) -- node[above left,gray] (lab) {$a\vphantom{b}$} (aa);
\path[-latex,draw] (a) -- node[above right,gray] {$b$} (ab);
\path[-latex,draw] (b) -- node[above left,gray] {$a\vphantom{b}$} (ba);
\path[-latex,draw] (b) -- node[above right,gray] {$b$} (bb);
\path[-latex,draw] (aa) -- node[yshift=.5ex,left,gray] {$a\vphantom{b}$} (aax.west);
\path[-latex,draw] (aa) -- node[yshift=.5ex,right,gray] {$b$} (aax.east);
\path[-latex,draw] (ab) -- node[yshift=.5ex,left,gray] {$a\vphantom{b}$} (abx.west);
\path[-latex,draw] (ab) -- node[yshift=.5ex,right,gray] {$b$} (abx.east);
\path[-latex,draw] (ba) -- node[yshift=.5ex,left,gray] {$a\vphantom{b}$} (bax.west);
\path[-latex,draw] (ba) -- node[yshift=.5ex,right,gray] {$b$} (bax.east);
\path[-latex,draw] (bb) -- node[yshift=.5ex,left,gray] {$a\vphantom{b}$} (bbx.west);
\path[-latex,draw] (bb) -- node[yshift=.5ex,right,gray] {$b$} (bbx.east);
\end{tikzpicture}
\caption{Infinite trie $\mathit{even}$}
\label{fig:3:even}
\end{figure}

We gave our type the name $\langT{\alpha}$, to remind us to think of its
inhabitants as formal languages. In the following, we use the terms language and
trie synonymously.

Beyond defining the type and the constants, the ${\keyw{codatatype}}$ command also
exports a wealth of properties about them such as $\final{({\const{L}}\;b\;d)} = b$,
the injectivity of ${\const{L}}$, or more interestingly the coinduction rule.
Informally, coinduction allows us to prove equality of tries which cannot be
distinguished by finitely many selector applications.

Clearly, we would like to identify the trie $\mathit{even}$ with the regular language
of all words of even length $\{w \in \{a,\,b\}^* \mid \length{w} \mathrel{\const{mod}} 2 = 0\}$,
also represented by the regular expression
$\Star{(\Times{(\Plus{\Atom{a}}{\Atom{b}})}{(\Plus{\Atom{a}}{\Atom{b}})})}$.
Therefore, we define the notion of word membership ${\in\nobreak\kern-1.15ex\in}$ on tries by
primitive (or structural) recursion on the word using Isabelle's ${\keyw{primrec}}$ command. %
\begin{quotex}
${\keyw{primrec}}~{\in\nobreak\kern-1.15ex\in} {}\mathrel{:\mskip-.5mu:} \listT{\alpha}\to\langT{\alpha}\to{\ty{bool}}~{\keyw{where}}\\
\phantom{\Let} \inLang{\Nil}{L} = \final{L}\\
\phantom{\Let} \inLang{\Cons{a}{w}}{L} = \inLang{w}{\deriv{L}{a}}$
\end{quotex}

Using ${\in\nobreak\kern-1.15ex\in}$, each trie can be assigned a language in the traditional set
of lists view.
\begin{quotex}
${\keyw{definition}}~\const{out} \mathrel{:\mskip-.5mu:}~ \langT{\alpha} \to \setT{\listT{\alpha}}~{\keyw{where}}\\
\phantom{\Let} \fromLang{L} = \{w \mid \inLang{w}{L}\}$
\end{quotex}
With this definition, we obtain $\fromLang{\mathit{even}} = \{w \in \{a,\,b\}^* \mid
\length{w} \mathrel{\const{mod}} 2 = 0\}$.

\section{Operations on Tries}
\label{sec:3:corec}

So far, we have only specified some concrete infinite tries informally.
Formally, we will use primitive corecursion, which is dual to primitive
recursion. Primitively recursive functions consume one constructor before
proceeding recursively. Primitively corecursive functions produce one
\emph{guarding} constructor whose arguments are allowed to be either
non-recursive terms or a corecursive call (applied to arbitrary non-recursive
arguments). We call a function truly primitively corecursive if not all of the constructor's argument are non-recursive. %
The ${\keyw{primcorec}}$ command reduces a primitively corecursive specification to a
non-recursive definition, which is accepted by Isabelle's inference
kernel~\cite{BlanchetteHLPPT-ITP14}. Internally, the reduction employs a
dedicated combinator for primitive corecursion on tries generated by the
${\keyw{codatatype}}$ command. The ${\keyw{primcorec}}$ command slightly relaxes the above  restriction of primitive corecursion by allowing syntactic
conveniences, such as lambda abstractions, ${\keyw{case}}$-, and ${\keyw{if}}$-expressions, to
appear between the guarding constructor and the corecursive call. The relaxation is resembling the syntactic guardedness check used in type theory~\cite[Section~2.3]{Coquand93}, however still allowing only exactly one constructor to guard a corecursive call.

\subsection{Primitively Corecursive Operations}

We start with some simple examples: the languages of the base cases of regular
expressions. Intuitively, the trie $\emptyset} %{{\pmbx{$\emptyset$}}$ representing the empty language is
labeled with $\bot$ everywhere and the trie $\epsilon} %{{\pmbx{$\epsilon$}}$ representing the empty word
language is labeled with $\top$ at its root and with $\bot$ everywhere else.
The trie $\Atomx{a}$ representing the singleton language of the one letter word
$a$ is labeled with $\bot$ everywhere except for the root of its $a$-subtree.
This intuition is easy to capture formally. %
\begin{quotex}
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.34\textwidth}>{\raggedright\arraybackslash}p{0.34\textwidth}@{}}
${\keyw{primcorec}}~\emptyset} %{{\pmbx{$\emptyset$}} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}~{\keyw{where}}\allowbreak
\phantom{\Let} \emptyset} %{{\pmbx{$\emptyset$}} = {\const{L}}~\bot~(\lambda x.\;\emptyset} %{{\pmbx{$\emptyset$}})$&
${\keyw{primcorec}}~\epsilon} %{{\pmbx{$\epsilon$}} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}~{\keyw{where}}\allowbreak
\phantom{\Let} \epsilon} %{{\pmbx{$\epsilon$}} = {\const{L}}~\top~(\lambda x.\;\emptyset} %{{\pmbx{$\emptyset$}})$
\end{tabular}\\[2\jot]
${\keyw{primcorec}}~{\const{A}} {}\mathrel{:\mskip-.5mu:} \alpha \to \langT{\alpha}~{\keyw{where}}\\
\phantom{\Let} \final{(\Atomx{a})} = \bot\\
\phantom{\Let} \derivx{(\Atomx{a})} = \lambda x.\;{\keyw{if}}\;a = x\;{\keyw{then}}\;\epsilon} %{{\pmbx{$\epsilon$}}\;{\keyw{else}}\;\emptyset} %{{\pmbx{$\emptyset$}}$
\end{quotex}
Among these three definitions only $\emptyset} %{{\pmbx{$\emptyset$}}$ is truly primitively corecursive.

The specifications of $\emptyset} %{{\pmbx{$\emptyset$}}$ and $\epsilon} %{{\pmbx{$\epsilon$}}$ differ syntactically from the one of ${\const{A}}$.
The constants $\emptyset} %{{\pmbx{$\emptyset$}}$ and $\epsilon} %{{\pmbx{$\epsilon$}}$ are defined using the so called
\emph{constructor view}. The constructor view allows the user to enter equations of the form
constant or function equals constructor, where the arguments of the constructor
are restricted as described above. Such
definitions should be familiar to any (lazy) functional programmer.

In contrast, the specification of ${\const{A}}$ is expressed in the \emph{destructor
view}. Here, we specify the constant or function being defined by observations
or experiments via \emph{selector equations}. The allowed experiments on a trie
are given by its selectors ${\omicron}$ and ${\delta}$. We can observe the label
at the root and the subtrees. Specifying the observation for each
selector---again restricted either to be a non-recursive term or to contain the
corecursive call only at the outermost position (ignoring lambda abstractions, ${\keyw{case}}$-, and ${\keyw{if}}$-expressions)---yields a unique
characterization of the function being defined.

It is straightforward to rewrite specifications in either of the views into the
other one. The ${\keyw{primcorec}}$ command performs this rewriting internally and
outputs the theorems corresponding to the user's input specification in both
views. The constructor view theorems serve as executable code equations.
Isabelle's code generator~\cite{HaftmannN10} can use these equations to generate
code which make sense in programming languages with lazy evaluation. In
contrast, the destructor view offers safe simplification rules even when applied
eagerly during rewriting as done by Isabelle's simplifier. Note that constructor
view specifications such as $\emptyset} %{{\pmbx{$\emptyset$}} = {\const{L}}~\bot~(\lambda x.\;\emptyset} %{{\pmbx{$\emptyset$}})$ will
cause the simplifier to loop when applied eagerly.

Now that the basic building blocks $\emptyset} %{{\pmbx{$\emptyset$}}$, $\epsilon} %{{\pmbx{$\epsilon$}}$, and ${\const{A}}$ are in place,
we turn our attention to how to combine them to obtain more complex languages.
We start with the simpler combinators for union, intersection, and complement,
before moving to the more interesting concatenation and iteration. The union
${+}$ of two tries should denote set union of languages (i.e.,
$\fromLang{(\Plus{L}{K})} = \fromLang{L} \mathrel\cup \fromLang{K}$ should hold). It is
defined corecursively by traversing the two tries in parallel and computing for
each pair of labels their disjunction. Intersection ${\CAP}$ is analogous.
Complement $\Not{\phantom{X}}$ simply inverts every label.
\begin{quotex}
${\keyw{primcorec}}~{+} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let} \final{(\Plus{L}{K})} = \final{L} \mathrel\lor \final{K}\\
\phantom{\Let} \derivx{(\Plus{L}{K})} = \lambda x.\;\Plus{\deriv{L}{x}}{\deriv{K}{x}}\\[2\jot]
{\keyw{primcorec}}~{\CAP} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let} \final{(\Inter{L}{K})} = \final{L} \mathrel\land \final{K}\\
\phantom{\Let} \derivx{(\Inter{L}{K})} = \lambda x.\;\Inter{\deriv{L}{x}}{\deriv{K}{x}}\\[2\jot]
{\keyw{primcorec}}~\Not{\phantom{X}} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let} \final{\Not{L}} = \neg\;\final{L}\\
\phantom{\Let} \derivx{\Not{L}} = \lambda x.\;\Not{\deriv{L}{x}}$
\end{quotex}

Let us look at the specifying selector equations which we have seen so far from
a different perspective. Imagine $L$ and $K$ being not tries but instead
syntactic regular expressions, ${\const{A}}$, ${+}$, ${\CAP}$, and $\Not{\phantom{X}}$
constructors of a datatype for regular expressions, and ${\omicron}$ and
${\delta}$ two operations that we define recursively on this syntax. From that
perspective, the operations are familiar: rediscovered Brzozowski derivatives of
regular expressions~\cite{Brzozowski64} and the empty word acceptance (often
also called \emph{nullability}) test on regular expressions in the destructor view
equations for the selectors ${\delta}$ and ${\omicron}$.
There is an important difference, though: while Brzozowski derivatives work with
syntactic objects, our tries are semantic objects on which equality denotes
language equivalence. For example, we will later prove $\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{L} = L$ for
tries, whereas $\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{L} \not= L$ holds for regular expressions. The
coinductive view reveals that derivatives and the acceptance test are the two
fundamental ingredients that completely characterize regular languages and arise
naturally when only considering the semantics.

\subsection{Reducing Corecursion Up-to to Primitive Corecursion}
\label{subsec:upto}

Concatenation ${\CDOT}$ is the next regular operation that we want
to define on tries. Thinking of Brzozowski derivatives and the acceptance test,
we would usually specify it by the following two equations.
\newcommand{\eqref{eqconc}}{\eqref{eqconc}}
\begin{align}
\label{eqconc}
  \begin{split}
    \final{(\Times{L}{K})} &= \final{L} \mathrel\land \final{K} \\
    \derivx{(\Times{L}{K})} &= \lambda x.\;\Plus{(\Times{\deriv{L}{x}}{K})}{
      ({\keyw{if}}\;\final{L}\;{\keyw{then}}\;\deriv{K}{x}\;{\keyw{else}}\;\emptyset} %{{\pmbx{$\emptyset$}})}
  \end{split}
\end{align}

A difficulty arises here, since this specification is not primitively
corecursive---the right hand side of the second equation contains a corecursive
call but not at the topmost position (but rather under ${+}$ here). We call this
kind of corecursion \emph{up to ${+}$}.

Without tool support for corecursion up-to, concatenation must be defined
dif\-fer\-ent\-ly---as a composition of other primitively corecursive
operations. Intuitively, we would like to separate the above ${\delta}$-equation
into two along the ${+}$ and sum them up afterwards. Technically, the
situation is more involved. Since the ${\delta}$-equation is corecursive, we
cannot just create two tries by primitive corecursion.

Figure~\ref{fig:3:times} depicts the trie that should result from concatenating
an arbitrary trie $K$ to the concrete given trie $L$. Procedurally, the
concatenation must replace every subtree $T$ of $L$ that has $\top$ at the
root (those are positions where words from $L$ end) by the trie $\Plus{U}{K}$
where $U$ is the trie obtained from $T$ by changing its root from $\top$ to
$\final{K}$. For uniformity with the above ${\delta}$-equation, we imagine
subtrees $F$ of $L$ with label $\bot$ at the root as also being replaced by
$\Plus{F}{\emptyset} %{{\pmbx{$\emptyset$}}}$, which, as we will prove later, has the same effect as leaving
$F$ alone.

\newcommand{\TreePic}[1]{
\raisebox{-1em}[0pt][0pt]{
\begin{tikzpicture}[scale=0.8]
\node at (.5,-0.25) {$#1$};
\node at (.5,-.55) {$\ldots$};
\path[draw, thick] (0,-.5) -- (.5,.5) -- (1,-.5);
\end{tikzpicture}
}}

\newcommand{\TreePicW}[1]{
\raisebox{-2em}[0pt][0pt]{
\begin{tikzpicture}[scale=0.8]
\node at (.5,-0.25) {$#1$};
\node at (.5,-.55) {$\ldots$};
\path[draw, thick] (-.5,-.5) -- (.5,.5) -- (1.5,-.5);
\end{tikzpicture}
}}

\begin{figure}
\centering
\begin{tikzpicture}[node distance=3em]
\node (eps) {$\top$};
\node[below left of=eps, xshift=-2em] (a) {$\top$};
\node[below right of=eps, xshift=2em] (b) {$\bot$};
\node[below of=a, yshift=2ex] (ax) {$\ldots$};
\node[below of=b, yshift=2ex] (bx) {$\ldots$};

\path[-latex,draw] (eps) -- node[above left,gray] {$a\vphantom{b}$} (a);
\path[-latex,draw] (eps) -- node[above right,gray] {$b$} (b);
\path[-latex,draw] (a) -- node[yshift=.5ex,left,gray] {$a\vphantom{b}$} (ax.west);
\path[-latex,draw] (a) -- node[yshift=.5ex,right,gray] {$b$} (ax.east);
\path[-latex,draw] (b) -- node[yshift=.5ex,left,gray] {$a\vphantom{b}$} (bx.west);
\path[-latex,draw] (b) -- node[yshift=.5ex,right,gray] {$b$} (bx.east);
\end{tikzpicture}
\hspace*{7em}
\begin{tikzpicture}[node distance=3em]
\node (eps) {\rlap{$\Plus{\final{K}\;\quad}{\!\!\TreePic{K}}$}\phantom{$\final{K}$}};
\node[below left of=eps, xshift=-2em] (a) {\phantom{$\final{K}$}\llap{$\Plus{\TreePic{K}\!\!}{\;\quad\final{K}}$}};
\node[below right of=eps, xshift=2em] (b) {\rlap{$\Plus{\bot\;\quad}{\!\!\TreePic{\emptyset} %{{\pmbx{$\emptyset$}}}}$}\phantom{$\bot$}};
\node[below right of=eps, xshift=2em] (phantomb) {
\phantom{$\Plus{\TreePic{\emptyset} %{{\pmbx{$\emptyset$}}}\!\!}{\Plus{\quad\;\bot\;\quad}{\!\!\TreePic{\emptyset} %{{\pmbx{$\emptyset$}}}}}$}};
\node[below of=a, yshift=2ex] (ax) {$\ldots$};
\node[below of=b, yshift=2ex] (bx) {$\ldots$};

\path[-latex,draw] (eps) -- node[above left,gray] {$a\vphantom{b}$} (a);
\path[-latex,draw] (eps) -- node[below left,gray] {$b$} (b);
\path[-latex,draw] (a) -- node[yshift=.5ex,left,gray] (lab) {$a\vphantom{b}$} (ax.west);
\path[-latex,draw] (a) -- node[yshift=.5ex,right,gray] {$b$} (ax.east);
\path[-latex,draw] (b) -- node[yshift=.5ex,left,gray] {$a\vphantom{b}$} (bx.west);
\path[-latex,draw] (b) -- node[yshift=.5ex,right,gray] {$b$} (bx.east);
\end{tikzpicture}
\caption{Tries for $L$ (left) and the concatenation $\Times{L}{K}$ (right)}
\label{fig:3:times}
\end{figure}

\begin{figure}
\centering
\begin{tikzpicture}[node distance=4em]
\node (eps) {$\final{K}$};
\node[below left of=eps, xshift=-2em] (a) {$\final{K}$};
\node[below left of=eps, xshift=-8em] (a') {$\TreePicW{\deriv{K}{a}}$};
\node[below right of=eps, xshift=2em] (b) {$\bot$};
\node[below right of=eps, xshift=8em] (b') {$\TreePicW{\deriv{K}{b}}$};
\node[below of=a, yshift=2ex] (ax) {$\ldots$};
\node[below of=b, yshift=2ex] (bx) {$\ldots$};

\path[-latex,draw] (eps) -- node[yshift=-.5ex,right,gray] {$a\vphantom{b}$} (a);
\path[-latex,draw] (eps) -- node[yshift=-.5ex,left,gray] {$b$} (b);
\path[-latex,draw] (eps) -- node[above left,gray] {$a'\vphantom{b'}$} ([xshift=1ex,yshift=.5ex]a'.north);
\path[-latex,draw] (eps) -- node[above right,gray] {$b'$} ([xshift=-1ex,yshift=.5ex]b'.north);
\path[-latex,draw] (a) -- node[left,gray] {$a\vphantom{b}$} (ax.west);
\path[-latex,draw] (a) -- node[right,gray] {$b$} (ax.east);
\path[-latex,draw] (a) -- node[above,gray] {$a'\vphantom{b'}$} ([xshift=-1.4em,yshift=.7ex]ax.north west);
\path[-latex,draw] (a) -- node[above,gray,xshift=0.1em] {$b'$} ([xshift=1.4em,yshift=.7ex]ax.north east);
\path[-latex,draw] (b) -- node[left,gray] {$a\vphantom{b}$} (bx.west);
\path[-latex,draw] (b) -- node[right,gray] {$b$} (bx.east);
\path[-latex,draw] (b) -- node[above,gray] {$a'\vphantom{b'}$} ([xshift=-1.4em,yshift=.7ex]bx.north west);
\path[-latex,draw] (b) -- node[above,gray,xshift=0.1em] {$b'$} ([xshift=1.4em,yshift=.7ex]bx.north east);

\node[yshift=-1.5ex] at ([xshift=-1.5em]ax.north west) {$\TreePicW{\deriv{K}{a}}$};
\node[yshift=-1.5ex] at ([xshift=1.5em]ax.north east) {$\TreePicW{\deriv{K}{b}}$};
\node[yshift=-1em-1.5ex, xshift=.1ex] at ([xshift=-1.5em]bx.north west) {$\TreePic{\emptyset} %{{\pmbx{$\emptyset$}}}$};
\node[yshift=-1em-1.5ex, xshift=-.1ex] at ([xshift=1.5em]bx.north east) {$\TreePic{\emptyset} %{{\pmbx{$\emptyset$}}}$};

\node[below of=ax, yshift=2.7ex] {};
\end{tikzpicture}
\caption{Trie for deferred concatenation $\TimesLR{L}{K}$}
\label{fig:3:timesLR}
\end{figure}

{
\looseness=-1
Figure~\ref{fig:3:timesLR} presents one way to bypass the restrictions imposed
by primitive corecursion. We are not allowed to use ${+}$ \emph{after} proceeding
corecursively, but we may arrange the arguments of ${+}$ in a broader trie
over a doubled alphabet formally modeled by pairing letters of the alphabet with
a Boolean flag. In Figure~\ref{fig:3:timesLR} we write $a$ for
$(a,\,\top)$ and $a'$ for $(a,\,\bot)$. Because it defers the summation, we
call this primitively corecursive procedure \emph{deferred concatenation}
${\hat{\CDOT}}$. %
\begin{quotex}
${\keyw{primcorec}}~{\hat{\CDOT}} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}\to\langT{(\alpha\times{\ty{bool}})}~{\keyw{where}}\\
\phantom{\Let} \final{(\TimesLR{L}{K})} = \final{L} \mathrel\land \final{K}\\
\phantom{\Let} \derivx{(\TimesLR{L}{K})} = \lambda (x,\,b).\;{\keyw{if}}\;b\;{\keyw{then}}\;\TimesLR{\deriv{L}{x}}{K}\;{\keyw{else}}\;
  {\keyw{if}}\;\final{L}\;{\keyw{then}}\;\TimesLR{\deriv{K}{x}}{\epsilon} %{{\pmbx{$\epsilon$}}}\;{\keyw{else}}\;\emptyset} %{{\pmbx{$\emptyset$}}$\kern-2em
\end{quotex}
Note that unlike in the Figure~\ref{fig:3:timesLR}, where we informally plug the
trie $\deriv{K}{x}$ as some $x'$-subtrees, the formal definition must be more
careful with the types. More precisely, $\deriv{K}{x}$ is of type
$\langT{\alpha}$, while something of type $\langT{(\alpha\times{\ty{bool}})}$ is
expected. This type mismatch is resolved by further concatenating $\epsilon} %{{\pmbx{$\epsilon$}}$ to
$\deriv{K}{x}$ (again in a deferred fashion) without corrupting the intended
semantics.

}

Once the trie for the deferred concatenation has been built, the desired trie
for concatenation can be obtained by a second primitively corecursive traversal
that sums the $x$- and $x'$-subtrees \emph{before} proceeding corecursively. %
\begin{quotex}
${\keyw{primcorec}}~{\hat{\oplus}} {}\mathrel{:\mskip-.5mu:} \langT{(\alpha\times{\ty{bool}})}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let} \final{(\TimesPlus{L})} = \final{L}\\
\phantom{\Let} \derivx{(\TimesPlus{L})} = \lambda x.\;\TimesPlus{(\Plus{\deriv{L}{(x,\,\top)}}{\deriv{L}{(x,\,\bot)}})}$
\end{quotex}

Finally, we can define the concatenation as the composition of ${\hat{\CDOT}}$ and
${\hat{\oplus}}$. The earlier natural selector equations \eqref{eqconc}{} for ${\CDOT}$ are provable for this
definition. %
\begin{quotex}
${\keyw{definition}}~{\CDOT} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let} \Times{L}{K} = \TimesPlus{(\TimesLR{L}{K})}$
\end{quotex}

The situation with iteration is similar. The selector equations following the
Brzozowski derivative of $\Star{L}$ yield a non-primitively corecursive
specification: it is corecursive up to ${\CDOT}$.%
\newcommand{\eqref{eqstar}}{\eqref{eqstar}}
\begin{align}
\label{eqstar}
\begin{split}
\final{(\Star{L})} &= \top\\
\derivx{(\Star{L})} &= \lambda x.\;\Times{\deriv{L}{x}}{\Star{L}}
\end{split}
\end{align}

As before, the restriction is circumvented by altering the operation slightly.
We define the binary operation \emph{deferred iteration} $\StarLR{L}{K}$, whose
language should represent $\Times{L}{\Star{K}}$ (although we have not defined
${}^*$ yet). When constructing the subtrees of $\StarLR{L}{K}$ we keep
pulling copies of the second argument into the first argument before proceeding
corecursively (the second argument itself stays unchanged). %
\begin{quotex}
${\keyw{primcorec}}~{\hat{*}} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let} \final{(\StarLR{L}{K})} = \final{L}\\
\phantom{\Let} \derivx{(\StarLR{L}{K})} =
  \lambda x.\;\StarLR{(\deriv{(\Times{L}{(\Plus{\epsilon} %{{\pmbx{$\epsilon$}}}{K})})}{x})}{K}$
\end{quotex}

Supplying $\epsilon} %{{\pmbx{$\epsilon$}}$ as the first argument to ${\hat{*}}$ defines iteration
for which the original selector equations~\eqref{eqstar}{} hold. %
\begin{quotex}
${\keyw{definition}}~\_{}^* {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let} \Star{L} = \StarLR{\epsilon} %{{\pmbx{$\epsilon$}}}{L}$
\end{quotex}

We have defined all the standard regular operations on tries. Later we will
prove that those definitions satisfy the axioms of Kleene algebra, meaning that
they behave as expected. Already now we can compose the operations to define new tries, for example the introductory $\mathit{even} = \Star{(\Times{(\Plus{\Atomx{a}}{\Atomx{b}})}{(\Plus{\Atomx{a}}{\Atomx{b}})})}$.

\subsection{Adding Further Operations}
\label{subsec:shuffle}

In the coinductive representation, adding new operations corresponds to
defining a new corecursive function on tries. Compared with adding a new
constructor to the inductive datatype of regular expressions and extending all
previously defined recursive functions on regular expressions to
account for this new case, this a is rather low-cost library extension.
Wadler called this tension between extending syntactic and semantic objects the
Expression Problem~\cite{wadler-expression}.\footnote{Note that codatatypes alone are not
the solution to the Expression Problem---they just populate the other side of
the spectrum with respect to datatypes. In fact, adding new selectors to
tries would be as painful as adding new constructors to the datatype of regular
expressions. %
Rendel et al.~\cite{RendelTO15} outline how automatic conversions between the
inductive and the coinductive view can help solving the Expression Problem.}

As an example library extension, we define the regular shuffle product operation on
languages, which adheres to the following selector equations.
\newcommand{\eqref{eqshuffle}}{\eqref{eqshuffle}}
\begin{align}
\label{eqshuffle}
\begin{split}
\final{(\Shuffle{L}{K})} &= \final{L} \mathrel\land \final{K} \\
\derivx{(\Shuffle{L}{K})} &= \lambda x.\;\Plus{(\Shuffle{\deriv{L}{x}}{K})}{
    (\Shuffle{L}{\deriv{K}{x}})}
\end{split}
\end{align}
Intuitively, for words $\inLang{w}{L}$ and $\inLang{v}{K}$, the shuffle product $\Shuffle{L}{K}$ contains all possible interleavings of $w$ and $v$.
As it is the case for concatenation, the selector equations for the shuffle product ${\parallel}$ are corecursive up to ${+}$. Thus, as for ${\CDOT}$, we first define a \emph{deferred shuffle product} operation, which keeps the ${+}$ occurring outside of the corecursive calls in the second equation ``unevaluated'' by using the doubled alphabet $\alpha \times {\ty{bool}}$ instead of $\alpha$.
\begin{quotex}
    ${\keyw{primcorec}}~{\hat{\ShuffleOp}} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}\to\langT{(\alpha\times{\ty{bool}})}~{\keyw{where}}\\
    \phantom{\Let} \final{(\ShuffleLR{L}{K})} = \final{L} \mathrel\land \final{K}\\
    \phantom{\Let} \derivx{(\ShuffleLR{L}{K})} = \lambda (x,\,b).\;{\keyw{if}}\;b\;{\keyw{then}}\;\ShuffleLR{\deriv{L}{x}}{K}\;{\keyw{else}}\;\ShuffleLR{L}{\deriv{K}{x}}$
\end{quotex}
{
\looseness=-1
A second primitively corecursive traversal sums the $(a,\,\top)$- and $(a,\,\bot)$-subtrees using the same function ${\hat{\oplus}}$ as in the definition of concatenation. Then, the shuffle product can be defined as the composition of ${\hat{\ShuffleOp}}$ and ${\hat{\oplus}}$.

}
\begin{quotex}
    ${\keyw{definition}}~{\parallel} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
    \phantom{\Let} \Shuffle{L}{K} = \TimesPlus{(\ShuffleLR{L}{K})}$
\end{quotex}

\subsection{Context-Free Grammars as Tries}
\label{subsec:cfg}

\newcommand{\mathsf{G}}{\mathsf{G}}
\newcommand{\mathcal{T}}{\mathcal{T}}
\newcommand{\mathcal{N}}{\mathcal{N}}
\newcommand{\mathit{N}}{\mathit{N}}
\newcommand{\mathsf{S}}{\mathsf{S}}
\newcommand{\mathsf{P}}{\mathsf{P}}
\newcommand{\mathsf{mk}}{\mathsf{mk}}
\newcommand{\mathsf{mk0}}{\mathsf{mk0}}
\newcommand{\CFGx}[1]{\mathsf{x}(#1)}
\newcommand{\mathsf{PLUS}}{\mathsf{PLUS}}
\newcommand{\PLUS}[1]{\mathsf{PLUS}(#1)}
\newcommand{\mathsf{TIMES}}{\mathsf{TIMES}}
\newcommand{\TIMES}[1]{\mathsf{TIMES}(#1)}
\newcommand{\vlist}[1]{\mathit{#1}}
\newcommand{\mathsf{fold}}{\mathsf{fold}}
\newcommand{\mathsf{close}}{\mathsf{close}}
\newcommand{\mathsf{close}}{\mathsf{close}}
\newcommand{\keyw{in}}{\keyw{in}}
\newcommand{\mathsf{NT}}{\mathsf{NT}}
\newcommand{\mathsf{T}}{\mathsf{T}}

Tries are not restricted to regular operations. We define an operation that
transforms a context-free grammar (in a particular normal form) into the
 trie denoting the same context-free language. The operation borrows ideas from Winter's et al.~\cite{WinterBR11} coalgebraic
exposition of context-free languages.

For the rest of the subsection, we fix a context-free grammar given by the type of its terminal symbols $\mathcal{T}$, the type of its non-terminal symbols $\mathcal{N}$, a distinguished starting non-terminal $\mathsf{S} \mathrel{:\mskip-.5mu:} \mathcal{N}$, and its productions $\mathsf{P} \mathrel{:\mskip-.5mu:} \mathcal{N} \to \setT{\listT{(\mathcal{T} + \mathcal{N})}}$---an assignment of a set of words consisting of terminal and non-terminal symbols for each non-terminal. For readability, we write $\mathsf{T}$ for ${\const{Inl}} \mathrel{:\mskip-.5mu:} \mathcal{T} \to \mathcal{T}  + \mathcal{N}$ and $\mathsf{NT}$ for ${\const{Inr}} \mathrel{:\mskip-.5mu:} \mathcal{N} \to \mathcal{T}  + \mathcal{N}$ in this section. The inductive semantics of such a grammar is standard: a word over the alphabet $\mathcal{T}$ is accepted, if there is a finite derivation of that word using a sequence of productions. (For a formal definition, see Subsection~\ref{ssec:3:cfg}.)
For example, the grammar given by the productions
\begin{quotex}
$\kern-2em\mathsf{P}\;N = {\keyw{if}}\;N = \mathsf{S}\;{\keyw{then}}\;\{\Nil,\,\List{\mathsf{T}\;a},\,\List{\mathsf{T}\;b},\,\List{\mathsf{T}\;a,\,\mathsf{NT}\;\mathsf{S},\,\mathsf{T}\;a},\,
\List{\mathsf{T}\;b,\,\mathsf{NT}\;\mathsf{S},\,\mathsf{T}\;b}\}\;{\keyw{else}}\;\{\}$
\end{quotex}
where $a,\, b \mathrel{:\mskip-.5mu:} \mathcal{T}$ with $a \not= b$, denotes the non-regular language of palindromes over $\{a,\,b\}$. In conventional syntax, we would write the above productions as $\mathsf{S} \to \epsilon \mid a \mid b \mid a\mathsf{S}a \mid b\mathsf{S}b$.

To give a coinductive semantics in form of a trie to a grammar, we must solve the word problem for context-free grammars and use that algorithm
to assign corecursively the Boolean labels in the trie. Different
algorithms solve the word problem for context-free grammars. Earley's algorithm~\cite{Earley70} is the most flexible (but also complex) one: it works for arbitrary grammars without requiring a syntactic normal form. To simplify the presentation, we work with a syntactic normal form that allows us to use a much simplified version of Earley's algorithm.
We require the productions to be in \emph{weak Greibach normal form}~\cite{WinterBR11}: every produced word should either be the empty list or start with a terminal. Formally:
\begin{quotex}
    $\forall N.\;\forall \alpha \in \mathsf{P}\;N.\;{\keyw{case}}\;\alpha\;{\keyw{of}}\;\mathsf{NT}\;M \mathbin{\#} \_ \Rightarrow \bot \mid \_ \Rightarrow \top$
\end{quotex}
{\looseness=-1
Weak Greibach normal form is a relaxation of the standard Greibach normal form~\cite{Greibach65}, which additionally requires the starting terminal to be followed only by non-terminals. The example palindrome grammar is in weak Greibach normal form but not in Greibach normal form.

}

{\setlooseness{-1}
The intermediate \emph{states} $\alpha,\,\beta,\,\ldots$ of a word derivation are words of type $\listT{(\mathcal{T} + \mathcal{N})}$, which are reachable from the initial non-terminal. We observe that such a state can only produce the empty word according to $\mathsf{P}$, if it consists only of non-terminals, each of which can immediately produce the empty word, i.e., $\Nil \in \mathsf{P}\;N$. Note that due to weak Greibach normal form any non-$\Nil$ production will produce at least one terminal symbol.
We compute recursively whether a state can produce the empty word according to $\mathsf{P}$ .
\begin{quotex}
    ${\keyw{primrec}}~{\omicron}_\mathsf{P} \mathrel{:\mskip-.5mu:} \listT{(\mathcal{T} + \mathcal{N})} \to {\ty{bool}}~{\keyw{where}}\\
    \phantom{\Let} {\omicron}_\mathsf{P}\;\Nil = \top\\
    \phantom{\Let} {\omicron}_\mathsf{P}\;(x \mathbin{\#} \alpha) = {\keyw{case}}~x~{\keyw{of}}~\mathsf{T}\;\_ \Rightarrow \bot \mid \mathsf{NT}\;N \Rightarrow \Nil \in \mathsf{P}\;N \mathrel\land {\omicron}_\mathsf{P}\;\alpha$
\end{quotex}

}

A second useful function ${\delta}_\mathsf{P}$ ``reads'' a terminal symbol $a$ in a state from the left, yielding a set of successor states to choose from non-deterministically. The recursive definition of ${\delta}_\mathsf{P}$ is based on a similar observation as the one of ${\omicron}_\mathsf{P}$. If the state starts with a terminal $b$, the only successor state is the tail of the state if $a = b$. There is no successor state if $a \not = b$. If the state starts with a non-terminal $N$, we consider all non-empty productions in $\mathsf{P}\;N$ starting with $a$ and replace $N$ with their tails. Additionally, if $N$ may produce the empty word, we drop it and continue recursively with the next terminal or non-terminal symbol of the state, which possibly results in additional successor states. Formally:
\begin{quotex}
    ${\keyw{primrec}}~{\delta}_\mathsf{P} \mathrel{:\mskip-.5mu:} \listT{(\mathcal{T} + \mathcal{N})} \to \mathcal{T} \to \setT{\listT{(\mathcal{T} + \mathcal{N})}}~{\keyw{where}}\\
    \phantom{\Let} {\delta}_\mathsf{P}\;\Nil\;\_ = \{\}\\
    \phantom{\Let} {\delta}_\mathsf{P}\;(x \mathbin{\#} \alpha)\;a = {\keyw{case}}~x~{\keyw{of}}~\\\phantom{\Let}\TAB\phantom{{}\mid{}}\mathsf{T}\;b \Rightarrow {\keyw{if}}~a=b~{\keyw{then}}~\{\alpha\}~{\keyw{else}}~\{\}\\\phantom{\Let}\TAB\mid \mathsf{NT}\;N \Rightarrow
    \{\beta \mathbin{+\kern-4pt+} \alpha \mid (\mathsf{T}\;a)\mathbin{\#}\beta \in \mathsf{P}\;N \} \mathrel\cup
    {\keyw{if}}~\Nil \in \mathsf{P}\;N~{\keyw{then}}~{\delta}_\mathsf{P}\;\alpha\;a~{\keyw{else}}~\{\}$
\end{quotex}

Finally, we obtain a trie from a set of states by primitive corecursion using the two above functions to specify the observations. Note that the set of states changes when proceeding corecursively. For this definition we use the constructor view.
\begin{quotex}
    ${\keyw{primcorec}}~\mathsf{close} \mathrel{:\mskip-.5mu:} \setT{\listT{(\mathcal{T} + \mathcal{N})}} \to \langT{\mathcal{T}}~{\keyw{where}}\\
    \phantom{\Let} \mathsf{close}\;X = {\const{L}}\;(\exists \alpha \in X.\;{\omicron}_\mathsf{P}\;\alpha)\;(\lambda a.\;\mathsf{close}\;{\left(\bigcup_{\alpha \in X}{\delta}_\mathsf{P}\;\alpha\;a\right))}$
\end{quotex}

The initial state, in which no terminal has been read yet, is the singleton list $[\mathsf{S}]$. We obtain the trie $\mathsf{G}$ corresponding to our fixed grammar.
\begin{quotex}
    ${\keyw{definition}}~\mathsf{G} \mathrel{:\mskip-.5mu:} \langT{\mathcal{T}}~{\keyw{where}}\\
    \phantom{\Let} \mathsf{G} = \mathsf{close}\;\{[\mathsf{S}]\}$
\end{quotex}

\subsection{Arbitrary Formal Languages}

Before we turn to proving, let us exercise one more corecursive definition.
Earlier, we have assigned each trie a set of lists via the function
$\const{out}$. Primitive corecursion enables us to define the converse operation.
\begin{quotex}
${\keyw{primcorec}}~\const{in} \mathrel{:\mskip-.5mu:} \setT{\listT{\alpha}} \to \langT{\alpha}~{\keyw{where}}\\
\phantom{\Let} \final{(\toLang{L})} = \Nil \in L\\
\phantom{\Let} \derivx{(\toLang{L})} = \lambda a.\;\toLang{\{w \mid \Cons{a}{w} \in L\}}$
\end{quotex}

The function $\const{out}$ and $\const{in}$ are both bijections. We show this by
proving that their compositions (either way) are both the identity function. One
direction, $\fromLang{(\toLang{L})} = L$, follows by set extensionality and a
subsequent induction on words. The reverse direction requires a proof by
coinduction,  which is the topic of the next section.

Using $\const{in}$ we can turn every (even undecidable) set of lists into a trie.
This is somewhat counterintuitive, since, given a concrete trie, its word
problem seems easily decidable (via the function ${\in\nobreak\kern-1.15ex\in}$). But of course in
order to compute the trie out of a set of lists $L$ via $\const{in}$ the word
problem for $L$ must be solved---we are reminded that higher-order logic is not
a programming language where everything is executable, but a logic in which we
write down specifications (and not programs). %
For regular operations and context-free grammars from the previous
subsections the situation is different. For example, Isabelle's code generator
can produce valid Haskell code that evaluates
$\inLang{\Cons{a}{\Cons{b}{\Cons{a}{a}}}}{
\Star{(\Times{\Atomx{a}}{(\Plus{\Atomx{a}}{\Atomx{b}})})}}$ to $\top$ and $\inLang{\Cons{a}{\Cons{b}{\Cons{a}{a}}}}{\mathsf{G}}$ to $\bot$, where $\mathsf{G}$ is the trie for the palindrome grammar from Subsection~\ref{subsec:cfg}. The latter is possible, despite the seemingly non-executable existential quantification and unions in the definition of $\mathsf{close}$, due to Isabelle's code generator, which makes (co)finite sets executable through data refinement to lists or red-black trees~\cite{HaftmannKKN-ITP13}.

\section{Reasoning about Tries}
\label{sec:3:coind}

We have seen the definitions of many operations, justifying their meaningfulness
by appealing to the reader's intuition. This is often not enough to guarantee
correctness, especially if we have a theorem prover at hand. So let us formally
prove in Isabelle that the regular operations on tries form a Kleene algebra by
proving Kozen's famous axioms~\cite{Kozen94} as equalities (Subsection~\ref{ssec:3:coind}) or inequalities (Subsection~\ref{ssec:3:sim}) on tries and prove the soundness our our trie construction for a context free grammar with respect to the standard inductive semantics of grammars (Subsection~\ref{ssec:3:cfg}).

\subsection{Proving Equalities on Tries}
\label{ssec:3:coind}

Codatatypes are equipped with the perfect tool for proving equalities: the
coinduction principle. Intuitively, this principle states that the existence of
a relation $R$ that is \emph{closed} under the codatatype's observations (given
by selectors) implies that elements related by $R$ are equal. Being closed means
here that for all $R$-related codatatype elements their immediate
(non-corecursive) observations are equal and the corecursive observations are
again related by $R$. In other words, if we cannot distinguish elements of a
codatatype by (finite) observations, they must be equal. Formally, for our
codatatype $\langT{\alpha}$ we obtain the following coinduction rule. %
\vskip\abovedisplayskip
\begin{center}
\AXC{$R\;L\;K$}
\AXC{\quad$\forall L_1\;L_2.\;R\;L_1\;L_2 \longrightarrow (\final{L_1} = \final{L_2} \mathrel\land \forall x.\;
  R\;(\deriv{L_1}{x})\;(\deriv{L_2}{x}))$}
\RightLabel{${\mathit{coinduct}_\ty{lang}}$}
\BIC{$L = K$}
\DP
\end{center}
\vskip\belowdisplayskip
The second assumption of this rule formalizes the notion of being closed under
observations: If two tries are related then their root's labels are
the same and all their subtrees are related. A relation that satisfies this
assumption is called a \emph{bisimulation}. Thus, proving an equation by
coinduction amounts to exhibiting a bisimulation witness that relates the left
and the right hand sides.

Let us observe the coinduction rule, which we call ${\mathit{coinduct}_\ty{lang}}$, in action. Figure~\ref{fig-proof} shows a detailed proof of the Kleene algebra axiom
that the empty language is the left identity of union that is accepted by Isabelle.%
\begin{figure}
\begin{quotex}
{\small1}\phantom{\Let}${\keyw{theorem}}~\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{L} = L$\\
\noindent{\small2}\phantom{\Let}${\keyw{proof}}~({\mathit{rule}}~{\mathit{coinduct}_\ty{lang}})$\\
\noindent{\small3}\phantom{\Let}$\phantom{\Let} {\keyw{def}}~R~L_1~L_2 = (\exists K.~L_1 = \Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{K} \mathrel\land L_2 = K)$\\[2\jot]
\noindent{\small4}\phantom{\Let}$\phantom{\Let} {\keyw{show}}~R~(\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{L})~L~{\keyw{by}}~{\mathit{simp}}$\\[2\jot]
\noindent{\small5}\phantom{\Let}$\phantom{\Let} {\keyw{fix}}~L_1~L_2$\\
\noindent{\small6}\phantom{\Let}$\phantom{\Let} {\keyw{assume}}~R~L_1~L_2$\\
\noindent{\small7}\phantom{\Let}$\phantom{\Let} {\keyw{then}}~{\keyw{obtain}}~K~{\keyw{where}}~L_1 = \Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{K}~{\keyw{and}}~L_2 = K~{\keyw{by}}~{\mathit{simp}}$\\
\noindent{\small8}\phantom{\Let}$\phantom{\Let} {\keyw{then}}~{\keyw{show}}~\final{L_1} = \final{L_2} \mathrel\land \forall x.\;
  R\;(\deriv{L_1}{x})\;(\deriv{L_2}{x})~{\keyw{by}}~{\mathit{simp}}$\\
\noindent{\small9}\phantom{\Let}${\keyw{qed}}$
\end{quotex}
\caption{A detailed proof by coinduction}
\label{fig-proof}
\end{figure}
After applying the coinduction rule backwards (line~2), the proof has three
parts. First, we supply a definition of a witness relation $R$ (line~3). Second, we prove
that $R$ relates the left and the right hand side (line~4). Third, we prove that $R$ is a
bisimulation (lines~5--8). Proving $R~(\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{L})~L$ for
our particular definition of $R$ is trivial after instantiating the
existentially quantified $K$ with $L$. Proving the bisimulation property is
barely harder: for two tries $L_1$ and $L_2$ related by $R$ we need to show
$\final{L_1} = \final{L_2}$ and $\forall x.\;
R\;(\deriv{L_1}{x})\;(\deriv{L_2}{x})$. Both properties follow by simple
calculations rewriting $L_1$ and $L_2$ in terms of a trie $K$ (line 7), whose existence
is guaranteed by $R~L_1~L_2$, and simplifying with the selector equations for
${+}$ and $\emptyset} %{{\pmbx{$\emptyset$}}$. %
\begin{quotex}
$\final{L_1} = \final{(\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{K})} = (\final{\emptyset} %{{\pmbx{$\emptyset$}}} \mathrel\lor \final{K}) =
(\bot \mathrel\lor \final{K}) = \final{K} = \final{L_2}$\\[2\jot]
$R\;(\deriv{L_1}{x})\;(\deriv{L_2}{x}) =
 R\;(\deriv{(\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{K})}{x})\;(\deriv{K}{x}) \\=
 R\;(\Plus{\deriv{\emptyset} %{{\pmbx{$\emptyset$}}}{x}}{\deriv{K}{x}})\;(\deriv{K}{x}) =
 R\;(\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{\deriv{K}{x}})\;(\deriv{K}{x}) \\=
(\exists K'.~\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{\deriv{K}{x}} =\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{K'} \mathrel\land \deriv{K}{x} = K') = \top$
\end{quotex}
The last step is justified by instantiating $K'$ with $\deriv{K}{x}$.

So in the end, the only part that required ingenuity was the definition of the witness $R$. But was it truly ingenious?
It turns out that in general, when proving a conditional equation
$P\;\overline{x} \longrightarrow l\;\overline{x} = r\;\overline{x}$ by coinduction, where
$\overline{x}$ denotes a list of variables occurring freely in the equation, the
canonical choice for the bisimulation witness is $R\;a\;b =\allowbreak
(P\;\overline{x} \mathrel\land \exists\overline{x}.~a = l\;\overline{x} \mathrel\land b = r\;\overline{x})$. There is no guarantee that this definition yields a
bisimulation. However, after performing a few proofs by coinduction, this
particular pattern emerges as a natural first choice to try.
Indeed, the choice is so natural, that it was worth to automate it in the
${\mathit{coinduction}}$ proof method~\cite{BlanchetteHLPPT-ITP14}. This method
instantiates the coinduction rule ${\mathit{coinduct}_\ty{lang}}$ with the canonical bisimulation
witness constructed from the goal, where the existentially quantified variables
must be given explicitly using the ${\mathit{arbitrary}}$ modifier.
Then it applies the instantiated rule in a resolution step, discharges the first
assumption, and unpacks the existential quantifiers from $R$ in the remaining
subgoal (the ${\keyw{obtain}}$ step in the above proof).
Many proofs collapse to an automatic one-line proof using this convenience, including the one above. Some
examples follow. %
\begin{quotex}
${\keyw{theorem}}~\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{L} = L~~$
${\keyw{by}}~({\mathit{coinduction}}~{\Arbitrary\!:}~L)~{\mathit{auto}}$\\[2\jot]
${\keyw{theorem}}~\Plus{L}{L} = L~~$
${\keyw{by}}~({\mathit{coinduction}}~{\Arbitrary\!:}~L)~{\mathit{auto}}$\\[2\jot]
${\keyw{theorem}}~\Plus{L_1}{L_2} = \Plus{L_2}{L_1}~~$
${\keyw{by}}~({\mathit{coinduction}}~{\Arbitrary\!:}~L_1~L_2)~{\mathit{auto}}$\\[2\jot]
${\keyw{theorem}}~\Plus{(\Plus{L_1}{L_2})}{L_3} = \Plus{L_1}{\Plus{L_2}{L_3}}~~$
${\keyw{by}}~({\mathit{coinduction}}~{\Arbitrary\!:}~L_1~L_2~L_3)~{\mathit{auto}}$\\[2\jot]
${\keyw{theorem}}~\toLang{(\fromLang{L})} = L~~$
${\keyw{by}}~({\mathit{coinduction}}~{\Arbitrary\!:}~L)~{\mathit{auto}}$\\[2\jot]
${\keyw{theorem}}~\toLang{(L \mathrel\cup K)} = \Plus{\toLang{L}}{\toLang{K}}~~$
${\keyw{by}}~({\mathit{coinduction}}~{\Arbitrary\!:}~L~K)~{\mathit{auto}}$
\end{quotex}

As indicated earlier, sometimes the ${\mathit{coinduction}}$ method does not succeed. It
is instructive to consider one example where this is the case:
$\final{L} \longrightarrow \Plus{\epsilon} %{{\pmbx{$\epsilon$}}}{L} = L$.

If we attempt to prove the above statement by coinduction instantiated with the
canonical bisimulation witness $R~L_1~L_2 = (\exists K.~L_1 = \Plus{\epsilon} %{{\pmbx{$\epsilon$}}}{K}
\mathrel\land L_2 = K \mathrel\land \final{K})$, after some simplification we are stuck with
proving that $R$ is a bisimulation. %
\begin{quotex}
$R\;(\deriv{L_1}{x})\;(\deriv{L_2}{x}) =
 R\;(\deriv{(\Plus{\epsilon} %{{\pmbx{$\epsilon$}}}{K})}{x})\;(\deriv{K}{x}) \\=
 R\;(\Plus{\deriv{\epsilon} %{{\pmbx{$\epsilon$}}}{x}}{\deriv{K}{x}})\;(\deriv{K}{x}) =
 R\;(\Plus{\emptyset} %{{\pmbx{$\emptyset$}}}{\deriv{K}{x}})\;(\deriv{K}{x}) \\=
 R\;(\deriv{K}{x})\;(\deriv{K}{x}) = (\exists K'.~\deriv{K}{x} =\Plus{\epsilon} %{{\pmbx{$\epsilon$}}}{K'} \mathrel\land \deriv{K}{x} = K' \mathrel\land \final{K'})$
\end{quotex}

The remaining goal is not provable: we would need to instantiate $K'$ with
$\deriv{K}{x}$, but then, we are left to prove $\final{(\deriv{K}{x})}$, which
we cannot deduce (we only know $\final{K}$). If we, however, instantiate the
coinduction rule with $\reflCl{R}~L_1~L_2 = R~L_1~L_2 \mathrel\lor L_1 = L_2$, we are
able to finish the proof. This means that our canonical bisimulation witness $R$
is not a bisimulation, but $\reflCl{R}$ is. In such cases $R$ is called a
\emph{bisimulation up to equality}~\cite{Sangiorgi98}.

Instead of modifying the ${\mathit{coinduction}}$ method to instantiate the rule ${\mathit{coinduct}_\ty{lang}}$ with
$\reflCl{R}$, it is more convenient to capture this improvement directly in the
coinduction rule. This results in the following rule which we call
\emph{coinduction up to equality} or ${\mathit{coinduct}^=_\ty{lang}}$. %
\vskip\abovedisplayskip
\begin{center}
\AXC{$R\;L\;K$}
\AXC{\quad$\forall L_1\;L_2.\;R\;L_1\;L_2 \longrightarrow (\final{L_1} = \final{L_2} \mathrel\land \forall x.\;
  \reflCl{R}\;(\deriv{L_1}{x})\;(\deriv{L_2}{x}))$}
\RightLabel{${\mathit{coinduct}^=_\ty{lang}}$}
\BIC{$L = K$}
\DP
\end{center}
\vskip\belowdisplayskip

Note that ${\mathit{coinduct}^=_\ty{lang}}$ is not just an instance of ${\mathit{coinduct}_\ty{lang}}$, with $R$ replaced by
$\reflCl{R}$. Instead, after performing this replacement, the first assumption
is further simplified to $R~L~K$---we would not use coinduction in the first
place, if we could prove $\reflCl{R}~L~K$ by reflexivity. Similarly, the
reflexivity part in the occurrence on the left of the implication in the second
assumption is needless and therefore eliminated. The resulting coinduction up to
equality principles are independent of the particular codatatypes and thus
uniformly produced by the \keyw{codatatype} command. Using this coinduction up
to equality rule, we have regained the ability to write one-line proofs. %
\begin{quotex}
${\keyw{theorem}}~\final{L} \longrightarrow \Plus{\epsilon} %{{\pmbx{$\epsilon$}}}{L} = L~~$
${\keyw{by}}~({\mathit{coinduction}}~{\Arbitrary\!:}~L~{\Rule\!:}~{\mathit{coinduct}^=_\ty{lang}})~{\mathit{auto}}$
\end{quotex}

One might think that the principle ${\mathit{coinduct}^=_\ty{lang}}$ is always preferable to ${\mathit{coinduct}_\ty{lang}}$. This is true from the expressiveness point of view: whatever can be proved with ${\mathit{coinduct}_\ty{lang}}$, can also be proved with ${\mathit{coinduct}^=_\ty{lang}}$. However, for proof automation ${\mathit{coinduct}^=_\ty{lang}}$ is often less beneficial: to prove membership in $\reflCl{R}$ we need to prove a disjunction which may result in a larger search space, given that neither of the disjuncts is trivially false. In summary, using the weakest rule that suffices to finish the proof helps proof automation.

This brings us to the next hurdle. Suppose that we already have
proved the natural selector equations~\eqref{eqconc}{} for concatenation ${\CDOT}$. (This
requires finding some auxiliary properties of ${\hat{\CDOT}}$ and ${\hat{\oplus}}$
but is an overall straightforward usage of coinduction up to equality.) Next,
we want to reason about ${\CDOT}$. For example, we prove its distributivity
over ${+}$: $\Times{(\Plus{L}{K})}{M} =
\Plus{(\Times{L}{M})}{(\Times{K}{M})}$. As before, we are stuck proving that the
canonical bisimulation witness $R~L_1~L_2 = (\exists L'~K'~M'.~L_1 =
\Times{(\Plus{L'}{K'})}{M'} \mathrel\land L_2 =
\Plus{(\Times{L'}{M'})}{(\Times{K'}{M'})})$ is a bisimulation (and this time
even for up to equality). %
\begin{quotex}
$\reflCl{R}\;(\deriv{L_1}{x})\;(\deriv{L_2}{x}) =
 \reflCl{R}\;(\deriv{(\Times{(\Plus{L'}{K'})}{M'})}{x})\;(\deriv{(\Plus{(\Times{L'}{M'})}{(\Times{K'}{M'})})}{x}) \kern-2em\\[1\jot]=
  \begin{cases}
    \reflCl{R}\;(\Times{(\Plus{\deriv{L'}{x}}{\deriv{K'}{x}})}{M'})\\
    \phantom{\reflCl{R}}\;(\Plus{(\Times{\deriv{L'}{x}}{M'})}{(\Times{\deriv{K'}{x}}{M'})})&{\keyw{if}}~ \neg \final{L'} \mathrel\land \neg \final{K'}\\
   \reflCl{R}\;(\Plus{\Times{(\Plus{\deriv{L'}{x}}{\deriv{K'}{x}})}{M'}}{\deriv{M'}{x}})\\
     \phantom{\reflCl{R}}\;(\Plus{(\Plus{\Times{\deriv{L'}{x}}{M'}}{\deriv{M'}{x}})}{(\Times{\deriv{K'}{x}}{M'})})&{\keyw{if}}~\final{L'} \mathrel\land \neg \final{K'}\\
   \reflCl{R}\;(\Plus{\Times{(\Plus{\deriv{L'}{x}}{\deriv{K'}{x}})}{M'}}{\deriv{M'}{x}})\\
   \phantom{\reflCl{R}}\;(\Plus{(\Times{\deriv{L'}{x}}{M'})}{(\Plus{\Times{\deriv{K'}{x}}{M'}}{\deriv{M'}{x}})})&{\keyw{if}}~\neg \final{L'} \mathrel\land \final{K'}\\
   \reflCl{R}\;(\Plus{\Times{(\Plus{\deriv{L'}{x}}{\deriv{K'}{x}})}{M'}}{\deriv{M'}{x}})\\
   \phantom{\reflCl{R}}\;(\Plus{(\Plus{\Times{\deriv{L'}{x}}{M'}}{\deriv{M'}{x}})}{(\Plus{\Times{\deriv{K'}{x}}{M'}}{\deriv{M'}{x}})})&{\keyw{if}}~\final{L'} \mathrel\land \final{K'}
  \end{cases}\kern-3em\\[1\jot]=
   \begin{cases}
     \top&{\keyw{if}}~ \neg \final{L'} \mathrel\land \neg \final{K'}\\
    \reflCl{R}\;(\Plusg{\Times{(\Plus{\deriv{L'}{x}}{\deriv{K'}{x}})}{M'}}{\deriv{M'}{x}})\\
    \phantom{\reflCl{R}}\;(\Plusg{(\Plus{\Times{\deriv{L'}{x}}{M'}}{\Times{\deriv{K'}{x}}{M'}})}{\deriv{M'}{x}})&\text{otherwise}
   \end{cases}\kern-2em\\$
\end{quotex}

The remaining subgoal cannot be discharged by the definition of $R$. In
principle it could be discharged by equality (the two tries are equal), but this
is almost exactly the property we originally started proving, so we have not
simplified the problem by coinduction but rather are going in circles here.
However, if our relation could somehow split its arguments across the outermost
${+}$ highlighted in gray, we could prove the left pair being related by $R$ and the right pair
by $=$. The solution is easy: we allow the relation to do just that. Accordingly,
we define the congruence closure $\PlusCl{R}$ of a relation $R$ under ${+}$
inductively by the following rules.  %

\begin{quotex}\leavevmode\kern-3em
\begin{tabular}{@{}c@{\qquad}c@{\qquad}c@{\qquad}c@{\qquad}c@{}}
\AXC{$L = K\vphantom{\PlusCl{R}}$}
\UIC{$\PlusCl{R}\;L\;K$}
\DP
&
\AXC{$R\;L\;K\vphantom{\PlusCl{R}}$}
\UIC{$\PlusCl{R}\;L\;K$}
\DP
&
\AXC{$\PlusCl{R}\;L\;K$}
\UIC{$\PlusCl{R}\;K\;L$}
\DP
&
\AXC{$\PlusCl{R}\;L_1\;L_2$}
\AXC{$\PlusCl{R}\;L_2\;L_3$}
\BIC{$\PlusCl{R}\;L_1\;L_3$}
\DP
&
\AXC{$\PlusCl{R}\;L_1\;K_1$}
\AXC{$\PlusCl{R}\;L_2\;K_2$}
\BIC{$\PlusCl{R}\;(\Plus{L_1}{L_2})\;(\Plus{K_1}{K_2})$}
\DP
\end{tabular}\kern-1em
\end{quotex}

The closure $\PlusCl{R}$ is then used to strengthen the coinduction rule, just
as the earlier reflexive closure $\reflCl{R}$ strengthening. Note that the
closure $\reflCl{R}$ can also be viewed as inductively generated by the first
two of the above rules. In summary, we obtain \emph{coinduction up to congruence of
${+}$}, denoted by ${\mathit{coinduct}^{+}_\ty{lang}}$. %
\vskip\abovedisplayskip
\begin{center}
\AXC{$R\;L\;K$}
\AXC{$\forall L_1\;L_2.\;R\;L_1\;L_2 \longrightarrow (\final{L_1} = \final{L_2} \mathrel\land \forall x.\;
  \PlusCl{R}\;(\deriv{L_1}{x})\;(\deriv{L_2}{x}))$}
\RightLabel{${\mathit{coinduct}^{+}_\ty{lang}}$}
\BIC{$L = K$}
\DP
\end{center}
\vskip\belowdisplayskip
This rule is easily derived from plain coinduction by instantiating $R$ in ${\mathit{coinduct}_\ty{lang}}$ with $\PlusCl{R}$ and proceeding by induction on the definition of the congruence closure.

{\setlooseness{-1}
As intended ${\mathit{coinduct}^{+}_\ty{lang}}$ makes the proof of distributivity into another
automatic one-liner. This is because our new proof principle,
coinduction up to congruence of ${+}$, matches exactly the definitional
principle of corecursion up to ${+}$ used in the selector equations~\eqref{eqconc}{} of~${\CDOT}$. %
\begin{quotex}
${\keyw{theorem}}~\Times{(\Plus{L}{K})}{M} = \Plus{(\Times{L}{M})}{(\Times{K}{M})}$\\
$\phantom{\Let} {\keyw{by}}~({\mathit{coinduction}}~{\Arbitrary\!:}~L~K~M~{\Rule\!:}~{\mathit{coinduct}^{+}_\ty{lang}})~{\mathit{auto}}$
\end{quotex}

}

Coinduction up to congruence of $+$ allows us also to prove properties of the shuffle product, e.g., commutativity $\Shuffle{L}{K} = \Shuffle{K}{L}$ and associativity $\Shuffle{(\Shuffle{K}{L})}{M} = \Shuffle{K}{(\Shuffle{L}{M})}$.

For properties involving iteration ${}^*$, whose selector equations~\eqref{eqstar}{} are
corecursive up to~${\CDOT}$, we will need a further strengthening of the
coinduction rule (using the congruence closure under ${\CDOT}$). Overall, the
most robust solution to keep track of the different rules is to maintain a
coinduction rule up to all previously defined operations on tries: we define
$\regCl{R}$ to be the congruence closure of $R$ under ${+}$, ${\CDOT}$, and
${}^*$ and then use the following rule for proving. %
\vskip\abovedisplayskip
\begin{center}
\AXC{$R\;L\;K$}
\AXC{$\forall L_1\;L_2.\;R\;L_1\;L_2 \longrightarrow (\final{L_1} = \final{L_2} \mathrel\land \forall x.\;
  \regCl{R}\;(\deriv{L_1}{x})\;(\deriv{L_2}{x}))$}
\RightLabel{${\mathit{coinduct}^{\bullet}_\ty{lang}}$}
\BIC{$L = K$}
\DP
\end{center}
\vskip\belowdisplayskip

We will not spell out all equational axioms of Kleene algebra~\cite{Kozen94} and their
formal proofs~\cite{Traytel-AFP13} here. Most proofs are automatic; some require
a few manual hints in which order to apply the congruence rules.

\subsection{Proving Inequalities on Tries}
\label{ssec:3:sim}

A few axioms of Kleene algebra also contain inequalities, such as
$\Plus{\epsilon} %{{\pmbx{$\epsilon$}}}{\Times{L}{\Star{L}}} \leq \Star{L}$, and even conditional
inequalities, such as $\Plus{L}{\Times{M}{K}} \leq M \longrightarrow \Times{L}{\Star{K}}
\leq M$. On languages, $L \leq K$ is defined as $\Plus{L}{K} = K$, such that in principle proofs by
coinduction also are applicable here. However, we can achieve even better proof automation, if we formulate and use the following dedicated coinduction principle for $\leq$.
\vskip\abovedisplayskip
\begin{center}
\AXC{$R\;L\;K$}
\AXC{$\forall L_1\;L_2.\;R\;L_1\;L_2 \longrightarrow ((\final{L_1} \longrightarrow \final{L_2}) \mathrel\land \forall x.\;
R\;(\deriv{L_1}{x})\;(\deriv{L_2}{x}))$}
\RightLabel{${\mathit{coinduct}_{\leq}}$}
\BIC{$L \leq K$}
\DP
\end{center}
\vskip\belowdisplayskip
This theorem has the same shape as the usual coinduction principle ${\mathit{coinduct}_\ty{lang}}$, however the relation $R$ is only required to be a simulation instead of a bisimulation. In other words $R$ still needs to be closed under corecursive observations, however the immediate observation of the first argument must only imply the one of the second argument (as opposed to being equal to it). We call this coinduction principle ${\mathit{coinduct}_{\leq}}$ and prove it by unfolding the definition of $\leq$ and then using the equational coinduction principle ${\mathit{coinduct}_\ty{lang}}$.

While ${\mathit{coinduct}_{\leq}}$ allows us to prove simple properties like $r \leq \Plus{r}{s}$, it is not strong enough to automatically prove the inequational Kleene algebra axioms, which involve concatenation and iteration. As in the case of equations, up-to reasoning is the familiar way out of this dilemma. However, since $R$ is only a simulation, and thus in general not an equivalence relation, we can not consider its congruence closure. Instead, we follow Rot et al.~\cite{RotBR16} and define inductively the so-called precongruence closure $\PlusClsim{R}$\,.

\begin{quotex}
    \begin{tabular}{@{}c@{\qquad}c@{\qquad}c@{\qquad}c@{}}
        \AXC{$L \leq K\vphantom{\PlusClsim{R}}$}
        \UIC{$\PlusClsim{R}\;L\;K$}
        \DP
        &
        \AXC{$R\;L\;K\vphantom{\PlusClsim{R}}$}
        \UIC{$\PlusClsim{R}\;L\;K$}
        \DP
        &
        \AXC{$\PlusClsim{R}\;L_1\;L_2$}
        \AXC{$\PlusClsim{R}\;L_2\;L_3$}
        \BIC{$\PlusClsim{R}\;L_1\;L_3$}
        \DP
        &
        \AXC{$\PlusClsim{R}\;L_1\;K_1$}
        \AXC{$\PlusClsim{R}\;L_2\;K_2$}
        \BIC{$\PlusClsim{R}\;(\Plus{L_1}{L_2})\;(\Plus{K_1}{K_2})$}
        \DP
        \\\\
        \multicolumn{2}{@{}c@{\quad}}{
        \AXC{$\PlusClsim{R}\;L_1\;K_1$}
        \AXC{$\PlusClsim{R}\;L_2\;K_2$}
        \BIC{$\PlusClsim{R}\;(\Times{L_1}{L_2})\;(\Times{K_1}{K_2})$}
        \DP}
        &
        \AXC{$\PlusClsim{R}\;L\;K$}
        \UIC{$\PlusClsim{R}\;(\Star{L})\;(\Star{K})$}
        \DP
        &
        \AXC{$\PlusClsim{R}\;L_1\;K_1$}
        \AXC{$\PlusClsim{R}\;L_2\;K_2$}
        \BIC{$\PlusClsim{R}\;(\Inter{L_1}{L_2})\;(\Inter{K_1}{K_2})$}
        \DP
    \end{tabular}\kern-1em
\end{quotex}

With this definition we are able to prove the following strengthened coinduction principle up to precongruence closure, called ${\mathit{coinduct}^{\bullet}_{\leq}}$.
\vskip\abovedisplayskip
\begin{center}
\AXC{$R\;L\;K$}
\AXC{$\forall L_1\;L_2.\;R\;L_1\;L_2 \longrightarrow ((\final{L_1} \longrightarrow \final{L_2}) \mathrel\land \forall x.\;
    \PlusClsim{R}\;(\deriv{L_1}{x})\;(\deriv{L_2}{x}))$}
\RightLabel{${\mathit{coinduct}^{\bullet}_{\leq}}$}
\BIC{$L \leq K$}
\DP
\end{center}
\vskip\belowdisplayskip
The proof of ${\mathit{coinduct}^{\bullet}_{\leq}}$ is structurally very similar to the one of ${\mathit{coinduct}^{\bullet}_\ty{lang}}$: after using the plain ${\mathit{coinduct}_{\leq}}$ rule, we are left with proving that the precongruence closure $\PlusClsim{R}$ is a simulation. This follows by induction on the definition of the preconguence closure.
Crucially, the complement operation $\Not{\phantom{X}}$ is not included in this definition. For simulation up-to preconguence closure to be a simulation, all operations must be monotone with respect to their immediate observations ${\omicron}$, which is not the case for $\Not{\phantom{X}}$~\cite{RotBR16}.

Finally, we are capable to write automatic proofs for inequalities.

\begin{quotex}
    ${\keyw{theorem}}~\Plus{\epsilon} %{{\pmbx{$\epsilon$}}}{\Times{L}{\Star{L}}} \leq \Star{L}~~$
    ${\keyw{by}}~({\mathit{coinduction}}~{\Rule\!:}~{\mathit{coinduct}^{\bullet}_{\leq}})~{\mathit{auto}}$\\[2\jot]
    ${\keyw{theorem}}~\final{K} \longrightarrow L \leq \Times{L}{K}~~$
    ${\keyw{by}}~({\mathit{coinduction}}~{\Arbitrary\!:}~L~{\Rule\!:}~{\mathit{coinduct}^{\bullet}_{\leq}})~{\mathit{auto}}$
\end{quotex}

We remark that working with inequalities also has its cost. The reason for this is that Isabelle excels at equational reasoning. Isabelle also provides automation for reasoning with orders, but it is noticeably less powerful than the one for $=$. On the other hand, equations of the form $\Plus{L}{K} = K$, which one gets after unfolding the definition of $\leq$, are not ideal for rewriting. Proofs that reduce inequalities to equalities ofter require manual hints to expand $K$ into $\Plus{L}{K}$ at the right places. In the end, when using up-to simulations a careful setup of rewriting rules and classical reasoning support for $\leq$ results in a higher degree of automation. This is especially perceivable for more complicated inequational properties like $\Plus{L}{\Times{M}{K}} \leq M \longrightarrow \Times{L}{\Star{K}}
\leq M$.

\subsection{Reasoning about Context-Free Languages}
\label{ssec:3:cfg}

We connect our trie construction from Subsection~\ref{subsec:cfg} for a context-free grammar in weak Greibach normal form to the traditional inductive semantics of context-free grammars. We use the notational conventions and definition of Subsection~\ref{subsec:cfg}, including fixing the starting non-terminal $\mathsf{S} \mathrel{:\mskip-.5mu:} \mathcal{N}$ and the productions $\mathsf{P} \mathrel{:\mskip-.5mu:} \mathcal{N} \to \setT{\listT{(\mathcal{T} + \mathcal{N})}}$. First, we formalize the traditional inductive semantics using an inductive binary predicate ${\in\nobreak\kern-1.15ex\in}_\mathsf{P} \mathrel{:\mskip-.5mu:} \listT{\mathcal{T}} \to \listT{(\mathcal{T} + \mathcal{N})} \to {\ty{bool}}$ (written infix). Intuitively, $w \mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} \alpha$ holds if and only if $w$ is derivable from $\alpha$ in finitely many production steps via $\mathsf{P}$, where each time we replace the leftmost non-terminal first.
\vskip\abovedisplayskip
\begin{center}
\begin{tabular}{@{}c@{\qquad}c@{\qquad}c@{}}
\AXC{$\Nil \mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} \Nil$}
\DP&
\AXC{$w \mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} \alpha$}
\UIC{$(a \mathbin{\#} w) \mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} (\mathsf{T}\;a \mathbin{\#} \alpha)$}
\DP&
\AXC{$\exists \beta \in \mathsf{P}\;N.\;w \mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} \beta\mathbin{+\kern-4pt+}\alpha$}
\UIC{$w \mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} (\mathsf{NT}\;N \mathbin{\#} \alpha)$}
\DP
\end{tabular}
\end{center}
\vskip\belowdisplayskip
Note that ${\in\nobreak\kern-1.15ex\in}_\mathsf{P}$ gives a way to assign the language $\{w \mid w \mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} [N]\}$ to each non-terminal $N$, and in particular the language $\{w \mid w \mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} [\mathsf{S}]\}$ for the whole grammar given by $\mathsf{P}$ and $\mathsf{S}$.
We now prove that our trie $\mathsf{G}$ for the fixed grammar represents the same language, i.e., $\mathsf{G} = \toLang{\{w \mid w \mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} [\mathsf{S}]\}}$. Our proof uses an auxiliary intermediate inductive predicate ${\in\nobreak\kern-1.15ex\in}^{{\omicron}{\delta}}_\mathsf{P} \mathrel{:\mskip-.5mu:} \listT{\mathcal{T}} \to \setT{\listT{(\mathcal{T} + \mathcal{N})}} \to {\ty{bool}}$ (written infix) that reflects the change of the set of states during corecursion in $\mathsf{close}$ function (which is used to construct $\mathsf{G}$).
\vskip\abovedisplayskip
\begin{center}
\begin{tabular}{@{}c@{\qquad}c@{\qquad}c@{}}
\AXC{$\exists \alpha \in X.\;{\omicron}_\mathsf{P}\;\alpha$}
\UIC{$\Nil \mathrel{{\in\nobreak\kern-1.15ex\in}^{{\omicron}{\delta}}_\mathsf{P}} X$}
\DP&
\AXC{$w \mathrel{{\in\nobreak\kern-1.15ex\in}^{{\omicron}{\delta}}_\mathsf{P}} (\bigcup_{\alpha \in X}.\;{\delta}_\mathsf{P}\;\alpha\;a)$}
\UIC{$(a \mathbin{\#} w) \mathrel{{\in\nobreak\kern-1.15ex\in}^{{\omicron}{\delta}}_\mathsf{P}} X$}
\DP
\end{tabular}
\end{center}
\vskip\belowdisplayskip
In some sense, ${\in\nobreak\kern-1.15ex\in}^{{\omicron}{\delta}}_\mathsf{P}$ is the inductive view on the $\mathsf{close}$ function, as established next.
\begin{quotex}
${\keyw{theorem}}~\mathsf{close}\;X = \toLang{\{w\mid w \mathrel{{\in\nobreak\kern-1.15ex\in}^{{\omicron}{\delta}}_\mathsf{P}} X\}}
~{\keyw{by}}~({\mathit{coinduction}}~{\Arbitrary\!:}~X)~{\mathit{auto}}$
\end{quotex}
The proof uses the simplest coinduction rule ${\mathit{coinduct}_\ty{lang}}$ and relies on injectivity of $\const{in}$.

Next, we establish that $w\mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} \alpha$ holds if and only if $w\mathrel{{\in\nobreak\kern-1.15ex\in}^{{\omicron}{\delta}}_\mathsf{P}} \{\alpha\}$ holds. We prove the two directions separately. Thereby we generalize the ``if''-direction.
\begin{quotex}
${\keyw{theorem}}~w \mathrel{{\in\nobreak\kern-1.15ex\in}^{{\omicron}{\delta}}_\mathsf{P}} X \longrightarrow \exists \alpha \in X.\;w\mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} \alpha$\\
${\keyw{theorem}}~w\mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} \alpha \longrightarrow w \mathrel{{\in\nobreak\kern-1.15ex\in}^{{\omicron}{\delta}}_\mathsf{P}} \{\alpha\}$
\end{quotex}
We do not show the proofs for the above statements about since both are standard inductions on the inductive definitions of ${\in\nobreak\kern-1.15ex\in}^{{\omicron}{\delta}}_\mathsf{P}$ and ${\in\nobreak\kern-1.15ex\in}_\mathsf{P}$. Out of all theorems shown in this subsection, only the last one requires the grammar to be in weak Greibach normal form. Putting the three theorems together, we obtain the desired characterization: $\mathsf{G} = \toLang{\{w \mid w \mathrel{{\in\nobreak\kern-1.15ex\in}_\mathsf{P}} [\mathsf{S}]\}}$.

We remark that a definition of the trie $\mathsf{G}$ via a full Earley parser, would not only remove the need of weak Greibach normal form, but also enable coinductive reasoning about arbitrary grammars. For example, one could also formalize and prove correct the translation of grammars to certain normal forms without resorting to the traditional inductive semantics (and thus induction). We leave this study as future work, as it may burst the scope of an introduction to coinduction.

\section{Coalgebraic Foundations}
\label{sec:3:coalg}

We briefly connect the formalized but still intuitive notions, such as tries,
from earlier sections with the key coalgebraic concepts and terminology that is
usually used to present the coalgebraic view on formal languages. Thereby, we
explain how particularly useful abstract objects gave rise to concrete tools in
Isabelle\slash HOL. More theoretical and detailed introductions to coalgebra can
be found elsewhere~\cite{Rutten00,Jacobs1997}.

Given a functor $\ty{F}$ an ($\ty{F}$-)\emph{coalgebra} is a \emph{carrier} object
$A$ together with a map $A \to \ty{F}\;A$---the \emph{structural map} of a
coalgebra. In the context of higher-order logic---that is in the category of
types which consists of types as objects and of functions
between types as arrows---a functor is a type constructor $\ty{F}$ together
with a map function ${\const{map}}_\ty{F} \mathrel{:\mskip-.5mu:} (\alpha \to \beta) \to \alpha\;\ty{F}
\to \beta\;\ty{F}$ that preserves identity and composition: ${\const{map}}_\ty{F}\;{\const{id}} =
{\const{id}}$ and ${\const{map}}_\ty{F}\;(f \circ g) = {\const{map}}_\ty{F}\;f\circ {\const{map}}_\ty{F}\;g$. An
$\ty{F}$-coalgebra in HOL is therefore simply a function $s \mathrel{:\mskip-.5mu:} \alpha \to
\alpha\;\ty{F}$. A function $f \mathrel{:\mskip-.5mu:} \alpha \to \beta$ is a coalgebra
\emph{morphism} between two coalgebras $s \mathrel{:\mskip-.5mu:} \alpha \to \alpha\;\ty{F}$ and
$t \mathrel{:\mskip-.5mu:} \beta \to \beta\;\ty{F}$ if it satisfies the commutation property $t \circ
f = {\const{map}}_\ty{F}\;f \circ s$, also depicted by the commutative diagram in
Figure~\ref{fig:3:morphism}.

\begin{figure}[t]
\centering
$
\xymatrix@C=3pc@R=1pc{
\alpha
\ar^{\hspace*{-1ex}s}[r]
\ar_{f}[d]    &
\alpha\;\ty{F}
\ar^{{\const{map}}_\ty{F}\;f}[d]  \\
\beta
\ar^{\hspace*{-1ex}t}[r]  & \beta\;\ty{F}
}
$
\caption{Commutation property of a coalgebra morphism}
\label{fig:3:morphism}
\end{figure}

{
\looseness=-1
An ($\ty{F}$-)coalgebra to which there exists a unique morphism from any other
coalgebra is called a \emph{final} ($\ty{F}$-)\emph{coalgebra}. Not all functors
$\ty{F}$ admit a final coalgebra~\cite[Section~10]{Rutten00}. Two different final coalgebras are necessarily
isomorphic. Final coalgebras correspond to codatatypes in Isabelle\slash HOL.
Isabelle's facility for defining codatatypes maintains a large class of
functors---bounded natural functors~\cite{TraytelPB-LICS12}---for which a final
coalgebra does exists. Moreover, for any bounded natural functor $\ty{F}$,
Isabelle can construct its final coalgebra with the codatatype $\ty{CF}$ as the
carrier and define a bijective constructor $\const{C_\ty{F}} \mathrel{:\mskip-.5mu:}
\ty{CF}\;\ty{F} \to \ty{CF}$ and its inverse, the destructor $\const{D_\ty{F}} \mathrel{:\mskip-.5mu:}
\ty{CF} \to \ty{CF}\;\ty{F}$. The latter takes the role of the structural map of
the coalgebra. %
\begin{quotex}
${\keyw{codatatype}}~\ty{CF} = \const{C_\ty{F}}~(\const{D_\ty{F}}:\ty{CF}\;\ty{F})$
\end{quotex}

}

Finally, we are ready to connect these abstract notions to our tries. The
codatatype of tries $\langT{\alpha}$ is the final coalgebra of the functor
$\beta\;\ty{D} = {\ty{bool}} \times (\alpha \to \beta)$ with the associated map
function ${\const{map}}_\ty{D}\;g = {\const{id}} \times (\lambda f.\;g\circ f)$, where $(f \times
g)\;(x,\,y) = (f\;x,\,g\;y)$. The structural map of this final coalgebra is the
function $\const{D_\ty{D}} = \langle{\omicron},\,{\delta}\rangle$, where $\langle
f,\; g\rangle\;x = (f\;x,\,g\;x)$.

The finality of $\langT{\alpha}$ gives rise to the definitional principles of
primitive coiteration and corecursion. In Isabelle the coiteration principle is embodied by the primitive
\emph{coiterator} ${\const{coiter}} \mathrel{:\mskip-.5mu:} (\tau \to \tau\;\ty{D}) \to \tau \to \langT{\alpha}$,
that assigns to the given $\ty{D}$-coalgebra the unique morphism from itself to the
final coalgebra. In other words, the primitive coiterator allows us to define
functions of type $\tau \to \langT{\alpha}$ by providing a $\ty{D}$-coalgebra
on $\tau$, i.e., a function of type $\tau \to {\ty{bool}} \times (\alpha \to \tau)$
that essentially describes a deterministic (not necessarily finite) automaton
without an initial state. To clarify this automaton analogy, it is customary to
present the $\ty{F}$-coalgebra $s$ as two functions $s = \langle \const{o},\,
\const{d} \rangle$ with $\tau$ being the states of the automaton, $\const{o} :
\tau \to {\ty{bool}}$ denoting accepting states, and $\const{d} : \alpha \to \tau \to
\tau$ being the transition function. From a given $s$, we uniquely obtain the
function ${\const{coiter}}\;s$ that assigns to a separately given initial state $t : \tau$
the language ${\const{coiter}}\;s\;t : \langT{\alpha}$ and makes the diagram in
Figure~\ref{fig-coiter} commute. Note that Figure~\ref{fig-coiter} is an instance of Figure~\ref{fig:3:morphism}.

\begin{figure}[t]
\centering
$
\xymatrix@C=3pc@R=.8pc{
\tau
\ar^{\hspace*{-1em}s}[r]
\ar_{{\const{coiter}}\;s}[d]    &
\tau\;\ty{D}
\ar^{{\const{map}}_\ty{D}\;({\const{coiter}}\;s)}[d]  \\
\langT{\alpha}
\ar^{\hspace*{-1em} \langle {\omicron},\, {\delta}\rangle}[r]  &
\langT{\alpha}\;\ty{D}
}
$
\caption{Unique morphism ${\const{coiter}}\;s$ to the
  final coalgebra $(\langT{\alpha},\,\langle {\omicron},\, {\delta}\rangle)$}
\label{fig-coiter}
\end{figure}

\begin{figure}[t]
    \centering\vspace{-.5ex}
    $
    \xymatrix@C=3pc@R=.8pc{
        \tau
        \ar^{\hspace*{-1em}s}[r]
        \ar_{{\const{corec}}\;s}[d]    &
        (\langT{\alpha} + \tau)\;\ty{D}
        \ar^{{\const{map}}_\ty{D}\;[{\const{id}},\,{\const{corec}}\;s]}[d]  \\
        \langT{\alpha}
        \ar^{\hspace*{-1em} \langle {\omicron},\, {\delta}\rangle}[r]  &
        \langT{\alpha}\;\ty{D}
    }
    $
    \caption{Characteristic theorem of the corecursor}
    \label{fig-corec}
\end{figure}

Corecursion differs from coiteration by additionally allowing the user to stop the
coiteration process by providing a fixed non-corecursive value. In Isabelle this
is mirrored by another combinator: the \emph{corecursor} ${\const{corec}} \mathrel{:\mskip-.5mu:} (\tau
\to (\langT{\alpha}+\tau)\;\ty{D}) \to \tau \to \langT{\alpha}$ where the sum
type $+$ offers the possibility either to continue corecursively as before
(represented by the type $\tau$) or to stop with a fixed value of type
$\langT{\alpha}$. The corecursor satisfies the characteristic property shown in
Figure~\ref{fig-corec}, where the square brackets denote a case distinction on
$+$, i.e.\ $[f,\,g]\;x = {\keyw{case}}\;x\;{\keyw{of}}\;{\const{Inl}}\;l \Rightarrow f\;l \mid {\const{Inr}}\;r
\Rightarrow g\;r$.
Corecursion is not more expressive than coiteration (since ${\const{corec}}$ can be
defined in terms of ${\const{coiter}}$), but it is more convenient to use. For
instance, the non-corecursive specifications of $\epsilon} %{{\pmbx{$\epsilon$}}$ and ${\const{A}}$, and the
${\keyw{else}}$ branch of ${\hat{\CDOT}}$ exploit this additional flexibility.

{ \looseness=-1 The ${\keyw{primcorec}}$ command~\cite{BlanchetteHLPPT-ITP14} reduces a
user specification to a non-recursive definition using the corecursor. For
example, the union operation ${+}$ is internally defined as $\lambda
L~K.~{\const{corec}}~(\lambda (L,\,K).\;(\final{L} \mathrel\land \final{K},\,\lambda
a.~\const{Inr}\;(\deriv{L}{a},\,\deriv{K}{a})))~(L,\,K)$. The $\ty{D}$-coalgebra
argument to ${\const{corec}}$ resembles the right hand sides of the selector equations
for ${+}$ (with the corecursive calls replaced by ${\const{Inr}}$). In fact, for this
simple definition mere coiteration would suffice.
An example that uses the convenience that corecursion provides, is the deferred concatenation ${\hat{\CDOT}}$. Its internal definition reads: $\lambda
L~K.~{\const{corec}}~(\lambda (L,\,K).\;(\final{L} \mathrel\land \final{K},\,\lambda (x,\,b).\;{\keyw{if}}\;b\;{\keyw{then}}\;{\const{Inr}}\;(\deriv{L}{x},\,K)\;{\keyw{else}}\;
{\keyw{if}}\;\final{L}\;{\keyw{then}}\;{\const{Inr}}\;(\deriv{K}{x},\,\epsilon} %{{\pmbx{$\epsilon$}})\;{\keyw{else}}\;{\const{Inl}}\;\emptyset} %{{\pmbx{$\emptyset$}})$.
As end users, most of the time we are happy being able to write the high-level
corecursive specifications, without having to explicitly supply coalgebras.

}

It is worth noting that the final coalgebra $\langT{\alpha}$ itself corresponds
to the automaton, whose states are languages, acceptance is given by
$\const{o}\;L = \final{L}$, and the transition function by $\const{d}\;a\;L =
\deriv{L}{a}$.  For these definitions, we obtain ${\const{corec}}\;\langle \const{o},\,
\const{d} \rangle\;(L : \langT{\alpha}) = L$. For regular languages this
automaton corresponds to the minimal automaton (since equality on tries
corresponds to language equivalence), which is finite by the Myhill--Nerode
theorem. This correspondence is not very practical though, since we typically
label states of automata with something finite, in particular not with languages
(represented by infinite tries).

A second consequence of the finality of $\langT{\alpha}$ is the coinduction
principle that we have seen earlier. It follows from the fact that final
coalgebras are quotients by bisimilarity, where bisimilarity is defined as the
existence of a bisimulation relation.

\section{Discussion and Related Work}
\label{sec:3:discuss}

Our development is a formalized counterpart of Rutten's introduction to the
coalgebraic view on languages~\cite{Rutten98}. In this section we discuss
further related work.

\PARA{Coalgebraic View on Formal Languages}

The coalgebraic approach to languages has recently received some attention.
Landmark results in language theory were rediscovered and generalized. Silva's
recent survey~\cite{silva15} highlights some of those results including the
proofs of correctness of Brzozowski's subtle deterministic finite automaton
minimization algorithm~\cite{BonchiBRS12}. %
The coalgebraic approach yields some algorithmic advantages, too. Bonchi and Pous
present a coinductive algorithm for checking equivalence of non-deterministic
automata that outperforms all previously known algorithms by one order of
magnitude~\cite{BonchiP13}. Another recent development is our formally
verified coalgebraic algorithm for deciding weak monadic second-order logic of
one successor (WS1S)~\cite{Traytel-CSL15}. This formalization employs the
Isabelle library presented here.

\PARA{Formal Languages in Proof Assistants}

The traditional set-of-words view on formal languages is
formalized in most proof assistants. In contrast, we are not aware of any other
formalization of the coalgebraic view on formal languages in a proof assistant.

\looseness=-1 Here, we want to compare our formalization with the Isabelle
incarnation of the set-of-words view developed by Krauss and Nipkow for the
correctness proof of their regular expression equivalence
checker~\cite{KraussN11}. Both libraries are comparably concise. In 500 lines
Krauss and Nipkow prove almost all axioms of Kleene algebra and the
characteristic equations for the left quotients (the ${\delta}$-specifications
in our case). They reuse Isabelle's libraries for sets and lists, which come
with carefully tuned automation setup. Still, their proofs tend to require
additional induction proofs of auxiliary lemmas, especially when reasoning about
iteration. Our formalization is 700 lines long. We prove all axioms of Kleene
algebra and connect our representation to the set-of-words view via the
bijections $\const{out}$ and $\const{in}$. Except for those bijections our
formalization does not rely on any other library. Moreover, when we changed our
5000 lines long formalization of a coalgebraic decision procedure for
WS1S~\cite{Traytel-CSL15} to use the infinite tries instead of the set-of-words
view, our proofs about WS1S became approximately 300 lines shorter. Apparently,
a coalgebraic library is a good fit for a coalgebraic procedure.

Paulson presents a concise formalization of automata theory based
on hereditarily finite sets~\cite{Paulson15}. For the semantics he reuses Krauss
and Nipkow's set-of-words formalization.

\PARA{Non-Primitive Corecursion in Proof Assistants}

Automation for corecursion in proof assistants is much less developed than its
recursive counterpart. The Coq proof assistant supports corecursion
up to constructors~\cite{Chlipala13}. Looking at our examples, however, this
means that Coq will not be able to prove productivity of the natural
concatenation and iteration specifications automatically, since both go beyond
up-to constructors. Instead, our reduction to primitive corecursion can be
employed to bypass Coq's productivity checker.

Recently, we have added the support for corecursion up to so
called friendly operations to
Isabelle/HOL~\cite{BlanchetteBLPT, BlanchettePT-ICFP15}. (Before this addition, Isabelle supported only primitive corecursion~\cite{BlanchetteHLPPT-ITP14}.) An operation is friendly if, under lazy
evaluation, it does not peek too deeply into its arguments, before producing at
least one constructor. %
For example, the friendly operation $\Plus{L}{K} = {\const{L}}\;(\final{L} \mathrel\lor
\final{K})\;(\lambda x.\;\Plus{\deriv{L}{x}}{\deriv{K}{x}})$ destructs only one
layer of constructors, in order to produce the topmost ${\const{L}}$.
In contrast, the primitively corecursive
equation $\mathsf{deep}\;L = {\const{L}}\;(\final{L})\;(\lambda
x.\;\mathsf{deep}\;(\deriv{(\deriv{L}{x})}{x}))$ destructs two layers of
constructors (via ${\delta}$) before producing one and is therefore not
friendly. Indeed, we will not be able to reduce the equation $\mathsf{bad} =
{\const{L}}\;\top\;(\lambda\_.\;\mathsf{deep}\;\mathsf{bad})$ (which is corecursive
up to $\mathsf{deep}$) to a primitively corecursive specification. And there is
a reason for it: $\mathsf{bad}$ is not uniquely specified by the above equation,
or in other words not productive.

Since ${+}$
is friendly, and ${\CDOT}$ and ${\parallel}$ are corecursive up to ${+}$, this new infrastructure
allows us to use the constructor view version of the natural selector equations~\eqref{eqconc}{} and \eqref{eqshuffle}{} for ${\CDOT}$ and ${\parallel}$ instead of the more complicated primitively corecursive definitions from
Section~\ref{sec:3:corec}.
\begin{quotex}
$\keyw{corec}~(\keyw{friend})~{+} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let}\Plus{L}{K} = {\const{L}}\;(\final{L} \mathrel\lor \final{K})\;
(\lambda x.\;\Plus{\deriv{L}{x}}{\deriv{K}{x}})$\\[1\jot]
$\keyw{corec}~(\keyw{friend})~{\CDOT} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let}\Times{L}{K} = {\const{L}}\;(\final{L} \mathrel\land \final{K})\;
(\lambda x.\;\Plus{(\Times{\deriv{L}{x}}{K})}{
    ({\keyw{if}}\;\final{L}\;{\keyw{then}}\;\deriv{K}{x}\;{\keyw{else}}\;\emptyset} %{{\pmbx{$\emptyset$}})})$\\[1\jot]
$\keyw{corec}~(\keyw{friend})~{\parallel} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let}\Shuffle{L}{K} = {\const{L}}\;(\final{L} \mathrel\land \final{K})\;
(\lambda x.\;\Plus{(\Shuffle{\deriv{L}{x}}{K})}{(\Shuffle{L}{\deriv{K}{x}})})$
\end{quotex}
The $\keyw{corec}$ command defines the specified constants and the $\keyw{friend}$ option registers them as friendly operations by automatically discharging the emerging proof obligations ensuring that the operations
consume at most one constructor to produce one constructor. Since ${\CDOT}$ is friendly, too, we can define the corecursive up to ${\CDOT}$ iteration ${}^*$ using its natural equations~\eqref{eqstar}.
\begin{quotex}
$\keyw{corec}~(\keyw{friend})~\Star{\_} {}\mathrel{:\mskip-.5mu:} \langT{\alpha}\to\langT{\alpha}~{\keyw{where}}\\
\phantom{\Let}\Star{L} = {\const{L}}\;\top\;
(\lambda x.\;\Times{\deriv{L}{x}}{\Star{L}})$
\end{quotex}

Internally, \keyw{corec} reduces the corecursive specification to a primitively corecursive one following an abstract, category theory inspired construction. Yet, what
this abstract construction yields in practice is relatively close to our manual construction for
concatenation. (In contrast, the iteration case takes some shortcuts, which the
abstract view does not offer.)

{
\looseness=-1
On the reasoning side, \keyw{corec} provides some automation, too. It automatically derives the corresponding coinduction up-to rules for the registered (sets of) friendly operations.
Overall, the usage of \keyw{corec} compresses our development
from 700 to 550 lines of Isabelle text.

}

{\setlooseness{-1}
Agda's combination of copatterns (i.e., destructor view) and sized
types~\cite{AbelPTS-POPL13,abelP-2013} is the most expressive implemented support for
corecursion in proof assistants to date. However, using sized types often means
that one has to encode proofs of productivity manually in the type of the
defined function. Thus, it is possible to define concatenation and
iteration using their natural equations \eqref{eqconc}{} and \eqref{eqstar}{} in Agda. Recently, Abel~\cite{Abel2016CMCS,Abel} has formalized those definitions of regular operations up to proving the
recursion equation $L^* = \Plus{\epsilon} %{{\pmbx{$\epsilon$}}}{\Times{L}{\Star{L}}}$ for iteration in 219~lines of Agda text,
which correspond to 125~lines in our version.
His definitions are equally concise as the ones using $\keyw{corec}$, but his proofs require more
manual steps.

}

\section{Conclusion}
\label{sec:concl}

We have presented a particular formal structure for computation and deduction:
infinite tries modeling formal languages. Although this representation is
semantic and infinite, it is suitable for computation---in particular we obtain
a matching algorithm for free on tries constructed by regular operations.
Deduction does not come short either: coinduction is the convenient reasoning
tool for infinite tries. Coinductive proofs are concise, especially for
(in)equational theorems such as the axioms of Kleene algebra.

Codatatypes might be just the right tool for thinking algorithmically about
semantics. We hope to have contributed to their dissemination by outlining some
of their advantages.

\paragraph*{\textbf{Acknowledgments}}

{\relax

I thank Andrei Popescu for introducing me to the coinductive view on formal
languages. I am grateful to Tobias Nipkow and David Basin for encouraging this
work. Jasmin Blanchette, Andrei Popescu, Ralf Sasse, and the anonymous FSCD and LMCS
reviewers gave many precious hints on early drafts of this article helping to
improve both the presentation and the content. Jurriaan Rot suggested important related
work and recommended proving inequalities of tries by coinduction on $\leq$ rather than on $=$.

}

\bibliographystyle{myabbrv}

redpajama_set_name: RedPajamaArXiv


The exterior canvas is clean and beautiful but shows faint rubbing at the bottom corners. The leather has developed a honey patina with water spots and light soiling. The shoulder strap has minor scuffing and scratches. The hardware has surface scratches. The interior is clean and in great condition, but has light wear and a faint perfume scent.


Keep your photos contained in a Plush Animal Print Photo Album. The attention-grabbing cover is also soft to the touch.
Available in Zebra print, Leopard and Cow print.
Holds 200 photos (4″ x 6″). 9-1/4″ x 7-1/4″.
Tame those wildly disorganized photos!


We're in the business of helping people – people like you. We provide the space, time and a few novel tools to help you dig in, do the work and let your inner gritty goddess shine through (sounds cliche, but it's what we do).
We wanted to introduce you to a few very special women, our Grace & Grit Ambassadors, who have attended a Rejuvenation Retreat and have graciously agreed to share their story with the hope of helping you discover yours.
You may need more than a testimonial to know if the Rejuvenation Retreat is right for you. We hope their powerful stories get you fired up and ready to take the plunge and join our growing community.
I was coming off of a challenging summer season, where I needed to demonstrate a lot of personal grit – and work on giving myself a lot of grace. When a friend sent me Live It Active's Rejuvenation Retreat in Guelph, ON, it felt a bit like fate. I looked forward to a day where I could take in others' stories, have fun and reflect. I was surprised by the level of consideration, compassion and encouragement I received throughout the day – it gave me more peace of mind than anticipated. I chose to be a Grace & Grit Ambassador because, to me, the role means supporting opportunities for people to invest in themselves and their goals, and to understand their inherent worthiness in a world where it's easy to forget it. For me, that's not just a priority for myself – it's something I hope to help others see in themselves and celebrate.
Image features Jess at the Rejuvenation Retreat, ON, 2018. Photo taken by Jenny Thompson.
I was scrolling social media at a time in my life when I felt disconnected – from work, my family and myself. It was like I was just going through the motions – each day the same. A never ending cycle of early mornings, eating my lunch at my desk and rushing to pick up my kid at the last minute before making dinner.
When I saw the retreat, two words stood out: grit and grace; traits I strove to conjure in everything I did but felt I was sadly lacking. At that moment in life, I was shifting to a new role and the thought of continuing the cycle of running through life but not experiencing it called for fostering more of this illusive grit and grace.
I asked two friends to join me and quickly registered. One said yes, but when the day came she wasn't able to go. However, I was on a mission. A mission to find the grace I was missing from life.
The quiet space and the first snow of the season helped set the stage for a intentional session led by Morgan at The Heart of Bragg Creek. Everything felt right – the group of women coming together to harness our internal grace seemed fitting as we started the day on our mats in a circle. The workbook asked questions that needed to be asked and allowed us the time and space to consider them. I walked away feeling something that I hadn't felt in years – self love for reconnecting through yoga, meditation and this beautiful world next to the ethereal Treaty 7 land.
After the session, I came back and chose to do things different – I chose to be more active in my life with my family (yoga mornings with a 3 year old anyone?!!). I chose to find my path to my passion in my career and while I left the retreat without a personal manifesto, I spent the next month thinking, revisiting the workbook and finally, cultivated one that fit.
Originally I felt pulled in all directions: a mom, a wife, an employee, and my own self. Through this session, it felt good to remember that everything starts with finding space for the grace for myself.
In talking with Morgan and considering my journey, I said yes to becoming an ambassador because we all need a space to find ourselves. This retreat provided the balance to move, both physically and mentally with other strong women. Sharing stories and experience (Buti yoga!!!!). You don't need to be a certain person, size, fitness level to attend these sessions. You just have to have an open mind and heart.
My journey of self-discovery started the day I lost my baby girl. I was 10.5 weeks pregnant and deep in my heart I knew she was a girl. In response to my loss, I threw myself into work, the holidays – just about anything to avoid the pain.
It all came crashing down on what would have been my due date. One bad day turned into two, and quickly every day became a struggle.
One session with an amazing therapist revealed I was suffering from postpartum depression, unresolved grief and an identity crisis. I spent the next few months peeling back the layers until I found myself – my true self. This process was extremely painful. Every layer unearthed memories I had attempted to exile.
I experienced the Rejuvenation Retreat: Cultivating Grace & Grit a ways into my journey. What it gave me was the opportunity and permission to record and reflect on my deepest thoughts and put them into perspective. My personal manifesto is something I live by and hold myself accountable to every day. I can look back and view this period of my life as a time of immense personal growth. I'm not sure where my journey will take me but I've learned to embrace uncertainty. What I will be able to do is carry some grace and grit along with me for the ride.


We are your partner when valves need to be serviced and repaired. Quick reaction times, reliability, competence and high flexibility are required for on-site valve service. These requirements are fulfilled by ARTES Valve & Service GmbH with its qualified personnel. Shop containers and service vehicles are available that are fitted with extensive equipment for working on the valves in the system. The provisioning of spare parts is an important component of our services. Our on-site service is ready for you around the clock.
We can advise you during planning of your condition-based maintenance as well as future inspection reviews.