$(\gamma^{\prime},\delta^{\prime})$ is not obtained by a pair of matching
transitions, then $\gamma^{\prime}=\beta\alpha^{\prime}$ and
$\delta^{\prime}=\beta^{\prime}$. Moreover, we have
$X\alpha^{\prime}\overset{u}{\rightarrow}\gamma^{\prime}$ and
$Y\beta^{\prime}\overset{u}{\rightarrow}\delta^{\prime}$, from which it is
immediate that $(X\alpha^{\prime},Y\beta^{\prime})$ is incomparable.

Next, consider the subcase in which $(X,Y)$ is in $\mathcal{S}$ or
$Y\overset{u}{\rightarrow}\varepsilon$ but
$X\overset{u}{\not\rightarrow}\beta$. In either case, there is a pair of
matching transitions
$X\alpha^{\prime}\overset{a}{\rightarrow}\gamma^{\prime}$,
$Y\beta^{\prime}\overset{a}{\rightarrow}\delta^{\prime}$, so that
$(X\alpha^{\prime},Y\beta^{\prime})$ is incomparable.

  * •

(case 5.10 \- partial failure) Here $(X\alpha^{\prime},Y\beta^{\prime})$ was a
BPA1 guess turned into a BPA2 guess, and there is a pair of matching
transitions $X\alpha^{\prime}\overset{a}{\rightarrow}\gamma^{\prime}$,
$Y\beta^{\prime}\overset{a}{\rightarrow}\delta^{\prime}$. Since
$(\gamma^{\prime},\delta^{\prime})$ is incomparable, so is
$(X\alpha^{\prime},Y\beta^{\prime})$.

∎

###  6.3 Termination

Intuitively, to prove termination we shall argue that the basis $\mathcal{B}$
changes polynomially many times. Moreover, between any two changes of
$\mathcal{B}$, the basis-updating algorithm is essentially verifying
coinductive congruence, and we can bound the number of pairs generated in the
same way as in theorem 23.

######  Lemma 30.

During the basis-updating algorithm, the basis $\mathcal{B}$ changes at most
$\mathcal{O}(n^{4})$ times, where $n$ is the number of non-terminals in the
grammar.

###### Proof.

We begin by noticing that:

  * •

initially, $\mathcal{S}=\emptyset$;

  * •

at every partial failure, there is at least one pair $(X,Y)$ not in
$\mathcal{S}$ which enters $\mathcal{S}$;

  * •

there is no way for a pair in $\mathcal{S}$ to leave $\mathcal{S}$.

Let $n$ be the number of non-terminals in the grammar. Since there are
$\mathcal{O}(n^{2})$ many pairs of non-terminals, we get that there can only
be at most $\mathcal{O}(n^{2})$ partial failures during the execution of the
algorithm. During a partial failure, the basis is changed once (by replacing a
pair $(X,Y\beta^{\prime})$ by a pair $(X\alpha,Y\beta)$ and removing all pairs
in $\mathcal{B}$ which correspond to removed BPA1 or BPA2 guesses).

Next, let us bound the number of times $\mathcal{B}$ is changed between one
partial failure and the next. In such situations, the only way to change
$\mathcal{B}$ is by adding new pairs (cases 5.7, 5.8 and 5.9). Since
$\mathcal{B}$ is simple, for each pair $(X,Y)$ we can add at most one element
to $\mathcal{B}$. Therefore, there can only be $\mathcal{O}(n^{2})$ additions
to $\mathcal{B}$ before the algorithm either terminates or enters a partial
failure.

Since there are at most $\mathcal{O}(n^{2})$ partial failures and between any
two consecutive partial failures there are at most $\mathcal{O}(n^{2})$
additions to $\mathcal{B}$, we conclude that $\mathcal{B}$ changes at most
$\mathcal{O}(n^{4})$ times. ∎

######  Theorem 31.

The basis-updating algorithm terminates, for any simple grammar $\mathcal{G}$
without dead symbols and any pair $(\gamma,\delta)$ of words of non-terminals.
Its time complexity is polynomial on the size of $\mathcal{G}$, the valuation
of $\mathcal{G}$, and the seminorms of $\gamma,\delta$.

###### Proof.

Let $n$ be the number of non-terminals in $\mathcal{G}$, $d$ be the maximum
number of transitions of a non-terminal in $\mathcal{G}$ (the degree of
$\mathcal{G}$), and $v$ be the maximum among the valuation of $\mathcal{G}$
and the seminorms of $\gamma$, $\delta$. Whenever the expansion of a node
$(X\alpha^{\prime},Y\beta^{\prime})$ produces children, they fit into one of
two cases. One case is that the children is obtained by applying a BPA rule
(cases 5.4 and 5.5). By the reasoning in theorem 23 (using the fact that
$\mathcal{B}$ is functional and simple), the children belongs to the canonical
norm-reducing sequence of either $X\alpha^{\prime},Y\beta^{\prime}$ in the
parent node, or some $X\alpha,Y\beta$ in $\mathcal{B}$. The other case is that
a pair associated with $X,Y$ is added to $\mathcal{B}$ and the children is
obtained by following a pair of matching transitions
$X\overset{a}{\rightarrow}\gamma^{\prime\prime}$,
$Y\overset{a}{\rightarrow}\delta^{\prime\prime}$. Let us call these _unruly_
children (since they do not follow from BPA rules). We can observe that the
words in the unruly children node are taken from
$\gamma^{\prime\prime},\delta^{\prime\prime},\gamma^{\prime\prime}\alpha^{\prime},\delta^{\prime\prime}\beta^{\prime}$.
Comparing with $X\alpha^{\prime},Y\beta^{\prime}$, the seminorm of the
resulting children increases by at most
$\max(\mathsf{s}(\gamma^{\prime\prime}),\mathsf{s}(\delta^{\prime\prime}))\leq
v$.

At any point during the basis-updating algorithm, there may be at most
$\mathcal{O}(n^{2})$ nodes whose expansion produces unruly children (at most
one for each pair in $\mathcal{B}$). Hence there are at most
$\mathcal{O}(n^{2}d)$ unruly children. Each word belonging to an unruly
children can have a seminorm of at most $\mathcal{O}(n^{2}v)$, since it can
occur after at most $\mathcal{O}(n^{2})$ unruly expansions that each increase
the seminorm by at most $v$.

Now let us analyse the behaviour of the algorithm between two consecutive
changes in $\mathcal{B}$. During this phase, any node produced by the
algorithm is obtained from the application of BPA rules to either the root
node or one of the unruly children. Therefore, by the reasoning in theorem 23,
any word produced in this stage must belong to the canonical norm-reducing
sequence of either the root node, some unruly children, or some pair
$X\alpha,Y\beta$ in $\mathcal{B}$. There are $\mathcal{O}(n^{2}d)$ such words,
each having seminorm of at most $\mathcal{O}(n^{2}v)$. Hence, there are at
most $\mathcal{O}((n^{2}d\times n^{2}v)^{2})=\mathcal{O}(n^{8}d^{2}v^{2})$
different pairs that can be produced by the algorithm. In summary, between any
two consecutive changes in $\mathcal{B}$ there can be at most
$\mathcal{O}(n^{8}d^{2}v^{2})$ expansion steps. Since, by lemma 30, the basis
changes at most $\mathcal{O}(n^{4})$ times, the algorithm must terminate after
at most $\mathcal{O}(n^{12}d^{2}v^{2})$ iterations, which is polynomial in the
size of $\mathcal{G}$, the valuation of $\mathcal{G}$ and the seminorms of
$\gamma,\delta$.

Finally, we need to bound the complexity of each iteration. It is obvious that
most iterations can be done efficiently, as long as we use appropriate data
structures (such as hash tables) to store the nodes in the tree (for the
effect of loop detection, case 5.1) and the pairs in $\mathcal{B}$. There are
two exceptions requiring further justification, one of which being partial
failures (which may occur in cases 5.3, 5.10, 5.8 and 5.9). Notice that if a
node is visited in a partial failure, causing the partial failure to be
propagated up the tree, then that node will be removed at the end of that
chain of partial failures. Therefore, each node is visited at most once during
all partial failures occurring during the algorithm. The total complexity of
partial failures is thus bounded by the number of all nodes considered during
the algorithm, which is bounded by the number of iterations
$\mathcal{O}(n^{12}d^{2}v^{2})$. The other exception is checking whether
$X\overset{u}{\rightarrow}\beta$ during case 5.9. Here we need to follow a
chain of transitions of size $|u|=\|Y\|$, which is bounded by the valuation of
$\mathcal{G}$ (and thus by $v$). We only need to do this each time we are
trying to add a BPA1 pair in $\mathcal{B}$, and this happens at most
$\mathcal{O}(n^{4})$ times by lemma 30. Thus, the total complexity of these
checks is bounded by $\mathcal{O}(n^{4}v)$. ∎

##  7 Application: context-free session types

Session types are an approach for modeling communication protocols [19, 20,
44]. Among the several proposed formalisms for defining the universe of
session types, we shall consider context-free session types as presented by
Almeida et al. [4]. This framework is simple but expressive enough to move
beyond tail recursion (regular session types [20]). Since its introduction
[45], context-free session types have been augmented with constructors such as
functions, records and variants [1], higher-order messages, functional
polymorphism [13, 14], type-level abstraction, and type-level application
[37]. Each of those formalisms can still be converted into simple grammars.
Thus, the results in this section can be adapted to those settings as well.

###  7.1 Syntax of types

We assume a finite set of _message types_ including
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(for integers),
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(for booleans) and so on. We let
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>denote a generic message type. We also assume a countable set of _type
references_ , denoted by
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and so on. Let us take a look at the different constructors for defining
session types.

$\displaystyle\begin{split}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{M}}&\;::=\;\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{int}}}\;\mid\;\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{bool}}}\;\mid\;\ldots\\\
{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}&\;::=\;{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{M}}}\;\mid\;{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{!{M}}}\;\mid\;{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\oplus}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\\{{\ell}\colon{T_{\ell}}\\}_{{\ell}\in{L}}}}\;\mid\;{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\&}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\\{{\ell}\colon{T_{\ell}}\\}_{{\ell}\in{L}}}}\;\mid\;\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{skip}}}\;\mid\;{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{T};{T}}}\;\mid\;{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{x}}\;\mid\;{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}\end{split}$
(1)

We use
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{M}}}$
to represent the action of receiving a value of type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{!{M}}}$
for sending a value of type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\oplus}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>represents an internal choice, corresponding to the action of selecting a
choice according to some label
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>L$ and continuing as type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Dually, type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\&}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>represents an external choice, where some choice
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is received and communication continues with
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Context-free session types introduce sequential composition
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{T};{U}}}$
for the action of executing type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>followed by type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Type
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is the neutral element of sequential composition; a lone
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>represents absence of communication. Finally, we introduce recursion
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}$
where
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is a type variable. Recursion is used for representing potentially infinite
behaviour, as it is often the case with communication protocols.

Let us look at some examples.

  * •

Type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\mathrm{query}}}}={\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{int}}}}}}};{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{!{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>specifies a channel that receives an integer and replies with a boolean.

  * •

Type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\mathrm{pingpong}}}}={\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{int}}}}}}};{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{!{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{bool}}}}}}};{x}}}}}}}}}$
specifies a channel that continuously receives an integer and replies with a
boolean.

  * •

Type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\mathrm{math}}}}={\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\&}}\\{{\mathrm{add}\colon{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{int}}}}}}};{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{int}}}}}}};{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{!{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{int}}}}}}};{x}}}}}}}}},\mathrm{isprime}\colon{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{int}}}}}}};{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{!{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{bool}}}}}}};{x}}}}}},\mathrm{quit}\colon\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>specifies a math server offering three choices:
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(receives two integers, sends an integer, and goes back to the start),
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(receives an integer, sends a boolean, and goes back to the start), or
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(ends communication).

  * •

Type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\mathrm{tree}}}}={\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\&}}\\{{\mathrm{leaf}\colon\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{skip}}},\mathrm{node}\colon{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{x};{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{int}}}}}}};{x}}}}}}}\\}}}}$
specifies a channel for receiving a tree of integers. When choice
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is selected, the channel receives the left subtree, then the (integer) value
at that node, and then the right subtree.

###  7.2 Termination and contractivity

An object syntactically produced by syntax (1) is called a _pretype_. Not
every pretype is a type. Intuitively, we need to exclude syntax that does not
correspond to ‘actual’ communication. The standard approach is to define
predicates for termination and contractivity, as in fig. 5.

*[Right=$\checkmark$-Skip] $\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>✓ *[Right=$\checkmark$-Seq] T ✓ U ✓ T;U ✓ *[Right=$\checkmark$-Rec] T ✓ μ x.T ✓

*[Right=C-In] ?M contr *[Right=C-Out] !M contr *[Right=C-IntC] ⊕{ℓ:T_ℓ}_ℓ∈L contr *[Right=C-ExtC] &{ℓ:T_ℓ}_ℓ∈L contr
*[Right=C-Skip] $\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>contr *[Right=C-Seq1] T ✓ U contr T;U contr *[Right=C-Seq2] T ／✓ T contr T;U contr *[Right=C-Rec] T contr μ X.T contr

*[Right=T-In] Δ ⊢?M *[Right=T-Out] Δ ⊢!M *[Right=T-IntC] Δ ⊢T_ℓ ℓ∈L Δ ⊢⊕{ℓ:T_ℓ}_ℓ∈L *[Right=T-ExtC] Δ ⊢T_ℓ ℓ∈L Δ ⊢&{ℓ:T_ℓ}_ℓ∈L
*[Right=T-Skip] Δ ⊢$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>*[Right=T-Seq] Δ ⊢T Δ ⊢U Δ ⊢T;U *[Right=T-Var] x∈Δ Δ ⊢x *[Right=T-Rec] μ x.T contr Δ,x ⊢T Δ ⊢μ x.T

Figure 5: Session types: rules for termination
(${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}}\>\mathrm{\checkmark}$),
contractivity
(${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}}\>\mathrm{contr}$),
and type formation
(${\Delta}\vdash{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}$).

The is-terminated predicate
(${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}}\>\mathrm{\checkmark}$),
materializes the intuition of a pretype that provides no operation; it
comprises only sequential composition of terminated pretypes and recursions of
terminated pretypes. For example,
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{skip}}}};{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{skip}}}};{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{y}.{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{skip}}}}}}}}})}}}$
are terminated, but
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{skip}}}};{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{x}}}$
are not.

Contractivity
(${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}}\>\mathrm{contr}$),
ensures that a pretype eventually rewrites to a pretype constructor. The is-
terminated predicate is decidable [4, 13], which justifies the inclusion of
its negation
${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}}\>\mathrm{\not\\!\checkmark}$
in rule C-Seq2. For example,
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{int}}}}}}};{x}}}}}}$
is contractive, but
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{skip}}}};{x}}}}}}$
is not.

Type formation
(${\Delta}\vdash{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>states that
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is a type under context $\Delta$. A _context_ is an (unordered) set of type
variables, and the comma operator
$\Delta,{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>extends a context by adding a new variable. Recursion
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}$
binds variable
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>We say that
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is a _type_ if
${}\vdash{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>i.e., if
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is a type under the empty context (this is only true if
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>has no free variables). Rules for type formation are mostly straightforward.
We remark only that in rule T-Rec, we check the formation of
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}$
by adding
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>to the context and verifying that
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}$
is contractive. For example,
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{int}}}}}}};{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{y}.{x}}}}}}}}}$
is contractive, but not a type.

###  7.3 Type equivalence

Type equivalence is denoted by
${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}}\;{\simeq}\;{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and can be defined in several equivalent ways [13]. For example, it can be
defined by means of coinductive derivation rules, or by means of bisimulation
among labelled transition systems. Briefly, we desire type equivalence to
extend syntactic equality (if
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}={\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>then
${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}}\;{\simeq}\;{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>with the monoidal axioms of sequential composition:

${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{skip}}}};{T}}}}}}\;{\simeq}\;{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}}\quad\text{and}\quad{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{T};{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{skip}}}}}}}}}\;{\simeq}\;{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(neutral element)
${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{T};{U}}})};{V}}}}}}\;{\simeq}\;{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{T};{({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{U};{V}}})}}}}}}$
(associativity)
${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\oplus}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\\{{\ell}\colon{T_{\ell}}\\}_{{\ell}\in{L}}}}};{U}}}}}}\;{\simeq}\;{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\oplus}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\\{{\ell}\colon{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{T_{\ell}};{U}}}}\\}_{{\ell}\in{L}}}}}}}\quad\text{and}\quad{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\&}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\\{{\ell}\colon{T_{\ell}}\\}_{{\ell}\in{L}}}}};{U}}}}}}\;{\simeq}\;{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\&}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\\{{\ell}\colon{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{T_{\ell}};{U}}}}\\}_{{\ell}\in{L}}}}}}}$
(distributivity)

as well as an equirecursive treatment of recursive types:

${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}}}}\;{\simeq}\;{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{[}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{/}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{x}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{]}}}}}$
(unfolding)

We can define a conversion from types to simple grammars and show that it
preserves and reflects type equivalence into simple grammar bisimilarity. We
define the procedure $\operatorname{word}(\cdot)$ that receives a type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and returns a word of nonterminal symbols
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})$,
while constructing a simple grammar $\mathcal{G}$ as a side effect. The
procedure creates fresh nonterminal symbols as needed.

  * •

$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{M}}})=X$
for a fresh nonterminal symbol $X$ with production
$X\overset{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{M}}}}{\rightarrow}\varepsilon$.

  * •

$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{!{M}}})=X$
for a fresh nonterminal symbol $X$ with production
$X\overset{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{!{M}}}}{\rightarrow}\varepsilon$.

  * •

$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\oplus}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\\{{\ell}\colon{T_{\ell}}\\}_{{\ell}\in{L}}}})=X$
for a fresh nonterminal symbol $X$ with productions
$X\overset{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\oplus}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\ell}}}{\rightarrow}\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\ell}}})$.

  * •

$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\&}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\\{{\ell}\colon{T_{\ell}}\\}_{{\ell}\in{L}}}})=X$
for a fresh nonterminal symbol $X$ with productions
$X\overset{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\&}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\ell}}}{\rightarrow}\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\ell}}})$.

  * •

$\operatorname{word}(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{skip}}})=\varepsilon$.

  * •

$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{T};{U}}})=\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}})$.

  * •

If
${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}}}}\>\mathrm{\checkmark}$,
then
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}})=\varepsilon$.

  * •

If
${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}}}}\>\mathrm{\not\\!\checkmark}$,
then
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}})=X$
for a fresh nonterminal symbol $X$. Let
$Y\delta=\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})$.
Then $X$ has a production $X\overset{a}{\rightarrow}\gamma\delta$ for each
production $Y\overset{a}{\rightarrow}\gamma$. Moreover,
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{x}})=X$.

For the purposes of this paper, we may assume by definition that types
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}},{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>are equivalent
(${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}}\;{\simeq}\;{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>if their corresponding conversions to simple grammars yield bisimilar words,
that is,
${{\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})}}\;{\sim}\;{{\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}})}}$).
For simplicity, we assume that the sets of nonterminals built during the
construction of
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})$
and
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}})$
are disjoint, so we can trivially fuse the two simple grammars into one.

###  7.4 Conversion to simple grammars

As an estimate for the encoding size of a type, we define the _size_ of
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>denoted
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>inductively on
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>as follows:
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{M}}}|=|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{!{M}}}|=1$,
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\oplus}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\\{{\ell}\colon{T_{\ell}}\\}_{{\ell}\in{L}}}}|=|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\&}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>L}|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$|\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{T};{U}}}|=1+|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}|+|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}|=1+|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
######  Lemma 32.

Let
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>be a type and
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})$
its conversion to a simple grammar $\mathcal{G}$. Then the number of
nonterminals of $\mathcal{G}$, the degree of $\mathcal{G}$, the seminorm of
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})$
and the valuation of $\mathcal{G}$ are all less than or equal to
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
###### Proof.

We begin by noticing that
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>corresponds to the number of distinct subexpressions of
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(or alternatively, to the number of nodes in an abstract syntax tree
representation of
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}$).
By inspection on the rules defining the procedure
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})$,
we notice that at most one nonterminal is created for each subexpression of
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Hence at most
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>nonterminals are generated. A similar argument can be made for the number of
terminals. Regarding the number of productions, when computing
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}})$
we create one new production for each production for
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})$.
In all other cases we create at most one production for each subexpression of
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Therefore, the maximum number of transitions of a non-terminal in
$\mathcal{G}$ (i.e., the degree of $\mathcal{G}$) is again bounded by
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>The next step is to prove that
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}))\leq|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>This is done by induction on
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
  * •

Suppose
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{?{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Then
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}))=1=|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>The case where
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{!{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is similar.

  * •

Suppose
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\oplus}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Then
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})=X$
for a fresh nonterminal symbol $X$ with productions
$X\overset{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\oplus}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\ell}}}{\rightarrow}\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\ell}}})$.
By induction,
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\ell}}}))\leq|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>for each
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>If $X$ is unnormed, then
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}))=\mathsf{s}(X)=0$,
which is trivially less than
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Otherwise, let
$X\overset{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\oplus}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\ell}}}{\rightarrow}\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\ell}}})$
be a norm-reducing transition. We have that
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}))=\mathsf{s}(X)=1+\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\ell}}}))\leq
1+|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>1+\sum_{\ell\in
L}|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{\ell}}}|=|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>as desired. The case where
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\&}}{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is similar.

  * •

Suppose
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Then
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}))=0<1=|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
  * •

Suppose
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{U};{V}}}$.
Then
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})=\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}})\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{V}})$
and, by induction,
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}))\leq|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{V}}))\leq|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>If
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}})$
is unnormed, then
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}})\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{V}}))=\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}))\leq|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Otherwise,
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}})\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{V}}))=\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}))+\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{V}}))\leq|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}|+|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>In either case, we have
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}))<1+|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}|+|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{V}}|=|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
  * •

The case that
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is not applicable since
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is not a type (under the empty context).

  * •

Suppose
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{U}}}$,
with
${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Then
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}))=\mathsf{s}(\varepsilon)=0<|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
  * •

Suppose
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{U}}}$,
with
${{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}}}}\>\mathrm{\not\\!\checkmark}$.
Then
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{U}}})$
is some nonterminal symbol $X$. If $X$ is unnormed, then again
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}))=0<|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Finally, suppose that $X$ is normed. This last case is not trivial, since we
cannot directly apply the induction hypothesis to
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>as
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>may occur free in
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Let us use
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>to denote the type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>i.e., an empty choice. Notice that
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\bot}})=\bot$
is a nonterminal symbol without productions (we slightly abuse notation here,
reusing the symbol $\bot$). Consider the type
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{[}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\bot}}}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{/}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{x}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{]}}$
obtained by replacing all free occurrences of
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>in
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>by
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Let $\mathcal{G}^{\prime}$ be the grammar obtained when computing
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{[}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\bot}}}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{/}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{x}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{]}})$.
The only difference between $\mathcal{G}$ and $\mathcal{G}^{\prime}$ is that
$X$ is replaced by $\bot$ in the right-hand side of all productions. Since $X$
is normed in $\mathcal{G}$, any of its norm-reducing sequences in
$\mathcal{G}$ never visits a word containing $X$ itself. Thus, any such
sequence is also norm-reducing in $\mathcal{G}^{\prime}$. We conclude that $X$
is normed in $G^{\prime}$, and moreover
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}))^{\mathcal{G}}$
=
$\mathsf{s}(X)^{\mathcal{G}}=\mathsf{s}(X)^{\mathcal{G}^{\prime}}=\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{[}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\bot}}}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{/}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{x}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{]}}))^{\mathcal{G}^{\prime}}$.
Notice that
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{[}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\bot}}}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{/}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{x}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{]}}$
is a type since
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>no longer appears free. By induction hypothesis,
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{[}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\bot}}}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{/}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{x}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{]}}))^{\mathcal{G}^{\prime}}\leq|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{[}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\bot}}}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{/}}{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{x}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{]}}|=|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}}|<|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
We just need to conclude that the valuation of $\mathcal{G}$ is at most
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Each of the words appearing on the right-hand side of productions of
$\mathcal{G}$ is of the form
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{1}}})\ldots\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{n}}})$,
where
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{1}}}$,…,${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>are non-overlapping subexpressions of
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>By the previous bound, we have
$\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{1}}})\ldots\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{n}}}))\leq\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{1}}}))+\ldots+\mathsf{s}(\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{n}}}))\leq|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{1}}}|+\ldots+|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T_{n}}}|\leq|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Thus, the valuation of $\mathcal{G}$ is at most
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>∎

######  Theorem 33.

There is a polynomial-time algorithm for determining whether two context-free
session types
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>are equivalent.

###### Proof.

The algorithm for type equivalence converts both types
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>into words
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})$,
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}})$
over a common simple grammar $\mathcal{G}$, and then applies the basis-
updating algorithm presented in section 5. Clearly, the conversion to a simple
grammar runs in polynomial time. By lemma 32, the size and valuation of
$\mathcal{G}$, as well as the seminorms of
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})$,
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}})$,
are all bounded by
$\max\\{|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}}|,|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>By theorem 31, the time complexity of the basis-updating algorithm is
polynomial on the size of $\mathcal{G}$, the valuation of $\mathcal{G}$, and
the seminorms of
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{T}})$,
$\operatorname{word}({\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{U}})$.
Therefore, the algorithm for type equivalence has total running time
polynomial in
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
$|{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>∎

##  8 Conclusion

This paper presents a single-exponential running time algorithm for the simple
grammar bisimilarity problem. As an application, we provide the first
polynomial-time algorithm for deciding context-free session type equivalence.

As future work, we plan to develop an implementation of the basis-updating
algorithm, to be incorporated into the FreeST programming language [2]. We
would also like to compare the empirical running time of such an
implementation against the current implementation in FreeST, which is based on
the 2-EXPTIME algorithm for context-free grammars.

It remains open the question whether a polynomial-time algorithm exists for
simple grammar bisimilarity. In our basis-updating updating algorithm, between
any two consecutive changes in $\mathcal{B}$, new nodes are generated by
applying BPA rules to existing nodes, i.e., the algorithm is essentially
checking for coinductive congruence during these stages. This is the key point
at which our analysis yields an exponential running time, since the number of
new nodes generated is polynomial in the maximum seminorm among all words,
which itself may grow exponentially. In order to reach a polynomial-time
algorithm (or prove that none exist, conditioned on some complexity-theoretic
assumption), it is thus worthwhile to gain a deeper understanding of the
_coinductive congruence decision problem_ :

Given a simple grammar $\mathcal{G}=(\mathcal{V},\mathcal{T},\mathcal{P})$, a
basis $\mathcal{B}$ over $\mathcal{G}$, and words of nonterminals
$\gamma,\delta\in\mathcal{V}^{\ast}$, determine whether
${{\gamma}}\;{\equiv^{\mathsf{c}}_{\mathcal{B}}}\;{{\delta}}$.

We can restrict $\mathcal{B}$ to satisfy “suitable” assumptions such as those
given in definition 17. It might be possible to explore cyclic properties on
the structure of congruent pairs of words to design an improved algorithm, in
an approach similar to Hirshfeld et al. [18] or Jančar [24]. Besides its
theoretical importance, a polynomial-time algorithm would have a practical
application in other formulations of context-free session types, such as those
where infinite types are represented by means of (mutually recursive)
equations rather than the
${\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mu\,{x}.{T}}}$
recursion operator [13].

Another significant open question in the area is closing the complexity gap
for context-free grammar bisimilarity (between EXPTIME-hardness and
2-EXPTIME). It is not clear whether the techniques presented in this paper can
be applied in the general setting. The main issue is that the uniqueness
results in lemmas 15 and 16 no longer hold. In fact, given $X$, $Y$, there
might be finite but exponentially many non-bisimilar solutions to
${{X\alpha}}\;{\sim}\;{{Y\beta}}$. As a natural approach, we would propose
understanding the structure of such solutions and, for example, extending our
basis-updating algorithm to allow for exponentially many BPA pairs
$(X\alpha,Y\beta)$ in the basis for given nonterminals $X,Y$.

## References

  * [1] Bernardo Almeida, Andreia Mordido, Peter Thiemann, and Vasco T. Vasconcelos.  Polymorphic context-free session types.  CoRR, 2021.  arXiv:2106.06658.
  * [2] Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos.  FreeST, a programming language with context-free session types.  https://freest-lang.github.io/, 2019.
  * [3] Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos.  FreeST: Context-free session types in a functional language.  In PLACES, volume 291 of EPTCS, pages 12–23, 2019.  doi:10.4204/EPTCS.291.2.
  * [4] Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos.  Deciding the bisimilarity of context-free session types.  In TACAS, volume 12079 of LNCS, pages 39–56. Springer, 2020\.  doi:10.1007/978-3-030-45237-7\\_3.
  * [5] Jos C. M. Baeten, Jan A. Bergstra, and Jan Willem Klop.  Decidability of bisimulation equivalence for processes generating context-free languages.  In PARLE, volume 259 of LNCS, pages 94–111. Springer, 1987\.  doi:10.1007/3-540-17945-3\\_5.
  * [6] Yehoshua Bar-Hillel, Micha Perles, and Eli Shamir.  On formal properties of simple phrase structure grammars.  Sprachtypologie und Universalienforschung, 14:143–172, 1961.
  * [7] Michael Benedikt, Stefan Göller, Stefan Kiefer, and Andrzej S. Murawski.  Bisimilarity of pushdown automata is nonelementary.  In LICS, pages 488–498. IEEE Computer Society, 2013.  doi:10.1109/LICS.2013.55.
  * [8] Jan A. Bergstra and Jan Willem Klop.  Process theory based on bisimulation semantics.  In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS, pages 50–122. Springer, 1988\.  doi:10.1007/BFB0013021.
  * [9] Olaf Burkart, Didier Caucal, and Bernhard Steffen.  An elementary bisimulation decision procedure for arbitrary context-free processes.  In MFCS, volume 969 of LNCS, pages 423–433. Springer, 1995\.  doi:10.1007/3-540-60246-1\\_148.
  * [10] Didier Caucal.  A fast algorithm to decide on simple grammars equivalence.  In Optimal Algorithms, volume 401 of LNCS, pages 66–85. Springer, 1989.  doi:10.1007/3-540-51859-2\\_8.
  * [11] Didier Caucal.  Graphes canoniques de graphes algébriques.  RAIRO - Theoretical Informatics and Applications, 24(4):339–352, 1990.  doi:10.1051/ita/1990240403391.
  * [12] Søren Christensen, Hans Hüttel, and Colin Stirling.  Bisimulation equivalence is decidable for all context-free processes.  Inf. Comput., 121(2):143–148, 1995.  doi:10.1006/inco.1995.1129.
  * [13] Diana Costa, Andreia Mordido, Diogo Poças, and Vasco T. Vasconcelos.  Polymorphic higher-order context-free session types.  Theor. Comput. Sci., 1001:114582, 2024.  doi:10.1016/J.TCS.2024.114582.
  * [14] Diana Costa, Andreia Mordido, Diogo Poças, and Vasco T. Vasconcelos.  Higher-order context-free session types in system F.  Electronic Proceedings in Theoretical Computer Science, 356:24–35, 2022.  doi:10.4204/eptcs.356.3.
  * [15] Wojciech Czerwinski and Slawomir Lasota.  Fast equivalence-checking for normed context-free processes.  In FSTTCS, volume 8 of LIPIcs, pages 260–271. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010.  doi:10.4230/LIPIcs.FSTTCS.2010.260.
  * [16] Rob J. van Glabbeek.  The linear time-branching time spectrum (extended abstract).  In CONCUR, volume 458 of LNCS, pages 278–297. Springer, 1990\.  doi:10.1007/BFB0039066.
  * [17] Sheila A. Greibach.  A new normal-form theorem for context-free phrase structure grammars.  J. ACM, 12(1):42—52, 1965.  doi:10.1145/321250.321254.
  * [18] Yoram Hirshfeld, Mark Jerrum, and Faron Moller.  A polynomial algorithm for deciding bisimilarity of normed context-free processes.  Theor. Comput. Sci., 158(1):143–159, 1996.  doi:10.1016/0304-3975(95)00064-X.
  * [19] Kohei Honda.  Types for dyadic interaction.  In CONCUR, volume 715 of LNCS, pages 509–523. Springer, 1993.  doi:10.1007/3-540-57208-2\\_35.
  * [20] Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo.  Language primitives and type discipline for structured communication-based programming.  In ESOP, volume 1381 of LNCS, pages 122–138. Springer, 1998\.  doi:10.1007/BFb0053567.
  * [21] John E Hopcroft and Richard M. Karp.  A linear algorithm for testing equivalence of finite automata.  Technical report, Cornell University, 1971.
  * [22] Harry B. Hunt III, Daniel J. Rosenkrantz, and Thomas G. Szymanski.  On the equivalence, containment, and covering problems for the regular and context-free languages.  J. Comput. Syst. Sci., 12(2):222–268, 1976.  doi:10.1016/S0022-0000(76)80038-4.
  * [23] Petr Jančar.  A short decidability proof for DPDA language equivalence via first-order grammars.  CoRR, 2010.  arXiv:1010.4760.
  * [24] Petr Jančar.  Bisimilarity on basic process algebra is in 2-EXPTIME (an explicit proof).  Log. Methods Comput. Sci., 9(1), 2012.  doi:10.2168/LMCS-9(1:10)2013.
  * [25] Petr Jančar.  Equivalence of pushdown automata via first-order grammars.  J. Comput. Syst. Sci., 115:86–112, 2021.  doi:10.1016/J.JCSS.2020.07.004.
  * [26] Petr Jančar and Faron Moller.  Techniques for decidability and undecidability of bisimilarity.  In CONCUR, volume 1664 of LNCS, pages 30–45. Springer, 1999\.  doi:10.1007/3-540-48320-9\\_5.
  * [27] Paris C. Kanellakis and Scott A. Smolka.  CCS expressions, finite state processes, and three problems of equivalence.  Inf. Comput., 86(1):43–68, 1990.  doi:10.1016/0890-5401(90)90025-d.
  * [28] Stefan Kiefer.  BPA bisimilarity is EXPTIME-hard.  Inf. Process. Lett., 113(4):101–106, 2013.  doi:10.1016/j.ipl.2012.12.004.
  * [29] R. Milner.  Communication and Concurrency.  Prentice Hall, 1989.
  * [30] Robin Milner.  An algebraic definition of simulation between programs.  In IJCAI, pages 481–489. William Kaufmann, 1971.  URL: http://ijcai.org/Proceedings/71/Papers/044.pdf.
  * [31] Robin Milner.  A Calculus of Communicating Systems, volume 92 of LNCS.  Springer, 1980.  doi:10.1007/3-540-10235-3.
  * [32] Robin Milner, Joachim Parrow, and David Walker.  A calculus of mobile processes, I.  Inf. Comput., 100(1):1–40, 1992.  doi:10.1016/0890-5401(92)90008-4.
  * [33] Robin Milner, Joachim Parrow, and David Walker.  A calculus of mobile processes, II.  Inf. Comput., 100(1):41–77, 1992.  doi:10.1016/0890-5401(92)90009-5.
  * [34] Faron Moller, Scott A. Smolka, and Jirí Srba.  On the computational complexity of bisimulation, redux.  Inf. Comput., 194(2):129–143, 2004.  doi:10.1016/J.IC.2004.06.003.
  * [35] Robert Paige and Robert Endre Tarjan.  Three partition refinement algorithms.  SIAM J. Comput., 16(6):973–989, 1987.  doi:10.1137/0216062.
  * [36] David Michael Ritchie Park.  Concurrency and automata on infinite sequences.  In Conference on Theoretical Computer Science, volume 104 of LNCS, pages 167–183. Springer, 1981.  doi:10.1007/BFB0017309.
  * [37] Diogo Poças, Diana Costa, Andreia Mordido, and Vasco T. Vasconcelos.  System $F^{\mu}_{\omega}$ with context-free session types.  In ESOP, volume 13990 of LNCS, pages 392–420. Springer, 2023\.  doi:10.1007/978-3-031-30044-8\\_15.
  * [38] Géraud Sénizergues.  Decidability of bisimulation equivalence for equational graphs of finite out-degree.  In FOCS, pages 120–129. IEEE Computer Society, 1998.  doi:10.1109/SFCS.1998.743435.
  * [39] Géraud Sénizergues.  L(A)=L(B)? decidability results from complete formal systems.  Theor. Comput. Sci., 251(1-2):1–166, 2001.  doi:10.1016/S0304-3975(00)00285-1.
  * [40] Jirí Srba.  Roadmap of infinite results.  Bull. EATCS, 78:163–175, 2002.  doi:10.1142/9789812562494_0054.
  * [41] Jirí Srba.  Strong bisimilarity and regularity of basic process algebra is PSPACE-hard.  In ICALP, volume 2380 of LNCS, pages 716–727. Springer, 2002\.  doi:10.1007/3-540-45465-9\\_61.
  * [42] Colin Stirling.  Decidability of bisimulation equivalence for normed pushdown processes.  Theor. Comput. Sci., 195(2):113–131, 1998.  doi:10.1016/S0304-3975(97)00216-8.
  * [43] Colin Stirling.  Deciding DPDA equivalence is primitive recursive.  In ICALP, volume 2380 of LNCS, pages 821–832. Springer, 2002\.  doi:10.1007/3-540-45465-9\\_70.
  * [44] Kaku Takeuchi, Kohei Honda, and Makoto Kubo.  An interaction-based language and its typing system.  In PARLE, volume 817 of LNCS, pages 398–413. Springer, 1994\.  doi:10.1007/3-540-58184-7\\_118.
  * [45] Peter Thiemann and Vasco T. Vasconcelos.  Context-free session types.  In ICFP, pages 462–475. ACM, 2016.  doi:10.1145/2951913.2951926.

##  Appendix A Alternative notions of congruences

In this appendix we compare our notion of coinductive congruence (definition
18) with two alternative notions: least congruence and inductive congruence.
We adapt some of the results in section 4 for these notions. Namely, we show
that lemmas 19 and 21 also hold for least congruence and inductive congruence;
and that theorem 23 also holds for inductive congruence (under suitable
assumptions on the basis).

######  Definition 34 (Least congruence [11, 12, 18]).

Let $\mathcal{B}$ be a basis for some given context-free grammar
$\mathcal{G}=(\mathcal{V},\mathcal{T},\mathcal{P})$. We define the _least
congruence_ induced by $\mathcal{B}$, $\equiv^{\ell}_{\mathcal{B}}$,
inductively as follows.

  * •

inclusion: If $(\alpha,\beta)\in\mathcal{B}$, then
${{\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\beta}}$.

  * •

reflexivity: For every $\alpha\in\mathcal{V}^{\ast}$,
${{\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\alpha}}$.

  * •

symmetry: If ${{\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\beta}}$, then
${{\beta}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\alpha}}$.

  * •

transitivity: If ${{\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\beta}}$ and
${{\beta}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\gamma}}$, then
${{\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\gamma}}$.

  * •

congruence: If ${{\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\beta}}$ and
${{\gamma}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta}}$, then
${{\alpha\gamma}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\beta\delta}}$.

*[Right=$\varepsilon$-Ax] ε ≡^i_B ε *[Right=BPA1-L] γα ≡^i_B β (X,Yγ)∈B Xα ≡^i_B Yβ *[Right=BPA2-L] α ≡^i_B α’ β ≡^i_B β’ (Xα,Yβ)∈B Xα’ ≡^i_B Yβ’

Figure 6: Inductive congruence. Right-hand rules omitted.

Inductive congruence follows the exact same rules as coinductive congruence.
The difference is that they are interpreted inductively (least fixed point
instead of greatest fixed point).

######  Definition 35 (Inductive congruence).

Let $\mathcal{B}$ be a basis for some given context-free grammar. We define
_inductive congruence_ , $\equiv^{\mathsf{i}}_{\mathcal{B}}$, according to the
rules in fig. 6, interpreted inductively. That is,
$\equiv^{\mathsf{i}}_{\mathcal{B}}$ is the smallest relation on
$\mathcal{V}^{\ast}\times\mathcal{V}^{\ast}$ such that:

  * •

($\varepsilon$-Ax)
${{\varepsilon}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\varepsilon}}$;

  * •

(BPA1-L) if ${{\gamma\alpha}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\beta}}$
and $(X,Y\gamma)\in\mathcal{B}$, then
${{X\alpha}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{Y\beta}}$;

  * •

(BPA1-R) if ${{\gamma\alpha}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\beta}}$
and $(X,Y\gamma)\in\mathcal{B}$, then
${{Y\beta}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{X\alpha}}$;

  * •

(BPA2-L) if
${{\alpha}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\alpha^{\prime}}}$,
${{\beta}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\beta^{\prime}}}$ and
$(X\alpha,Y\beta)\in\mathcal{B}$, then
${{X\alpha^{\prime}}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{Y\beta^{\prime}}}$;

  * •

(BPA2-R) if
${{\alpha}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\alpha^{\prime}}}$,
${{\beta}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\beta^{\prime}}}$ and
$(X\alpha,Y\beta)\in\mathcal{B}$, then
${{Y\beta^{\prime}}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{X\alpha^{\prime}}}$.

Let us compare the three notions of congruence defined in this paper.

######  Proposition 36.

Let $\mathcal{B}$ be a basis for some given context-free grammar. Then
$\equiv^{\mathsf{i}}_{\mathcal{B}}\ \subseteq\ \equiv^{\ell}_{\mathcal{B}}$
and $\equiv^{\mathsf{i}}_{\mathcal{B}}\ \subseteq\
\equiv^{\mathsf{c}}_{\mathcal{B}}$.

###### Proof.

The proof that $\equiv^{\mathsf{i}}_{\mathcal{B}}\ \subseteq\
\equiv^{\ell}_{\mathcal{B}}$ follows by structural induction. Supposing that
${{\sigma}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\tau}}$, we consider a
case analysis on the last rule in the derivation.

($\varepsilon$-Ax): then $\sigma=\tau=\varepsilon$. It follows that
${{\varepsilon}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\varepsilon}}$ due to
reflexivity.

(BPA1-L): then $\sigma=X\alpha$ and $\tau=Y\beta$, where
${{\gamma\alpha}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\beta}}$ and
$(X,Y\gamma)\in\mathcal{B}$. By induction,
${{\gamma\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\beta}}$. By inclusion,
${{X}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{Y\gamma}}$. By congruence and
reflexivity, ${{X\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{Y\gamma\alpha}}$
and ${{Y\gamma\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{Y\beta}}$. By
transitivity, ${{X\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{Y\beta}}$. Rule
(BPA1-R) is handled similarly.

(BPA2-L): then $\sigma=X\alpha^{\prime}$ and $\tau=Y\beta^{\prime}$, where
${{\alpha}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\alpha^{\prime}}}$,
${{\beta}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\beta^{\prime}}}$ and
$(X\alpha,Y\beta)\in\mathcal{B}$. By induction,
${{\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\alpha^{\prime}}}$ and
${{\beta}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\beta^{\prime}}}$. By inclusion,
${{X\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{Y\beta}}$. By congruence and
reflexivity,
${{X\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{X\alpha^{\prime}}}$ and
${{Y\beta}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{Y\beta^{\prime}}}$. By symmetry
and transitivity,
${{X\alpha^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{Y\beta^{\prime}}}$.
Rule (BPA2-R) is handled similarly.

To prove that $\equiv^{\mathsf{i}}_{\mathcal{B}}\ \subseteq\
\equiv^{\mathsf{c}}_{\mathcal{B}}$, we may simply observe that
$\equiv^{\mathsf{i}}_{\mathcal{B}}$ is backward closed for the rules defining
$\equiv^{\mathsf{c}}_{\mathcal{B}}$ coinductively. Again, this is a simple
proof by structural induction. Supposing that
${{\sigma}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\tau}}$, we consider a
case analysis on the last rule in the derivation.

(BPA2-L): then $\sigma=X\alpha^{\prime}$ and $\tau=Y\beta^{\prime}$, where
${{\alpha}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\alpha^{\prime}}}$,
${{\beta}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\beta^{\prime}}}$ and
$(X\alpha,Y\beta)\in\mathcal{B}$. Applying rule (BPA2-L) to
${{\sigma}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\tau}}$ gives us exactly
the judgements
${{\alpha}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\alpha^{\prime}}}$ and
${{\beta}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\beta^{\prime}}}$. The
remaining rules are dealt in a similar manner. ∎

The following example shows that, in general, $\equiv^{\ell}_{\mathcal{B}}\
\not\subseteq\ \equiv^{\mathsf{i}}_{\mathcal{B}}$ and
$\equiv^{\ell}_{\mathcal{B}}\ \not\subseteq\
\equiv^{\mathsf{c}}_{\mathcal{B}}$. Consider $\mathcal{V}=\\{X,Y,Z\\}$ and
$\mathcal{B}=\\{(X,Y),(Y,Z)\\}$. Then, by inclusion and transitivity,
${{X}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{Z}}$. However, neither
${{X}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{Z}}$ nor
${{X}}\;{\equiv^{\mathsf{c}}_{\mathcal{B}}}\;{{Z}}$ as no rule can be applied
to pair $(X,Z)$. This example also shows that, in general,
$\equiv^{\mathsf{i}}_{\mathcal{B}}$ and $\equiv^{\mathsf{c}}_{\mathcal{B}}$
are not transitive relations.

The following example shows that, in general,
$\equiv^{\mathsf{c}}_{\mathcal{B}}\ \not\subseteq\
\equiv^{\mathsf{i}}_{\mathcal{B}}$ and $\equiv^{\mathsf{c}}_{\mathcal{B}}\
\not\subseteq\ \equiv^{\ell}_{\mathcal{B}}$ (in particular,
$\equiv^{\mathsf{c}}_{\mathcal{B}}$ and $\equiv^{\ell}_{\mathcal{B}}$ are
incomparable). Consider $\mathcal{V}=\\{X,Y,Z,W\\}$ and
$\mathcal{B}=\\{(X,YWYZ),(Z,WX)\\}$. Then
${{X}}\;{\equiv^{\mathsf{c}}_{\mathcal{B}}}\;{{YZ}}$, as witnessed by the
following (infinite) derivation.

$\inferrule*[Right=BPA1-L]{\inferrule*[Right=BPA1-R]{\inferrule*[Right=BPA1-L]{\vdots}{{{X}}\;{\equiv^{\mathsf{c}}_{\mathcal{B}}}\;{{YZ}}}}{{{WYZ}}\;{\equiv^{\mathsf{c}}_{\mathcal{B}}}\;{{Z}}}}{{{X}}\;{\equiv^{\mathsf{c}}_{\mathcal{B}}}\;{{YZ}}}$

Alternatively, observe that $\mathcal{R}=\\{(X,YZ),(WYZ,Z)\\}$ is backward
closed for the rules defining coinductive congruence, so that
$\mathcal{R}\subseteq\ \equiv^{\mathsf{c}}_{\mathcal{B}}$ and thus
${{X}}\;{\equiv^{\mathsf{c}}_{\mathcal{B}}}\;{{YZ}}$.

On the other hand, it is not the case that
${{X}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{YZ}}$. Any attempt at deriving
${{X}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{YZ}}$ must either use rule
BPA1-L, arriving at judgement
${{WYZ}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{Z}}$, or rule BPA2-L,
arriving at judgements
${{\varepsilon}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\varepsilon}}$ (which
does hold due to rule $\varepsilon$-Ax) and
${{WYZ}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{Z}}$. Similarly, any attempt
at deriving ${{WYZ}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{Z}}$ must either
use rule BPA1-R, arriving at judgement
${{X}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{YZ}}$, or rule BPA2-R, arriving
at judgements
${{\varepsilon}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\varepsilon}}$ (which
does hold due to rule $\varepsilon$-Ax) and
${{X}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{YZ}}$. In any case, any attempt
at deriving ${{X}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{YZ}}$ gets stuck in
a loop, alternating between judgements
${{X}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{YZ}}$ and
${{WYZ}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{Z}}$.

Finally, it is also not the case that
${{X}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{YZ}}$. By repeatedly applying the
pairs in $\mathcal{B}$, we can see that the equivalence classes of $X$ and
$YZ$ are disjoint and given by the sequences

${{X}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{{{YWYZ}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{{{YWYWX}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{{{YWYWYZ}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\cdots}}}}}}}}$
${{YZ}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{{{YWX}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{{{YWYWYZ}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{{{YWYWYWX}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\cdots}}}}}}}}$

######  Lemma 37.

Let $\mathcal{B}$ be a basis for some given context-free grammar without dead
nonterminals. If $\mathcal{B}\subseteq\ \sim$, then
$\equiv^{\ell}_{\mathcal{B}}\ \subseteq\ \sim$ and
$\equiv^{\mathsf{i}}_{\mathcal{B}}\ \subseteq\ \sim$.

###### Proof.

Suppose that $\mathcal{B}\subseteq\ \sim$. The fact that
$\equiv^{\ell}_{\mathcal{B}}\ \subseteq\ \sim$ is a simple consequence of the
fact that $\sim$ is itself closed under reflexivity, symmetry, transitivity
and congruence (proposition 6). The fact that
$\equiv^{\mathsf{i}}_{\mathcal{B}}\ \subseteq\ \sim$ follows from
$\equiv^{\mathsf{i}}_{\mathcal{B}}\ \subseteq\ \equiv^{\ell}_{\mathcal{B}}$
(proposition 36) plus the above observation. ∎

######  Definition 38 (Self-bisimulation).

Let $\mathcal{B}$ be a basis for some given context-free grammar. Let
$\equiv^{\mathsf{x}}_{\mathcal{B}}$ denote one of the three notions of
congruence (least congruence, inductive congruence, or coinductive congruence)
according to $\mathcal{B}$. We say that $\mathcal{B}$ is a _self-bisimulation_
with respect to $\equiv^{\mathsf{x}}_{\mathcal{B}}$ if, for every pair
$(\gamma,\delta)\in\mathcal{B}$ and every nonterminal $a\in\mathcal{T}$:

  1. 1.

if $\gamma\overset{a}{\rightarrow}\gamma^{\prime}$ for some $\gamma^{\prime}$,
then there exists some $\delta^{\prime}$ such that
$\delta\overset{a}{\rightarrow}\delta^{\prime}$ and
${{\gamma^{\prime}}}\;{\equiv^{\mathsf{x}}_{\mathcal{B}}}\;{{\delta^{\prime}}}$;

  2. 2.

if $\delta\overset{a}{\rightarrow}\delta^{\prime}$ for some $\delta^{\prime}$,
then there exists some $\gamma^{\prime}$ such that
$\gamma\overset{a}{\rightarrow}\gamma^{\prime}$ and
${{\gamma^{\prime}}}\;{\equiv^{\mathsf{x}}_{\mathcal{B}}}\;{{\delta^{\prime}}}$.

######  Lemma 39.

Let $\mathcal{B}$ be a basis for some given context-free grammar without dead
symbols.

  1. 1.

If $\mathcal{B}$ is a self-bisimulation with respect to
$\equiv^{\ell}_{\mathcal{B}}$, then $\equiv^{\ell}_{\mathcal{B}}$ is a
bisimulation; in particular, $\equiv^{\ell}_{\mathcal{B}}\ \subseteq\ \sim$.

  2. 2.

If $\mathcal{B}$ is a self-bisimulation with respect to
$\equiv^{\mathsf{i}}_{\mathcal{B}}$, then $\equiv^{\mathsf{i}}_{\mathcal{B}}\
\subseteq\ \sim$.

###### Proof.

Let us first consider the least congruence $\equiv^{\ell}_{\mathcal{B}}$.
Given ${{\gamma}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta}}$, we need to show
that any transition $\gamma\overset{a}{\rightarrow}\gamma^{\prime}$ has a
matching transition $\delta\overset{a}{\rightarrow}\delta^{\prime}$ with
${{\gamma^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta^{\prime}}}$, and
vice-versa. The proof is by structural induction on the (finite) proof of
${{\gamma}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta}}$.

(inclusion): then $(\gamma,\delta)\in\mathcal{B}$. By the definition of self-
bisimulation, we immediately get that any transition
$\gamma\overset{a}{\rightarrow}\gamma^{\prime}$ has a matching transition
$\delta\overset{a}{\rightarrow}\delta^{\prime}$ with
${{\gamma^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta^{\prime}}}$, and
vice-versa.

(reflexivity): if $\gamma=\delta$, then any transition
$\gamma\overset{a}{\rightarrow}\gamma^{\prime}$ has the (same) matching
transition $\gamma\overset{a}{\rightarrow}\gamma^{\prime}$. Moreover,
${{\gamma^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\gamma^{\prime}}}$ due
to reflexivity.

(symmetry): suppose that the proof of
${{\gamma}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta}}$ ends with the symmetry
rule, i.e., the proof continues with
${{\delta}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\gamma}}$. By structural
induction, any transition $\delta\overset{a}{\rightarrow}\delta^{\prime}$ has
a matching transition $\gamma\overset{a}{\rightarrow}\gamma^{\prime}$ with
${{\delta^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\gamma^{\prime}}}$ (and
thus,
${{\gamma^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta^{\prime}}}$ by
symmetry), and vice-versa. This is precisely what we needed to prove.

(transitivity): suppose that the proof of
${{\gamma}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta}}$ ends with the
transitivity rule, i.e., the proof continues with
${{\gamma}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\alpha}}$ and
${{\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta}}$ for some $\alpha$.
Consider a transition $\gamma\overset{a}{\rightarrow}\gamma^{\prime}$. By
structural induction, there is a matching transition
$\alpha\overset{a}{\rightarrow}\alpha^{\prime}$ with
${{\gamma^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\alpha^{\prime}}}$. In
turn, there is a matching transition
$\delta\overset{a}{\rightarrow}\delta^{\prime}$ with
${{\alpha^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta^{\prime}}}$. By
transitivity, we get
${{\gamma^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta^{\prime}}}$. Any
transition $\delta\overset{a}{\rightarrow}\delta^{\prime}$ may be matched by a
transition $\gamma\overset{a}{\rightarrow}\gamma^{\prime}$ in a similar
manner.

(congruence): suppose that the proof of
${{\gamma}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta}}$ ends with the
congruence rule, i.e., $\gamma=\alpha\gamma^{\prime}$,
$\delta=\beta\delta^{\prime}$, and the proof continues with
${{\alpha}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\beta}}$ and
${{\gamma^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta^{\prime}}}$. We
need to further consider three sub-cases.

In the case that $\alpha=\varepsilon$, by structural induction we get matching
transitions between $\alpha$ and $\beta$. Since the grammar has no dead
nonterminals, $\varepsilon$ is the only word with no transitions, hence
$\beta=\varepsilon$. By structural induction, we get matching transitions
between $\gamma^{\prime}$ and $\delta^{\prime}$, which are also matching
transitions between $\gamma=\alpha\gamma^{\prime}=\gamma^{\prime}$ and
$\delta=\beta\delta^{\prime}=\delta^{\prime}$.

The case that $\beta=\varepsilon$ is handled similarly.

Finally, consider the case that $\alpha,\beta\neq\varepsilon$. Any transition
from $\alpha\gamma^{\prime}$ is of the form
$\alpha\gamma^{\prime}\overset{a}{\rightarrow}\alpha^{\prime}\gamma^{\prime}$
with $\alpha\overset{a}{\rightarrow}\alpha^{\prime}$. By structural induction,
there is a matching transition $\beta\overset{a}{\rightarrow}\beta^{\prime}$,
yielding the transition
$\beta\delta^{\prime}\overset{a}{\rightarrow}\beta^{\prime}\delta^{\prime}$.
Since ${{\alpha^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\beta^{\prime}}}$
and ${{\gamma^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\delta^{\prime}}}$,
we get by congruence that
${{\alpha^{\prime}\gamma^{\prime}}}\;{\equiv^{\ell}_{\mathcal{B}}}\;{{\beta^{\prime}\delta^{\prime}}}$.
Transitions from $\beta\delta^{\prime}$ are handled in a similar manner. This
concludes the proof that $\equiv^{\ell}_{\mathcal{B}}$ is a bisimulation.

Let us next consider inductive congruence,
$\equiv^{\mathsf{i}}_{\mathcal{B}}$. By proposition 36,
$\equiv^{\mathsf{i}}_{\mathcal{B}}\subseteq\equiv^{\ell}_{\mathcal{B}}$, and
thus if $\mathcal{B}$ is a self-bisimulation with respect to
$\equiv^{\mathsf{i}}_{\mathcal{B}}$, it is also with respect to
$\equiv^{\ell}_{\mathcal{B}}$. By the previous case, this implies
$\equiv^{\mathsf{i}}_{\mathcal{B}}\ \subseteq\ \equiv^{\ell}_{\mathcal{B}}\
\subseteq\ \sim$ as desired. ∎

######  Theorem 40.

Let $\mathcal{B}$ be a basis for some given simple grammar. Suppose that
$\mathcal{B}$ is functional and simple. Then
$\equiv^{\mathsf{i}}_{\mathcal{B}}$ is decidable. More precisely, given a pair
$\gamma$, $\delta$, we can determine whether
${{\gamma}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\delta}}$ in time
polynomial in the size of $\mathcal{B}$ and the maximum seminorm among
$\gamma$, $\delta$, and the words in $\mathcal{B}$.

###### Proof.

We can apply almost the same algorithm presented in the proof of theorem 23,
where we show that $\equiv^{\mathsf{c}}_{\mathcal{B}}$ is decidable. Given a
pair $\gamma$, $\delta$, we try to build the (unique) proof tree for
${{\gamma}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\delta}}$, preferring BPA1
rules over BPA2 when multiple rules are possible. By the argument presented in
the proof of theorem 23, only finitely many distinct pairs appear in the proof
tree. In both the inductive and coinductive algorithm, whenever a node
$(\gamma^{\prime},\delta^{\prime})$ is found such that no rule can be applied,
we can correctly conclude that $\gamma,\delta$ are not congruent; and if all
nodes have been expanded, we can correctly conclude that $\gamma,\delta$ are
congruent.

The only difference occurs in the handling of loops. Suppose that a node has a
pair $(\gamma^{\prime},\delta^{\prime})$ which has already appeared in one of
the node’s ancestors in the proof tree. While the coinductive algorithm would
accept this node (since, for coinductive congruence, infinite derivation trees
are allowed), the inductive algorithm instead correctly concludes that
$\gamma,\delta$ are not congruent, as any attempt to prove
${{\gamma^{\prime}}}\;{\equiv^{\mathsf{i}}_{\mathcal{B}}}\;{{\delta^{\prime}}}$
would result in an infinite derivation.

The upper bound on the total number of nodes generated by the inductive
algorithm is the same as in the coinductive algorithm, namely
$\mathcal{O}(|\mathcal{B}|^{2}m^{2})$, where $m$ is the maximum seminorm among
$\gamma,\delta$ and the words in $\mathcal{B}$.

∎