# Processes Parametrised by an Algebraic Theory††thanks: Schmid, Rozowski, and
Silva’s work was partially supported by ERC grant Autoprobe (grant agreement
101002697).

Todd Schmid<EMAIL_ADDRESS>UCL, London, UK  Wojciech Rozowski
<EMAIL_ADDRESS>UCL, London, UK  Alexandra Silva
<EMAIL_ADDRESS>Cornell University, Ithaca, New York, USA
Jurriaan Rot<EMAIL_ADDRESS>Radboud University, Nijmegen, The Netherlands

###### Abstract

We develop a (co)algebraic framework to study a family of process calculi with
monadic branching structures and recursion operators. Our framework features a
uniform semantics of process terms and a complete axiomatisation of semantic
equivalence. We show that there are uniformly defined fragments of our calculi
that capture well-known examples from the literature like regular expressions
modulo bisimilarity and guarded Kleene algebra with tests. We also derive new
calculi for probabilistic and convex processes with an analogue of Kleene
star.

##  1 Introduction

The theory of processes has a long tradition, notably in the study of
concurrency, pioneered by seminal works of Milner [1, 2] and many others [3].
In labelled transition systems, a popular model of computation in process
theory, processes branch nondeterministically. This means that any given
action or observation transitions a starting state into any member of a
predetermined set of states. In Milner’s CCS [2], nondeterminism appears as a
binary operation that constructs from a pair of programs $e$ and $f$ the
program $e+f$ that nondeterministically chooses between executing either $e$
or $f$. This acts precisely like the join operation in a semilattice. In fact,
elements of a free semilattice are exactly sets, as the free semilattice
generated by a collection $X$ is the set $\mathcal{P}_{\omega}^{+}X$ of finite
nonempty subsets of $X$ [4]. This is our first example of a more general
phenomenon: the type of branching in models of process calculi can often be
captured with an algebraic theory.

A second example appears in the probabilistic process algebra literature,
where the process denoted $e+_{p}f$ flips a weighted coin and runs $e$ with
probability $p$ and $f$ with probability $1-p$. The properties of $+_{p}$ are
axiomatised and studied in convex algebra, an often revisited algebraic theory
of probability [5, 6, 7, 8]. The free convex algebra on a set $X$ is the set
$\mathcal{D}_{\omega}X$ of finitely supported probability distributions on $X$
[8, 9, 10].

A third example is guarded Kleene algebra with tests ($\mathsf{GKAT}$), where
the process $e+_{b}f$ proceeds with $e$ if a certain Boolean predicate $b$
holds and otherwise proceeds with $f$, emulating the if-then-else constructs
of imperative programming languages [11, 12, 13]. If the predicates are taken
from a finite Boolean algebra $2^{\texttt{At}}$, the free algebra of if-then-
else clauses on a set $X$ is the function space $X^{\texttt{At}}$. This
explains why adjacency sets for tree models of $\mathsf{GKAT}$ programs take
the form of functions $\texttt{At}\to X$.

This paper proposes a framework in which these languages can be uniformly
described and studied. We use the _algebra of regular behaviours_ (or
$\mathsf{ARB}$) introduced in [1] as a prototypical example. $\mathsf{ARB}$
employs nondeterministic choice as a branching operation, prefixing of terms
by atomic actions, a constant representing deadlock, variables, and a
recursion operator for each variable. Specifications are interpreted using
structural operational semantics in the style of [14], which sees the set
$\mathtt{Exp}$ of all process terms as one large labelled transition system.
This is captured succinctly as a _coalgebra_ , in this case a function

$\beta:\mathtt{Exp}\to\mathcal{P}(V+A\times\mathtt{Exp})$ (1)

Only finitely branching processes can be specified in $\mathsf{ARB}$, so we
will replace $\mathcal{P}$ with $\mathcal{P}_{\omega}$ in (1). From a
technical point of view, $\mathcal{P}_{\omega}$ is the monad on the category
$\mathbf{Sets}$ of sets and functions presented by the algebraic theory of
semilattices with bottom.

By substituting the finite powerset functor in (1) with other monads presented
by algebraic theories, we obtain a parametrised family of process types that
covers the examples above and a general framework for studying the processes
of each type. Instantiating the framework with an algebraic theory gives a
fully expressive specification language for processes and a complete
axiomatisation of behavioural equivalence for specifications.

One striking feature of many of the specification languages we construct is
that they contain a fragment consisting of nonstandard analogues of regular
expressions. We call these expressions _star expressions_ and the fragment
composed of star expressions the _star fragment_. Star fragments extend
several existing analogues of basic regular algebra found in the process
theory literature, including basic process algebra [15] and Andova’s
probabilistic basic process algebra [5], by adding recursion operators
modelled after the Kleene star.

Milner is the first to notice the star fragment of $\mathsf{ARB}$ in [1]. He
observes that the algebra of processes denoted by star expressions is more
unruly than Kleene’s algebra of regular languages, and that it is not clear
what the appropriate axiomatisation should be. He offers a reasonable
candidate based on Salomaa’s first axiomatisation of Kleene algebra [16], but
ultimately leaves completeness as an open problem. This problem has been
subjected to many years of extensive research [17, 18, 19, 20, 21, 22]. A
potential solution has recently been announced by Clemens Grabmayer and will
appear in the upcoming LICS.

Replacing nondeterministic choice with the if-then-else branching structure of
$\mathsf{GKAT}$, we obtain the process behaviours explored in the recent
rethinking of the language [23]. This makes the open problem of axiomatising
$\mathsf{GKAT}$ (without the use of extremely powerful axioms like the
_Uniqueness Axiom_ of [24]), stated first in [24] and again in [23], yet
another problem of axiomatising an algebra of star expressions. Our general
characterisation of star expressions puts all these languages under one
umbrella, and shows how they are derived canonically from a single abstract
framework.

In summary, the contributions of this paper are as follows:

  * •

We present a family of process types parametrised by an algebraic theory
(Section 2) together with a uniform syntax and operational semantics (Section
3). We show how these can be instantiated to concrete algebraic theories,
including guarded semilattices and pointed convex algebras. These provide,
respectively, a calculus of processes capturing control flow of simple
imperative programs and a calculus of probabilistic processes.

  * •

We define an associated denotational semantics and show that it agrees with
the operational semantics (Section 4). This coincidence result is important in
order to prove completeness of the uniform axiomatisation we propose for each
process type (Section 5).

  * •

Finally, we study the star fragment of our parameterised family and propose a
sound axiomatisation for this fragment (Section 6). We show that star
fragments of concrete instances of our calculi yield known examples in the
literature, e.g. Guarded Kleene Algebra with tests ($\mathsf{GKAT}$) [24, 23]
and probabilistic processes of Stark and Smolka [25].

Related work is surveyed in Section 7, and future research directions are
discussed in Section 8.

##  2 A Parametrised Family of Process Types

In this section, we present a family of process types parametrised by a
certain kind of algebraic theory. The processes we care about are stateful,
meaning they consist of a set of states and a suitably structured set of
transitions between states. Stateful systems fit neatly into the general
framework of universal coalgebra [26], which stipulates that the type of
structure carried by the transitions can be encoded in an endofunctor on the
category $\mathbf{Sets}$ of sets and functions. Formally, given a functor
$B:\mathbf{Sets}\to\mathbf{Sets}$, a _$B$ -coalgebra_ is a pair $(X,\beta)$
consisting of a set $X$ of _states_ and a _structure_ map $\beta:X\to BX$. A
coalgebra homomorphism $h:(X,\beta)\to(Y,\vartheta)$ is a function $h:X\to Y$
satisfying $\vartheta\circ h=B(h)\circ\beta$. Many types of processes found in
the literature coincide with $B$-coalgebras for some $B$, and so do their
homomorphisms. For example, finitely branching labelled transition systems are
$\mathcal{P}_{\omega}(A\times\text{Id})$-coalgebras, and deterministic Moore
automata are $O\times\text{Id}^{A}$-coalgebras [27].

In this paper, we consider coalgebras for functors of the form

$B_{M}:=M(V+A\times\text{Id})$ (2)

for fixed sets $V$ and $A$ and a specific kind of functor
$M:\mathbf{Sets}\to\mathbf{Sets}$. Intuitively, there are two layers to the
process behaviours we care about: one layer consists of either an _output
variable_ in $V$ or an _action_ from $A$ that moves on to another state, and
the other layer (encoded by $M$) combines output variables and action steps in
a structured way.

######  Example 2.1.

When $M=\mathcal{P}_{\omega}$, we obtain Milner’s nondeterministic processes
[1]. Coalgebras for $B_{\mathcal{P}_{\omega}}$ are functions of the form
$\beta:X\to\mathcal{P}_{\omega}(V+A\times X)$, or labelled transition systems
with an additional decoration by variables. Write
$x\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\xrightarrow{a}$}}}y$ to mean
$(a,y)\in\beta(x)$ and $x\Rightarrow v$ to mean $v\in\beta(x)$. The image
below posits a well-defined $B_{\mathcal{P}_{\omega}}$-coalgebra

$v$$x_{1}$$x_{2}$$x_{3}$$a_{1}$$a_{1}$$a_{2}$

Its state space is $\\{x_{1},x_{2},x_{2}\\}$, $A$ includes $a_{1}$ and
$a_{2}$, and $v$ is a variable in $V$.

#### Algebraic Theories and Their Monads

We are particularly interested in $B_{M}$-coalgebras when $M$ is the functor
component of a monad $(M,\eta,\mu)$ that is presented by an algebraic theory
capturing a type of branching. A monad consists of natural transformations
$\eta:\text{Id}\Rightarrow M$ and $\mu:MM\Rightarrow M$, called the _unit_ and
_multiplication_ respectively, satisfying two laws:
$\mu\circ\eta_{M}=\operatorname{id}_{M}=\mu\circ M(\eta)$ and
$\mu_{M}\circ\mu=M(\mu)\circ\mu$. For our purposes, an _algebraic theory_ is a
pair $(S,\mathsf{E})$ consisting of a polynomial endofunctor
$S=\coprod_{\sigma\in I}\text{Id}^{n_{\sigma}}$ on $\mathbf{Sets}$ called an
algebraic signature and a set $\mathsf{E}$ of equations in the signature $S$.
An element $\sigma$ of $I$ should be thought of as an operation with arity
$n_{\sigma}$. An algebraic theory $(S,\mathsf{E})$ presents a monad
$(M,\eta,\mu)$ if there is a natural transformation $\rho:SM\Rightarrow M$
such that for any set $X$, $(MX,\rho_{X})$ is the free
$(S,\mathsf{E})$-algebra on $X$. That is, $(MX,\rho_{X})$ satisfies
$\mathsf{E}$ and for any $S$-algebra $(Y,\varphi)$ also satisfying
$\mathsf{E}$ and any function $h:X\to Y$, there is a unique $S$-algebra
homomorphism $\hat{h}:(MX,\rho_{X})\to(Y,\varphi)$ such that
$h=\hat{h}\circ\eta$. This universal property implies that any two
presentations of a given algebraic theory are isomorphic, so we speak simply
of “the” monad presented by an algebraic theory.

######  Example 2.2.

The finite powerset functor is part of the monad
$(\mathcal{P}_{\omega},\\{-\\},\bigcup)$ that is presented by the theory of
semilattices (with bottom). The theory of semilattices is the pair
$(1+\text{Id}^{2},\mathsf{SL})$, since the arity of a constant operation is
$0$ and $+$ is a binary operation, and $\mathsf{SL}$ consists of

$x+0\stackrel{{\scriptstyle(\mathsf{SL1})}}{{=}}x\qquad
x+x\stackrel{{\scriptstyle(\mathsf{SL2})}}{{=}}x\qquad
x+y\stackrel{{\scriptstyle(\mathsf{SL3})}}{{=}}y+x\qquad
x+(y+z)\stackrel{{\scriptstyle(\mathsf{SL4})}}{{=}}(x+y)+z$

Not every algebraic theory has such a familiar presentation as the theory of
semilattices, but it is nevertheless true that every algebraic theory presents
a monad. If we let $S^{*}X$ denote the set of $S$-terms, expressions built
from $X$ and the operations in $S$, then $(S,\mathsf{E})$ automatically
presents the monad $(M,\eta,\mu)$ where
$MX=(S^{*}X)/\mathsf{E}:=\\{[q]_{\mathsf{E}}\mid q\in S^{*}X\\}$ is the set of
$\mathsf{E}$-congruence classes of $S$-terms, $\eta$ computes congruence
classes of variables, and $\mu$ evaluates terms. This is witnessed by letting
the transformation $\rho$ be the restriction of $\mu$ to the operations of $S$
on $S$-terms. We take this to be the default presentation of an arbitrary
algebraic theory.

Our aim is to develop a (co)algebraic framework for studying
$B_{M}$-coalgebras when $M$ is the functor part of a monad presented by an
algebraic theory. We will make three assumptions about the algebraic theories.
First, we rule out the case of $M$ being the constant $1$ functor.

######  Assumption 1.

The theory $\mathsf{E}$ is _nontrivial_ , meaning that the equation $x=y$ is
not a consequence of $\mathsf{E}$ for distinct $x$ and $y$.

This is equivalent to requiring that the unit $\eta$ is injective. That is,
the $\mathsf{E}$-congruence classes $[x]_{\mathsf{E}}$ and $[y]_{\mathsf{E}}$
in $MX$ are distinct for distinct variables $x$ and $y$ in $X$.

Second, we assume the existence of a constant symbol denoting deadlock, which
might occur when recursing on unguarded programs.

######  Assumption 2.

Algebraic theories contain a designated constant $0$.

Finally, to keep the specifications of processes finite, we make the following
assumption despite the fact that it has no bearing on the results presented
before Section 5.

######  Assumption 3.

Each operation from S has a finite arity.

We conclude this section with examples of algebraic theories and the monads
they present.

######  Example 2.3.

For a fixed finite set At of _atomic tests_ , the algebraic theory of _guarded
semilattices_ is the pair
$(1+\coprod_{b\subseteq\texttt{At}}\text{Id}^{2},\mathsf{GS})$, where
$\mathsf{GS}$ consists of the equations

$x+_{b}x\stackrel{{\scriptstyle(\mathsf{GS1})}}{{=}}x\qquad
x+_{\texttt{At}}y\stackrel{{\scriptstyle(\mathsf{GS2})}}{{=}}x\qquad
x+_{b}y\stackrel{{\scriptstyle(\mathsf{GS3})}}{{=}}y+_{\bar{b}}x\qquad(x+_{b}y)+_{c}z\stackrel{{\scriptstyle(\mathsf{GS4})}}{{=}}x+_{bc}(y+_{c}z)$

Here, $+_{b}$ is the binary operation associated with the subset
$b\subseteq\texttt{At}$, $\bar{b}:=\texttt{At}\setminus b$, and $bc:=b\cap c$.
The theory of guarded semilattices is presented by the monad
$((1+\text{Id})^{\texttt{At}},\lambda\xi.(-),\Delta^{*})$, where
$(\lambda\xi.x)(\xi)=x$ and $\Delta^{*}(F)(\xi)=F(\xi)(\xi)$. The idea is that
$+_{b}$ acts like an if-then-else clause in an imperative program. This is
reflected in a free guarded semilattice $((1+X)^{\texttt{At}},\rho_{X})$,
where for a pair of maps $h_{1},h_{2}:\texttt{At}\to X$ we define

$\rho_{X}(h_{1}+_{b}h_{2})(\xi):=\begin{cases}h_{1}(\xi)&\text{if $\xi\in
b$}\\\ h_{2}(\xi)&\text{otherwise}\end{cases}$

The theory of guarded semilattices dates back to the algebras of if-then-else
clauses studied in [13, 11, 12, 28]. For instance, guarded semilattices are
examples of _McCarthy algebras_ , introduced by Manes in [11].555More
information on the theory of guarded semilattices can be found in Appendix A.

######  Example 2.4.

By deleting the second axiom of $\mathsf{SL}$, we obtain the theory of
commutative monoids $(\text{Id}^{2},\mathsf{CM})$. This theory presents the
finite multiset monad $(\mathcal{M}_{\omega},\delta_{(-)},\sum)$, where

$\mathcal{M}_{\omega}X=\\{m:X\to\mathbb{N}\mid\\{x\mid m(x)>0\\}~{}\text{is
finite}\\}$

and

$\delta_{y}(x)=[x=y?]\qquad\sum(F)(x)=\sum_{m\in\mathcal{M}_{\omega}X}F(m)\cdot
m(x)$

######  Example 2.5.

The theory of _pointed convex algebras_ studied in [29] is
$(1+\coprod_{p\in[0,1]}\text{Id}^{2},\mathsf{CA})$, where $\mathsf{CA}$
consists of the equations

$x+_{p}x\stackrel{{\scriptstyle(\mathsf{CA1})}}{{=}}x\qquad
x+_{1}y\stackrel{{\scriptstyle(\mathsf{CA2})}}{{=}}x\qquad
x+_{p}y\stackrel{{\scriptstyle(\mathsf{CA3})}}{{=}}y+_{\bar{p}}x\qquad(x+_{p}y)+_{q}z\stackrel{{\scriptstyle(\mathsf{CA4})}}{{=}}x+_{pq}(y+_{\frac{q\bar{p}}{1-{pq}}}z)$

Here, $+_{p}$ is the binary operation with index $p\in[0,1]$, $\bar{p}:=1-p$,
and $pq\neq 1$. This theory presents the pointed finite subprobability
distribution monad $(\mathcal{D}_{\omega}(1+\text{Id}),\delta_{(-)},\sum)$,
where

$\mathcal{D}_{\omega}(1+X)=\left\\{\theta:X\to[0,1]\middle|\begin{array}[]{c}\\{x\mid\theta(x)>0\\}~{}\text{is
finite}\\\ \sum_{x\in X}\theta(x)\leq 1\end{array}\right\\}$

for any set $X$, and for any $x\in X$, $\theta\in\mathcal{D}_{\omega}(1+X)$,
and $\Theta\in\mathcal{D}_{\omega}(1+\mathcal{D}_{\omega}(1+X))$,

$\delta_{x}(y)=[x=y?]\qquad\qquad\sum(\Theta)(\theta)=\sum_{y\in
X}\Theta(\theta)\cdot\theta(y)$

This is witnessed by the transformation $\rho$ that takes $0$ to the trivial
subdistribution and computes the Minkowski sum
$\rho_{X}(\theta+_{p}\psi)=p\cdot\theta+(1-p)\cdot\psi$ for each $p\in[0,1]$,
$\theta,\psi\in\mathcal{D}_{\omega}(1+X)$.

######  Example 2.6.

The theory of _pointed convex semilattices_ studied in [29, 30, 31] combines
the theory of semilattices and the theory of convex algebras. It has both a
binary operation $+$ mimicking nondeterministic choice and the probabilistic
choice operations $+_{p}$ indexed by $p\in[0,1]$. Formally, it is given by the
pair $(1+\text{Id}^{2}+\coprod_{p\in[0,1]}\text{Id}^{2},\mathsf{CS})$, where
$\mathsf{CS}$ is the union of $\mathsf{SL}$, $\mathsf{CA}$, and the
distributive law

$(x+y)+_{p}z\stackrel{{\scriptstyle(\mathsf{D})}}{{=}}(x+_{p}z)+(y+_{p}z)$

This theory presents the pointed convex powerset monad
$(\mathcal{C},\eta^{\mathcal{C}},\mu^{\mathcal{C}})$, where $\mathcal{C}X$ is
the set of finitely generated convex subsets of $\mathcal{D}_{\omega}(1+X)$
containing $\delta_{0}$, and for $x\in X$ and $Q\in\mathcal{C}\mathcal{C}X$,

$\eta^{\mathcal{C}}(x)=\\{p\cdot\delta_{x}\mid
p\in[0,1]\\}\qquad\qquad\mu^{\mathcal{C}}(Q)=\bigcup_{\Theta\in
Q}\left\\{\sum_{U\in\mathcal{C}_{0}X}\Theta(U)\cdot\theta_{U}~{}\middle|~{}(\forall
U\in\mathcal{C}_{0}X)~{}\theta_{U}\in U\right\\}$

The witnessing transformation $\rho^{\mathcal{C}}$ takes $0$ to
$\\{\delta_{0}\\}$, computes the Minkowski sum (extended to subsets) in place
of $+_{p}$, and interprets the $+$ operation as the convex union

$\rho_{X}^{\mathcal{C}}(U+V)=\\{p\cdot\theta_{1}+(1-p)\cdot\theta_{2}\mid
p\in[0,1],\theta_{1}\in U,\theta_{2}\in V\\}$

##  3 Specifications of Processes

Fix an algebraic theory $(S,\mathsf{E})$ presenting a monad $(M,\eta,\mu)$. In
this section, we give a syntactic and uniformly defined specification system
for $B_{M}$-coalgebras and an associated operational semantics. We are
primarily concerned with the specifications of finite processes, and indeed
the process terms we construct below denote processes with finitely many
states. The converse is also true, that every finite $B_{M}$-coalgebra admits
a specification in the form of a process term, but we defer this result to
Section 5 because of its relevance to the completeness theorem there.

The syntax of our specifications consists of variables from an infinite set
$V$, actions from a set $A$, and operations from $S$. The set $\mathtt{Exp}$
of _process terms_ is given with the grammar

$e,e_{i}::=0\mid v\mid\sigma(e_{1},\dots,e_{n})\mid ae\mid\mu v~{}e$

where $v\in V$, $a\in A$, and $\sigma$ is an $S$-operation. Abstractly,
process terms form the initial $\Sigma_{M}$-algebra $(\mathtt{Exp},\alpha)$,
where $\Sigma_{M}:\mathbf{Sets}\to\mathbf{Sets}$ is the functor defined by

$\Sigma_{M}:=S+V+A\times\text{Id}+V\times\text{Id}$

and the algebra map $\alpha:\Sigma_{M}\mathtt{Exp}\to\mathtt{Exp}$ evaluates
$\Sigma_{M}$-terms.

$\begin{aligned} \epsilon(v)&=\eta(v)\\\
\epsilon(ae)&=\eta((a,e))\end{aligned}\qquad\qquad\begin{aligned}
\epsilon(\sigma(e_{1},\dots,e_{n}))&=\sigma(\epsilon(e_{1}),\dots,\epsilon(e_{n}))\\\
\epsilon(\mu v~{}e)&=\epsilon(e)[\mu v~{}e/\\!/v]\end{aligned}$ Figure 1:
Operational semantics of process terms. Here, $v\in V$, $a\in A$, and
$e,e_{i}\in\mathtt{Exp}$.

Intuitively, the symbol $0$ is the designated constant of $S$ denoting the
_deadlock_ process, which takes no action. Output variables are used in one of
two ways, depending on the expression in which they appear. A variable $v$ is
_free_ in an expression $e$ if it does not appear within the scope of $\mu v$
and _bound_ otherwise. If $v$ is free in $e$, then $v$ denotes “output $v$”.
Otherwise, $v$ denotes a _goto_ statement that returns the computation to the
$\mu v$ that binds $v$. The process $\sigma(e_{1},\dots,e_{n})$ is the process
that branches into $e_{1},\dots,e_{n}$ using an $n$-ary operation $\sigma$ as
the branching constructor. The expression $ae$ denotes the process that
performs the action $a$ and then proceeds with $e$. Finally, $\mu v~{}e$
denotes recursion in the variable $v$.

#### Small-step Semantics

Next we give a small-step (operational) semantics to process terms that is
uniformly defined for the process types in our parametrised family. Many of
the algebraic theories we consider lack a familiar presentation, which
ultimately prevents the corresponding semantics from taking the traditional
form of a set of inference rules describing transition relations. We take an
abstract approach instead by defining a $B_{M}$-coalgebra structure
$\epsilon:\mathtt{Exp}\to B_{M}\mathtt{Exp}$ that mirrors the intuitive
descriptions of the executions of process terms above. The formal description
of $\epsilon$ is summarised in Fig. 1.

The operational interpretation of the recursion operators requires further
explanation. Intuitively, $\mu v~{}e$ performs the process denoted by $e$
until it reaches an exit in channel $v$, at which point it loops back to the
beginning. However, this is really only an accurate description of recursion
in $v$ when $e$ performs an action before exiting in $v$. For example, the
process $\mu v~{}v$ not only never exits in channel $v$, but it also never
performs any action at all. Thus, the operational interpretation of $\mu
v~{}v$ is indistinguishable from that of deadlock. We deal with this issue as
follows: if an exit in channel $v$ is immediately reached by a branch of $e$,
then we replace that exit with deadlock in $\mu v~{}e$. Formally, we say that
a variable $v$ is _guarded_ in a process term $e$ if (i) $e\in
V\setminus\\{v\\}$, (ii) $e=af$ or (iii) $e=\mu v~{}f$ for some
$f\in\mathtt{Exp}$, or (iv) either $e=\mu u~{}e_{1}$ or (v)
$e=\sigma(e_{1},\dots,e_{n})$ and $v$ is guarded in $e_{i}$ for each $i\leq
n$. In our calculus, we syntactically allow for recursion in unguarded
variables, but one should keep in mind that those variables are ultimately
deadlock under the recursion operator.

The operational interpretation of recursion is formally defined using a
_guarded syntactic substitution operator_ $[g/\\!/v]:B_{M}\mathtt{Exp}\to
B_{M}\mathtt{Exp}$,666Technically, it is only partially defined. See Appendix
C for details. a variant of the usual syntactic substitution of variables.
Given $g\in\mathtt{Exp}$, we first define $[g/\\!/v]$ by induction on
$S^{*}(V+A\times\mathtt{Exp})$ as

$\begin{aligned} u[g/\\!/v]&=\begin{cases}\eta(u)&u\neq v\\\
\eta(0)&u=v\end{cases}\end{aligned}\qquad\qquad\begin{aligned}
(a,f)[g/\\!/v]&=(a,f[g/v])\\\
\sigma(p_{1},\dots,p_{n})[g/\\!/v]&=\sigma(p_{1}[g/\\!/v],\dots,p_{n}[g/\\!/v])\end{aligned}$

where $u\in V$, $p_{i}\in S^{*}(V+A\times\mathtt{Exp})$, $f\in\mathtt{Exp}$,
and $[g/v]$ replaces free occurrence of $v$ with $g$. The following lemma
completes the description of the operational semantics of process terms.

######  Lemma 3.1.

For any $g\in\mathtt{Exp}$ and $v\in V$, the map $[g/\\!/v]$ factors uniquely
through $B_{M}\mathtt{Exp}$.

For more information on these substitution operators, see Appendix C.

Formally, the map $\epsilon$ assigns to each process term $e$ an
$\mathsf{E}$-congruence class $\epsilon(e)$ of terms from
$S^{*}(V+A\times\mathtt{Exp})$. A term from $S^{*}(V+A\times\mathtt{Exp})$ is
a combination of variables $v$ and transition-like pairs $(a,e_{i})$, so there
is often only a small conceptual leap from the coalgebra structure $\epsilon$
to a more traditional representation of transitions as decorated arrows. We
provide the following examples as illustrations of this phenomenon, as well as
the specification languages and operational semantics of terms defined
above.777See Appendix B.

######  Example 3.1.

The _algebra of control flows_ , or $\mathsf{ACF}$, is obtained from the
theory of guarded semilattices of Example 2.3 and $M=(1+Id)^{\texttt{At}}$.
Given a structure map $\beta:X\to B_{(1+\text{Id})^{\texttt{At}}}X$ and
$b\subseteq\texttt{At}$, write
$x\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\xrightarrow{b\mid a}$}}}y$ if
$\beta(x)(\xi)=(a,y)$ for all $\xi\in b$, and
$x\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\xRightarrow{b}$}}}v$ if
$\beta(x)(\xi)=v$ for all $\xi\in b$. The operational semantics returns the
constant map $\lambda\xi.v$ given a variable $v\in V$ and interprets
conditional choice as guarded union. For example, let $e=\mu
w~{}(a_{1}(v+_{b}a_{2}w)+_{b}u)$ and $f=v+_{b}a_{2}e$. The process denoted by
$e$ is

$u$$e$$f$$v$$b\mid a_{1}$$\bar{b}\mid a_{2}$$\bar{b}$$b$

######  Example 3.2.

The _algebra of probabilistic actions_ , or $\mathsf{APA}$, is obtained from
the theory of pointed convex algebras of Example 2.5 and
$M=\mathcal{D}_{\omega}(1+Id)$. For a structure map $\beta:X\to
B_{\mathcal{D}_{\omega}(1+\text{Id})}X$, write
$x\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\xrightarrow{k\mid a}$}}}y$
when $\beta(x)(a,y)=k$ and
$e\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\xRightarrow{k}$}}}v$ when
$\beta(e)(v)=k$. The operational semantics returns the Dirac distribution
$\delta_{v}$ for $v\in V$ and interprets probabilistic choice as the Minkowski
sum. The process denoted by $e=\mu
v~{}(a_{1}u+_{\frac{1}{2}}(a_{2}v+_{\frac{1}{3}}w))$ is

$w$$e$$u$$u$$\frac{1}{2}\mid a_{1}$$\frac{1}{3}$$\frac{1}{6}\mid a_{2}$$1$

######  Example 3.3.

The _algebra of nondeterministic probabilistic actions_ , or $\mathsf{ANP}$,
is obtained from the theory of pointed convex semilattices of Example 2.6. For
a structure map $\beta:X\to B_{\mathcal{C}}X$, write
$x\mathrel{\raisebox{-1.00006pt}{${\to}\circ$}{\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\dabar@\dabar@}\limits^{\hbox{\set@color$\scriptstyle\,k\mid
a$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@}\limits^{\hbox{\set@color$\scriptstyle\,k\mid
a$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@}\limits^{\hbox{\set@color$\scriptscriptstyle\,k\mid
a$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits^{\hbox{\set@color$\scriptstyle\,k\mid
a$}}}\mathrel{\mathchar 0\relax\symAMSa 04B}{}}}{}$}}}}}y$ to mean there is a
$\theta\in\beta(x)$ such that $\theta(a,y)=k$, and
$x\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\xRightarrow{k}$}}}v$ to mean
there is a $\theta\in\beta(x)$ with $\theta(v)=k$. The operational semantics
returns $\eta^{\mathcal{C}}(v)$ given $v\in V$, interprets nondeterministic
choice as convex union, and replaces probabilistic choice with Minkowski sum.
For example, $e=\mu v~{}((a_{1}v+_{\frac{1}{3}}a_{2}w)+a_{2}v)$ denotes

$\circ$e$\circ$$w$$w$$1\mid a_{2}$$\frac{1}{3}\mid a_{1}$$\frac{2}{3}\mid
a_{2}$$1$

##  4 Behavioural Equivalence and the Final Coalgebra

In this section, we relate the operational semantics arising from the
coalgebra structure on $\mathtt{Exp}$ in the previous section to a
denotational semantics, which arises through the definition of a suitable
algebra structure on the domain of process behaviours.

For an arbitrary functor $B:\mathbf{Sets}\to\mathbf{Sets}$, a behaviour is a
state of the final $B$-coalgebra $(Z,\zeta)$, the unique (up to isomorphism)
coalgebra (if it exists) such that there is exactly one homomorphism
$!_{\beta}:(X,\beta)\to(Z,\zeta)$ from every $B$-coalgebra $(X,\beta)$. It
follows from general considerations that the functor $B_{M}$ admits a final
coalgebra [26]. The universal property of the final $B_{M}$-coalgebra produces
the homomorphism ${!}_{\epsilon}:(\mathtt{Exp},\epsilon)\to(Z,\zeta)$. The
behaviour ${!}_{\epsilon}(e)$ is called the _final (coalgebra) semantics_ of
$e$, also known as its operational semantics [32].

For example, the final $B_{\mathcal{P}_{\omega}}$-coalgebra consists of
bisimulation equivalence classes of finite and infinite labelled trees of a
certain form [33]. In this setting, $(\mathtt{Exp},\epsilon)$ is a labelled
transition system and the final semantics ${!}_{\epsilon}$ constructs a tree
from a process term by unrolling. Intuitively, this captures the behaviour of
a specification by encoding all possible actions and outgoing messages at each
time-step in its execution.

$\begin{aligned} \zeta(\gamma(v))&=[v]_{\mathsf{E}}\\\
\zeta(\gamma(a,t))&=[(a,t)]_{\mathsf{E}}\end{aligned}\qquad\qquad\begin{aligned}
\zeta(\gamma(\sigma(t_{1},\dots,t_{n})))&=[\sigma(\zeta(t_{1}),\dots,\zeta(t_{n}))]_{\mathsf{E}}\\\
\zeta(\gamma(\mu v~{}t))&=\zeta(t)\\{\gamma(\mu v~{}t)/\\!/v\\}\end{aligned}$
Figure 2: The $\Sigma_{M}$-algebra structure of $(Z,\gamma)$. Here, $v\in V$,
$a\in A$, $t,t_{i}\in Z$ for $i\leq n$, and $\sigma$ is an $n$-ary operation
from $S$. By Lambek’s lemma [34], $\zeta:Z\to B_{M}Z$ is a bijection, so the
first three equations determine $\gamma:V+SZ+A\times V\to Z$. The fourth is a
behavioural differential equation [27].

In addition to forming the state space of the final $B_{M}$-coalgebra, the set
of process behaviours also carries the structure of a $\Sigma_{M}$-algebra
$(Z,\gamma)$, summarised in Fig. 2. Now, $(\mathtt{Exp},\alpha)$ is the
initial $\Sigma_{M}$-algebra, which in particular means there is a unique
algebra homomorphism
$\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor:(\mathtt{Exp},\alpha)\to(Z,\gamma)$.
The behaviour $\lceil\\!\\!\lfloor e\rceil\\!\\!\rfloor$ is called the initial
(algebra) semantics of $e$ [35], and provides a denotational semantics to our
process calculus.

The algebra structure $\gamma:\Sigma_{M}Z\to Z$ of $(Z,\gamma)$ can be seen as
a reinterpretation of the programming constructs of the language
$\mathtt{Exp}$ that mimics the operational semantics of process terms. The
basic constructs are the content of the first three equations in Fig. 2:
output variables are evaluated so as to behave like the variables of
$(\mathtt{Exp},\epsilon)$, the behaviour $at$ performs $a$ and moves on to
$t$, and $\sigma(t_{1},\dots,t_{n})$ branches into the behaviours
$t_{1},\dots,t_{n}$ with additional structure determined by the operation
$\sigma$. Interpreting recursive behaviours like $\mu v~{}t$ requires
coalgebraic analogues of syntactic and guarded syntactic substitution from
Section 3.

For a given behaviour $s\in Z$ and a variable $v\in V$, the _behavioural
substitution_ of $s$ for $v$ is the map $\\{s/v\\}:Z\to Z$ defined by the
identity

$\zeta(t\\{s/v\\})=\begin{cases}\zeta(s)&\zeta(t)=[v]_{\mathsf{E}}\\\
[u]_{\mathsf{E}}&\zeta(t)=[u]_{\mathsf{E}}\neq[v]_{\mathsf{E}}\\\
[(a,r\\{s/v\\})]_{\mathsf{E}}&\zeta(t)=[(a,r)]_{\mathsf{E}}\\\
\sigma(\zeta(t_{1}\\{s/v\\}),\dots,\zeta(t_{n}\\{s/v\\}))&\zeta(t)=[\sigma(\zeta(t_{1}),\dots,\zeta(t_{n}))]_{\mathsf{E}}\end{cases}$

for any $t\in Z$. The _guarded behavioural substitution_ of $s$ for $v$ is
constructed in analogy with guarded syntactic substitution from the previous
section. We start by defining guarded behavioural substitution in
$S^{*}(V+A\times Z)$ as

$\displaystyle u\\{s/\\!/v\\}$ $\displaystyle=\begin{cases}u&u\neq v\\\
0&u=v\end{cases}$ $\displaystyle\begin{aligned}
(a,r)\\{s/\\!/v\\}&=(a,r\\{s/v\\})\\\
\sigma(r_{1},\dots,r_{n})\\{s/\\!/v\\}&=\sigma(r_{1}\\{s/\\!/v\\},\dots,r_{n}\\{s/\\!/v\\})\end{aligned}$

where $u\in V$, $a\in A$, and $r,r_{i}\in Z$ for $i\leq n$. This map lifts to
an operator $B_{M}Z\to B_{M}Z$ for the same reason as the guarded syntactic
substitution operator. This completes the description of the algebraic
structure of $(Z,\gamma)$ in Fig. 2.

######  Theorem 4.1.

Let $\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor$ be the unique algebra homorphism
$(\mathtt{Exp},\alpha)\to(Z,\gamma)$. For any process term $e\in\mathtt{Exp}$,
we have ${!}_{\epsilon}(e)=\lceil\\!\\!\lfloor e\rceil\\!\\!\rfloor$.

In other words, the final semantics given with respect to operational rules in
$\mathtt{Exp}$ coincides with the initial semantics given with respect to the
programming constructs in $Z$. Consequently, we write
$\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor$ in place of ${!}_{\epsilon}$ and
simply refer to $\lceil\\!\\!\lfloor e\rceil\\!\\!\rfloor$ as the semantics of
$e$.

##  5 An Axiomatisation of Behavioural Equivalence

An important corollary of Theorem 4.1 is that behavioural equivalence is a
$\Sigma_{M}$-congruence on $(\mathtt{Exp},\alpha)$, meaning that it is
preserved by all the program constructs of $\Sigma_{M}$. This opens the door
to the possibility of deriving behavioural equivalences between process terms
from just a few axioms. The purpose of this section is to show that all
behavioural equivalences between process terms can be derived from the
equations in $\mathsf{E}$ presenting $(M,\eta,\mu)$ as well as three axiom
schemas concerning the recursion operators.

The first two out of the three recursion axiom schemas are

$\begin{aligned} \text{($\mathsf{R}$1)}&&\mu v~{}e&=e[\mu
v~{}e/\\!/v]\end{aligned}\qquad\qquad\begin{aligned}
\prftree[l]{($\mathsf{R}$2)\quad}{\text{$w$ not free in $e$}}{\mu v~{}e=\mu
w~{}(e[w/v])}\end{aligned}$

Above, $e[\mu v~{}e/\\!/v]$ is the expression obtained by replacing every
guarded free occurrence of $v$ in $e$ with the expression $\mu v~{}e$ and
every unguarded occurrence of $v$ in $e$ with $0$, in analogy with the
operator on $B_{M}\mathtt{Exp}$ of the same name.888Indeed, the identity
$\epsilon(e[\mu v~{}e/\\!/v])=\epsilon(e)[\mu v~{}e/\\!/v]$ holds for all
$e\in\mathtt{Exp}$ and $v\in V$ Lemma C.9.

The axiom ($\mathsf{R}$1) essentially allows for a sort of guarded unravelling
of recursive terms. This has the effect of identifying $\mu v~{}v$ with $0$,
for example, as well as $\mu v~{}av$ with $a(\mu v~{}av)$. The latter
satisfies our intuition that $\mu v~{}av$ should solve the recursive
specification $x=ax$ in the indeterminate $x$. The axiom ($\mathsf{R}$2)
allows for recursion variables to be swapped for fresh variables. This amounts
to the observation that pairs of terms like $\mu v~{}av$ and $\mu w~{}aw$
should both denote the unique solution to $x=ax$.

The third recursion axiom schema can be stated in the form of the proof rule

$\displaystyle\prftree[l]{($\mathsf{R}$3)\quad}{g=e[g/v]\quad\text{$v$ guarded
in $e$}}{g=\mu v~{}e}$

We let $\mathsf{R}$ denote the set of equations derived from
($\mathsf{R}$1)-($\mathsf{R}$3), and we let $\equiv$ denote the smallest
congruence in $(\mathtt{Exp},\alpha)$ containing the set of equations derived
from $\mathsf{E}$ and $\mathsf{R}$. When we refer to examples like
$\mathsf{ARB}$, $\mathsf{ACF}$, $\mathsf{APA}$, and $\mathsf{ANP}$, we are
often identifying each of these with their associated algebras
$({\mathtt{Exp}}/{\equiv},\hat{\alpha})$ of process terms modulo $\equiv$.

#### Soundness

We would like to argue that $\equiv$ is _sound_ with respect to behavioural
equivalence, meaning that $\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor=\lceil\\!\\!\lfloor f\rceil\\!\\!\rfloor$ whenever
$e\equiv f$. This is indeed the case, and can be derived from the fact that
the set of congruence classes of process terms itself forms a
$B_{M}$-coalgebra. For an arbitrary function $h:X\to Y$, call the set
$\ker(h):=\\{(x,y)\mid h(x)=h(y)\\}$ the _kernel_ of $h$.

######  Lemma 5.1.

The congruence $\equiv$ is the kernel of a coalgebra homomorphism.

We write $[-]_{\equiv}:\mathtt{Exp}\to{\mathtt{Exp}}/{\equiv}$ for the
quotient map and $({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$ for the coalgebra
structure on ${\mathtt{Exp}}/{\equiv}$ making $[-]_{\equiv}$ a coalgebra
homomorphism (there is at most one such coalgebra structure [26]). As
$\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor$ is the unique coalgebra homomorphism
$(\mathtt{Exp},\epsilon)\to(Z,\zeta)$, and because there is also a coalgebra
homomorphism
${!}_{\bar{\epsilon}}:({\mathtt{Exp}}/{\equiv},\bar{\epsilon})\to(Z,\zeta)$,
it must be the case that
${!}_{\bar{\epsilon}}\circ[-]_{\equiv}=\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor$.
By Lemma 5.1, if $e\equiv f$, then $\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor={!}_{\bar{\epsilon}}([e]_{\equiv})={!}_{\bar{\epsilon}}([f]_{\equiv})=\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor$. This establishes the following.

######  Theorem 5.1 (Soundness).

Let $e,f\in\mathtt{Exp}$. If $e\equiv f$, then $\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor=\lceil\\!\\!\lfloor f\rceil\\!\\!\rfloor$.

Soundness allows us to derive at least a subset of all the behavioural
equivalences between process terms from the axioms in $\mathsf{E}$ and
$\mathsf{R}$. If our aspiration were simply to have a set of behaviour-
preserving code-transformations, then we could simply stop here and be
satisfied, since in principle we could see the axioms of $\mathsf{E}$ and
$\mathsf{R}$ as rewrite rules that satisfy this purpose.

#### Completeness

Aiming a bit higher than deriving only a subset of the behavioural
equivalences between process terms, we move on to show the converse of Theorem
5.1, that $\equiv$ is _complete_ with respect to behavioural equivalence. We
use [36, Lemma 5.1], which can be stated as follows.

######  Lemma 5.2.

Let $B:\mathbf{Sets}\to\mathbf{Sets}$ be an endofunctor with a final coalgebra
$(Z,\zeta)$, and let $\mathbf{C}$ be a class of $B$-coalgebras. If
$\mathbf{C}$ is closed under homomorphic images999Ie., if
$(X,\beta)\in\mathbf{C}$ and $h:(X,\beta)\to(Y,\vartheta)$, then
$(h[X],\vartheta|_{h[X]})\in\mathbf{C}$. and has a final object
$(E,\varepsilon)$, then ${!}_{\varepsilon}:E\to Z$ is injective.

A _subcoalgebra_ of a $B$-coalgebra $(X,\beta)$ is an injective map
$\iota:U\hookrightarrow X$ such that $\beta|_{U}$ factors through $B(\iota)$.
A $B$-coalgebra is _locally finite_ if every of its states is contained in
(the image of) a finite subcoalgebra. We instantiate Lemma 5.2 in the case
where $B=B_{M}$, $(E,\varepsilon)=({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$,
and $\mathbf{C}$ is the class of locally finite $B_{M}$-coalgebras.
Completeness of $\equiv$ with respect to behavioural equivalence follows
shortly after, for if $\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor=\lceil\\!\\!\lfloor f\rceil\\!\\!\rfloor$, then
${!}_{\bar{\epsilon}}([e]_{\equiv})={!}_{\bar{\epsilon}}([f]_{\equiv})$. By
Lemma 5.2, ${!}_{\bar{\epsilon}}$ is injective, so $[e]_{\equiv}=[f]_{\equiv}$
or equivalently $e\equiv f$. To establish the converse of Theorem 5.1, it
suffices to show that our choices of $(E,\varepsilon)$ and $\mathbf{C}$
satisfy the hypotheses of Lemma 5.2.

Before we continue, we would like to remind the reader of Assumption 3, that
$S$ only has operations of finite arity, as up until now it has not been
strictly necessary.

######  Lemma 5.3.

The coalgebra $(\mathtt{Exp},\epsilon)$ is locally finite.

The class of locally finite coalgebras is closed under homomorphic images: if
$(X,\beta)$ is locally finite and $h:(X,\beta)\to(Y,\vartheta)$ is a
surjective homomorphism, then for any $y\in Y$ and $x\in X$ such that
$h(x)=y$, and for any finite subcoalgebra $U$ of $(X,\beta)$ containing $x$,
$h[U]$ is a finite subcoalgebra of $(Y,\vartheta)$ containing $y$ [37]. Since
$y$ was arbitrary, it follows from Lemma 5.1 that
$({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$ is locally finite.

What remains to be seen among the hypotheses of Lemma 5.2 is that
$({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$ is the _final_ locally finite
coalgebra, meaning that for any locally finite coalgebra $(X,\beta)$ there is
a unique coalgebra homomorphism
$(X,\beta)\to({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$. Every homomorphism
from a locally finite coalgebra is the union of its restrictions to finite
subcoalgebras, so it suffices to see that every finite subcoalgebra of
$(X,\beta)$ admits a unique coalgebra homomorphism into
$({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$.

To this end, we make use of an old idea, possibly originating in the work of
Salomaa [16]. We associate with every finite coalgebra a certain system of
equations whose solutions (in ${\mathtt{Exp}}/{\equiv}$) are in one-to-one
correspondence with coalgebra homomorphisms into
$({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$. Essentially, if a system admits a
unique solution, then its corresponding coalgebra admits a unique homomorphism
into $({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$. This would then establish
finality.

######  Definition 5.1.

A _(finite) system of equations_ is a sequence of the form
$\\{x_{i}=e_{i}\\}_{i\leq n}$ where $x_{i}\in V$ and $e_{i}\in\mathtt{Exp}$
for $i\leq n$, and none of $x_{1},\dots,x_{n}$ appear as bound variables in
any of $e_{1},\dots,e_{n}$. A system of equations $\\{x_{i}=e_{i}\\}_{i\leq
n}$ is _guarded_ if $x_{1},\dots,x_{n}$ are guarded in $e_{i}$ for each $i\leq
n$. A _solution_ to $\\{x_{i}=e_{i}\\}_{i\leq n}$ is a function
$\phi:\\{x_{1},\dots,x_{n}\\}\to\mathtt{Exp}$ such that

$\phi(x_{i})\equiv e_{i}[\phi(x_{1})/x_{1},\dots,\phi(x_{n})/x_{n}]$

for all $i\leq n$ and $x_{1},\dots,x_{n}$ do not appear free in $\phi(x_{i})$
for any $i\leq n$.

Every finite $B_{M}$-coalgebra $(X,\beta)$ gives rise to a guarded system of
equations in the following way: for each $p\in S^{*}(V+A\times X)$, define
$p^{\dagger}$ inductively as

$v^{\dagger}=v\qquad(a,e)^{\dagger}=ae\qquad\sigma(f_{1},\dots,f_{n})^{\dagger}=\sigma(f_{1}^{\dagger},\dots,f_{n}^{\dagger})$

and for each $x\in X$, let $p_{x}$ be a representative of $\beta(x)$.
The101010Technically speaking, there could be many systems of equations
associated with a given coalgebra. We say “the” system of equations because
any two have the same set of solutions up to $\mathsf{E}$. system of equations
_associated with_ $(X,\beta)$ is then defined to be
$\\{x=p_{x}^{\dagger}\\}_{x\in X}$. We treat the elements of $X$ as variables
in these equations, and note that by definition every $y\in X$ is guarded in
$p_{x}^{\dagger}$.

######  Theorem 5.2.

Let $(X,\beta)$ be a finite $B_{M}$-coalgebra and $\phi:X\to\mathtt{Exp}$ a
function. Then the composition
$[-]_{\equiv}\circ\phi:X\to{\mathtt{Exp}}/{\equiv}$ is a $B_{M}$-coalgebra
homomorphism if and only if $\phi$ is a solution to the system of equations
associated with $(X,\beta)$.

As a direct consequence of Theorem 5.2, we see that a finite subcoalgebra
$U\hookrightarrow\mathtt{Exp}$ of $(\mathtt{Exp},\epsilon)$ is a solution to
the system of equations associated with $(U,\epsilon|_{U})$.

######  Example 5.1.

The system of equations associated with the automaton in Example 3.1 is the
two-element set $\\{x_{1}=a_{1}x_{2}+_{b}u,x_{2}=v+_{b}a_{2}x_{1}\\}$. The map
$\phi:\\{x_{1},x_{2}\\}\to\mathtt{Exp}$ defined by $\phi(x_{1})=\mu
w~{}(a_{1}(v+_{b}a_{2}w)+_{b}u)$ and $\phi(x_{2})=v+_{b}a_{2}~{}\phi(x_{1})$
is a solution.

Theorem 5.2 establishes a one-to-one correspondence between solutions to
systems and coalgebra homomorphisms as follows. Say that two solutions $\phi$
and $\psi$ to a system $\\{x_{i}=e_{i}\\}_{i\leq n}$ are _$\equiv$
-equivalent_ if $\phi(x_{i})\equiv\psi(x_{i})$ for all $i\leq n$. Starting
with a solution $\phi:X\to\mathtt{Exp}$ to the system associated with
$(X,\beta)$, we obtain the homomorphism $[-]_{\equiv}\circ\phi$ using Theorem
5.2. A pair of solutions $\phi$ and $\psi$ are $\equiv$-equivalent if and only
if $[-]_{\equiv}\circ\phi=[-]_{\equiv}\circ\psi$, so up to
$\equiv$-equivalence the correspondence $\phi\mapsto[-]_{\equiv}\circ\phi$ is
injective. Going in the opposite direction and starting with a homomorphism
$\psi:(X,\beta)\to({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$, let $e_{x}$ be a
representative of $\psi(x)$ for each $x\in X$ and define $\phi:=\lambda
x.e_{x}$. Then $\phi$ is a solution to $(X,\beta)$, and
$[-]_{\equiv}\circ\phi=\psi$. Thus, up to $\equiv$-equivalence, solutions to
systems are in one-to-one correspondence with coalgebra homomorphisms into
$({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$.

Say that a system _admits a unique solution up to $\equiv$_ if it has a
solution and any two solutions to the system are $\equiv$-equivalent. Since,
up to $\equiv$-equivalence, solutions to a system associated with a coalgebra
$(X,\beta)$ are in one-to-one correspondence with coalgebra homomorphisms
$(X,\beta)\to({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$, it suffices for the
purposes of satisfying the hypotheses of Lemma 5.2 to show that every finite
guarded system of equations admits a unique solution up to $\equiv$. The
following theorem is a generalisation of [1, Theorem 5.7].

######  Theorem 5.3.

Every finite guarded system of equations admits a unique solution up to
$\equiv$.

The proof is a recreation of the one that appears under [1, Theorem 5.7] with
the more general context of our paper in mind. Remarkably, the essential
details of the proof remain unchanged despite the jump in the level of
abstraction between the two results.

Completeness of $\equiv$ with respect to behavioural equivalence is now a
direct consequence of Lemmas 5.2, 5.2 and 5.3.

######  Corollary 5.1 (Completeness).

Let $e,f\in\mathtt{Exp}$. If $\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor=\lceil\\!\\!\lfloor f\rceil\\!\\!\rfloor$, then $e\equiv
f$.

One way to interpret this theorem is that the algebra
$({\mathtt{Exp}}/{\equiv},\hat{\alpha})$ of process terms modulo $\equiv$ is
isomorphic to a subalgebra of $(Z,\gamma)$, or dually
$({\mathtt{Exp}}/{\equiv},\bar{\epsilon})$ is a subcoalgebra of $(Z,\zeta)$.
It is in this sense that $\mathsf{ARB}$, $\mathsf{ACF}$, $\mathsf{APA}$, and
$\mathsf{ANP}$ are algebras of behaviours.

##  6 Star Fragments

In this section we study a fragment of our specification languages consisting
of _star expressions_. These include primitive actions from $A$, a form of
sequential composition, and analogues of the Kleene star. We do not aim to
give a complete axiomatisation of behavioural equivalence for star
expressions, as even in simple cases this is notoriously difficult.
Nevertheless, we think it is valuable to extrapolate from known examples a
speculative axiomatisation independent of the specification languages from
previous sections.

Fix an algebraic theory $(S,\mathsf{E})$ and assume $S$ consists of only
constants and binary operations. Its _star fragment_ is the set
$\mathtt{SExp}$ of expressions given by the grammar

$e,e_{i}::=c\mid\mathtt{1}\mid a\mid e_{1}+_{\sigma}e_{2}\mid e_{1}e_{2}\mid
e^{(\sigma)}$

where $a\in A$, $c$ is a constant in $S$, and $\sigma$ is a binary
$S$-operation.

The star fragment of an algebraic theory is a fragment of $\mathtt{Exp}$ in
the sense that star expressions can be thought of as shorthands for process
terms, as we explain next. In this translation, we fix a distinguished
variable $\underline{u}\in V$, called the _unit_ , which will denote
successful termination, and we also fix a variable $v$ distinct from the unit,
which will appear in the fixpoint. The translation of star expressions to
process terms is defined to be

$\mathtt{1}\mapsto\underline{u}\qquad a\mapsto a\underline{u}\qquad
e_{1}+_{\sigma}e_{2}\mapsto\sigma(e_{1},e_{2})\qquad e_{1}e_{2}\mapsto
e_{1}[e_{2}/\underline{u}]\qquad e^{(\sigma)}\mapsto\mu
v~{}(e[v/\underline{u}]+_{\sigma}\underline{u})$

Sequential composition of terms is associative and distributes over branching
operations on the right-hand side111111But not on the left-hand side! Observe
the difference between the processes $a(b+c)$ and $ab+ac$ here.: for any
$e_{1},e_{2},f\in\mathtt{SExp}$, $(e_{1}+_{\sigma}e_{2})f$ and
$e_{1}f+_{\sigma}e_{2}f$ translate to the same process term. Similarly, the
intuitively correct identities $\mathtt{1}e=e=e\mathtt{1}$ hold modulo
translation, as well as the identity $0e=0$.121212But not $e0=0$! See also the
previous footnote.

$\begin{aligned} \ell(c)&=[c]_{\mathsf{E}}\\\
\ell(\mathtt{1})&=[\checkmark]_{\mathsf{E}}\\\
\ell(a)&=[(a,\mathtt{1})]_{\mathsf{E}}\end{aligned}\qquad\qquad\begin{aligned}
\ell(e_{1}+_{\sigma}e_{2})&=\sigma(\ell(e_{1}),\ell(e_{2}))\\\
\ell(ef)&=p(\ell(f),[(a_{1},e_{1}f)]_{\mathsf{E}},\dots,[(a_{n},e_{n}f)]_{\mathsf{E}})\\\
\ell(e^{(\sigma)})&=p([0]_{\mathsf{E}},[(a_{1},e_{1}e^{(\sigma)})]_{\mathsf{E}},\dots,[(a_{n},e_{n}e^{(\sigma)})]_{\mathsf{E}})+_{\sigma}[\checkmark]_{\mathsf{E}}\end{aligned}$
Figure 3:  The coalgebra structure map $\ell:\mathtt{SExp}\to
L_{M}\mathtt{SExp}$. Here, $c$ is a constant of $S$, $\sigma$ is a binary
operation of $S$, $a\in A$, and $e,e_{i}\in\mathtt{SExp}$. In the last two
equations,
$\ell(e)=[p(\checkmark,(a_{1},e_{1}),\dots,(a_{n},e_{n}))]_{\mathsf{E}}$ for
some $p\in S^{*}(\\{\checkmark\\}+A\times\mathtt{SExp})$.

The operational semantics for star expressions is given by an
$L_{M}$-coalgebra $(\mathtt{SExp},\ell)$ in Fig. 3, where
$L_{M}=M(\\{\checkmark\\}+A\times\text{Id})$. Abstractly, the operational
interpretation $\ell(e)$ of a star expression $e$ is obtained by translating
$e$ into a process term (also called $e$) and then identifying $\underline{u}$
with $\checkmark$ in $\epsilon(e)$. While the notation is somewhat opaque at
this level of generality, in specific instances the map $\ell$ amounts to a
familiar transition structure.

######  Example 6.1.

The star fragment of $\mathsf{ACF}$ from Example 2.3 and Example 3.1 coincides
with $\mathsf{GKAT}$, the algebra of programs introduced in [38] and studied
further in [24, 23]. Instantiating $\mathtt{SExp}$ in this context reveals the
syntax

$e_{i}::=0\mid\mathtt{1}\mid a\mid e_{1}+_{b}e_{2}\mid e_{1}e_{2}\mid e^{(b)}$

for $b\subseteq\texttt{At}$ and $a\in A$. This is nearly the syntax of
$\mathsf{GKAT}$, the only difference being the presence of $\mathtt{1}$ and
$0$ instead of Boolean constants $b\subseteq\texttt{At}$. This is merely
cosmetic, as we can just as well define $b:=\mathtt{1}+_{b}0$.

In this context, $M=(1+\text{Id})^{\texttt{At}}$, and so
$L_{M}\cong(2+A\times\text{Id})^{\texttt{At}}$, which is the precise
coalgebraic signature of the automaton models of $\mathsf{GKAT}$ expressions.
It is readily checked that the operational semantics of $\mathsf{GKAT}$ also
coincides with the operational semantics of the star fragment of
$\mathsf{ACF}$ given above.

######  Example 6.2.

The star fragment of $\mathsf{APA}$ from Example 2.5 and Example 3.2 is a
subset of the calculus of programs introduced in [9], but with an iteration
operator for each $p\in[0,1]$. Instantiating $\mathtt{SExp}$ in this context
reveals the syntax

$e_{i}::=0\mid\mathtt{1}\mid a\mid e_{1}+_{p}e_{2}\mid e_{1}e_{2}\mid e^{(p)}$

for $p\in[0,1]$ and $a\in A$. The process $e^{(p)}$ can be thought of as a
generalised Bernoulli process that runs $e$ until it reaches $\checkmark$ and
then flips a weighted coin to decide whether to start from the beginning of
$e$ or to terminate successfully.

We now provide a candidate axiomatisation for the star fragment while leaving
the question of completeness open. Say that a star expression $e$ is _guarded_
if the unit is guarded in $e$ as an expression in $\mathtt{Exp}$. We define
$\mathsf{E}^{*}$ to be the theory consisting of $\mathsf{E}$, the axiom schema

$\begin{aligned} (\mathsf{E^{*}1})&&1e&=e1=e\\\
(\mathsf{E^{*}2})&&ce&=c\end{aligned}\qquad\qquad\begin{aligned}
(\mathsf{E^{*}3})&&e_{1}(e_{2}e_{3})&=(e_{1}e_{2})e_{3}\\\
(\mathsf{E^{*}4})&&(e+_{\tau}\mathtt{1})^{(\sigma)}&=(e+_{\tau}0)^{(\sigma)}\end{aligned}$

and the inference rules

$\prftree[l]{($\mathsf{E^{*}5}$)\quad}{\text{$e$ is
guarded}}{e^{(\sigma)}=ee^{(\sigma)}+_{\sigma}\mathtt{1}}\qquad\qquad\prftree[l]{($\mathsf{E^{*}6}$)\quad}{g=eg+_{\sigma}f\qquad\text{$e$
is guarded}}{g=e^{(\sigma)}f}$

In the specific cases where $\mathsf{E}=\mathsf{SL}$ and
$\mathsf{E}=\mathsf{GS}$, $\mathsf{E}^{*}$ is equivalent to the candidate
axiomatisations for the star fragments of $\mathsf{ARB}$ [1] and
$\mathsf{ACF}$ [24, 23].131313See Appendix F for details.

There is a difference between our axioms and the axioms in [1, 24, 23]:
instead of ($\mathsf{E^{*}5}$), all equations of the form
$e^{(\sigma)}=ee^{(\sigma)}+_{\sigma}1$ appear in loc cit, even those where
$e$ is unguarded. We adopt ($\mathsf{E^{*}5}$) instead because the
unrestricted version of ($\mathsf{E^{*}5}$) fails to be sound for the star
expressions of $\mathsf{APA}$. For example, if $e=\mathtt{1}+_{\frac{1}{3}}a$,
then
$ee^{(1/2)}+_{\frac{1}{2}}\mathtt{1}\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\xRightarrow{7/{12}}$}}}\checkmark$
while
$e^{(\frac{1}{2})}\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\xRightarrow{1/2}$}}}\checkmark$.
Secondly, the unrestricted axioms can be derived from ($\mathsf{E^{*}5}$) in
the cases of Milner’s star fragment and the star fragment of
$\mathsf{ACF}$.141414See Appendix F.

We are confident that a completeness result can be obtained in several
instances of the framework for the axiomatisation we have suggested above.
However, in several cases this cannot happen. For example, there is no way to
derive the identity
$((a+_{\frac{1}{2}}\mathtt{1})+b)^{*}=((a+_{\frac{1}{2}}0)+b)^{*}$ from
$\mathsf{CS}^{*}$ (see Example 2.6) despite these expressions being
behaviourally equivalent. What is likely missing from $\mathsf{CS}$ is a
number of axioms that would allow $\mathtt{1}$ to be moved to the top level of
every $S$-term (and then replaced by $0$ using ($\mathsf{E^{*}4}$)). Algebraic
theories where this is doable are called skew-associative, which we define
formally as follows.

######  Definition 6.1.

An algebraic theory $(S,\mathsf{E})$ consisting of constants and binary
operations is called _skew-associative_ if for any pair of binary operations
$\sigma_{1},\tau_{1}$, there is a pair of binary operations
$\sigma_{2},\tau_{2}$ such that
$\sigma_{1}(x,\tau_{1}(y,z))=\tau_{2}(\sigma_{2}(x,y),z)$ appears in
$\mathsf{E}$.

Many of the examples we care about are skew-associative, including the
theories of semilattices, guarded semilattices, and convex algebras.

######  Question 1.

Assume $(S,\mathsf{E})$ is a skew-associative algebraic theory. If $e$ and $f$
are behaviourally equivalent star expressions, is it true that
$\mathsf{E^{*}}\vdash e=f$?

##  7 Related Work

Our framework can be seen as a generalisation of Milner’s $\mathsf{ARB}$ [1]
that reaches beyond nondeterministic choice and covers several other process
algebras already identified in the literature. For example, instantiating our
framework in the theory of pointed convex algebras produces the algebra we
have called $\mathsf{APA}$ (see Example 3.2), which only differs from the
algebra $\mathsf{PE}$ of Stark and Smolka [25] in the axiom ($\mathsf{R1}$).
In loc cit, the requirement that the variable be guarded in the recursed
expression is absent because recursion is computed as a least fixed point in
their semantics. This is not how we interpret recursion. We have included the
guardedness requirement because it is necessary for the soundness of the axiom
in our semantics: for example, where $e=u+_{\frac{1}{2}}v$, we have $\mu
v~{}e\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\xRightarrow{1/2}$}}}u$ and
$e[\mu
v~{}e/v]\mathrel{\raisebox{-1.00006pt}{{\footnotesize$\xRightarrow{3/4}$}}}u$.
In contrast, both $\mu v~{}e$ and $e[\mu v~{}e/v]$ exit in $u$ with
probability $1$ in [25].

For another example, instantiating our framework in the theory $\mathsf{CS}$
of pointed convex semilattices gives $\mathsf{ANP}$ (see Example 2.6), which
differs from the calculus of Mislove, Ouaknine, and Worrell [39] on two
points. Firstly, their axiomatisation contains an unguarded version of
($\mathsf{R1}$), like in [25]. Secondly, the underlying algebraic theory of
[39] corresponds to $\mathsf{CS}$ extended with the axiom $x+_{p}0=0$. The
resulting theory is known in the literature as that of _convex semilattices
with top_ [9].

Star expressions for non-deterministic processes appeared in the work of
Milner [1] as a fragment of $\mathsf{ARB}$ and can be thought of as a
bisimulation-focused analogue of Kleene’s regular expressions for NFAs. While
the syntaxes of Milner’s star expressions and Kleene’s regular expressions are
the same, there are several important differences between their
interpretations. For example, sequential composition is interpreted as the
variable substitution $ef:=e[f/\underline{u}]$ in Milner’s paper, which fails
to distribute over $+$ on the left. A notable insight from [1] is that,
despite these differences, an iteration operator $(-)^{*}$ can be defined for
Milner’s star expressions that satisfies many of the same identities as the
Kleene star. Given a variable $v$ distinct from the unit and a process term
$e$ of $\mathsf{ARB}$ in which at most the unit is free,

$e^{*}=\mu v~{}(e[v/\underline{u}]+\underline{u})$

defines the iteration operator in Milner’s star fragment of $\mathsf{ARB}$. In
Section 6, we generalised this construction of Milner for the more general
process types that we considered in this paper. Our proposed axiomatization is
also inspired by Milner’s work. We expect completeness of our general calculus
will be a hard problem, as completeness in the instantiation to $\mathsf{ARB}$
was open for decades despite the extensive literature on the subject [17, 18,
19, 20, 21].

There are clear parallels between our work and the thesis of Silva [40], in
which a family of calculi is introduced that includes one-exit versions of
$\mathsf{ARB}$, $\mathsf{ACF}$, and $\mathsf{APA}$ (see Examples 2.2, 3.1 and
3.2). The main difference is that our framework is parametric on a finitary
monad on $\mathbf{Sets}$ whereas Silva’s is centered around one particular
theory (semilattices). However, her work considers general polynomial functors
on $\mathbf{Sets}$, which we have not yet done in our paper. We could achieve
a similar level of generality by replacing $A\times\text{Id}$ in our
signatures $\Sigma_{M}$, $B_{M}$, and $L_{M}$ with an arbitrary polynomial
functor.

Our results are also in the same vein as the work of Myers on coalgebraic
expressions [41]. Coalgebraic expressions generalise the calculi of [40] to
arbitrary finitary coalgebraic signatures on a variety of algebras, and
furthermore have totally defined recursion operators similar to ours. However,
the focus of the framework of coalgebraic expressions is on language
semantics, achieved by lifting the coalgebraic signature to a variety. This
distinguishes the framework from our approach: we focus on bisimulation
semantics. This focus is also the reason we interpret our $B_{M}$-coalgebras
in $\mathbf{Sets}$ and not in the Kleisli category of the monad $M$, as is
done in [42] to capture trace semantics of coalgebras.

Finally, there is also a notable connection to the iterative theories of Elgot
[43, 44, 28, 45]. Theorem 5.3 in particular implies that our process algebras
are examples of iterative algebras.

##  8 Future Work

In this paper, we introduced a family of process types whose branching
structure is determined by an algebraic theory. We provided each process type
with a fully expressive specification language paired with a sound and
complete axiomatisation of behavioural equivalence.

There are several instantiations of our framework that we have not yet
explored and are of interest. For example, processes with multiset branching
given by the theory of commutative monoids produces nondeterministic processes
with a simplistic notion of resources. Another example is nondeterministic
weighted processes with branching captured by the monad arising from the weak
distributive law between the free semimodule and powerset monads [46]. Yet
another instantiation arises from the theory of monoids (presenting the list
monad), which produces processes related to breadth-first search algorithms.

Star fragments offer a uniform construction of Kleene-like algebras for a
variety of paradigms of computing. However, our framework does not suggest an
axiomatisation of the star fragment that combines nondeterministic and
probabilistic choice, as the theory $\mathsf{CS}$ is not skew-associative (see
Definition 6.1). We would like to expand our framework to include this
fragment as it provides an interesting but nonstandard interpretation of a
part of the language ProbNetKAT used to verify probabilistic networks [47].

We would also like to investigate the question at the end of Section 6 of
whether $\mathsf{E^{*}}$ is complete for skew-associative theories. In
particular, we believe that a connection can be made to the work of Grabmayer
and Fokkink [21] on LLEE-charts, which provides a completeness theorem for the
so-called 1-free expressions of the star fragment of $\mathsf{ARB}$. Our
process algebras also have uniformly defined 1-free star fragments, and it is
not difficult to give 1-free versions of the axiomatisation $\mathsf{E^{*}}$.
We intend to suitably generalise LLEE-charts to arbitrary skew-associative
theories and prove completeness theorems for 1-free star fragments.

Finally, we would like to know whether our operational semantics for process
terms is an instance of the mathematical operational semantics introduced by
Turi and Plotkin [48].

## References

  * [1] Robin Milner  “A Complete Inference System for a Class of Regular Behaviours”  In _J. Comput. Syst. Sci._ 28.3, 1984, pp. 439–466  DOI: 10.1016/0022-0000(84)90023-0
  * [2] Robin Milner  “A Calculus of Communicating Systems” 92, Lecture Notes in Computer Science  Springer, 1980  DOI: 10.1007/3-540-10235-3
  * [3] Jos C.. Baeten  “A brief history of process algebra”  In _Theor. Comput. Sci._ 335.2-3, 2005, pp. 131–146  DOI: 10.1016/j.tcs.2004.07.036
  * [4] Ernest G. Manes  “Algebraic Theories”, Graduate Texts in Mathematics  Springer-Verlag New York, 1976  DOI: 10.1007/978-1-4612-9860-1
  * [5] Suzana Andova  “Process Algebra with Probabilistic Choice”  In _Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, ARTS’99, Bamberg, Germany, May 26-28, 1999. Proceedings_ 1601, Lecture Notes in Computer Science  Springer, 1999, pp. 111–129  DOI: 10.1007/3-540-48778-6“˙7
  * [6] Tadeusz Świrszcz  “Monadic Functors and Convexity”  In _Bulletin de L’Académie Polonaise des Sciences_ XXII.1, Serie de math., astr., and phys., 1974, pp. 39–42
  * [7] D. Pumplün and Helmut Röhrl  “Convexity theories IV. Klein-Hilbert parts in convex modules”  In _Appl. Categorical Struct._ 3.2, 1995, pp. 173–200  DOI: 10.1007/BF00877635
  * [8] Marshall Harvey Stone  “Postulates for the barycentric calculus”  In _Annali di Matematica Pura ed Applicata_ 29.1 Springer, 1949, pp. 25–30
  * [9] Filippo Bonchi, Ana Sokolova and Valeria Vignudelli  “The Theory of Traces for Systems with Nondeterminism and Probability”  In _34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019_ IEEE, 2019, pp. 1–14  DOI: 10.1109/LICS.2019.8785673
  * [10] Bart Jacobs  “Convexity, Duality and Effects”  In _Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010, Brisbane, Australia, September 20-23, 2010. Proceedings_ 323, IFIP Advances in Information and Communication Technology  Springer, 2010, pp. 1–19  DOI: 10.1007/978-3-642-15240-5“˙1
  * [11] Ernest G. Manes  “Equations for if-then-else”  In _Mathematical Foundations of Programming Semantics, 7th International Conference, Pittsburgh, PA, USA, March 25-28, 1991, Proceedings_ 598, Lecture Notes in Computer Science  Springer, 1991, pp. 446–456  DOI: 10.1007/3-540-55511-0“˙23
  * [12] Stephen L. Bloom and Ralph Tindell  “Varieties of ”if-then-else””  In _SIAM J. Comput._ 12.4, 1983, pp. 677–707  DOI: 10.1137/0212047
  * [13] John McCarthy  “A basis for a mathematical theory of computation, preliminary report”  In _Papers presented at the 1961 western joint IRE-AIEE-ACM computer conference, IRE-AIEE-ACM 1961 (Western), Los Angeles, California, USA, May 9-11, 1961_ ACM, 1961, pp. 225–238  DOI: 10.1145/1460690.1460715
  * [14] Gordon D. Plotkin  “A structural approach to operational semantics”  In _J. Log. Algebraic Methods Program._ 60-61, 2004, pp. 17–139
  * [15] 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, School/ Workshop, Noordwijkerhout, The Netherlands, May 30 - June 3, 1988, Proceedings_ 354, Lecture Notes in Computer Science  Springer, 1988, pp. 50–122  DOI: 10.1007/BFb0013021
  * [16] Arto Salomaa  “Two Complete Axiom Systems for the Algebra of Regular Events”  In _J. ACM_ 13.1, 1966, pp. 158–169  DOI: 10.1145/321312.321326
  * [17] Wan J. Fokkink and Hans Zantema  “Basic Process Algebra with Iteration: Completeness of its Equational Axioms”  In _Comput. J._ 37.4, 1994, pp. 259–268  DOI: 10.1093/comjnl/37.4.259
  * [18] Wan Fokkink  “Axiomatizations for the perpetual loop in process algebra”  In _Automata, Languages and Programming_ Berlin, Heidelberg: Springer Berlin Heidelberg, 1997, pp. 571–581  DOI: 10.1145/321312.321326
  * [19] Wan J. Fokkink and Hans Zantema  “Termination Modulo Equations by Abstract Commutation with an Application to Iteration”  In _Theor. Comput. Sci._ 177.2, 1997, pp. 407–423  DOI: 10.1016/S0304-3975(96)00254-X
  * [20] Jos C.. Baeten, Flavio Corradini and Clemens Grabmayer  “On the Star Height of Regular Expressions Under Bisimulation (Extended Abstract)”, EXPRESS ’06, 2006
  * [21] Clemens Grabmayer and Wan J. Fokkink  “A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity”  In _LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020_ ACM, 2020, pp. 465–478  DOI: 10.1145/3373718.3394744
  * [22] Clemens Grabmayer  “A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity”  In _9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021, August 31 to September 3, 2021, Salzburg, Austria_ 211, LIPIcs  Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, pp. 16:1–16:23  DOI: 10.4230/LIPIcs.CALCO.2021.16
  * [23] Todd Schmid, Tobias Kappé, Dexter Kozen and Alexandra Silva  “Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness”  In _48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference)_ 198, LIPIcs  Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, pp. 142:1–142:14  DOI: 10.4230/LIPIcs.ICALP.2021.142
  * [24] Steffen Smolka et al.  “Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time”  In _Proc. ACM Program. Lang._ 4.POPL, 2020, pp. 61:1–61:28  DOI: 10.1145/3371129
  * [25] Eugene W. Stark and Scott A. Smolka  “A complete axiom system for finite-state probabilistic processes”  In _Proof, Language, and Interaction, Essays in Honour of Robin Milner_ The MIT Press, 2000, pp. 571–596
  * [26] Jan J… Rutten  “Universal coalgebra: a theory of systems”  In _Theor. Comput. Sci._ 249.1, 2000, pp. 3–80  DOI: 10.1016/S0304-3975(00)00056-6
  * [27] Jan J… Rutten  “Automata and Coinduction (An Exercise in Coalgebra)”  In _CONCUR ’98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings_ 1466, Lecture Notes in Computer Science  Springer, 1998, pp. 194–218  DOI: 10.1007/BFb0055624
  * [28] Stephen L. Bloom and Zoltán Ésik  “Varieties of Iteration Theories”  In _SIAM J. Comput._ 17.5, 1988, pp. 939–966  DOI: 10.1137/0217059
  * [29] Filippo Bonchi, Ana Sokolova and Valeria Vignudelli  “Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases”  In _9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)_ 211, Leibniz International Proceedings in Informatics (LIPIcs)  Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021, pp. 11:1–11:18  DOI: 10.4230/LIPIcs.CALCO.2021.11
  * [30] Daniele Varacca and Glynn Winskel  “Distributing probability over non-determinism”  In _Mathematical Structures in Computer Science_ 16.1 Cambridge University Press, 2006, pp. 87–113  DOI: 10.1017/S0960129505005074
  * [31] Filippo Bonchi, Alexandra Silva and Ana Sokolova  “The Power of Convex Algebras”  In _28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany_ 85, LIPIcs  Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, pp. 23:1–23:18  DOI: 10.4230/LIPIcs.CONCUR.2017.23
  * [32] Jan J… Rutten and Daniele Turi  “On the foundations of final semantics: Non-standard sets, metric spaces, partial orders”  In _Semantics: Foundations and Applications_ Berlin, Heidelberg: Springer Berlin Heidelberg, 1993, pp. 477–530
  * [33] Michael Barr  “Terminal Coalgebras in Well-Founded Set Theory”  In _Theor. Comput. Sci._ 114.2, 1993, pp. 299–315  DOI: 10.1016/0304-3975(93)90076-6
  * [34] Joachim Lambek  “A fixpoint theorem for complete categories”  In _Mathematische Zeitschrift_ 103.2 Springer, 1968, pp. 151–161
  * [35] Joseph A. Goguen, James W. Thatcher, Eric G. Wagner and Jesse B. Wright  “Initial Algebra Semantics and Continuous Algebras”  In _J. ACM_ 24.1, 1977, pp. 68–95  DOI: 10.1145/321992.321997
  * [36] Todd Schmid, Jurriaan Rot and Alexandra Silva  “On Star Expressions and Coalgebraic Completeness Theorems”  In _Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021_ 351, EPTCS, 2021, pp. 242–259  DOI: 10.4204/EPTCS.351.15
  * [37] H. Gumm  “Elements of the general theory of coalgebras”  In _LUATCS’99, Rand Afrikaans University, Johannesburg_ , 1999
  * [38] Dexter Kozen and Wei-Lung Dustin Tseng  “The Böhm-Jacopini Theorem Is False, Propositionally”  In _Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings_ 5133, Lecture Notes in Computer Science  Springer, 2008, pp. 177–192  DOI: 10.1007/978-3-540-70594-9“˙11
  * [39] Michael W. Mislove, Joël Ouaknine and James Worrell  “Axioms for Probability and Nondeterminism”  In _Proceedings of the 10th International Workshop on Expressiveness in Concurrency, EXPRESS 2003, Marseille, France, September 2, 2003_ 96, Electronic Notes in Theoretical Computer Science  Elsevier, 2003, pp. 7–28  DOI: 10.1016/j.entcs.2004.04.019
  * [40] Alexandra Silva  “Kleene coalgebra”, 2010
  * [41] Robert S.. Myers  “Coalgebraic Expressions”  In _6th Workshop on Fixed Points in Computer Science, FICS 2009, Coimbra, Portugal, September 12-13, 2009_ Institute of Cybernetics, 2009, pp. 61–69  URL: http://cs.ioc.ee/fics09/proceedings/contrib8.pdf
  * [42] Ichiro Hasuo, Bart Jacobs and Ana Sokolova  “Generic Trace Semantics via Coinduction”  In _Log. Methods Comput. Sci._ 3.4, 2007  DOI: 10.2168/LMCS-3(4:11)2007
  * [43] Calvin C. Elgot  “Monadic Computation And Iterative Algebraic Theories”  In _Logic Colloquium ’73_ 80, Studies in Logic and the Foundations of Mathematics  Elsevier, 1975, pp. 175–230  DOI: 10.1016/S0049-237X(08)71949-9
  * [44] Stephen L. Bloom and Calvin C. Elgot  “The Existence and Construction of Free Iterative Theories”  In _J. Comput. Syst. Sci._ 12.3, 1976, pp. 305–318  DOI: 10.1016/S0022-0000(76)80003-7
  * [45] Evelyn Nelson  “Iterative Algebras”  In _Theor. Comput. Sci._ 25, 1983, pp. 67–94  DOI: 10.1016/0304-3975(83)90014-2
  * [46] Filippo Bonchi and Alessio Santamaria  “Combining Semilattices and Semimodules”  In _Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings_ 12650, Lecture Notes in Computer Science  Springer, 2021, pp. 102–123  DOI: 10.1007/978-3-030-71995-1“˙6
  * [47] Nate Foster et al.  “Probabilistic NetKAT”  In _Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings_ 9632, Lecture Notes in Computer Science  Springer, 2016, pp. 282–309  DOI: 10.1007/978-3-662-49498-1“˙12
  * [48] Daniele Turi and Gordon D. Plotkin  “Towards a Mathematical Operational Semantics”  In _Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997_ IEEE Computer Society, 1997, pp. 280–291  DOI: 10.1109/LICS.1997.614955
  * [49] Bart Jacobs  “A Bialgebraic Review of Deterministic Automata, Regular Expressions and Languages”  In _Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday_ 4060, Lecture Notes in Computer Science  Springer, 2006, pp. 375–404  DOI: 10.1007/11780274“˙20

##  Appendix A Notes on Guarded Semilattices

This appendix is here mainly to give an account of what is essentially the
algebra of if-then-else statements of a propositional imperative programming
language. For a fixed finite set At, call a structure
$(X,0,\\{+_{b}\\}_{b\subseteq\texttt{At}})$ consisting of an underlying set
$X$, a constant $0\in X$, and a binary operation $+_{b}:X^{2}\to X$ for each
$b\subseteq\texttt{At}$ a _guarded semilattice_ if
$(X,0,\\{+_{b}\\}_{b\subseteq\texttt{At}})$ satisfies all instances of the
equations ($\mathsf{GS}$1)-($\mathsf{GS}$4) from Example 2.3. Guarded
semilattices are examples of the so-called _McCarthy algebras_ of [11], and
conversely every McCarthy algebra in finitely many propositions is a guarded
semilattice. We change the name to emphasise the presence of finite Boolean
guards, as well as the inherent order structure of guarded semilattices that
will be expanded upon in future work.

Let $\mathbf{GS}$ denote the category of guarded semilattices and their
homomorphisms. We define the functor $F:\mathbf{Sets}\to\mathbf{GS}$ such that
$FX=((1+X)^{\texttt{At}},0,\\{+_{b}\\}_{b\subseteq\texttt{At}})$ for every set
$X$, where $0:=\lambda\xi.0$ and

$h+_{b}k:=\lambda\xi.\begin{cases}h(\xi)&\xi\in b\\\ k(\xi)&\xi\not\in
b\end{cases}$

and given a function $f:X\to Y$, $F(f)(h)=(1+f)\circ h$. It is straightforward
to verify that $FX$ is indeed a guarded semilattice for any $X$.

######  Lemma A.1.

Every guarded semilattice can be embedded into a guarded semilattice of the
form $FX$ for some set $X$.

###### Proof.

Let $(X,0,\\{+_{b}\\}_{b\subseteq\texttt{At}})$ be a guarded semilattice and
define the map $\eta:X\to(1+X)^{\texttt{At}}$ by
$\eta(x)=\lambda\xi.x+_{\xi}0$. Let $\texttt{At}=\\{\xi_{1},\dots,\xi_{n}\\}$.
It follows from ($\mathsf{GS}$4) and ($\mathsf{GS}$2) that for any $x\in X$,

$x=x+_{\xi_{n}}(x+_{\xi_{n-1}}(\dots(x+_{\xi_{1}}0)))$

Whence, $\eta$ is clearly injective, for if $x+_{\xi}0=y+_{\xi}0$ for all
$\xi\in\texttt{At}$, one can show by induction on $n$ that

$x+_{\xi_{n}}(x+_{\xi_{n-1}}(\dots(x+_{\xi_{1}}0)))=y+_{\xi_{n}}(y+_{\xi_{n-1}}(\dots(y+_{\xi_{1}}0)))$

Hence, it suffices to see that $\eta$ is an algebra homomorphism. Given
$x,y\in X$ and $b\subseteq\texttt{At}$, we have

$\displaystyle\eta({x+_{b}y})(\xi)$
$\displaystyle=(x+_{b}y)+_{\xi}0=x+_{b\cap\xi}(y+_{\xi}0)=\begin{cases}x+_{\xi}(y+_{\xi}0)&\xi\in
b\\\ x+_{0}(y+_{\xi}0)&\xi\not\in b\end{cases}$
$\displaystyle=\begin{cases}x+_{\xi}\bar{\xi}(y+_{\xi}0)&\xi\in b\\\
y+_{\xi}0&\xi\not\in b\end{cases}\quad=\begin{cases}x+_{\xi}0&\xi\in b\\\
y+_{\xi}0&\xi\not\in b\end{cases}\quad=(\eta({x})+_{b}\eta({y}))(\xi)$

∎

As a corollary, we obtain the following theorem, which essentially states that
the theory of guarded semilattices presents the monad
$(1+\text{Id})^{\texttt{At}}$.

######  Theorem A.1.

Where $U:\mathbf{GSL}\to\mathbf{Sets}$ is the forgetful functor taking an
algebra to its underlying set, there exists an adjunction $F\dashv U$.

The unit of the adjunction $\text{Id}\Rightarrow UF$ is the map $\eta$ defined
in the proof of Lemma A.1, and where
$\texttt{At}=\\{\xi_{1},\dots,\xi_{n}\\}$, the counit
$\varepsilon:FU\Rightarrow\text{Id}$ is given by

$\varepsilon(h)\mapsto
h(\xi_{n})+_{\xi_{n}}(h(\xi_{n-1})+_{\xi_{n-1}}(\dots(h(\xi_{1})+_{\xi_{1}}0)))$

Furthermore, the transformation $\Delta^{*}:UFUF\Rightarrow UF$, as it is
defined in Example 2.3, is precisely the transformation $U(\varepsilon_{F})$.

##  Appendix B Examples from Section 3

  * •

Consider $M=(1+\text{Id})^{\texttt{At}}$ and an expression $e=\mu
w~{}(a_{1}(v+_{b}a_{2}w)+_{b}u)$. The $B_{M}$-coalgebra structure on this
expression is given by:

$\displaystyle\epsilon(e)$
$\displaystyle=\epsilon(a_{1}(v+_{b}a_{2}w)+_{b}u)[e/\\!/w]=(\lambda\xi.(a_{1},v+_{b}a_{2}w)+_{b}\lambda\xi.u)[e/\\!/w]$
$\displaystyle=(\lambda\xi.(a_{1},v+_{b}a_{2}w))[e/\\!/v]+_{b}(\lambda\xi.u)[e/\\!/w]=\lambda\xi.(a_{1},v+_{b}a_{2}e)+_{b}\lambda\xi.u$
$\displaystyle=\lambda\xi.(a_{1},f)+_{b}\lambda\xi.u$

  * •

Consider $M=\mathcal{D}_{\omega}(1+\text{Id})$ and an expression $e=\mu
v~{}(a_{1}u+_{\frac{1}{2}}(a_{2}v+_{\frac{1}{3}}w))$. The derivation of the
coalgebra structure for this expression is given by:

$\displaystyle\epsilon(e)$
$\displaystyle=\epsilon(a_{1}u+_{\frac{1}{2}}(a_{2}v+_{\frac{1}{3}}w))[e/\\!/v]=\frac{1}{2}\epsilon(a_{1}u)[e/\\!/v]+\frac{1}{2}\epsilon(a_{2}v+_{\frac{1}{3}}w)[e/\\!/v]$
$\displaystyle=\frac{1}{2}\epsilon(a_{1}u)[e/\\!/v]+\frac{1}{2}(\frac{1}{3}\epsilon(a_{2}v)[e/\\!/v]+\frac{2}{3}\epsilon(w)[e/\\!/v])$
$\displaystyle=\frac{1}{2}\delta_{(a_{1},u)}[e/\\!/v]+\frac{1}{6}\delta_{(a_{2},v)}[e/\\!/v]+\frac{2}{6}\delta_{w}[e/\\!/v]$
$\displaystyle=\frac{1}{2}\delta_{(a_{1},u)}+\frac{1}{6}\delta_{(a_{2},e)}+\frac{2}{6}\delta_{w}$

  * •

Finally, consider $M=\mathcal{C}_{0}$ and an expression $e=\mu
v~{}((a_{1}v+_{\frac{1}{3}}a_{2}w)+a_{2}v)$. The $B_{M}$-coalgebra structure
is given by:

$\displaystyle\epsilon(e)$
$\displaystyle=\epsilon((a_{1}v+_{\frac{1}{3}}a_{2}w)+a_{2}v))[e/\\!/v]=\operatorname{conv}(\epsilon(a_{1}v+_{\frac{1}{3}}a_{2}w)[e/\\!/v],\epsilon(a_{2}v)[e/\\!/v])$
$\displaystyle=\operatorname{conv}(\epsilon(a_{1}v)[e/\\!/v]+_{\frac{1}{3}}\epsilon(a_{2}w)[e/\\!/v],\epsilon(a_{2}v)[e/\\!/v])=\operatorname{conv}(\epsilon(a_{1}e)+_{\frac{1}{3}}\epsilon(a_{2}w),\epsilon(a_{2}e))$
$\displaystyle=\operatorname{conv}(\\{\frac{1}{3}\delta_{(a_{1},e)}+\frac{2}{3}\delta_{(a_{2},w)}\\},\\{\delta_{(a_{2},e)}\\})=\operatorname{conv}(\\{\delta_{(a_{1},e)}\\}+_{\frac{1}{3}}\\{\delta_{(a_{2},w)}\\},\\{\delta_{(a_{1},e)}\\})$

##  Appendix C Notes on Substitution Operators

In this paper, several different kinds of substitution operators are used. We
have left this appendix to explain their properties and prepare for their use
in proof later in the document.

The first kind of substitution that appears is _syntactic_ substitution. Given
two expressions $e$ and $f$ and a variable $v$, we define the expression
$e[f/v]$ by induction on $e$ as follows: For the basic constructions,

$u[f/v]=\begin{cases}f&u=v\\\ u&u\neq
v\end{cases}\quad(ae)[f/v]=a(e[f/v])\quad\sigma(e_{1},\dots,e_{n})[f/v]=\sigma(e_{1}[f/v],\dots,e_{n}[f/v])$

but for the recursion case, we only let $(\mu u~{}e)[f/v]$ be well-defined if
either $u=v$, in which case $(\mu v~{}e)[f/v]=\mu v~{}e$ (because $v$ is not
free in $\mu v~{}e$), or $u$ is not free in $f$, in which case $(\mu
u~{}e)[f/v]=\mu u~{}(e[f/v])$. Thus, $[f/v]$ is a partial map
$\mathtt{Exp}\rightharpoonup\mathtt{Exp}$.

We similarly define $e[f_{1}/v_{1},\dots,f_{n}/v_{n}]$ for a distinct list of
variables $v_{1},\dots,v_{n}$ to be the simultaneous substitution of $f_{i}$
for $v_{i}$, $i=1,\dots,n$. For this kind of substitution,

$u[f_{1}/v_{1},\dots,f_{n}/v_{n}]=\begin{cases}f_{i}&u=v_{i}\\\ u&(\forall
i\leq n)~{}u\neq v_{i}\end{cases}$

and if $u=v_{i}$, then

$(\mu u~{}e)[f_{1}/v_{1},\dots,f_{n}/v_{n}]=(\mu
u~{}e)[f_{1}/v_{1},\dots,f_{i-1}/v_{i-1},f_{i+1}/v_{i+1},\dots,f_{n}/v_{n}]$

and otherwise, if $u$ is not free in $f_{i}$ for all $i\leq n$, then

$(\mu u~{}e)[f_{1}/v_{1},\dots,f_{n}/v_{n}]=\mu
u~{}(e[f_{1}/v_{1},\dots,f_{n}/v_{n}])$

Again, $[f_{1}/v_{1},\dots,f_{n}/v_{n}]$ defines a partial operation
$\mathtt{Exp}\rightharpoonup\mathtt{Exp}$.

######  Lemma C.1.

Let $e,f\in\mathtt{Exp}$ and $v\in V$. If no free variable of $f$ is bound in
$e$, then $e[f/v]$ is well-defined.

###### Proof.

Variables bound in $e$ are formally given by a function
$\operatorname{bv}:\mathtt{Exp}\to\mathcal{P}(V)$:

$\begin{aligned} \operatorname{bv}(v)&=\emptyset\\\
\operatorname{bv}(ae)&=\operatorname{bv}(e)\\\
\end{aligned}\qquad\qquad\begin{aligned}
\operatorname{bv}(\sigma(e_{1},\dots,e_{n}))&=\operatorname{bv}(e_{1})~{}\cup\dots\cup~{}\operatorname{bv}(e_{n})\\\
\operatorname{bv}(\mu
v~{}e)&=\\{v\\}~{}\cup~{}\operatorname{bv}(e)\end{aligned}$

Similarly, the free variables of expression $e$ are a function
$\operatorname{fv}:\mathtt{Exp}\to\mathcal{P}(V)$ defined as:

$\begin{aligned} \operatorname{fv}(v)&=\\{v\\}\\\
\operatorname{fv}(ae)&=\operatorname{fv}(e)\\\
\end{aligned}\qquad\qquad\begin{aligned}
\operatorname{fv}(\sigma(e_{1},\dots,e_{n}))&=\operatorname{fv}(e_{1})~{}\cup\dots\cup~{}\operatorname{fv}(e_{n})\\\
\operatorname{fv}(\mu v~{}e)&=\operatorname{fv}(e)\setminus\\{v\\}\\\
\end{aligned}$

We prove the lemma by induction on $e$. We assume that
$\operatorname{fv}(f)\cap\operatorname{bv}(e)=\emptyset$.

  * •

The variable case is trivial, as the syntactic substitution is always well-
defined.

  * •

For the prefixing case, assume that $e=ag$. By definition
$(ag)[f/v]=a(g[f/v])$, so either is well-defined whenever $g[f/v]$ is well-
defined. Since $\operatorname{bv}(ag)=\operatorname{bv}(g)$, by the induction
hypothesis $ag[f/v]$ is well-defined.

  * •

Now suppose $e=\sigma(e_{1},\dots,e_{n})$. By definition,
$\sigma(e_{1},\dots,e_{n})[f/v]=\sigma(e_{1}[f/v],\dots,e_{n}[f/v])$, so
substituting $f$ for $v$ is well defined for each $e_{1},\dots,e_{n}$. Since
$\operatorname{bv}(e_{k})\subseteq\operatorname{bv}(\sigma(e_{1},\dots,e_{n}))$
for each subexpression $e_{k}$, for any $x\in\operatorname{fv}(f)$ we have
that $x\notin\operatorname{bv}(\sigma(e_{1},\dots,e_{k},\dots,e_{n}))$ and
therefore $x\notin\operatorname{bv}(e_{k})$. By the induction hypothesis,
$e_{k}[f/v]$ is well-defined for each $e_{k}$. It follows that $e[f/v]$ is
well-defined.

  * •

For the recursion case, assume that $e=\mu u~{}g$. We consider two subcases.

    * –

If $u=v$, then syntactic substitution is well-defined and is given by $(\mu
u~{}g)[f/v]=\mu u~{}g$.

    * –

Otherwise, $u\neq v$. By assumption we know that if
$x\in\operatorname{fv}(f)$, then $x\notin\operatorname{bv}(g)\cup\\{u\\}$, so
$u$ is not free in $f$. It follows that $(\mu u~{}g)[f/v]$ is well defined if
and only if $g[f/v]$ is well-defined. By the induction hypothesis, for any
$x\in\operatorname{fv}(f)$ we have that $x\notin\operatorname{bv}(g)$. ∎

Semantic substitution has a cousin that appears in the paper, namely _guarded
syntactic substitution_. Given $e,f\in\mathtt{Exp}$ and $v\in V$, we define
$e[f/\\!/v]$ to be the expression

$u[f/\\!/v]=\begin{cases}0&u=v\\\ u&u\neq
v\end{cases}\qquad(ae)[f/\\!/v]=a(e[f/v])\qquad\sigma(e_{1},\dots,e_{n})[f/\\!/v]=\sigma(e_{1}[f/\\!/v],\dots,e_{n}[f/\\!/v])$

Again, we only let $(\mu u~{}e)[f/\\!/v]$ be well-defined if either $u=v$, in
which case $(\mu v~{}e)[f/\\!/v]=\mu v~{}e$, or $u$ is not free in $f$, in
which case $(\mu u~{}e)[f/\\!/v]=\mu u~{}(e[f/\\!/v])$. Thus, $[f/\\!/v]$ is
yet another partial map $\mathtt{Exp}\rightharpoonup\mathtt{Exp}$.

The first appearance of the guarded substitution operator in the paper is
actually as a partial operator on $B_{M}(\mathtt{Exp})$, however. Recalling
that $B_{M}(\mathtt{Exp})=M(V+A\times\mathtt{Exp})$ is the set
$S^{*}(V+A\times\mathtt{Exp})$ modulo $\mathsf{E}$, it is defined first as a
map $V+A\times\mathtt{Exp}\to B_{M}\mathtt{Exp}$ as follows: given $u\in V$
and $(a,e)\in A\times\mathtt{Exp}$, let

$u[f/\\!/v]=\begin{cases}[0]_{\mathsf{E}}&u=v\\\ [u]_{\mathsf{E}}&u\neq
v\end{cases}\qquad(a,e)[f/\\!/v]=a(e[f/v])$

We record the existence of a lift in the following lemma.

See 3.1

###### Proof.

By definition, $[\mu v~{}e/\\!/v]$ is obtained from the unique lifting of the
partial map $h:V+A\times\mathtt{Exp}\rightharpoonup
S^{*}(V+A\times\mathtt{Exp})$ defined

$h(u)=\begin{cases}u&u\neq v\\\ 0&u=v\end{cases}\qquad h(a,f)=(a,f[\mu
v~{}e/v])$

to a partial $S$-algebra homomorphism
$h^{\\#}:S^{*}(V+A\times\mathtt{Exp})\rightharpoonup
S^{*}(V+A\times\mathtt{Exp})$ by further composing with the quotient
homomorphism $[-]_{\mathsf{E}}:S^{*}(V+A\times\mathtt{Exp})\to
B_{M}\mathtt{Exp}$ (this factorisation exists for partial maps because $S^{*}$
preserves monos). Thus,

$\ker([\mu
v~{}e/\\!/v])=\ker([-]_{\mathsf{E}}~{}h^{\\#})\supseteq\ker([-]_{\mathsf{E}})\cap\operatorname{dom}(h^{\\#})^{2}$

where for an arbitrary partial map $f:X\rightharpoonup Y$,
$\ker(f)=\\{(x_{1},x_{2})\mid f(x_{1})=f(x_{2})\\}$. In other words, $[\mu
v~{}e/\\!/v]$ is constant on $\mathsf{E}$-congruence classes. Since $B_{M}$
preserves monos and $[-]_{\mathsf{E}}$ is surjective, there is a unique
$B_{M}\mathtt{Exp}\rightharpoonup B_{M}\mathtt{Exp}$ such that the following
diagram commutes.

$\leavevmode\hbox to184.22pt{\vbox
to61.32pt{\pgfpicture\makeatletter\hbox{\hskip 31.7476pt\lower-48.04863pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{-29.08119pt}{-2.25443pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$S^{*}(V+A\times\mathtt{Exp})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{{{{}{}{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{91.63954pt}{-2.25443pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$S^{*}(V+A\times\mathtt{Exp})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{{{ {}{}{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{-12.70767pt}{-43.82668pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$B_{M}\mathtt{Exp}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{
{}{}{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{108.01306pt}{-43.82668pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$B_{M}\mathtt{Exp}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{{{{}}}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{21.78075pt}{-28.6311pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\circlearrowleft$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{{
{\pgfsys@beginscope\pgfsys@setlinewidth{0.32pt}\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{}
{}{}{} {}{}{} {}
\pgfsys@moveto{-1.19998pt}{1.59998pt}\pgfsys@curveto{-1.09998pt}{0.99998pt}{0.0pt}{0.09999pt}{0.29999pt}{0.0pt}\pgfsys@curveto{0.21999pt}{-0.04pt}{0.2pt}{-0.04pt}{0.2pt}{-0.04pt}\pgfsys@lineto{0.0pt}{-0.04pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{31.90762pt}{0.0pt}\pgfsys@lineto{88.35315pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{88.35315pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{55.38907pt}{2.8264pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$h^{\\#}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-7.08084pt}\pgfsys@lineto{0.0pt}{-35.07361pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-35.07361pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{-12.98645pt}{-23.30722pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$[-]_{\mathsf{E}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{}{}{{}}\pgfsys@moveto{20.40004pt}{-7.08084pt}\pgfsys@lineto{104.75208pt}{-36.33623pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9448}{-0.32768}{0.32768}{0.9448}{104.75206pt}{-36.33621pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}\pgfsys@moveto{84.34036pt}{-15.11746pt}\pgfsys@lineto{41.24634pt}{-15.11746pt}\pgfsys@lineto{41.24634pt}{-28.4503pt}\pgfsys@lineto{84.34036pt}{-28.4503pt}\pgfsys@closepath\pgfsys@moveto{41.24634pt}{-28.4503pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{43.91275pt}{-23.78389pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$[\mu v~{}e/\\!/v]$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{}{}{{}}\pgfsys@moveto{120.72073pt}{-7.08084pt}\pgfsys@lineto{120.72073pt}{-35.07361pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{120.72073pt}{-35.07361pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{123.54713pt}{-23.30722pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$[-]_{\mathsf{E}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{15.53409pt}{-41.87112pt}\pgfsys@lineto{104.72667pt}{-41.87112pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{104.72667pt}{-41.87112pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\qed$

The two versions of guarded syntactic substitution interact as expected.

######  Lemma C.2.

For any $p\in S^{*}(V+A\times\mathtt{Exp})$ and $f\in\mathtt{Exp}$ and $v\in
V$, $p[f/\\!/v]$ is well-defined if and only if $p^{\dagger}[f/\\!/v]$ is
well-defined, and in such a case
$[p]_{\mathsf{E}}[f/\\!/v]=\epsilon(p^{\dagger}[f/\\!/v])$.

###### Proof.

We proceed by induction on $p$.

  * •

Suppose that $p=w$ for some $w\in V$. In this case, $w^{\dagger}=w$, so both
$w[f/\\!/v]$ and $w^{\dagger}[f/\\!/v]$ are trivially well-defined. For the
desired identity, consider following subcases.

    * –

If $w=v$, then
$[w]_{\mathsf{E}}[f/\\!/v]=\eta^{M}(0)=\epsilon(0)=\epsilon(w[f/\\!/v])=\epsilon(w^{\dagger}[f/\\!/v])$.

    * –

Otherwise, if $w\neq v$, then
$[w]_{\mathsf{E}}[f/\\!/v]=\eta^{M}(w)=\epsilon(w)=\epsilon(w[f/\\!/v])=\epsilon(w^{\dagger}[f/\\!/v])$.

  * •

Suppose that $p=(a,e)$ for some $a\in A$ and $e\in\mathtt{Exp}$. Since
$(a,e)^{\dagger}=ae$ in this case, both $p[f/\\!/v]$ and
$p^{\dagger}[f/\\!/v]$ are well-defined when $e[f/v]$ is. Therefore
$ae[f/\\!/v]$ is well-defined if and only if $(a,e)^{\dagger}[f/\\!/v]$ is
well defined. Furthermore, we know
$[(a,e)]_{\mathsf{E}}[f/\\!/v]=[(a,e[f/v])]_{\mathsf{E}}$, so
$[(a,e)]_{\mathsf{E}}[f/\\!/v]=[(a,e[f/v])]_{\mathsf{E}}=\epsilon(ae[f/v])=\epsilon((a,e)^{\dagger}[f/\\!/v])$.

  * •

Finally, suppose $p=\sigma(p_{1},\dots,p_{n})$ for some $p_{1},\dots,p_{n}\in
S^{*}(V+A\times\mathtt{Exp})$, and recall that
$\sigma(p_{1},\dots,p_{n})^{\dagger}=\sigma(p_{1}^{\dagger},\dots,p_{n}^{\dagger})$.
Since
$\sigma(p_{1},\dots,p_{n})[f/\\!/v]=\sigma(p_{1}[f/\\!/v],\dots,p_{n}[f/\\!/v])$,
we have

$\sigma(p_{1},\dots,p_{n})^{\dagger}[f/\\!/v]=\sigma(p_{1}^{\dagger}[f/\\!/v],\dots,p_{n}^{\dagger}[f/\\!/v])$

By the induction hypothesis, $p_{i}[f/\\!/v]$ is well-defined if and only if
$p_{i}^{\dagger}[f/\\!/v]$ is well-defined, for $1\leq i\leq n$. Towards the
desired identity, recall that

$[\sigma(p_{1},\dots,p_{n})]_{\mathsf{E}}[f/\\!/v]=\sigma([p_{1}]_{\mathsf{E}},\dots,[p_{n}]_{\mathsf{E}})[f/\\!/v]=\sigma([p_{1}]_{\mathsf{E}}[f/\\!/v],\dots,[p_{n}]_{\mathsf{E}}[f/\\!/v])$

It follows from the induction hypothesis that

$\displaystyle[\sigma(p_{1},\dots,p_{n})]_{\mathsf{E}}[f/\\!/v]$
$\displaystyle=[\sigma(p_{1}[f/\\!/v],\dots,p_{n}[f/\\!/v])]_{\mathsf{E}}$
$\displaystyle=\sigma(\epsilon(p_{1}^{\dagger}[f/\\!/v])),\dots,\epsilon(p_{n}^{\dagger}[f/\\!/v]))$
$\displaystyle=\epsilon(\sigma(p_{1},\dots,p_{n})^{\dagger}[f/\\!/v])\qed$

In the paper, we also introduced two versions of substitution for behaviours.
Given $t,s\in Z$, and $v\in V$, we define $t\\{s/v\\}$ by a behavioural
differential equation that depends on $\zeta(t)$ as follows:

$\zeta(t\\{s/v\\})=\begin{cases}\zeta(s)&\zeta(t)=[v]_{\mathsf{E}}\\\
[u]_{\mathsf{E}}&\zeta(t)=[u]_{\mathsf{E}}\neq[v]_{\mathsf{E}}\\\
[(a,r\\{s/v\\})]_{\mathsf{E}}&\zeta(t)=[(a,r)]_{\mathsf{E}}\\\
\sigma(\zeta(t_{1}\\{s/v\\}),\dots,\zeta(t_{n}\\{s/v\\}))&\zeta(t)=[\sigma(\zeta(t_{1}),\dots,\zeta(t_{n}))]_{\mathsf{E}}\end{cases}$

Note that unlike its syntactic relative, $\\{s/v\\}$ is a total function $Z\to
Z$. Despite their differences, however, behavioural substitution enjoys many
of the important properties of syntactic substitution. The following theorem
provides a simplified coinductive principle with which we can prove these
properties for our processes.

######  Theorem C.1.

Let $h,k:Z\to Z$. If $h$ and $k$ satisfy properties (i)-(iii) below, then
$h=k$.

  1. (i)

if $\zeta(t)=[w]_{\mathsf{E}}$, then $\zeta(h(t))=\zeta(k(t))$;

  2. (ii)

if $\zeta(t)=[(a,r)]_{\mathsf{E}}$, then $\zeta(h(t))=[(a,h(r))]_{\mathsf{E}}$
and $\zeta(k(t))=[(a,k(r))]_{\mathsf{E}}$; and

  3. (iii)

if $\zeta(t)=\sigma(\zeta(t_{1}),\dots,\zeta(t_{n}))$, then

$\zeta(h(t))=\sigma(\zeta(h(t_{1})),\dots,\zeta(h(t_{n})))\quad\text{and}\quad\zeta(k(t))=\sigma(\zeta(k(t_{1})),\dots,\zeta(k(t_{n})))$

###### Proof.

We proceed with a proof by _coinduction_. Namely, we will give the relation

$R:=\Delta_{Z}\cup\\{(h(r),k(r))\mid r\in Z\\}$

a $B_{M}$-coalgebra structure $\rho:R\to B_{M}R$ such that the projections
$\pi_{i}:R\to Z$, $i=1,2$, are coalgebra homomorphisms. By finality of
$(Z,\zeta)$, this then implies that $\pi_{1}={!}_{\rho}=\pi_{2}$, which
establishes the identity we are hoping to prove.

Consider a $t\in Z$ and let
$\zeta(t)=[p(v_{1},\dots,v_{n},(a_{1},s_{1}),\dots,(a_{m},s_{m}))]_{\mathsf{E}}$
for some $p\in S^{*}(V+A\times Z)$. Along the diagonal, define

$\rho(t,t)=[p(v_{1},\dots,v_{n},(a_{1},(s_{1},s_{1})),\dots,(a_{n},(s_{n},s_{n})))]_{\mathsf{E}}$

For the other pairs, assume
$[v_{i}]_{\mathsf{E}}=\zeta(h(t_{i}))=\zeta(k(t_{i}))$ for $i=1,\dots,n$ using
(i) and write

$\rho(h(t),k(t))=[p(v_{1},\dots,v_{n},(a_{1},(h(s_{1}),k(s_{1}))),\dots,(a_{m},(h(s_{m}),k(s_{m}))))]_{\mathsf{E}}$

using (ii) and (iii). To see that $\pi_{i}$ is a coalgebra homomorphism for
each $i=1,2$, observe

$\displaystyle B_{M}(\pi_{1})(\rho(h(t),k(t)))$
$\displaystyle=[S^{*}(\pi_{1})(p(v_{1},\dots,v_{n},(a_{1},(h(s_{1}),k(s_{1}))),\dots,(a_{m},(h(s_{m}),k(s_{m})))))]_{\mathsf{E}}$
$\displaystyle=[p(v_{1},\dots,v_{n},(a_{1},h(s_{1}),\dots,(a_{m},h(s_{m}))]_{\mathsf{E}}$
$\displaystyle=\zeta\circ\pi_{1}(h(r),k(r))$

and similarly for $\pi_{2}$. ∎

For the following lemma, we say that a variable $v$ is _dead_ in a behaviour
$t$ if for any other behaviour $s$, $t\\{s/v\\}=t$.

######  Lemma C.3.

Let $u,v\in V$ and $r,s,t\in Z$. If $v$ is dead in $t$ and $u\neq v$, then

$r\\{s/v\\}\\{t/u\\}=r\\{t/u\\}\\{s\\{t/u\\}/v\\}$

###### Proof.

We use Theorem C.1, which requires us to verify (i)-(iii) for the maps
$\\{s/v\\}\\{t/u\\}$ and $\\{t/u\\}\\{s\\{t/u\\}/v\\}$. Assume $u,v,w$ are
distinct variables, and let $a\in A$. There are several cases to consider.

  * (i)

If $\zeta(r)=[v]_{\mathsf{E}}$, then $\zeta(r\\{s/v\\})=\zeta(s)$ and
$\zeta(r\\{t/u\\})=\zeta(r)$. This means that

$\zeta(r\\{s/v\\}\\{t/u\\})=\zeta(s\\{t/u\\})=\zeta(r\\{s\\{t/u\\}/v\\})=\zeta(r\\{t/u\\}\\{s\\{t/u\\}/v\\})$

  * (i’)

If $\zeta(r)=[u]_{\mathsf{E}}$, then $\zeta(r\\{s/v\\})=\zeta(r)$ and
$\zeta(r\\{t/u\\})=\zeta(t)$. This means that

$\zeta(r\\{s/v\\}\\{t/u\\})=\zeta(r\\{t/u\\})=\zeta(t)=\zeta(t\\{s\\{t/u\\}/v\\})=\zeta(r\\{t/u\\}\\{s\\{t/u\\}/v\\})$

  * (i”)

If $\zeta(r)=[w]_{\mathsf{E}}$, then
$\zeta(r\\{s/v\\}\\{t/u\\})=\zeta(r)=\zeta(r\\{t/u\\}\\{s\\{t/u\\}/v\\})$.

  * (ii)

If $\zeta(r)=[(a,r^{\prime})]_{\mathsf{E}}$, then
$\zeta(r\\{s/v\\})=[(a,r^{\prime}\\{s/v\\})]_{\mathsf{E}}$ and
$\zeta(r\\{t/u\\})=[(a,r^{\prime}\\{t/u\\})]_{\mathsf{E}}$. It follows that

$\zeta(r\\{s/v\\}\\{t/u\\})=[(a,r^{\prime}\\{s/v\\}\\{t/u\\})]_{\mathsf{E}}$

and

$\zeta(r\\{t/u\\}\\{s\\{t/u\\}/v\\})=[(a,r^{\prime}\\{t/u\\}\\{s\\{t/u\\}/v\\})]_{\mathsf{E}}$

  * (iii)

Now let $\zeta(r)=\sigma(\zeta(r_{1}),\dots,\zeta(r_{n}))$. By definition,

$\zeta(r\\{s/v\\}\\{t/u\\})=\sigma(\zeta(r_{1}\\{s/v\\}\\{t/u\\}),\dots,\zeta(r_{n}\\{s/v\\}\\{t/u\\}))$

and

$\zeta(r\\{t/u\\}\\{s\\{t/u/v\\})=\sigma(\zeta(r_{1}\\{t/u\\}\\{s\\{t/u/v\\}),\dots,\zeta(r_{n}\\{t/u\\}\\{s\\{t/u/v\\}))$

as desired.∎

######  Lemma C.4.

For any $r,s,t\in Z$ and $v\in V$, $r\\{s/v\\}\\{t/v\\}=r\\{s\\{t/v\\}/v\\}$.

###### Proof.

This also follows from Theorem C.1, where this time we take
$h=\\{s/v\\}\\{t/v\\}$ and $k=\\{s\\{t/v\\}/v\\}$. ∎

We also found the need to define a _guarded_ version of behavioural
substitution. Given $u\in V$ and $(a,r)\in A\times Z$, we define

$\displaystyle u\\{s/\\!/v\\}$ $\displaystyle=\begin{cases}u&u\neq v\\\
0&u=v\end{cases}$ $\displaystyle(a,r)\\{s/\\!/v\\}$
$\displaystyle=(a,r\\{s/v\\})$

and denote by $\\{s/\\!/v\\}$ the unique lifting of this map to an operator on
$B_{M}Z$.151515By Lambek’s lemma, $\zeta:Z\cong B_{M}Z$, so $\\{s/\\!/v\\}$
may also denote the corresponding operator
$\zeta^{-1}~{}\\{s/\\!/v\\}~{}\zeta$ on $Z$ (but we don’t really find occasion
for this here).

######  Lemma C.5.

Let $v\in V$ and $t,s\in Z$. If $v$ is dead in $t$, then
$\zeta(t)\\{s/\\!/v\\}=\zeta(t)$.

###### Proof.

Let $\zeta(t)=[p]_{\mathsf{E}}$ for some $p\in S^{*}(V+A\times Z)$. We proceed
by induction on $p$.

  * •

For the variable case, suppose $p=w\neq v$. We have
$[w]_{\mathsf{E}}\\{s/\\!/v\\}=[w]_{\mathsf{E}}=\zeta(t)$.

  * •

Now assume that $p=(a,e)$ for some $e\in\mathtt{Exp}$. Since $v$ is dead in
$t$,
$[(a,e)]_{\mathsf{E}}\\{s/\\!/v\\}=[(a,e\\{s/v\\})]_{\mathsf{E}}=\zeta(t\\{s/v\\})=\zeta(t)$.

  * •

For the inductive step, assume that
$p=\sigma(\zeta(t_{1}),\dots,\zeta(t_{n}))$. By the induction hypothesis,

$\displaystyle\zeta(t)\\{s/\\!/v\\}$
$\displaystyle=[\sigma(\zeta(t_{1})\\{s/\\!/v\\},\dots,\zeta(t_{n})\\{s/\\!/v\\})]_{\mathsf{E}}$
$\displaystyle=[\sigma(\zeta(t_{1}),\dots,\zeta(t_{n}))]_{\mathsf{E}}=\zeta(t)\qed$

######  Lemma C.6.

Let $u,v$ be distinct variables and $s,t\in Z$. If $v$ is dead in $s$, then

$(\mu v~{}t)\\{s/u\\}=\mu v~{}(t\\{s/u\\})$

###### Proof.

The behaviour $\mu v~{}(t\\{s/u\\})$ is (by definition) the unique solution to
the behavioural differential equation

$\zeta(r)=\zeta(t\\{s/u\\})\\{r/\\!/v\\}$

in the variable $r$. Thus, it suffices to see that $r=(\mu v~{}t)\\{s/u\\}$
satisfies this equation. To this end, there are a few cases to consider.

  * •

If $\zeta(t)=[v]_{\mathsf{E}}$, then $\zeta(\mu v~{}t)=\zeta(t)\\{\mu
v~{}t/\\!/v\\}=[0]_{\mathsf{E}}$. Hence,

$\zeta((\mu v~{}t)\\{s/u\\})=[0]_{\mathsf{E}}=\zeta(t)\\{(\mu
v~{}t)\\{s/u\\}/\\!/v\\}=\zeta(t\\{s/u\\})\\{(\mu v~{}t)\\{s/u\\}/\\!/v\\}$

since $u$ is dead in $t$ as well. Setting $r=(\mu v~{}t)\\{s/u\\}$ satisfies
(*), as desired.

  * •

If $\zeta(t)=[u]_{\mathsf{E}}$, then $\zeta(\mu v~{}t)=\zeta(t)\\{\mu
v~{}t/\\!/v\\}=\zeta(t)$. Taking $r=(\mu v~{}t)\\{s/u\\}$, we see that

$\zeta(r)=\zeta(t\\{s/u\\})=\zeta(s)=\zeta(s)\\{r/\\!/v\\}=\zeta(t\\{s/u\\})\\{r/\\!/v\\}$

by Lemma C.5, since $v$ is dead in $s$.

  * •

Let $w$ be distinct from $u$ and $v$. If $\zeta(t)=[w]_{\mathsf{E}}$, then
trivially
$\zeta(r)=[w]_{\mathsf{E}}=\zeta(t)=\zeta(t\\{s/u\\})=\zeta(t\\{s/u\\})\\{r/\\!/v\\}$.

  * •

If $\zeta(t)=[(a,t^{\prime})]_{\mathsf{E}}$, then $\zeta(\mu
v~{}t)=[(a,t^{\prime}\\{\mu v~{}t/v\\})]_{\mathsf{E}}$. Where $r:=(\mu
v~{}t)\\{s/u\\}$,

$\displaystyle\zeta((\mu v~{}t)\\{s/u\\})$
$\displaystyle=[(a,t^{\prime}\\{(\mu v~{}t)/v\\}\\{s/u\\}\\})]_{\mathsf{E}}$
$\displaystyle=[(a,t^{\prime}\\{s/u\\}\\{(\mu
v~{}t)\\{s/u\\}/v\\}\\})]_{\mathsf{E}}$ (Lemma C.3)
$\displaystyle=[(a,t^{\prime}\\{s/u\\})]_{\mathsf{E}}\\{r/\\!/v\\}=\zeta(t\\{s/u\\})\\{r/\\!/v\\}$

because $v$ is dead in $s$.

  * •

Finally, let
$\zeta(t)=[p(v_{1},\dots,v_{n},(a_{1},r_{1}),\dots,(a_{m},r_{m}))]_{\mathsf{E}}$.
We have

$\displaystyle\zeta(r)$ $\displaystyle=\zeta((\mu v~{}t)\\{s/u\\})$
$\displaystyle=[p(w_{1},\dots,w_{n},(a_{1},r_{1}\\{\mu
v~{}t/v\\}\\{s/u\\}),\dots,(a_{m},r_{m}\\{\mu
v~{}t/v\\}\\{s/u\\}))]_{\mathsf{E}}$
$\displaystyle=[p(w_{1},\dots,w_{n},(a_{1},r_{1}\\{s/u\\}\\{r/v\\}),\dots,(a_{m},r_{m}\\{s/u\\}\\{r/v\\}))]_{\mathsf{E}}$
$\displaystyle=[p(v_{1}^{\prime},\dots,v_{n}^{\prime},(a_{1},r_{1}\\{s/u\\}),\dots,(a_{m},r_{m}\\{s/u\\}))]_{\mathsf{E}}\\{r/\\!/v\\}=\zeta(t\\{s/u\\})\\{r/\\!/v\\}$

where $v_{i}^{\prime}=v_{i}$ if $v_{i}\neq u$ else $v_{i}^{\prime}=u$, and
$w_{i}=v_{i}^{\prime}$ if $v_{i}^{\prime}\neq v$ else $w_{i}=0$. ∎

######  Lemma C.7.

Let $v\in V$ and $e\in\mathtt{Exp}$. If $v$ is not free in $e$, then $v$ is
dead in $\lceil\\!\\!\lfloor e\rceil\\!\\!\rfloor$.

###### Proof.

We show that $\zeta(\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor\\{s/v\\})=\zeta(\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)$ for all $s$ by induction on $e$.

  * •

In the variable case, we only consider $u\neq v$. Here,
$\zeta(\lceil\\!\\!\lfloor u\rceil\\!\\!\rfloor)=[u]_{\mathsf{E}}$, so
$\zeta(\lceil\\!\\!\lfloor u\\{s/v\\}\rceil\\!\\!\rfloor)=\lceil\\!\\!\lfloor
u\rceil\\!\\!\rfloor$.

  * •

Now suppose the result is true for $e$. Since $v$ is free in $ae$ if and only
if $v$ is free in $e$, it must be the case that $v$ is not free in $e$. By the
induction hypothesis, $\zeta(\lceil\\!\\!\lfloor
ae\rceil\\!\\!\rfloor\\{s/v\\})=[(a,\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor\\{s/v\\})]_{\mathsf{E}}=[(a,\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)]_{\mathsf{E}}$.

  * •

Next, assume the result for $e_{1},\dots,e_{n}$, and let $\sigma$ be an
$S$-operation. Since $v$ is not free in $\sigma(e_{1},\dots,e_{n})$ if and
only if $v$ is not free in any of the $e_{i}$, and
$\zeta(\lceil\\!\\!\lfloor\sigma(e_{1},\dots,e_{n})\rceil\\!\\!\rfloor)=\sigma(\zeta(\lceil\\!\\!\lfloor
e_{1}\rceil\\!\\!\rfloor),\dots,\zeta(\lceil\\!\\!\lfloor
e_{n}\rceil\\!\\!\rfloor))$ we have

$\displaystyle\zeta(\lceil\\!\\!\lfloor\sigma(e_{1},\dots,e_{n})\rceil\\!\\!\rfloor\\{s/v\\})$
$\displaystyle=\sigma(\zeta(\lceil\\!\\!\lfloor
e_{1}\rceil\\!\\!\rfloor\\{s/v\\}),\dots,\zeta(\lceil\\!\\!\lfloor
e_{n}\rceil\\!\\!\rfloor\\{s/v\\}))$
$\displaystyle=\sigma(\zeta(\lceil\\!\\!\lfloor
e_{1}\rceil\\!\\!\rfloor),\dots,\zeta(\lceil\\!\\!\lfloor
e_{n}\rceil\\!\\!\rfloor))=\zeta(\lceil\\!\\!\lfloor\sigma(e_{1},\dots,e_{n})\rceil\\!\\!\rfloor)$

  * •

Now assume the result for $e$ and let $u\in V$. In this case, we consider the
expression $\mu u~{}e$ and the following two subcases.

    * –

If $u=v$, then by assumption $v$ is not free in $\mu u~{}e$. Here,
$\zeta(\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor)=\zeta(e)\\{\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor/\\!/v\\}$. Let
$p(v_{1},\dots,v_{n},(a_{1},t_{1}),\dots,(a_{m},t_{m}))\in S^{*}(V+A\times Z)$
such that

$\zeta(\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)=[p(v_{1},\dots,v_{n},(a_{1},t_{1}),\dots,(a_{m},t_{m}))]_{\mathsf{E}}$

and set $w_{i}=0$ if $v_{i}=v$ else $w_{i}=v_{i}$. By definition,

$\displaystyle\zeta(\lceil\\!\\!\lfloor\mu v~{}e\rceil\\!\\!\rfloor)$
$\displaystyle=\zeta(e)\\{\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor/\\!/v\\}$
$\displaystyle=[p(w_{1},\dots,w_{n},(a_{1},t_{1}\\{\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor/v\\}),\dots,(a_{m},t_{m}\\{\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor/v\\}))]_{\mathsf{E}}$

because $w_{i}\neq v$ for any $i\leq n$, and consequently,

$\displaystyle\zeta(\lceil\\!\\!\lfloor\mu v~{}e\rceil\\!\\!\rfloor\\{s/v\\})$
$\displaystyle=[p(w_{1},\dots,w_{n},(a_{1},t_{1}\\{\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor/v\\}\\{s/v\\}),\dots,(a_{m},t_{m}\\{\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor/v\\}\\{s/v\\}))]_{\mathsf{E}}$
$\displaystyle=[p(w_{1},\dots,w_{n},(a_{1},t_{1}\\{\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor\\{s/v\\}/v\\}),\dots,(a_{m},t_{m}\\{\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor\\{s/v\\}/v\\}))]_{\mathsf{E}}$
$\displaystyle=[p(w_{1},\dots,w_{n},(a_{1},t_{1}),\dots,(a_{m},t_{m}))]_{\mathsf{E}}\\{\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor\\{s/v\\}/\\!/v\\}$
$\displaystyle=\zeta(\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)\\{\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor\\{s/v\\}/\\!/v\\}$

Now $\lceil\\!\\!\lfloor\mu v~{}e\rceil\\!\\!\rfloor$ is the unique solution
to the behavioural differential equation $\zeta(r)=\zeta(\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)\\{r/\\!/v\\}$ in the indeterminate $r$, and
$r=\lceil\\!\\!\lfloor\mu v~{}e\rceil\\!\\!\rfloor\\{s/t\\}$ satisfies this
equation, so it must be the case that $\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor=\lceil\\!\\!\lfloor\mu
v~{}e\rceil\\!\\!\rfloor\\{s/v\\}$. Hence, $v$ is dead in
$\lceil\\!\\!\lfloor\mu v~{}e\rceil\\!\\!\rfloor$.

    * –

Now assume $u\neq v$. This means that $v$ is free in $\mu u~{}e$ if and only
if it is free in $e$, so by the inductive hypothesis $v$ is dead in
$\lceil\\!\\!\lfloor e\rceil\\!\\!\rfloor$. Again, we let

$\zeta(\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)=[p(v_{1},\dots,v_{n},(a_{1},t_{1}),\dots,(a_{m},t_{m}))]_{\mathsf{E}}$

and $w_{i}=0$ if $v_{i}=v$ else $w_{i}=v_{i}$. In the previous case, we showed
that $u$ is dead in $\lceil\\!\\!\lfloor\mu u~{}e\rceil\\!\\!\rfloor$, so we
begin by showing that $\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{s/v\\}=\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor$ for each $s\in Z$ such that $u$ is dead in $s$. We
have

$\displaystyle\zeta(\lceil\\!\\!\lfloor\mu u~{}e\rceil\\!\\!\rfloor\\{s/v\\})$
$\displaystyle=[p(w_{1},\dots,w_{n},(a_{1},t_{1}\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor/u\\}\\{s/v\\}),\dots,(a_{m},t_{m}\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor/u\\}\\{s/v\\}))]_{\mathsf{E}}$
$\displaystyle=[p(w_{1},\dots,w_{n},(a_{1},t_{1}\\{s/v\\}\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{s/v\\}/u\\}),\dots,$ $\displaystyle\hskip
113.81102pt(a_{m},t_{m}\\{s/v\\}\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{s/v\\}/u\\}))]_{\mathsf{E}}$ (Lemma C.3)
$\displaystyle=[p(v_{1},\dots,v_{n},(a_{1},t_{1}\\{s/v\\}),\dots,(a_{m},t_{m}\\{s/v\\}))]_{\mathsf{E}}\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{s/v\\}/\\!/u\\}$
$\displaystyle=\zeta(\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{s/v\\}/\\!/u\\}$ ($v$ dead in $\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor$)

Hence, $r=\lceil\\!\\!\lfloor\mu u~{}e\rceil\\!\\!\rfloor\\{s/v\\}$ solves the
behavioural differential equation defining $\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor$, so $\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor=\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{s/v\\}$. The desired result follows from the
following observation: Both $u$ and $v$ are clearly dead in
$\lceil\\!\\!\lfloor 0\rceil\\!\\!\rfloor$, so for arbitrary $s\in Z$ we have

$\displaystyle\lceil\\!\\!\lfloor\mu u~{}e\rceil\\!\\!\rfloor\\{s/v\\}$
$\displaystyle=\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
0\rceil\\!\\!\rfloor/v\\}\\{s/v\\}=\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
0\rceil\\!\\!\rfloor\\{s/v\\}/v\\}$ $\displaystyle=\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
0\rceil\\!\\!\rfloor/v\\}=\lceil\\!\\!\lfloor\mu u~{}e\rceil\\!\\!\rfloor$

It follows that $v$ is dead in $\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor$. ∎

######  Lemma C.8.

Let $e,f\in\mathtt{Exp}$ and $v\in V$. Assume that $v$ is not free in $f$, and
that no free variable of $f$ appears bound in $e$. Then $\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\}=\lceil\\!\\!\lfloor e[f/v]\rceil\\!\\!\rfloor$.

###### Proof.

We proceed by induction on $e$.

  * •

For the variable case, let $u\neq v$. There are cases to consider.

    * –

First, suppose $e=v$. We have $\zeta(\lceil\\!\\!\lfloor
v\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\})=\zeta(\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor)=\zeta(\lceil\\!\\!\lfloor v[f/v]\rceil\\!\\!\rfloor)$.

    * –

Now assume $e=u$. Here, we have $\zeta(\lceil\\!\\!\lfloor
u\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\})=\zeta(\lceil\\!\\!\lfloor
u\rceil\\!\\!\rfloor)=\zeta(\lceil\\!\\!\lfloor u[f/v]\rceil\\!\\!\rfloor)$.

  * •

For the inductive step, assume the result for $e$ and consider the process
term $ae$. We have $\zeta(\lceil\\!\\!\lfloor
ae\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\})=[(a,\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\})]_{\mathsf{E}}=[(a,\lceil\\!\\!\lfloor
e[f/v]\rceil\\!\\!\rfloor)]_{\mathsf{E}})=\zeta(\lceil\\!\\!\lfloor
ae[f/v]\rceil\\!\\!\rfloor)$.

  * •

Now consider $\sigma(e_{1},\dots,e_{n})$ for $e_{i}\in\mathtt{Exp}$, $i\leq
n$, and assume the result for $e_{1},\dots,e_{n}$. We have

$\displaystyle\zeta(\lceil\\!\\!\lfloor\sigma(e_{1},\dots,e_{n})\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\})$ $\displaystyle=\sigma(\zeta(\lceil\\!\\!\lfloor
e_{1}\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\}),\dots,\zeta(\lceil\\!\\!\lfloor
e_{n}\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor f\rceil\\!\\!\rfloor/v\\}))$
$\displaystyle=\sigma(\zeta(\lceil\\!\\!\lfloor
e_{1}[f/v]\rceil\\!\\!\rfloor),\dots,\zeta(\lceil\\!\\!\lfloor
e_{n}[f/v]\rceil\\!\\!\rfloor))$
$\displaystyle=\zeta(\lceil\\!\\!\lfloor\sigma(e_{1},\dots,e_{n})[f/v]\rceil\\!\\!\rfloor)$

  * •

Finally, assume the result for $e$ and consider $\mu u~{}e$. Since no free
variable of $f$ is bound in $\mu u~{}e$, $u$ in particular is not free in $f$.
By Lemma C.7, $u$ is therefore dead in $\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor$. Where $\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor=[p(v_{1},\dots,v_{n},(a_{1},t_{1}),\dots,(a_{m},t_{m}))]_{\mathsf{E}}$
and $w_{i}=0$ if $v_{i}=u$ else $w_{i}=v_{i}$, this leads to the computation

$\displaystyle\zeta(\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor f\rceil\\!\\!\rfloor/v\\})$
$\displaystyle=[p(w_{1},\dots,w_{n},(a_{1},t_{1}\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor/u\\}\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\}),\dots,(a_{m},t_{m}\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor/u\\}\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\}))]_{\mathsf{E}}$
$\displaystyle=[p(w_{1},\dots,w_{n},(a_{1},t_{1}\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\}\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\}/u\\}),\dots,$ $\displaystyle\hskip
113.81102pt(a_{m},t_{m}\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\}\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\}/u\\}))]_{\mathsf{E}}$ (Lemma C.3)
$\displaystyle=\zeta(\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\})\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\}/\\!/u\\}$ $\displaystyle=\zeta(\lceil\\!\\!\lfloor
e[f/v]\rceil\\!\\!\rfloor)\\{\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor/v\\}/\\!/u\\}$ (inductive hypothesis)

It follows that, $r=\lceil\\!\\!\lfloor\mu
u~{}e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor f\rceil\\!\\!\rfloor/v\\}$
satisfies the defining behavioural differential equation of
$\lceil\\!\\!\lfloor\mu u~{}(e[f/v])\rceil\\!\\!\rfloor$. It follows that
$\lceil\\!\\!\lfloor(\mu u~{}e)[f/v]\rceil\\!\\!\rfloor=\lceil\\!\\!\lfloor\mu
u~{}(e[f/v])\rceil\\!\\!\rfloor=\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor\\{f/v\\}$. ∎

The last two lemmas of this section show that guarded syntactic substitution
at the level of $\mathtt{Exp}$ plays well with guarded syntactic substitution
at the level of $B_{M}\mathtt{Exp}$.

######  Lemma C.9.

Let $v\in V$ and $e,g\in\mathtt{Exp}$. Assume that no free variable of $g$
appears bound in $e$. Then $\epsilon(e)[g/\\!/v]=\epsilon(e[g/\\!/v])$.

###### Proof.

By induction on $e$.

  * •

If $u\neq v$, then
$\epsilon(u)[g/\\!/v]=[u]_{\mathsf{E}}=\epsilon(u[g/\\!/v])$ since $v$ does
not appear in $u$. Otherwise,
$\epsilon(v)[g/\\!/v]=[0]_{\mathsf{E}}=\epsilon(v[g/\\!/v])$.

  * •

In the prefixing case, assume the result for $e$ and simply observe that
$(ae)[g/\\!/v]=ae[g/v]$. Hence,

$\epsilon(ae)[g/\\!/v]=[(a,e[g/v])]_{\mathsf{E}}=\epsilon(ae[g/v])=\epsilon((ae)[g/\\!/v])$

  * •

Now assume the result for $e_{1},\dots e_{n}$. We have

$\displaystyle\epsilon(\sigma(e_{1},\dots,e_{n}))[g/\\!/v]$
$\displaystyle=\sigma(\epsilon(e_{1})[g/\\!/v],\dots,\epsilon(e_{n})[g/\\!/v])=\sigma(\epsilon(e_{1}[g/\\!/v]),\dots,\epsilon(e_{n}[g/\\!/v]))$
$\displaystyle=\epsilon(\sigma(e_{1}[g/\\!/v],\dots,e_{n}[g/\\!/v]))=\epsilon(\sigma(e_{1},\dots,e_{n}))[g/\\!/v]$

  * •

In the recursion step, assume the result for $e$ and consider $\mu u~{}e$. In
particular, $u$ is not free in $g$. It follows that
$[g/\\!/v][g/\\!/v]=[g/\\!/v]$, that $(\mu u~{}e)[g/\\!/v]=\mu
u~{}(e[g/\\!/v])$, and that the operators $[g/\\!/v]$ and $[\mu
u~{}e[g/\\!/v]/\\!/u]$ commute. Thus,

$\displaystyle\epsilon(\mu u~{}e[g/\\!/v])$
$\displaystyle=\epsilon(e[g/\\!/v])[\mu
u~{}e[g/\\!/v]/\\!/u]=\epsilon(e)[g/\\!/v][\mu u~{}e[g/\\!/v]/\\!/u]$
$\displaystyle=\epsilon(e)[g/\\!/v][\mu u~{}e/\\!/u][g/\\!/v]=\epsilon(e)[\mu
u~{}e/\\!/u][g/\\!/v][g/\\!/v]=\epsilon(\mu u~{}e)[g/\\!/v]\qed$

######  Lemma C.10.

Let $v\in V$ and $e,g\in\mathtt{Exp}$. If $v$ is guarded in $e$ and no free
variable of $g$ appears bound in $e$, then
$\epsilon(e[g/v])=\epsilon(e)[g/\\!/v]$.

###### Proof.

Suppose $v$ is guarded in $e$. We proceed by induction on the construction of
$e$.

  * •

In the base case we only have to consider $u\neq v$. Here,
$\epsilon(u[g/v])=\epsilon(u)=[u]_{\mathsf{E}}=[u[g/\\!/v]]_{\mathsf{E}}=\epsilon(u)[g/\\!/v]$.

  * •

In the inductive step, assume the result for $e$ and consider $ae$. We have
$\epsilon(ae[g/v])=[(a,e[g/v])]_{\mathsf{E}}=[(a,e)]_{\mathsf{E}}[g/\\!/v]=\epsilon(e)[g/\\!/v]$
as desired.

  * •

In the branched case, assume the result for $e_{1},\dots,e_{n}$ and that $v$
is guarded in $e_{1},\dots,e_{n}$. We have

$\displaystyle\epsilon(\sigma(e_{1},\dots,e_{n})[g/v])$
$\displaystyle=\epsilon(\sigma(e_{1}[g/v],\dots,e_{n}[g/v]))=\sigma(\epsilon(e_{1}[g/v]),\dots,\epsilon(e_{n}[g/v]))$
$\displaystyle=\sigma(\epsilon(e_{1})[g/\\!/v],\dots,\epsilon(e_{n})[g/\\!/v]))=\sigma(\epsilon(e_{1}),\dots,\sigma(e_{n}))[g/\\!/v]$
$\displaystyle=\epsilon(\sigma(e_{1},\dots,e_{n}))[g/\\!/v]$

  * •

Now assume the result for $e$ and consider $\mu u~{}e$. If $v=u$, then we have
$\epsilon((\mu v~{}e)[g/v])=\epsilon(\mu v~{}e)=\epsilon(e)[\mu
v~{}e/\\!/v]=\epsilon(e)[\mu v~{}e/\\!/v][g/\\!/v]=\epsilon(\mu
v~{}e)[g/\\!/v]$. Otherwise, assume $v$ is guarded in $e$ and compute

$\displaystyle\epsilon(\mu u~{}e)[g/\\!/v]$ $\displaystyle=\epsilon(e)[\mu
u~{}e/\\!/u][g/\\!/v]=\epsilon(e)[g/\\!/v][\mu u~{}e[g/\\!/v]/\\!/u]$
$\displaystyle\stackrel{{\scriptstyle(\text{i.h.})}}{{\epsilon}}(e[g/v])[\mu
u~{}e[g/v]/\\!/u]=\epsilon(\mu u~{}e[g/v])$

Here, $e[g/\\!/v]=e[g/v]$ precisely because $v$ is guarded in $e$. ∎

##  Appendix D Proofs from Section 4

In this section, we aim to prove the following theorem, which states that the
operational and denotational semantics coincide.

See 4.1

The proof requires the following lemma.

######  Lemma D.1.

Let $p\in S^{*}(V+A\times\mathtt{Exp})$, $f\in\mathtt{Exp}$ and $v\in V$.
Assume no free variable of $g$ appears bound in any expression that appears in
$p$. Then

$B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([p]_{\mathsf{E}})\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\}=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([p]_{\mathsf{E}}[g/\\!/v])$

###### Proof.

We proceed by induction on $p$.

  * •

Suppose $p=u$.

    * –

If $u=v$, then we have

$B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([v]_{\mathsf{E}})\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\}=[v]_{\mathsf{E}}\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\}=[0]_{\mathsf{E}}=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([0]_{\mathsf{E}})=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([v]_{\mathsf{E}}[g/\\!/v])$

    * –

If $u\neq v$, then

$B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([u]_{\mathsf{E}})\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\}=[u]_{\mathsf{E}}\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\}=[u]_{\mathsf{E}}=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([u]_{\mathsf{E}})=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([u]_{\mathsf{E}}[g/\\!/v])$

  * •

Now suppose $p=(a,e)$ for some $e\in\mathtt{Exp}$. We have that
$B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([(a,e)]_{\mathsf{E}})\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\}=[(a,\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)]_{\mathsf{E}}\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\}=[(a,\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/v\\}]_{\mathsf{E}})$. By Lemma C.8,

$\displaystyle
B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([(a,e)]_{\mathsf{E}})\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\}$ $\displaystyle=[(a,\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/v\\}]_{\mathsf{E}})=[(a,\lceil\\!\\!\lfloor
e[g/v]\rceil\\!\\!\rfloor)]_{\mathsf{E}}$
$\displaystyle=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([(a,e[g/v])]_{\mathsf{E}})=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([(a,e)]_{\mathsf{E}}[g/\\!/v])$

  * •

Now assume the result for $p_{1},\dots,p_{n}\in S^{*}(V+A\times\mathtt{Exp})$
and suppose $p=\sigma(p_{1},\dots,p_{n})$. We have

$\displaystyle
B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([p]_{\mathsf{E}})\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\}$
$\displaystyle=\sigma(B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([p_{1}]_{\mathsf{E}}),\dots,B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([p_{n}]_{\mathsf{E}}))\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\}$
$\displaystyle=\sigma(B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([p_{1}]_{\mathsf{E}})\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\},\dots,B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([p_{n}]_{\mathsf{E}})\\{\lceil\\!\\!\lfloor
g\rceil\\!\\!\rfloor/\\!/v\\})$
$\displaystyle=\sigma(B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([p_{1}]_{\mathsf{E}}[g/\\!/v]),\dots,B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([p_{n}]_{\mathsf{E}}[g/\\!/v]))$
$\displaystyle=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([p]_{\mathsf{E}}[g/\\!/v])\qed$

###### Proof of Theorem 4.1..

We prove the desired property by showing that
$\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor$ is a $B_{M}$-coalgebra homomorphism
between $(\mathtt{Exp},\epsilon)$ and $(Z,\gamma)$. This amounts to showing
that
$\zeta\circ\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)\circ\epsilon$,
which establishes the commutativity of the lower square in the diagram below.

$\Sigma_{M}Exp$$\Sigma_{M}Z$$Exp$$Z$$B_{M}Exp$$B_{M}Z$$\Sigma_{M}\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor$$\alpha$$\cong$$\epsilon$$\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor$$\zeta$$\cong$$B_{M}\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor$$\gamma$

To this end, we show $\zeta(\lceil\\!\\!\lfloor
e\rceil\\!\\!\rfloor)=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(e))$
by induction on $e$.

  * •

In the base case, $e=v$, and

$\zeta(\lceil\\!\\!\lfloor
v\rceil\\!\\!\rfloor)=[v]_{\mathsf{E}}=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([v]_{\mathsf{E}})=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(v))$

  * •

Now assume the result for $f$ and let $e=af$. We have

$\zeta(\lceil\\!\\!\lfloor af\rceil\\!\\!\rfloor)=[(a,\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor)]_{\mathsf{E}}=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)([(a,f)]_{\mathsf{E}})=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(af))$

  * •

Next, assume the result for $e_{1},\dots,e_{n}$ and let
$e=\sigma(e_{1},\dots,e_{n})$. We have

$\displaystyle\zeta(\lceil\\!\\!\lfloor e\rceil\\!\\!\rfloor)$
$\displaystyle=\sigma(\zeta(\lceil\\!\\!\lfloor
e_{1}\rceil\\!\\!\rfloor),\dots,\zeta(\lceil\\!\\!\lfloor
e_{n}\rceil\\!\\!\rfloor))=\sigma(B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(e_{1})),\dots,B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(e_{n})))$
$\displaystyle=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\sigma(\epsilon(e_{1}),\dots,\epsilon(e_{n})))=B_{M}(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(e))$

  * •

Now assume the result for $f$ and let $e=\mu v~{}f$. We have

$\displaystyle\zeta(\lceil\\!\\!\lfloor\mu v~{}f\rceil\\!\\!\rfloor)$
$\displaystyle=\zeta(\lceil\\!\\!\lfloor
f\rceil\\!\\!\rfloor)\\{\lceil\\!\\!\lfloor\mu
v~{}f\rceil\\!\\!\rfloor/\\!/v\\}=B(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(f))\\{\lceil\\!\\!\lfloor\mu
v~{}f\rceil\\!\\!\rfloor/\\!/v\\}$
$\displaystyle=B(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(f)[\mu
v~{}f/\\!/v])$ (Lemma D.1)
$\displaystyle=B(\lceil\\!\\!\lfloor-\rceil\\!\\!\rfloor)(\epsilon(\mu
v~{}f))\qed$

##  Appendix E Proofs from Section 5

See 5.1

The proof of this lemma requires the following lemma.

######  Lemma E.1.

Let $v\in V$ and $g_{1},g_{2}\in\mathtt{Exp}$. If $g_{1}\equiv g_{2}$, then
for any term $p\in S^{*}(V+A\times\mathtt{Exp})$ we have

$B_{M}([-]_{\equiv})(p[g_{1}/\\!/v])=B_{M}([-]_{\equiv})(p[g_{2}/\\!/v])$

###### Proof.

By induction on the construction of $p$.

  * •

Suppose $p=u$. If $u\neq v$, then we have $u[g_{1}/\\!/v]=u=u[g_{2}/\\!/v]$,
because $v$ is not free in $u$. On the other hand, if $u=v$, then
$v[g_{i}/\\!/v]=0$ for $i=1,2$ by definition.

  * •

Now let $p=(a,e)$. We have

$B_{M}([-]_{\equiv})((a,e)[g_{i}/\\!/v])=B_{M}([-]_{\equiv})((a,e[g_{i}/v]))=[(a,[e[g_{i}/v]]_{\equiv})]_{\mathsf{E}}$

for $i=1,2$. Since $\equiv$ is a congruence, $e[g_{1}/v]\equiv e[g_{2}/v]$, so
indeed $(a,[e[g_{1}/v]]_{\equiv})=(a,[e[g_{2}/v]]_{\equiv})$ as desired.

  * •

In the branched case, assume the identity for $p_{1},\dots,p_{n}$ and compute

$\displaystyle
B_{M}([-]_{\equiv})(\epsilon(\sigma(p_{1},\dots,p_{n}))[g_{i}/\\!/v])$
$\displaystyle=B_{M}([-]_{\equiv})(\sigma(p_{1}[g_{i}/\\!/v],\dots,p_{n}[g_{i}/\\!/v]))$