emptyset degree leftmoon rightmoon fullmoon newmoon diameter bigtimes langle
rangle triangleright triangleleft not otherlangle otherrangle
othertriangleright othertriangleleft othernot otheremptyset Rupak Majumdar and
Alexandra Silva 2 35th International Conference on Concurrency Theory (CONCUR
2024) CONCUR 2024 CONCUR 2024 September 9–13, 2024 Calgary, Canada 311 31
Friedrich-Alexander-Universität Erlangen-Nürnberg,
Germanysergey.goncharov@fau.dehttps://orcid.org/0000-0001-6924-8766German
Research Foundation (DFG) project 501369690, Icelandic Research Fund project
228684-052 Reykjavik University, Iceland, and Tallinn University of
Technology, Estoniatarmo@ru.ishttps://orcid.org/0000-0002-1297-0579Icelandic
Research Fund project 228684-052 Sergey Goncharov, Tarmo Uustalu [500]Theory
of computation Categorical semantics [500]Theory of computation Axiomatic
semantics Full Versionhttps://arxiv.org/abs/2407.08688

# A Unifying Categorical View of Nondeterministic Iteration and Tests

Sergey Goncharov  Tarmo Uustalu

###### Abstract

We study Kleene iteration in the categorical context. A celebrated
completeness result by Kozen introduced Kleene algebra (with tests) as a
ubiquitous tool for lightweight reasoning about program equivalence, and yet,
numerous variants of it came along afterwards to answer the demand for more
refined flavors of semantics, such as stateful, concurrent, exceptional,
hybrid, branching time, etc. We detach _Kleene iteration_ from _Kleene
algebra_ and analyze it from the categorical perspective. The notion, we
arrive at is that of _Kleene-iteration category_ (with coproducts and tests),
which we show to be general and robust in the sense of compatibility with
programming language features, such as exceptions, store, concurrent
behaviour, etc. We attest the proposed notion w.r.t. various yardsticks, most
importantly, by characterizing the free model as a certain category of
(nondeterministic) _rational trees_.

###### keywords:

Kleene iteration, Elgot iteration, Kleene algebra, coalgebraic resumptions

##  1 Introduction

Axiomatizing notions of iteration both algebraically and categorically is a
well-established topic in computer science where two schools of thought can be
distinguished rather crisply: the first one is based on the inherently
nondeterministic _Kleene iteration_ , stemming from the seminal work of
Stephen Kleene [24] and deeply rooted in automata and formal language theory;
the second one stems from another seminal work – by Calvin Elgot [12] – and is
based on another notion of iteration, we now call _Elgot iteration_. The most
well-known instance of Kleene iteration is the one that is accommodated in the
algebra of regular expressions where $a^{\ast}$ represents $n$-fold
compositions $a\cdots a$ and $n$ nondeterministically ranges over all
naturals. More abstractly, Kleene iteration is an operation of the following
type:

$\displaystyle\textbf{}\leavevmode\nobreak\ \leavevmode\nobreak\ \frac{p\colon
X\to X}{p^{\ast}\colon X\to X}$

Intuitively, we think of $p$ as a program whose inputs and outputs range over
$X$, and of $p^{\ast}$ as a result of composing $p$ nondeterministically many
times with itself. Elgot iteration, in contrast, is agnostic to
nondeterminism, but crucially relies on the categorical notion of binary
coproduct, and thus can only be implemented in categorical or type-theoretic
setting. Concretely, the typing rule for Elgot iteration is

$\displaystyle\textbf{}\leavevmode\nobreak\ \leavevmode\nobreak\ \frac{p\colon
X\to Y+X}{p^{\dagger}\colon X\to Y}$ ($\dagger$)

That is, given a program that receives an input from $X$, and can output
either to $Y$ or to $X$, $p^{\dagger}$ self-composes $p$ precisely as long as
$p$ outputs to $X$.

A profound exploration of both versions of iteration and their axiomatizations
in the categorical context, more precisely, in the context of _Lavwere
theories_ , has been done by Bloom and Ésik in a series of papers and subsumed
in their monograph [6]. One outcome of this work is that in the context of
Lawvere theories, in presence of nondeterminism, Kleene iteration and Elgot
iteration are essentially equivalent – the ensuing theory was dubbed
_iteration grove theory_ [5]. The existing analysis still does not cover
certain aspects, which we expressly address in our present work, most
importantly, the following.

  * •

Lavwere theories are only very special categories, while iteration is a common
ingredient of semantic frameworks, which often involve it directly via an
ambient category with coproducts, and not via the associated Lavwere theory.

  * •

Previous results on the equivalence of Elgot iteration and Kleene iteration do
not address the connection between control mechanisms involved in both
paradigms: Elgot iteration fully relies on coproducts for making decisions
whether to continue or to end the loop, while Kleene iteration for the same
purpose uses an additional mechanism of _tests_ [26], which are specified
axiomatically and thus yield a higher degree of flexibility.

  * •

A key feature of Kleene iteration of Kleene algebra, are the quasi-equational
laws, which can be recast [16] to a form of the versatile and powerful
_uniformity principle_ (e.g. [39]). The latter is parameterized by a class of
well-behaved elements, which in Kleene algebra coincide with the algebra’s
entire carrier. However, in many situations, this class has to be restricted,
which calls for axiomatizing it, analogously to tests.

Here, we seek a fundamental, general and robust categorical notion of Kleene
iteration, which addresses these issues, is in accord with Elgot iteration and
the corresponding established laws for it (Elgot iteration operators that
satisfy these laws are called _Conway operators_). In doing so, we depart from
the laws of Kleene algebra, and relax them significantly. Answering the
question how to do this precisely and in a principled way is the main insight
of our work.

Let us dwell briefly on the closely related issues of generality and
robustness. The laws of Kleene algebra, as originally axiomatized by Kozen
[25], capture a very concrete style of semantics, mirrored in the
corresponding free model, which is the algebra of regular events, i.e. the
algebra of regular sets of strings over a finite alphabet of symbols, with
iteration rendered as a least fixpoint. Equations validated by this model are
thus shared by the whole class of Kleene algebras. By regarding Kleene algebra
terms as programs, the interpretation over the free model can be viewed as
_finite trace semantics_ of linear-time nondeterminism. A standard example of
properly more fine-grained – branching-time – nondeterminism is (bisimulation-
based) process algebra, which fails the Kleene algebra’s law of distributivity
from the left:

$\displaystyle p\mspace{4.0mu};\mspace{2.0mu}(q+r)=$
$\displaystyle\;p\mspace{4.0mu};\mspace{2.0mu}q+p\mspace{4.0mu};\mspace{2.0mu}r.$
(1)

Similarly, if we wanted to allow our programs to raise exceptions, the laws of
Kleene algebra would undesirably force all exceptions to be equal:

$\displaystyle\operatorname{\mathsf{raise}}e_{1}=\operatorname{\mathsf{raise}}e_{1}\mspace{4.0mu};\mspace{2.0mu}0=0=\operatorname{\mathsf{raise}}e_{2}\mspace{4.0mu};\mspace{2.0mu}0=\operatorname{\mathsf{raise}}e_{2}.$

Here, we combine the law $p\mspace{4.0mu};\mspace{2.0mu}0=0$ of Kleene algebra
with the equation
$\operatorname{\mathsf{raise}}_{i}\mspace{4.0mu};\mspace{2.0mu}p=\operatorname{\mathsf{raise}}_{i}$
that alludes to the common programming knowledge that raising an exception
exits the program instantly and discards any subsequent fragment $p$. The
resulting equality
$\operatorname{\mathsf{raise}}e_{1}=\operatorname{\mathsf{raise}}e_{2}$ states
that raising exception $e_{1}$ is indistinguishable from raising exception
$e_{2}$.

We can interpret these and similar examples as evidence that the axioms of
Kleene algebra are not sufficiently robust under extensions by programming
language features. More precisely, Kleene algebras can be scaled up to _Kleene
monads_ [18], and thus reconciled with Moggi’s approach to computational
effects [33]. An important ingredient of this approach are _monad
transformers_ , which allow for combining effects in a principled way. For
example, one uses the _exception monad transformer_ to canonically add
exception raising to a given monad. The above indicates that Kleene monads are
not robust under this transformer.

Finally, even if we accept all iteration-free implications of Kleene algebra,
these will not jointly entail the following identity:

$\displaystyle 1^{\ast}=1,$ (2)

which is however entailed by the Kleene algebra axioms. One setting where (2)
is undesirable is domain theory, which insists on distinguishing _deadlock_
from _divergence_ , in particular, (2) is failed by interpreting programs over
the _Plotkin powerdomain_ [36]. Intuitively, (2) states that, if a loop _may_
be exited, it _will_ eventually be exited, while failure of (2) would mean
that the left program _may_ diverge, while the right program _must_ converge,
and this need not be the same. Let us call the corresponding variant of Kleene
algebra, failing (2), _may-diverge Kleene algebra_. However, it is not a
priori clear how the axioms of may-diverge Kleene algebras must look like,
given that (2) is not a Kleene algebra axiom, but a consequence of the
assumption that Kleene iteration is a least fixpoint. Hence, in may-diverge
Kleene algebras Kleene iteration is not a least fixpoint (w.r.t. the order,
induced by $+$).

The notion we develop and present here is that of _Kleene-iteration category
(with tests) (KiC(T))_. It is designed to address the above issues and to
provide a uniform general and robust framework for Kleene iteration in a
category. We argue in various ways that KiC(T) is in a certain sense the most
basic practical notion of Kleene iteration, most importantly by characterizing
its free model, as a certain category of (nondeterministic) rational trees.

#### Related work

The (finite or $\omega$-complete) partially additive categories (PACs) by
Arbib and Manes [2] and the PACs with effects of Cho [8] are similar in spirit
to KiCs in that they combine structured homsets and coproducts, but
significantly more special; in particular they support relational, sets of
traces and similar semantics, but not branching time semantics. A PAC is a
category with coproducts enriched in partial commutative monoids (PMC). The
PMC structure of homsets and the coproducts are connected by axioms that make
the PMC structure unique. In an $\omega$-complete PAC, these axioms also
ensure the presence of an Elgot iteration operator, which is computed as a
least fixpoint. A PAC with effects comes with a designated effect algebra
object; this defines a wide subcategory of total morphisms, with coproducts
inherited from the whole category. Effectuses [23] achieve the same as PACs
with effects, but starting with a category of total morphisms and then adding
partial morphisms. Cockett [9] recently proposed a notion of iteration in a
category, based on restriction categories, and analogous to Elgot iteration
($\dagger$ ‣ 1), but avoiding binary coproducts in favor of a suitably
axiomatized notion of disjointness for morphisms.

In the strand of Kleene algebra, various proposals were made with utilitarian
motivations to weaken or modify the Kleene algebra laws, and thus to cope with
process algebra [14], branching behaviour [34], probability [30], statefulness
[22], graded semantics [15], without however aiming to identify the conceptual
core of Kleene iteration, which is our objective here. A recent move within
this tendency is to eliminate nondeterminism altogether, with _guarded Kleene
algebras_ [40], which replace nondeterministic choice and iteration with
conditionals and while-loops. This is somewhat related to our analysis of
tests and iteration via while-loops, but largely orthogonal to our main
objective to stick to Kleene iteration as nondeterministic operator in the
original sense. Our aim to reconcile Kleene algebra, (co)products and Elgot
iteration is rather close to that of Kozen and Mamouras [27].

Our characterization of the free KiCT in a way reframes the original Kozen’s
characterization of the free Kleene algebra [25]. We are not generalizing this
result though, essentially because we work in categories with coproducts,
while a true generalization would only be achieved via categories without any
extra structure (noting that algebras are single-object categories). This
distinction becomes particularly important in the context of branching time
semantics, which we also cover by allowing a controlled use of programs that
fail distributivity from the left (1). An axiomatization for such semantics
has been proposed by Milner [32] and was shown to be complete only recently
[21]. Again, we are not generalizing this result, since the definability
issues, known to be the main obstruction for completeness arguments there, are
not effective in presence of coproducts.

#### Plan of the paper

We review minimal notations and conventions from category theory in Section 2.
We then introduce idempotent grove and Kleene-Kozen categories in Section 3 to
start off. In Section 4, we formally compare two control mechanisms in
categories: decisions and tests. In Section 5, 6, we establish equivalent
presentations of nondeterministic iteration as Kleene iteration, as Elgot
iteration and as while-iteration. In Section 7 we construct a free model for
our notion of iteration, and then come to conclusions in Section 8.

##  2 Notations and Conventions

We assume familiarity with the basics of category theory [29, 3]. In a
category $\mathbf{C}$, $|\mathbf{C}|$ will denote the class of objects and
$\mathbf{C}(X,Y)$ will denote the set of morphisms from $X$ to $Y$. The
judgement $f\colon X\to Y$ will be regarded as an equivalent to
$f\in\mathbf{C}(X,Y)$ if $\mathbf{C}$ is clear from the context. We tend to
omit indexes at natural transformations for readability. A subcategory
$\mathbf{D}$ of $\mathbf{C}$ is called _wide_ if $|\mathbf{C}|=|\mathbf{D}|$.
We will use diagrammatic composition $\mspace{4.0mu};\mspace{2.0mu}$ of
morphisms throughout, i.e. given $f\colon X\to Y$ and $g\colon Y\to Z$,
$f\mspace{4.0mu};\mspace{2.0mu}g\colon X\to Z$. We will denote by $1_{X}$, or
simply $1$ the identity morphism on $X$.

#### Coproducts

In this paper, by calling $\mathbf{C}$ “a category with coproducts” we will
always mean that $\mathbf{C}$ has _selected binary coproducts_ , i.e. that a
bi-functor $\oplus\colon\mathbf{C}\times\mathbf{C}\to\mathbf{C}$ exists such
that $X\oplus Y$ is a coproduct of $X$ and $Y$. In such a category, we write
$\operatorname{\mathsf{in_{0}}}\colon X\to X\oplus Y$ and
$\operatorname{\mathsf{in_{1}}}\colon Y\to X\oplus Y$ for the left and right
coproduct injections correspondingly. We will occasionally condense
$\operatorname{\mathsf{in_{i}}}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{j}}}$
to $\operatorname{\mathsf{in_{i\,j}}}$ for the sake of succinctness.

#### Monads

A monad ${\bm{\mathsf{T}}}$ on $\mathbf{C}$ is determined by a _Kleisli
triple_ $(T,\eta,(-)^{\sharp})$, consisting of a map
$T\colon{|\mathbf{C}|\to|\mathbf{C}|}$, a family of morphisms $(\eta_{X}\colon
X\to TX)_{X\in|\mathbf{C}|}$ and _Kleisli lifting_ sending each $f\colon X\to
TY$ to $f^{\sharp}\colon TX\to TY$ and obeying _monad laws_ :

$\displaystyle\eta^{\sharp}=1,$
$\displaystyle\eta\mspace{4.0mu};\mspace{2.0mu}f^{\sharp}=f,$
$\displaystyle(g\mspace{4.0mu};\mspace{2.0mu}f^{\sharp})^{\sharp}=g^{\sharp}\mspace{4.0mu};\mspace{2.0mu}f^{\sharp}.$

It follows that $T$ extends to a functor, $\eta$ extends to a natural
transformation – _unit_ , ${\mu=1^{\sharp}}\colon TTX\to TX$ extends to a
natural transformation – _multiplication_ , and that $(T,\eta,\mu)$ is a monad
in the standard sense [29]. We will generally use blackboard capitals (such as
${\bm{\mathsf{T}}}$) to refer to monads and the corresponding Roman letters
(such as $T$) to refer to their functor parts. Morphisms of the form $f\colon
X\to TY$ are called _Kleisli morphisms_ and form the _Kleisli category_
$\mathbf{C}_{{\bm{\mathsf{T}}}}$ of ${\bm{\mathsf{T}}}$ under _Kleisli
composition_ $f,g\mapsto f\mspace{4.0mu};\mspace{2.0mu}g^{\sharp}$ with
identity $\eta$. If $\mathbf{C}$ has binary coproducts then so does
$\mathbf{C}_{\bm{\mathsf{T}}}$: the coproduct injections are Kleisli morphisms
of the form
$\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}\eta\colon X\to
T(X\oplus Y)$,
$\operatorname{\mathsf{in_{1}}}\mspace{4.0mu};\mspace{2.0mu}\eta\colon Y\to
T(X\oplus Y)$.

#### Coalgebras

Given an endofunctor $F\colon\mathbf{C}\to\mathbf{C}$, a pair
$(X\in|\mathbf{C}|,c\colon X\to FX)$ is called an $F$-coalgebra. Coalgebras
form a category under the following notion of morphism: $h\colon X\to
X^{\prime}$ is a morphism from $(X,c)$ to $(X^{\prime},c^{\prime})$ if
$h\mspace{4.0mu};\mspace{2.0mu}c^{\prime}=c\mspace{4.0mu};\mspace{2.0mu}Fh$. A
terminal object in this category is called a _final coalgebra_. We reserve the
notation $(\nu F,\mathsf{out})$ for a selected final coalgebra if it exists. A
well-known fact (Lambek’s lemma) is that $\mathsf{out}$ is an isomorphism.

For a coalgebra $(X,c\colon X\to FX)$ on $\mathbf{Set}$ a relation
$\mathcal{B}\subseteq X\times X$ is a _(coalgebraic) bisimulation_ if it
extends to a coalgebra $(\mathcal{B},b\colon\mathcal{B}\to F\mathcal{B})$,
such that the left and the right projections from $\mathcal{B}$ to $X$ are
coalgebra morphisms; $x\in X$ and $y\in X$ are _bisimilar_ if
$x\mathrel{\mathcal{B}}y$ for some bisimulation $\mathcal{B}$; the coalgebra
$(X,c\colon X\to FX)$ is _strongly extensional_ [41] if bisimilarity entails
equality. Final coalgebras are the primary example of strongly extensional
coalgebras.

##  3 Idempotent Grove and Kleene-Kozen Categories

A monoid is precisely a single-object category. Various algebraic structures
extending monoids can be generalized to categories along this basic
observation (e.g. a group is a single-object groupoid, a quantale is a single-
object quantaloid, etc.). In this section, we consider two classes of
categories for nondeterminism and Kleene iteration, which demonstrate our
principled categorical approach of working with algebraic structures.

######  Definition 3.1 (Idempotent Grove Category, cf. [4, 5]).

Let us call a category $\mathbf{C}$ an _idempotent grove category_ if the hom-
sets of $\mathbf{C}(X,Y)$ are equipped with the structure $(0,+)$ of bounded
join-semilattice such that, for all $p\in\mathbf{C}(Y,Z)$ and
$q,r\in\mathbf{C}(X,Y)$,

$\displaystyle\qquad\qquad 0\mspace{4.0mu};\mspace{2.0mu}p=$
$\displaystyle\;0,$ $\displaystyle(q+r)\mspace{4.0mu};\mspace{2.0mu}p=$
$\displaystyle\;q\mspace{4.0mu};\mspace{2.0mu}p+r\mspace{4.0mu};\mspace{2.0mu}p.$
(3) In such a category, we call a morphism $p\in\mathbf{C}(X,Y)$ _linear_ if
it satisfies, for all $q,r\in\mathbf{C}(Y,Z)$, $\displaystyle\qquad\qquad
p\mspace{4.0mu};\mspace{2.0mu}0=$ $\displaystyle\;0,$ $\displaystyle
p\mspace{4.0mu};\mspace{2.0mu}(q+r)=$
$\displaystyle\;p\mspace{4.0mu};\mspace{2.0mu}q+p\mspace{4.0mu};\mspace{2.0mu}r.$
(4)

An _idempotent grove category with coproducts_ is an idempotent grove category
with selected binary coproducts and with $\operatorname{\mathsf{in_{0}}}$ and
$\operatorname{\mathsf{in_{1}}}$ linear.

Given $p,q\in\mathbf{C}(X,Y)$, let $p\leq q$ if $p+q=q$. This yields a partial
order with $0$ as the bottom element, and morphism composition is monotone on
the left, while linear morphisms are additionally monotone on the right. The
class of all linear morphisms of an idempotent grove category thus forms a
sub-category enriched in bounded join-semilattices (equivalently: commutative
and idempotent monoids) – thus, an idempotent grove category where all
morphisms are linear is an enriched category. However, we are interested in
categories where not all morphisms are linear. An instructive example is as
follows.

######  Example 3.2 (Synchronization Trees).

Let $A$ be some non-empty fixed set of _labels_ , and let
$TX=\nu\gamma.\,{\mathcal{P}}_{\omega_{1}}(X\oplus A\times\gamma)$ where
${\mathcal{P}}_{\omega_{1}}$ is the countable powerset functor. By
generalities [42], $T$ extends to a monad ${\bm{\mathsf{T}}}$ on
$\mathbf{Set}$. The elements of $TX$ can be characterized as  _countably-
branching strongly extensional synchronization trees with exit labels in $X$_.
Synchronization trees have originally been introduced by Milner [31] as
denotations of process algebra terms, and subsequently generalized to infinite
branching and to explicit exit labels (e.g. [1]). A generic element $t\in TX$
can be more explicitly represented using the following syntax:

$\displaystyle t=\sum_{i\in I}a_{i}.\,t_{i}+\sum_{i\in J}x_{i}$

where $I$ and $J$ are at most countable, the $a_{i}$ range over $A$, the
$t_{i}$ range over $TX$, and $x_{i}$ range over $X$. The involved summation
operators $\sum_{i\in I}$ are considered modulo countable versions of
associativity, commutativity and idempotence, and
$0=\sum_{i\in\emptyset}t_{i}$ and $t_{1}+t_{2}=\sum_{i\in\\{1,2\\}}t_{i}$.

Recall that strong extensionality means that bisimilar elements are equal
[41]. The Kleisli category of ${{\bm{\mathsf{T}}}}$ is idempotent grove with
$0$ and $+$ inherited from ${\mathcal{P}}_{\omega_{1}}$ and ensuring (3)
automatically. It is easy to see that linear morphisms are precisely those
that do not involve actions.

A straightforward way to add a Kleene iteration operator to a category is as
follows.

######  Definition 3.3 (Kleene-Kozen Category [16]).

An idempotent grove category $\mathbf{C}$ is a _Kleene-Kozen category_ if all
morphisms of $\mathbf{C}$ are linear and there is a _Kleene iteration_
operator
$(\operatorname{-\\!-})^{\ast}\colon\mathbf{C}(X,X)\to\mathbf{C}(X,X)$ such
that, for any $p\colon X\to X$, $q\colon Y\to X$ and ${r\colon X\to Z}$, the
morphism $q\mspace{4.0mu};\mspace{2.0mu}p^{\ast}$ is the least (pre-)fixpoint
of $q+(\operatorname{-\\!-})\mspace{4.0mu};\mspace{2.0mu}p$ and the morphism
$p^{\ast}\mspace{4.0mu};\mspace{2.0mu}r$ is the least (pre-)fixpoint of
$r+p\mspace{4.0mu};\mspace{2.0mu}(\operatorname{-\\!-})$.

It is known [16] that Kleene algebra is precisely a single-object Kleene-Kozen
category.

In idempotent grove categories with coproducts, the following property is a
direct consequence of linearity of $\operatorname{\mathsf{in_{0}}}$,
$\operatorname{\mathsf{in_{1}}}$, and will be used extensively throughout.

######  Proposition 3.4.

In idempotent grove categories with coproducts,
$[p,q]+[p^{\prime},q^{\prime}]={[p+p^{\prime},q+q^{\prime}]}$.

##  4 Decisions and Tests in Category

We proceed to compare two mechanisms for modeling control in categories:
_decisions_ and _tests_. The first one is inherently categorical, and requires
coproducts. The second one needs no coproducts, but requires nondeterminism.
The latter one is directly inspired by tests of the Kleene algebra with tests
[26]. We will show that tests and decisions are in a suitable sense
equivalent, when it comes to modeling control that satisfies Boolean algebra
laws.

######  Definition 4.1 (Decisions [10, 16]).

In a category $\mathbf{C}$ with binary coproducts, we call morphisms from
$\mathbf{C}(X,X\oplus X)$ _decisions_.

We consider the following operations on decisions, modeling truth values and
logical connectives:
$\operatorname{\mathsf{t\kern-0.45ptt}}=\operatorname{\mathsf{in_{1}}}$
(true),
$\operatorname{\mathsf{f\kern-0.78ptf}}=\operatorname{\mathsf{in_{0}}}$
(false),
$\mathrel{\texttt{{\raisebox{2.15277pt}{\,\texttildelow}}}}\kern-1.5ptd=d\mspace{4.0mu};\mspace{2.0mu}[\operatorname{\mathsf{in_{1}}},\operatorname{\mathsf{in_{0}}}]$
(negation),
$d\mathrel{\texttt{|\kern-2.95pt|}}e=d\mspace{4.0mu};\mspace{2.0mu}[e,\operatorname{\mathsf{in_{1}}}]$
(disjunction),
$d\mathrel{\texttt{\&\kern-0.5pt\&}}e=d\mspace{4.0mu};\mspace{2.0mu}[\operatorname{\mathsf{in_{0}}},e]$
(conjunction). Even without constraining decisions in any way, certain logical
properties can be established, e.g. (not necessarily commutative or
idempotent) monoidal structures
$(\operatorname{\mathsf{f\kern-0.78ptf}},\mathrel{\texttt{|\kern-2.95pt|}})$,
$(\operatorname{\mathsf{t\kern-0.45ptt}},\mathrel{\texttt{\&\kern-0.5pt\&}})$,
involutivity of
$\mathrel{\texttt{{\raisebox{2.15277pt}{\,\texttildelow}}}}\kern-1.5pt$, “de
Morgan laws”
$\mathrel{\texttt{{\raisebox{2.15277pt}{\,\texttildelow}}}}\kern-1.5pt(d\mathrel{\texttt{|\kern-2.95pt|}}e)=\mathrel{\texttt{{\raisebox{2.15277pt}{\,\texttildelow}}}}\kern-1.5ptd\mathrel{\texttt{\&\kern-0.5pt\&}}\mathrel{\texttt{{\raisebox{2.15277pt}{\,\texttildelow}}}}\kern-1.5pte$,
$\mathrel{\texttt{{\raisebox{2.15277pt}{\,\texttildelow}}}}\kern-1.5pt(d\mathrel{\texttt{\&\kern-0.5pt\&}}e)=\mathrel{\texttt{{\raisebox{2.15277pt}{\,\texttildelow}}}}\kern-1.5ptd\mathrel{\texttt{|\kern-2.95pt|}}\mathrel{\texttt{{\raisebox{2.15277pt}{\,\texttildelow}}}}\kern-1.5pte$,
and the laws
$\operatorname{\mathsf{t\kern-0.45ptt}}\mathrel{\texttt{|\kern-2.95pt|}}d=\operatorname{\mathsf{t\kern-0.45ptt}}$,
$\operatorname{\mathsf{f\kern-0.78ptf}}\mathrel{\texttt{\&\kern-0.5pt\&}}d=\operatorname{\mathsf{f\kern-0.78ptf}}$.

Given $d\in\mathbf{C}(X,X\oplus X)$ and $p,q\in\mathbf{C}(X,Y)$, let

$\displaystyle\operatorname{\mathsf{\underline{if}}}\mathbin{}d\operatorname{\mathsf{\underline{then}}}\mathbin{}p\operatorname{\mathsf{\underline{else}}}\mathbin{\,}q=d\mspace{4.0mu};\mspace{2.0mu}[q,p].$
(5)

######  Definition 4.2 (Tests).

Given an idempotent grove category $\mathbf{C}$, we call a family of linear
morphisms
$\mathbf{C}^{?}={(\mathbf{C}^{?}(X)\subseteq\mathbf{C}(X,X))_{X\in|\mathbf{C}|}}$
_tests_ if every $\mathbf{C}^{?}(X)$ forms a Boolean algebra under
$\mspace{4.0mu};\mspace{2.0mu}$ as conjunction and $+$ as disjunction.

It follows that $1\in\mathbf{C}^{?}(X)$ and $0\in\mathbf{C}^{?}(X)$
correspondingly are the top and bottom elements of $\mathbf{C}^{?}(X)$. Given
$b\in\mathbf{C}^{?}(X)$, $p,q\in\mathbf{C}(X,Y)$, let

$\displaystyle\operatorname{\mathsf{if}}\mathbin{}b\operatorname{\mathsf{then}}\mathbin{}p\operatorname{\mathsf{else}}\mathbin{}q=b\mspace{4.0mu};\mspace{2.0mu}p+\bar{b}\mspace{4.0mu};\mspace{2.0mu}q.$
(6)

In an idempotent grove category $\mathbf{C}$ with coproducts and tests
$\mathbf{C}^{?}$, let $?\colon\mathbf{C}(X,X\oplus X)\to\mathbf{C}^{?}(X)$ be
the morphism $d?=d\mspace{4.0mu};\mspace{2.0mu}[0,1].$

######  Proposition 4.3.

Let $\mathbf{C}$ be an idempotent grove category with coproducts. If a
decision $d$ is linear, then, for all $p$ and $q$, we have
$\operatorname{\mathsf{\underline{if}}}\mathbin{}d\operatorname{\mathsf{\underline{then}}}\mathbin{}p\operatorname{\mathsf{\underline{else}}}\mathbin{\,}q=\operatorname{\mathsf{if}}\mathbin{}d?\operatorname{\mathsf{then}}\mathbin{}p\operatorname{\mathsf{else}}\mathbin{}q$.

Let us say that a pair $(b,c)\in\mathbf{C}(X,X)\times\mathbf{C}(X,X)$
satisfies _(the law of) contradiction_ if $b\mspace{4.0mu};\mspace{2.0mu}c=0$,
and that it satisfies _(the law of) excluded middle_ if $b+c=1$. The following
characterization is instructive.

######  Proposition 4.4.

Given an idempotent grove category $\mathbf{C}$, a family of linear morphisms
$\mathbf{C}^{?}={(\mathbf{C}^{?}(X)\subseteq\mathbf{C}(X,X))_{X\in|\mathbf{C}|}}$
forms tests for $\mathbf{C}$ iff, for every $b\in\mathbf{C}^{?}$, there is
$\bar{b}\in\mathbf{C}^{?}$ such that $(b,\bar{b})$ satisfies contradiction and
excluded middle.

Note that the smallest choice of tests in $\mathbf{C}$ is
$\mathbf{C}^{?}(X)=\\{0,1\\}$. We proceed to characterize the smallest
possible choice of tests, sufficient for modeling control.

######  Definition 4.5 (Expressive Tests).

We call the tests $\mathbf{C}^{?}$ _expressive_ if every $\mathbf{C}^{?}(X)$
contains $[\operatorname{\mathsf{in_{0}}},0]$ whenever $X=X_{1}\oplus X_{2}$.

######  Lemma 4.6.

The smallest expressive family of tests always exists and is obtained by
closing tests of the form $0$, $1$, $[\operatorname{\mathsf{in_{0}}},0]$, and
$[0,\operatorname{\mathsf{in_{1}}}]$ under $+$ and
$\mspace{4.0mu};\mspace{2.0mu}$.

In the sequel, we will use the notation $\top$, $\bot$, $\land$, $\lor$ for
tests, synonymously to $1$, $0$, $\mspace{4.0mu};\mspace{2.0mu}$, $+$ to
emphasize their logical character.

######  Lemma 4.7.

Let $\mathbf{C}^{?}$ be tests in an idempotent grove category $\mathbf{C}$
with binary coproducts.

  1. 1.

The morphisms
$\mathinner{\raisebox{-1.0pt}{\scalebox{1.35}{$\diamond$}}}\colon\mathbf{C}^{?}(X)\to\mathbf{C}(X,X\oplus
X)$, ${?\colon\mathbf{C}(X,X\oplus X)\to\mathbf{C}^{?}(X)}$ defined by
$\mathinner{\raisebox{-1.0pt}{\scalebox{1.35}{$\diamond$}}}b=\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}$,
$d?=d\mspace{4.0mu};\mspace{2.0mu}[0,1]$ form a retraction.

  2. 2.

Every morphism $d$ in the image of
$\mathinner{\raisebox{-1.0pt}{\scalebox{1.35}{$\diamond$}}}$ is linear.
Moreover, we have $d\mspace{4.0mu};\mspace{2.0mu}\nabla=1$,
$d=d\mathrel{\texttt{\&\kern-0.5pt\&}}d$, and
$d=d\mathrel{\texttt{|\kern-2.95pt|}}d$.

  3. 3.

For all $e$ and $d$ in the image of
$\mathinner{\raisebox{-1.0pt}{\scalebox{1.35}{$\diamond$}}}$, it holds that
$(e\mathrel{\texttt{|\kern-2.95pt|}}d)?=e?\lor d?$,
$(e\mathrel{\texttt{\&\kern-0.5pt\&}}d)?=e?\land d?$, and
$(\mathrel{\texttt{{\raisebox{2.15277pt}{\,\texttildelow}}}}\kern-1.5ptd)?=\overline{d?}$.

4.7 indicates that in presence of coproducts and with linear coproduct
injections, instead of Boolean algebras on subsets of $\mathbf{C}(X,X)$, one
can equivalently work with Boolean algebras on subsets of
$\mathbf{C}(X,X\oplus X)$.

We conclude this section by an illustration that varying tests, in particular,
going beyond smallest expressive tests is practically advantageous.

######  Example 4.8.

Consider the _nondeterministic state monad_ ${\bm{\mathsf{T}}}$ with
$TX={\mathcal{P}}(S\times X)^{S}$ on $\mathbf{Set}$, where $S$ is a fixed
_global store_ , which the programs, represented by Kleisli morphisms of
${\bm{\mathsf{T}}}$ are allowed to read and modify. Morphisms of the Kleisli
category $\mathbf{Set}_{{\bm{\mathsf{T}}}}$ are equivalently (by uncurrying)
maps of the form $p\colon S\times X\to{\mathcal{P}}(S\times Y)$, meaning that
$\mathbf{Set}_{{\bm{\mathsf{T}}}}$ is equivalent to a full subcategory of
$\mathbf{Set}_{{\mathcal{P}}}$, from which $\mathbf{Set}_{{\bm{\mathsf{T}}}}$
inherits the structure of an idempotent grove category. The tests identified
in 4.6 are those maps $b\colon S\times X\to{\mathcal{P}}(S\times X)$ that are
determined by decompositions $X=X_{1}\oplus X_{2}$, in particular, they can
neither read nor modify the store. In practice, only the second is regarded as
undesirable (and indeed would break commutativity of tests), while reading is
typically allowed. This leads to a more permissive notion of tests, as those
that are determined by the decompositions $S\times X=X_{1}\oplus X_{2}$.

$\displaystyle\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}[p,q]=p\qquad\operatorname{\mathsf{in_{1}}}\mspace{4.0mu};\mspace{2.0mu}[p,q]=q\qquad[\operatorname{\mathsf{in_{0}}},\operatorname{\mathsf{in_{1}}}]=1\qquad[p,q]\mspace{4.0mu};\mspace{2.0mu}r=[p\mspace{4.0mu};\mspace{2.0mu}r,q\mspace{4.0mu};\mspace{2.0mu}r]$
$\displaystyle 0+p=p\qquad p+p=p\qquad p+q=q+p\qquad(p+q)+r=p+(q+r)$
$\displaystyle
0\mspace{4.0mu};\mspace{2.0mu}p=0\qquad(q+r)\mspace{4.0mu};\mspace{2.0mu}p=q\mspace{4.0mu};\mspace{2.0mu}p+r\mspace{4.0mu};\mspace{2.0mu}p\qquad
u\mspace{4.0mu};\mspace{2.0mu}0=0\qquad
u\mspace{4.0mu};\mspace{2.0mu}(p+q)=u\mspace{4.0mu};\mspace{2.0mu}p+u\mspace{4.0mu};\mspace{2.0mu}q$
$\displaystyle(\text{{$\ast$-Fix}})\leavevmode\nobreak\ \leavevmode\nobreak\
p^{\ast}=1+p\mspace{4.0mu};\mspace{2.0mu}p^{\ast}\quad(\text{{$\ast$-Sum}})\leavevmode\nobreak\
\leavevmode\nobreak\
(p+q)^{\ast}=p^{\ast}\mspace{4.0mu};\mspace{2.0mu}(q\mspace{4.0mu};\mspace{2.0mu}p^{\ast})^{\ast}\quad(\text{{$\ast$-Uni}})\leavevmode\nobreak\
\leavevmode\nobreak\ \vbox{
$u\mspace{4.0mu};\mspace{2.0mu}p^{\ast}=q^{\ast}\mspace{4.0mu};\mspace{2.0mu}uu\mspace{4.0mu};\mspace{2.0mu}p=q\mspace{4.0mu};\mspace{2.0mu}u$}$

Figure 1: Axioms of KiCs, including binary coproducts ($p,q,r$ range over
$\mathbf{C}$, $u$ ranges over
$\accentset{\rule{3.46501pt}{0.6pt}}{\mathbf{C}}$).

##  5 Kleene Iteration, Categorically

We now can introduce our central definition by extending idempotent grove
categories with a selected class of linear morphisms, called _tame morphisms_
, and with Kleene iteration. Crucially, we assume the ambient category
$\mathbf{C}$ to have coproducts as a necessary ingredient. Finding a general
definition, not relying on coproducts, presently remains open.

######  Definition 5.1 (KiC(T)).

We call a tuple $(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$
a _Kleene-iteration category (KiC)_ if

  1. 1.

$\mathbf{C}$ is an idempotent grove category with coproducts;

  2. 2.

$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ is a wide subcategory of
$\mathbf{C}$, whose morphisms we call _tame_ such that

     * •

$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ has coproducts strictly
preserved by the inclusion to $\mathbf{C}$;

     * •

the morphisms of $\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ are all
linear;

  3. 3.

for every $X\in|\mathbf{C}|$, there is a _Kleene iteration_ operator
$(\operatorname{-\\!-})^{\ast}\colon\mathbf{C}(X,X)\to\mathbf{C}(X,X)$ such
that the laws $\ast$-Fix, $\ast$-Sum and $\ast$-Uni in Figure 1, with $u$
ranging over $\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$, are satisfied.

A functor
$F\colon(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})\to(\mathbf{D},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{D}})$
between KiCs is a coproduct preserving functor
${F\colon\mathbf{C}\to\mathbf{D}}$ such that $F0=0$, $F(q+r)=Fq+Fr$ and
$Fp^{\ast}=(Fp)^{\ast}$ for all $q,r\in\mathbf{C}(X,Y)$,
$p\in\mathbf{C}(X,X)$, and
$Fp\in\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{D}}(FX,FY)$ for all
$p\in\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}(X,Y)$.

A KiC $(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$ equipped
with a choice of tests $\mathbf{C}^{?}$ in
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ we call a _KiCT_ (=KiC with
tests). Correspondingly, functors between KiCTs are additionally required to
send tests to tests.

It transpires from the definition that the role of tameness is to limit the
power of the uniformity rule $\ast$-Uni. The principal case for
$\mathbf{C}\neq\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ is 3.2. As we
see later (5.13), this yields a KiC. More generally, unless we restrict
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ to programs that satisfy the
linearity laws (4), the uniformity principle $\ast$-Uni would tend to be
unsound. Very roughly, uniformity is some infinitary form of distributivity
from the left and it fails for programs that fail the standard left
distributivity. This phenomenon is expected to occur for other flavors of
concurrent semantics: as long as $\mathbf{C}$ admits morphisms that fail (4),
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ would have to be properly
smaller than $\mathbf{C}$. Apart from concurrency, if
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ models a language with
exceptions, those must be excluded from
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$, for otherwise uniformity
would again become unsound.

If we demand all morphisms to be tame, we will obtain a notion very close to
that of Kleene-Kozen category (3.3).

######  Definition 5.2 ($\ast$-Idempotence).

A KiC is _$\ast$ -idempotent_ if it satisfies (2).

######  Proposition 5.3.

A category $\mathbf{C}$ is Kleene-Kozen iff $(\mathbf{C},\mathbf{C})$ is a
$\ast$-idempotent KiC.

######  Proof 5.4.

As shown previously [16], $\mathbf{C}$ is a Kleene-Kozen category iff

  1. 1.

$\mathbf{C}$ is enriched over bounded join-semilattices and strict join-
preserving morphisms;

  2. 2.

there is an operator
$(\operatorname{-\\!-})^{\ast}\colon\mathbf{C}(X,X)\to\mathbf{C}(X,X)$ such
that

    1. (a)

$p^{\ast}=1+p\mspace{4.0mu};\mspace{2.0mu}p^{\ast}$;

    2. (b)

$1^{\ast}=1$;

    3. (c)

$p^{\ast}=(p+1)^{\ast}$;

    4. (d)

$u\mspace{4.0mu};\mspace{2.0mu}p=q\mspace{4.0mu};\mspace{2.0mu}u$ implies
$u\mspace{4.0mu};\mspace{2.0mu}p^{\ast}=q^{\ast}\mspace{4.0mu};\mspace{2.0mu}u$.

This yields sufficiency by noting that (1) states precisely that all morphisms
in $\mathbf{C}$ are linear. To show necessity, it suffices to obtain (2.c)
from the assumptions that $(\mathbf{C},\mathbf{C})$ is a $\ast$-idempotent KiC
and that all morphisms in $\mathbf{C}$ are linear. Indeed, we have
$(p+1)^{\ast}=1^{\ast}\mspace{4.0mu};\mspace{2.0mu}(p\mspace{4.0mu};\mspace{2.0mu}1^{\ast})^{\ast}=p^{\ast}$.∎

KiCs thus deviate from Kleene algebras precisely in four respects:

  1. 1.

by generalizing from monoids to categories,

  2. 2.

by allowing non-linear morphisms,

  3. 3.

by dropping $\ast$-idempotence, and

  4. 4.

by requiring binary coproducts.

######  Example 5.5.

The axiom $\ast$-Sum, included in 5.1, is one of the classical _Conway
identities_. The other one
$(p\mspace{4.0mu};\mspace{2.0mu}q)^{\ast}=1+p\mspace{4.0mu};\mspace{2.0mu}(q\mspace{4.0mu};\mspace{2.0mu}p)^{\ast}\mspace{4.0mu};\mspace{2.0mu}q$
is derivable if $\mathbf{C}=\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$,
e.g. in Kleene-Kozen categories. Indeed,
$q\mspace{4.0mu};\mspace{2.0mu}p\mspace{4.0mu};\mspace{2.0mu}q=q\mspace{4.0mu};\mspace{2.0mu}p\mspace{4.0mu};\mspace{2.0mu}q$
entails
$q\mspace{4.0mu};\mspace{2.0mu}(p\mspace{4.0mu};\mspace{2.0mu}q)^{\ast}=(q\mspace{4.0mu};\mspace{2.0mu}p)^{\ast}\mspace{4.0mu};\mspace{2.0mu}q$
by $\ast$-Uni, and using $\ast$-Fix,
$(p\mspace{4.0mu};\mspace{2.0mu}q)^{\ast}=1+p\mspace{4.0mu};\mspace{2.0mu}q\mspace{4.0mu};\mspace{2.0mu}(p\mspace{4.0mu};\mspace{2.0mu}q)^{\ast}=1+p\mspace{4.0mu};\mspace{2.0mu}(q\mspace{4.0mu};\mspace{2.0mu}p)^{\ast}\mspace{4.0mu};\mspace{2.0mu}q$.

Clearly, this argument remains valid with only $q$ being tame, but otherwise
the requisite identity is not provable.

It may not be obvious why the requirement to support binary coproducts is part
of 5.1, given that the axioms of iteration do not involve them. The reason is
that certain identities that also do not involve coproducts are only derivable
in their presence.

######  Example 5.6.

The identity $p^{\ast}=(p\mspace{4.0mu};\mspace{2.0mu}(1+p))^{\ast}$ holds in
any KiC.

A standard way to instantiate 5.1 is to start with a category $\mathbf{V}$
with coproducts, and a monad ${\bm{\mathsf{T}}}$ on it, and take
$\mathbf{C}=\mathbf{V}_{{\bm{\mathsf{T}}}}$,
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}=\mathbf{V}$ or, possibly,
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}=\mathbf{V}_{{\bm{\mathsf{T}}}}$.
The monad must support nondeterminism and Kleene iteration so that the axioms
of KiC are satisfied. Consider a class of Kleene-Kozen categories that arise
in this way.

######  Example 5.7.

Let $Q$ be a unital quantale, and let $TX=Q^{X}$ for every set $X$. Then $T$
extends to a monad on $\mathbf{Set}$ as follows: $\eta(x)(x)=1$,
$\eta(x)(y)=\bot$ if $x\neq y$, and

$(p\colon X\to Q^{Y})^{\sharp}(f\colon X\to Q)(y\in Y)=\bigvee_{x\in
X}p(x)(y)\cdot f(x).$

We obtain a Kleene-Kozen structure in $\mathbf{Set}_{{\bm{\mathsf{T}}}}$ as
follows:

  * •

$0\colon X\to Q^{Y}$ sends $x$ to $\lambda y.\,\bot$;

  * •

$p+q\colon X\to Q^{Y}$ sends $x$ to $\lambda y.\,p(x)(y)\lor q(x)(y)$;

  * •

$p^{\ast}\colon X\to Q^{X}$ is the least fixpoint of the map $q\mapsto
1+q\mspace{4.0mu};\mspace{2.0mu}p$.

This construction restricts to $Q^{X}_{\omega_{1}}=\\{f\colon X\to
Q\mid|\operatorname{\mathsf{supp}}f|\leq\omega\\}$ where
${\operatorname{\mathsf{supp}}f}$ is the set of those $x\in X$, for which
$f(x)\neq 0$. Thus, e.g. the Kleisli categories of the powerset monad
${\mathcal{P}}$ and the countable powerset monad ${\mathcal{P}}_{\omega_{1}}$
are Kleene-Kozen.

For a contrast, consider a similar construction that yields a KiC, which is
not Kleene-Kozen.

######  Example 5.8.

Let $Q=\\{0,1,\infty\\}$ be the complete lattice under the ordering
$0<1<\infty$, and let us define commutative binary multiplication as follows:
$0\cdot x=0$, $1\cdot x=x$ and $\infty\cdot\infty=\infty$. This turns $Q$ into
a unital quantale, hence an idempotent semiring, whose binary summation $+$ is
binary join. Next, define infinite summation with the formula

$\displaystyle\sum_{i\in I}x_{i}=\begin{cases}\bigvee_{i\in
I^{\prime}}x_{i},&\text{if $I^{\prime}=\\{i\in I\mid x_{i}>0\\}$ is finite}\\\
\infty,&\text{otherwise}\end{cases}$

This makes $Q$ into a _complete semiring_ [11]. Let us define the monad
$\mathcal{R}$ and the idempotent grove structure on
$\mathbf{Set}_{\mathcal{R}}$ like $Q^{(\operatorname{-\\!-})}_{\omega_{1}}$ in
5.7 (with $\sum$ instead of $\bigvee$). For every ${f\colon
X\to\mathcal{R}X}$, let $p^{\ast}=\sum_{n\in{\rm Nature}}p^{n}\colon
X\to\mathcal{R}X$ where, inductively, $p^{0}=1$ and
$p^{n+1}=p\mspace{4.0mu};\mspace{2.0mu}p^{n}$, and infinite sums are extended
from $Q$ to the Kleisli hom-sets pointwise.

It is easy to verify that
$(\mathbf{Set}_{\mathcal{R}},\mathbf{Set}_{\mathcal{R}})$ is a KiC, but
$\mathbf{Set}_{\mathcal{R}}$ is not a Kleene-Kozen category, for
$\ast$-idempotence fails: $\eta^{\ast}=\sum_{n\in{\rm
Nature}}\eta^{n}=\sum_{n\in{\rm Nature}}\eta=\lambda x,y.\,\infty\neq\eta$. We
will use a more convenient notation for the elements of $\mathcal{R}X$ as
infinite formal sums $\sum_{i\in I}x_{i}$ ($x_{i}\in X$), modulo
associativity, commutativity, idempotence (but without countable idempotence
$\sum_{i\in I}x=x$!).

Below, we provide two results for constructing new KiCs from old: Theorem 5.9
and Theorem 5.12, which are also used prominently in our characterization
result in Section 7.

######  Theorem 5.9.

Let $(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$ be a KiC
and let ${\bm{\mathsf{T}}}$ be a monad on $\mathbf{C}$ such that

  1. 1.

$Tr^{\ast}=(Tr)^{\ast}$, for all $r\in\mathbf{C}(X,X)$;

  2. 2.

the monad ${\bm{\mathsf{T}}}$ restricts to a monad on
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$.

Then $\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}_{\bm{\mathsf{T}}}$ is a
subcategory of $\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ and
$(\mathbf{C}_{\bm{\mathsf{T}}},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}_{\bm{\mathsf{T}}})$
is a KiCT where $0$ and $+$ are defined as in $\mathbf{C}$, and for any
$p\colon X\to TX$, the corresponding Kleene iteration is computed as
$\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}$.

Let us illustrate the use of Theorem 5.9 by a simple example.

######  Example 5.10 (Finite Traces).

Consider the monad ${\mathcal{P}}(A^{\star}\times\operatorname{-\\!-})$ on
$\mathbf{Set}$. Elements of ${\mathcal{P}}(A^{\star}\times X)$ are standardly
used as (finite) trace semantics of programs. A trace is then a sequence of
actions from $A$, followed by an end result in $X$. Of course, it can be
verified directly that the Kleisli category of
${\mathcal{P}}(A^{\star}\times\operatorname{-\\!-})$ is Kleene-Kozen. Let us
show how this follows from Theorem 5.9.

The Kleisli category of ${\mathcal{P}}$ is isomorphic to the category of
relations, and is obviously Kleene-Kozen. For ${\mathcal{P}}$, like for any
commutative monad, the Kleisli category $\mathbf{Set}_{{\mathcal{P}}}$ is
symmetric monoidal: $X\mathbin{\otimes}Y=X\times Y$ and, given $p\colon
X\to{\mathcal{P}}Y$, $q\colon X^{\prime}\to{\mathcal{P}}Y^{\prime}$,

$(p\mathbin{\otimes}q)(x,x^{\prime})=\\{(y,y^{\prime})\mid y\in
p(x),\operatorname{}\linebreak[1]y^{\prime}\in q(x^{\prime})\\}.$

The set $A^{\star}$ is a monoid in $\mathbf{Set}_{{\mathcal{P}}}$ w.r.t. this
monoidal structure. This yields a writer monad ${\bm{\mathsf{T}}}$ on
$\mathbf{Set}_{{\mathcal{P}}}$ via $TX=A^{\star}\mathbin{\otimes}X$ and
$(Tp)(w,x)=\\{(w,y)\mid y\in p(x)\\}$. Its Kleisli category
$(\mathbf{Set}_{{\mathcal{P}}})_{{\bm{\mathsf{T}}}}$ is isomorphic to our
original Kleisli category of interest. The assumptions (1) of Theorem 5.9 are
thus satisfied in the obvious way. The assumption (2) is vacuous, as we chose
all morphisms to be tame.

Finally, we establish robustness of KiCs under the _generalized coalgebraic
resumption monad transformer_ [35, 17], which is defined as follows.

######  Definition 5.11 (Coalgebraic Resumptions).

Let $\mathbf{V}$ be a category with coproducts and let ${\bm{\mathsf{T}}}$ be
a monad on $\mathbf{V}$. Let $H\colon\mathbf{V}\to\mathbf{V}$ be some
endofunctor and assume that all final coalgebras $\nu\gamma.\,T(X\oplus
H\gamma)$ exist. The assignment $X\mapsto\nu\gamma.\,T(X\oplus H\gamma)$
yields a monad ${\bm{\mathsf{T}}}_{H}$, called the (generalized) coalgebraic
resumption monad transformer of ${\bm{\mathsf{T}}}$.

######  Theorem 5.12.

Let ${\bm{\mathsf{T}}}_{H}$ be as in 5.11 and such that
$(\mathbf{V}_{{\bm{\mathsf{T}}}},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$
is a KiC for some choice of $\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$.
Then $\mathbf{V}_{{\bm{\mathsf{T}}}}$ is a wide subcategory of
$\mathbf{V}_{{\bm{\mathsf{T}}}_{H}}$ and
$(\mathbf{V}_{{\bm{\mathsf{T}}}_{H}},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$
is a KiC w.r.t. the following structure:

  * •

the bottom element in every $\mathbf{V}(X,T_{H}Y)$ is
$0\mspace{4.0mu};\mspace{2.0mu}\mathsf{out}^{\text{\kern
0.5pt-}\mathsf{\kern-0.5pt1}}$, and the join of $p,q\in\mathbf{V}(X,T_{H}Y)$
is
$(p\mspace{4.0mu};\mspace{2.0mu}\mathsf{out}+q\mspace{4.0mu};\mspace{2.0mu}\mathsf{out})\mspace{4.0mu};\mspace{2.0mu}\mathsf{out}^{\text{\kern
0.5pt-}\mathsf{\kern-0.5pt1}}$;

  * •

given $p\in\mathbf{V}(X,T_{H}X)$, $p^{\ast}\in\mathbf{V}(X,T_{H}X)$ is the
unique solution of the equation

$p^{\ast}\mspace{4.0mu};\mspace{2.0mu}\mathsf{out}=\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}[p\mspace{4.0mu};\mspace{2.0mu}\mathsf{out},0]^{\ast}\mspace{4.0mu};\mspace{2.0mu}T(1\oplus
Hp^{\ast}).$

We defer the proof to Section 6 where we use reduction to the existing result
[19], using the equivalence of Kleene and Elgot iterations, we establish in
Section 6.

######  Example 5.13.

By taking $T={\mathcal{P}}_{\omega_{1}}$ and $H=A\times\operatorname{-\\!-}$
in Theorem 5.12, we obtain
$T_{H}X=\nu\gamma.\,{\mathcal{P}}_{\omega_{1}}(X\oplus A\times\gamma)$ from
3.2. Let us illustrate the effect of Kleene iteration by example. Consider the
system of equations

$\displaystyle P=a.\,P+Q,\qquad Q=b.\,Q+P$

for defining the behaviour of two processes $P$ and $Q$. This system induces a
function $p\colon\\{P,Q\\}\to T_{H}\\{P,Q\\}$, sending $P$ to $a.\,P+Q$ and
$Q$ to $b.\,Q+P$. The expression
$[p\mspace{4.0mu};\mspace{2.0mu}\mathsf{out},0]^{\ast}$ calls the iteration
operator of the powerset-monad, resulting in the function that sends both $P$
and $Q$ to $a.\,P+b.\,Q+Q+P$. Finally, $p^{\ast}$ sends $P$ to $P^{\prime}$
and $Q$ to $Q^{\prime}$, where $P^{\prime}$ and $Q^{\prime}$ are the
synchronization trees, obtained as unique solutions of the system:

$\displaystyle P^{\prime}=a.\,P^{\prime}+b.\,Q^{\prime}+Q+P,\qquad
Q=a.\,P^{\prime}+b.\,Q^{\prime}+Q+P.$

##  6 Elgot Iteration and While-Loops

In this section, we establish an equivalence between Kleene iteration, in the
sense of KiC and _Elgot iteration_ , as an operation with the following
profile in a category $\mathbf{C}$ with coproducts:

$\displaystyle(\operatorname{-\\!-})^{\dagger}\colon\mathbf{C}(X,Y\oplus
X)\to\mathbf{C}(X,Y).$ (7)

This could be done directly, but we prove an equivalence between Elgot
iteration and while-loops first, and then prove the equivalence of the latter
and Kleene iteration. In this chain of equivalences, only while-loops need
tests, and it will follow that a particular choice of tests is not relevant,
once they are expressive. On the other hand, existence of expressive tests is
guaranteed by 4.6. This explains why tests disappear in the resulting
equivalence.

######  Definition 6.1 (Conway Iteration, Uniformity).

An Elgot iteration operator (7) in a category $\mathbf{C}$ with coproducts is
_Conway iteration_ [13] if it satisfies the following principles:

$\displaystyle\text{{Naturality}}:$ $\displaystyle\leavevmode\nobreak\
\leavevmode\nobreak\
p^{\dagger}\mspace{4.0mu};\mspace{2.0mu}q=(p\mspace{4.0mu};\mspace{2.0mu}(q\oplus
1))^{\dagger}$ $\displaystyle\leavevmode\nobreak\
\text{{Dinaturality}}:\leavevmode\nobreak\
(p\mspace{4.0mu};\mspace{2.0mu}[\operatorname{\mathsf{in_{0}}},q])^{\dagger}=p\mspace{4.0mu};\mspace{2.0mu}[1,(q\mspace{4.0mu};\mspace{2.0mu}[\operatorname{\mathsf{in_{0}}},p])^{\dagger}]$
$\displaystyle\text{{Codiagonal}}:$ $\displaystyle\leavevmode\nobreak\
\leavevmode\nobreak\
(p\mspace{4.0mu};\mspace{2.0mu}[1,\operatorname{\mathsf{in_{1}}}])^{\dagger}=p^{\dagger\dagger}$

Moreover, given a subcategory $\mathbf{D}$ of $\mathbf{C}$,
$(\operatorname{-\\!-})^{\dagger}$ is _uniform_ w.r.t. $\mathbf{D}$, or
$\mathbf{D}$-uniform, if it satisfies

$\displaystyle\text{{Uniformity}}:$
$\displaystyle\quad\textbf{}\leavevmode\nobreak\ \leavevmode\nobreak\
\frac{u\mspace{4.0mu};\mspace{2.0mu}q=p\mspace{4.0mu};\mspace{2.0mu}(1\oplus
u)}{u\mspace{4.0mu};\mspace{2.0mu}q^{\dagger}=p^{\dagger}}\qquad\text{(with
$u$ from $\mathbf{D}$)}$

By taking $q=\operatorname{\mathsf{in_{1}}}$ in Dinaturality, we derive

$\displaystyle\text{{Fixpoint}}:p\mspace{4.0mu};\mspace{2.0mu}[1,p^{\dagger}]=p^{\dagger}.$

DW-Fix:
$\displaystyle\quad\operatorname{\mathsf{\underline{while}}}\mathbin{\,}d\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}p=\operatorname{\mathsf{\underline{if}}}\mathbin{}d\operatorname{\mathsf{\underline{then}}}\mathbin{}p\mspace{4.0mu};\mspace{2.0mu}(\operatorname{\mathsf{\underline{while}}}\mathbin{\,}d\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}p)\operatorname{\mathsf{\underline{else}}}\mathbin{\,}1$
DW-Or:
$\displaystyle\quad\operatorname{\mathsf{\underline{while}}}\mathbin{\,}(d\mathrel{\texttt{|\kern-2.95pt|}}e)\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}p=(\operatorname{\mathsf{\underline{while}}}\mathbin{\,}d\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}p)\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{\underline{while}}}\mathbin{\,}e\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}(p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{\underline{while}}}\mathbin{\,}d\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}p)$
DW-And:
$\displaystyle\quad\operatorname{\mathsf{\underline{while}}}\mathbin{\,}(d\mathrel{\texttt{\&\kern-0.5pt\&}}(e\mathrel{\texttt{|\kern-2.95pt|}}\operatorname{\mathsf{t\kern-0.45ptt}}))\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}p=\operatorname{\mathsf{\underline{while}}}\mathbin{\,}d\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}(\operatorname{\mathsf{\underline{if}}}\mathbin{}e\operatorname{\mathsf{\underline{then}}}\mathbin{}p\operatorname{\mathsf{\underline{else}}}\mathbin{\,}p)\qquad$
DW-Uni:
$\displaystyle\quad\frac{u\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{\underline{if}}}\mathbin{}d\operatorname{\mathsf{\underline{then}}}\mathbin{}p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{t\kern-0.45ptt}}\operatorname{\mathsf{\underline{else}}}\mathbin{\,}\operatorname{\mathsf{f\kern-0.78ptf}}=\operatorname{\mathsf{\underline{if}}}\mathbin{}e\operatorname{\mathsf{\underline{then}}}\mathbin{}q\mspace{4.0mu};\mspace{2.0mu}u\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{t\kern-0.45ptt}}\operatorname{\mathsf{\underline{else}}}\mathbin{\,}v\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{f\kern-0.78ptf}}}{u\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{\underline{while}}}\mathbin{\,}d\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}p=(\operatorname{\mathsf{\underline{while}}}\mathbin{\,}e\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}q)\mspace{4.0mu};\mspace{2.0mu}v}$

Figure 2: Uniform Conway iteration in terms of decisions.

######  Theorem 6.2.

Let $\mathbf{C}$ be a category with coproducts, let $\mathbf{D}$ be its wide
subcategory with coproducts, preserved by the inclusion, and let for every
${X\in|\mathbf{C}|}$,
$\mathbf{C}^{\raisebox{-1.0pt}{\scalebox{0.95}{$\diamond$}}}(X)$ be a set of
decisions such that (i)
$\operatorname{\mathsf{in_{0}}},\operatorname{\mathsf{in_{1}}}\in\mathbf{C}^{\raisebox{-1.0pt}{\scalebox{0.95}{$\diamond$}}}(X)$,
(ii) $\mathbf{C}^{\raisebox{-1.0pt}{\scalebox{0.95}{$\diamond$}}}(X)$ is
closed under (5), (iii)
$\operatorname{\mathsf{in_{0}}}\oplus\operatorname{\mathsf{in_{1}}}\in\mathbf{C}^{\raisebox{-1.0pt}{\scalebox{0.95}{$\diamond$}}}(X)$
if $X=X_{1}\oplus X_{2}$. Then, to give a $\mathbf{D}$-uniform Conway
iteration on $\mathbf{C}$ is the same as to give an operator

$\displaystyle\frac{d\in\mathbf{C}^{\raisebox{-1.0pt}{\scalebox{0.95}{$\diamond$}}}(X)\qquad
p\in\mathbf{C}(X,X)}{\operatorname{\mathsf{\underline{while}}}\mathbin{\,}d\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}p\in\mathbf{C}(X,X)}$

that satisfies the laws in Figure 2 with $p,q$ ranging over $\mathbf{C}$, and
with $u,v$ ranging over $\mathbf{D}$.

Theorem 6.2 yields an equivalence between two styles of iteration: Elgot
iteration and while-iteration. We next specialize it to idempotent grove
categories with tests using 4.7.

Note that in any KiC
$(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$ with tests
$\mathbf{C}^{?}$, in addition to the if-then-else (6), we have the while
operator, defined in the standard way: given $b\in\mathbf{C}^{?}(X)$,
$p\in\mathbf{C}(X,X)$,

$\displaystyle\operatorname{\mathsf{while}}\mathbin{}b\operatorname{\mathsf{do}}\mathbin{}p=(b\mspace{4.0mu};\mspace{2.0mu}p)^{\ast}\mspace{4.0mu};\mspace{2.0mu}\bar{b}.$
(8)

######  Proposition 6.3.

Let $\mathbf{C}$ be an idempotent grove category, let $\mathbf{D}$ be a wide
subcategory of $\mathbf{C}$ with coproducts, which are preserved by the
inclusion to $\mathbf{C}$, and with expressive tests $\mathbf{C}^{?}$. Then
$\mathbf{C}$ supports $\mathbf{D}$-uniform Conway iteration iff it supports a
while-operator that satisfies the laws in Figure 3, where $b$ and $c$ come
from $\mathbf{C}^{?}$, $p$ and $q$ come from $\mathbf{C}$ and $u,v$ come from
$\mathbf{D}$ and the if-then-else operator is defined as in (8).

######  Proof 6.4.

For every $X\in|\mathbf{C}|$, let
$\mathbf{C}^{\raisebox{-1.0pt}{\scalebox{0.95}{$\diamond$}}}(X)$ be the image
of $\mathbf{C}^{?}(X)$ under
$\mathinner{\raisebox{-1.0pt}{\scalebox{1.35}{$\diamond$}}}$ from 4.7. As
shown in the lemma,
$\mathbf{C}^{\raisebox{-1.0pt}{\scalebox{0.95}{$\diamond$}}}(X)$ inherits the
Boolean algebra structure from $\mathbf{C}^{?}(X)$. Using the isomorphism
between $\mathbf{C}^{\raisebox{-1.0pt}{\scalebox{0.95}{$\diamond$}}}(X)$ and
$\mathbf{C}^{?}(X)$ and 4.3, the laws from Figure 2 can be reformulated
equivalently, resulting in TW-Fix, TW-Or, TW-Uni, and additionally

$\displaystyle\operatorname{\mathsf{while}}\mathbin{}(b\land(c\lor\top))\operatorname{\mathsf{do}}\mathbin{}p=$
$\displaystyle\;\operatorname{\mathsf{while}}\mathbin{}b\operatorname{\mathsf{do}}\mathbin{}(\operatorname{\mathsf{if}}\mathbin{}c\operatorname{\mathsf{then}}\mathbin{}p\operatorname{\mathsf{else}}\mathbin{}p)$

which however holds trivially.

Thus, in grove categories with expressive tests, Elgot iteration and while-
loops are equivalent. We establish a similar equivalence between Kleene
iteration and while-loops, which will entail an equivalence between Elgot
iteration and Kleene iteration by transitivity.

######  Theorem 6.5.

Let $\mathbf{C}$, $\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ and
$\mathbf{C}^{?}$ be as follows.

  1. 1.

$\mathbf{C}$ is an idempotent grove category with coproducts.

  2. 2.

$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ is a wide subcategory of
$\mathbf{C}$ with coproducts, consisting of linear morphisms only and such
that the inclusion of $\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ to
$\mathbf{C}$ preserves coproducts.

  3. 3.

$\mathbf{C}^{?}$ are expressive tests in $\mathbf{C}$.

Then $(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$ is a KiCT
iff $\mathbf{C}$ supports a while-operator satisfying the laws in Figure 3.

We can now characterize KiCs in terms of Elgot iteration.

######  Theorem 6.6.

Let $\mathbf{C}$ be an idempotent grove category with coproducts, and let
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ be a wide subcategory of
$\mathbf{C}$ with coproducts, consisting of linear morphisms only and such
that the inclusion of $\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$ to
$\mathbf{C}$ preserves coproducts.

Then $(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$ is a KiC
iff $\mathbf{C}$ supports
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$-uniform Conway iteration.

######  Proof 6.7.

Let us define $\mathbf{C}^{?}$ as in 4.5. By Theorem 6.5,
$(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$ is a KiCT iff
$\mathbf{C}$ supports a while-operator, satisfying the laws in Figure 3. By
6.3, the latter is the case iff $\mathbf{C}$ supports
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$-uniform Conway iteration.

TW-Fix:
$\displaystyle\quad\operatorname{\mathsf{while}}\mathbin{}b\operatorname{\mathsf{do}}\mathbin{}p=\operatorname{\mathsf{if}}\mathbin{}b\operatorname{\mathsf{then}}\mathbin{}p\mspace{4.0mu};\mspace{2.0mu}(\operatorname{\mathsf{while}}\mathbin{}b\operatorname{\mathsf{do}}\mathbin{}p)\operatorname{\mathsf{else}}\mathbin{}1$
TW-Or: $\displaystyle\quad\operatorname{\mathsf{while}}\mathbin{}(b\lor
c)\operatorname{\mathsf{do}}\mathbin{}p=(\operatorname{\mathsf{while}}\mathbin{}b\operatorname{\mathsf{do}}\mathbin{}p)\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{while}}\mathbin{}c\operatorname{\mathsf{do}}\mathbin{}(p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{while}}\mathbin{}b\operatorname{\mathsf{do}}\mathbin{}p)\qquad$
TW-Uni:
$\displaystyle\quad\frac{u\mspace{4.0mu};\mspace{2.0mu}\bar{b}=\bar{c}\mspace{4.0mu};\mspace{2.0mu}v\qquad
u\mspace{4.0mu};\mspace{2.0mu}b\mspace{4.0mu};\mspace{2.0mu}p=c\mspace{4.0mu};\mspace{2.0mu}q\mspace{4.0mu};\mspace{2.0mu}u}{u\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{while}}\mathbin{}b\operatorname{\mathsf{do}}\mathbin{}p=(\operatorname{\mathsf{while}}\mathbin{}c\operatorname{\mathsf{do}}\mathbin{}q)\mspace{4.0mu};\mspace{2.0mu}v}$

Figure 3: Uniform Conway iteration in terms of tests.

Now we can prove Theorem 5.12.

######  Proof 6.8 (Proof Theorem 5.12 (Sketch)).

We need to check that
${(\mathbf{V}_{{\bm{\mathsf{T}}}_{H}},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})}$
is a KiC. By Theorem 6.6, we equivalently prove that
$\mathbf{V}_{{\bm{\mathsf{T}}}_{H}}$ supports
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}$-uniform Conway iteration. It
is already known [19, Lemma 7.2] that if ${\bm{\mathsf{T}}}$ supports Conway
iteration, then so does ${\bm{\mathsf{T}}}_{H}$. By Theorem 6.6, we are left
to check that ${\bm{\mathsf{T}}}_{H}$ satisfies Uniformity, which is a matter
of calculation.

##  7 Free KiCTs and Completeness

In this section, we characterize a free KiCT with strict coproducts (i.e.
those, for which coherence maps $X\oplus(Y\oplus Z)\mathbin{\cong}(X\oplus
Y)\oplus Z$ are identities) on a one-sorted signature. We achieve this by
combining techniques from formal languages [7], category theory and the theory
of Elgot iteration with coalgebraic reasoning [37], in particular proofs by
coalgebraic bisimilarity. We claim that a more general characterization of a
free KiCT on a multi-sorted signature can be achieved along the same lines,
modulo a significant notation overhead and the necessity to form final
coalgebras in the category of multisorted sets $\mathbf{Set}^{\mathcal{S}}$
where $\mathcal{S}$ is the set of sorts. We dispense with this option for the
sake of brevity and readability. Let us fix

  * •

a signatures of $n$-ary symbols $\Sigma_{n}$ for each $n\in{\rm Nature}$, and
let $\Sigma=\bigcup_{n}\Sigma_{n}$;

  * •

a signature $\Gamma$ of (unary) symbols, disjoint from $\Sigma$;

  * •

a finite (!) signature $\Theta$ of (unary) symbols, disjoint from
$\Sigma\cup\Gamma$.

Let  $\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$ $\textstyle\Theta$ denote
the set of finite subsets of $\Theta$. We regard $\Theta$ as a signature for
tests, $\Gamma$ as a signature for tame morphisms and $\Sigma$ as a signature
for general morphisms;  $\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$
$\textstyle\Theta$ is meant to capture finite conjunctions of the form
$\mathsf{b}_{1}\land\ldots\land\mathsf{b}_{n}\land\bar{\mathsf{b}}_{n+1}\land\ldots\land\bar{\mathsf{b}}_{m}$
as semantic correspondents of subsets
$\\{\mathsf{b}_{1},\ldots,\mathsf{b}_{n}\\}\in\mathchoice{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\widehat{\Theta}}{\widehat{\Theta}}$,
assuming an enumeration $\Theta=\\{\mathsf{b}_{1},\ldots,\mathsf{b}_{m}\\}$.
This is inspired by Kleene algebra with tests [26]. Furthermore, we
accommodate _guarded strings_ from _op. cit._ : let $\Gamma^{\Theta}$ be the
set of strings $\langle
b_{1},\mathsf{u}_{1},\ldots,b_{n},\mathsf{u}_{n},b_{n+1}\rangle$ with
$\mathsf{u}_{i}\in\Gamma$,
$b_{i}\in\mathchoice{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\widehat{\Theta}}{\widehat{\Theta}}$.

###  7.1 Interpretations

An _interpretation_ $\llbracket\operatorname{-\\!-}\rrbracket$ of
$(\Sigma,\Gamma,\Theta)$ over a KiCT
$(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}},\mathbf{C}^{?})$
is specified as follows:

$\displaystyle\llbracket 1\rrbracket\in\;$ $\displaystyle|\mathbf{C}|$
$\displaystyle\llbracket\mathsf{f}\rrbracket\in\;$
$\displaystyle\mathbf{C}(\llbracket 1\rrbracket,\llbracket
n\rrbracket)\qquad(\mathsf{f}\in\Sigma_{n})$
$\displaystyle\llbracket\mathsf{u}\rrbracket\in\;$
$\displaystyle\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}(\llbracket
1\rrbracket,\llbracket 1\rrbracket)\qquad(\mathsf{u}\in\Gamma)$
$\displaystyle\llbracket\mathsf{b}\rrbracket\in\;$
$\displaystyle\mathbf{C}^{?}(\llbracket 1\rrbracket,\llbracket
1\rrbracket)\qquad(\mathsf{b}\in\Theta)$

where $\llbracket n\rrbracket$ abbreviates the $n$-fold sum $\llbracket
1\rrbracket\oplus\ldots\oplus\llbracket 1\rrbracket$. The latter immediately
extends to  $\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$ $\textstyle\Theta$
: $\llbracket\\{\,\\}\rrbracket=1$,
$\llbracket\\{\mathsf{b}_{1},\ldots,\mathsf{b}_{n}\\}\rrbracket=\mathsf{b}_{1}\mspace{4.0mu};\mspace{2.0mu}\ldots\mspace{4.0mu};\mspace{2.0mu}\mathsf{b}_{n}\mspace{4.0mu};\mspace{2.0mu}\bar{\mathsf{b}}_{n+1}\mspace{4.0mu};\mspace{2.0mu}\ldots\mspace{4.0mu};\mspace{2.0mu}\bar{\mathsf{b}}_{m}$,
assuming that $\Theta=\\{\mathsf{b}_{1},\ldots,\mathsf{b}_{m}\\}$. Note that
we interpret $n$-ary symbols over $\mathbf{C}(\llbracket
1\rrbracket,\llbracket n\rrbracket)=\mathbf{C}^{\mathsf{op}}(\llbracket
1\rrbracket^{n},\llbracket 1\rrbracket)$. This equation seems to suggest that
it could be more natural to use categories with products as models, rather
than categories with coproducts. Our present choice helps us to treat generic
KiCTs on the same footing with the free KiCT, which is defined in terms of
coproducts and not products.

######  Definition 7.1 (Free KiCT).

A _free KiCT_ w.r.t. $(\Sigma,\Gamma,\Theta)$ is a KiCT
$(\mathfrak{F}_{\Sigma,\Gamma,\Theta},\overline{\mathfrak{F}_{\Sigma,\Gamma,\Theta}},{\mathfrak{F}^{?}_{\Sigma,\Gamma,\Theta}})$
together with an interpretation of $(\Sigma,\Gamma,\Theta)$ in
$\mathfrak{F}_{\Sigma,\Gamma,\Theta}$, such that for any other interpretation
of $(\Sigma,\Gamma,\Theta)$ over a KiCT
$(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}},\mathbf{C}^{?})$,
there is unique compatible functor from $\mathfrak{F}_{\Sigma,\Gamma,\Theta}$
to $\mathbf{C}$. More formally, for any interpretation
$\llbracket\operatorname{-\\!-}\rrbracket$, there is unique KiCT-functor
$\llbracket\operatorname{-\\!-}\rrbracket_{\shortuparrow}\colon(\mathfrak{F}_{\Sigma,\Gamma,\Theta},\overline{\mathfrak{F}_{\Sigma,\Gamma,\Theta}},{\mathfrak{F}^{?}_{\Sigma,\Gamma,\Theta}})\to(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}},\mathbf{C}^{?})$
such that the diagram

${\mathfrak{F}_{\Sigma,\Gamma,\Theta}}$${\mathbf{C}}$${(\Sigma,\Gamma,\Theta)}$$\scriptstyle{\llbracket\operatorname{-\\!-}\rrbracket_{\shortuparrow}}$$\scriptstyle{\llbracket\operatorname{-\\!-}\rrbracket^{\mathfrak{F}}}$$\scriptstyle{\llbracket\operatorname{-\\!-}\rrbracket}$
(9)

commutes.

In what follows, we characterize $\mathfrak{F}_{\Sigma,\Gamma,\Theta}$ as a
certain category of rational trees, i.e. trees with finitely many distinct
subtrees. An alternative, equivalent formulation would be to view
$\mathfrak{F}_{\Sigma,\Gamma,\Theta}$ as a free model of the (Lawvere) theory
of KiCTs.

Like in the case of original Kozen’s completeness result [25], a
characterization of the free model immediately entails completeness of the
corresponding axiomatization over it. Indeed, by generalities, a free KiCT is
isomorphic to the free algebra of terms, quotiented by the provable equality
relation. Hence, if an equality holds over the free model, it is provable.

###  7.2 A KiCT of Coalgebraic Resumptions

For any set $X$, define $TX=\mathcal{R}(\Gamma^{\Theta}\times X)$ and
$T_{\nu}X=\nu\gamma.\,T(X\oplus\Sigma\gamma)$, in the category of sets
$\mathbf{Set}$ where $\mathcal{R}$ is the monad from 5.8.

A stepping stone for constructing $\mathfrak{F}_{\Sigma,\Gamma,\Theta}$ is the
observation that
$(\mathbf{Set}_{{\bm{\mathsf{T}}}_{\nu}},\mathbf{Set}_{{\bm{\mathsf{T}}}})$
forms a KiC. Indeed, $(\mathbf{Set}_{\mathcal{R}},\mathbf{Set}_{\mathcal{R}})$
is a KiC and the monad $\mathcal{R}$ is commutative, hence symmetric monoidal.
In $\mathbf{Set}_{\mathcal{R}}$, $\Gamma^{\Theta}$ is a monoid under the
following operations:

$\displaystyle\langle w_{1},\ldots,w_{n+1}\rangle\cdot\langle
u_{1},\ldots,u_{m+1}\rangle=\begin{cases}\langle
w_{1},\ldots,w_{n},u_{2},\ldots,u_{m+1}\rangle&\text{if }w_{n}=u_{1}\\\
0&\text{otherwise}\end{cases}$

This produces the monad ${\bm{\mathsf{T}}}$, whose Kleisli category is a KiC
by Theorem 5.9, analogously to 5.10. Now,
$(\mathbf{Set}_{{\bm{\mathsf{T}}}_{\nu}},\mathbf{Set}_{{\bm{\mathsf{T}}}})$ is
a KiC by Theorem 5.12. We will use the following representation for generic
elements of $T_{\nu}X$:

$\displaystyle t=\sum_{i\in I}b_{i}.\,\mathsf{u}_{i}.\,t_{i}+\sum_{i\in
J}b_{i}.\,\mathsf{f}_{i}(t_{i,1},\ldots,t_{i,n_{i}})+\sum_{i\in
K}b_{i}.\,x_{i}$ (10)

where $I$, $J$, $K$ are mutually disjoint countable sets, $b_{i}$ range over
$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$ $\textstyle\Theta$ ,
$\mathsf{u}_{i}$ range over $\Gamma$, $\mathsf{f}_{i}$ range over $\Sigma$,
$t_{i},t_{i,j}$ range over $T_{\nu}X$ and $x_{i}$ range over $X$.

######  Definition 7.2 (Derivatives).

For every $t\in T_{\nu}X$, as in (10), define the following _derivative_
operations:

  * •

$\partial_{b,\mathsf{u}}(t)=\sum_{i\in
I,b=b_{i},\mathsf{u}=\mathsf{u}_{i}}t_{i}$, for
$b\in\mathchoice{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\widehat{\Theta}}{\widehat{\Theta}}$,
$\mathsf{u}\in\Gamma$;

  * •

$\partial_{b,\mathsf{f}}^{k}(t)=\sum_{i\in
J,b=b_{i},\mathsf{f}=\mathsf{f}_{i}}t_{i,k}$, for
$b\in\mathchoice{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\widehat{\Theta}}{\widehat{\Theta}}$,
$k\in\\{1,\ldots,n_{i}\\}$, $\mathsf{f}\in\Sigma_{n_{i}}$ with $n_{i}>0$.

Additionally, let $o(t)=\sum_{i\in K}b_{i}.\,x_{i}$. We extend these
operations to arbitrary morphisms $Y\to T_{\nu}X$ pointwise. The _set of
derivatives_ of $t\in T_{\nu}X$ is the smallest set $\mathfrak{D}(t)$ that
contains $t$ and is closed under all $\partial_{b,\mathsf{u}}$ and
$\partial_{b,\mathsf{f}}^{k}$.

The following property is a direct consequence of these definitions:

######  Lemma 7.3.

Let $t\in T_{\nu}X$ be as in (10), and let $s\colon X\to T_{\nu}Y$. Then

$\displaystyle\partial_{b,\mathsf{u}}(t\mspace{4.0mu};\mspace{2.0mu}s^{\sharp})=$
$\displaystyle\;\partial_{b,\mathsf{u}}(t)\mspace{4.0mu};\mspace{2.0mu}s^{\sharp}+o(t)\mspace{4.0mu};\mspace{2.0mu}(\partial_{b,\mathsf{u}}(s))^{\sharp}$
$\displaystyle o(t\mspace{4.0mu};\mspace{2.0mu}s^{\sharp})=$
$\displaystyle\;o(t)\mspace{4.0mu};\mspace{2.0mu}(o(s))^{\sharp}$
$\displaystyle\partial_{b,\mathsf{f}}^{k}(t\mspace{4.0mu};\mspace{2.0mu}s^{\sharp})=$
$\displaystyle\;\partial_{b,\mathsf{f}}^{k}(t)\mspace{4.0mu};\mspace{2.0mu}s^{\sharp}+o(t)\mspace{4.0mu};\mspace{2.0mu}(\partial_{b,\mathsf{f}}^{k}(s))^{\sharp}$

######  Lemma 7.4.

Given a set $X$, let $\mathcal{B}\subseteq T_{\nu}X\times T_{\nu}X$ be such a
relation that whenever $t\mathrel{\mathcal{B}}s$,

  1. 1.

$\partial_{b,\mathsf{u}}(t)\mathrel{\mathcal{B}}\partial_{b,\mathsf{u}}(s)$
for all $b\in\mathchoice{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\widehat{\Theta}}{\widehat{\Theta}}$,
$\mathsf{u}\in\Gamma$,

  2. 2.

$\partial_{b,\mathsf{f}}^{k}(t)\mathrel{\mathcal{B}}\partial_{b,\mathsf{f}}^{k}(s)$
for all $b\in\mathchoice{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{11.27492pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\mathchoice{{\ooalign{\hfil$\displaystyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\displaystyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\textstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\textstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptstyle\Theta$\hfil\cr}}}{{\ooalign{\hfil$\scriptscriptstyle\kern
0.15pt\scalebox{0.8}[0.65]{$\widehat{\phantom{\rule{8.0pt}{10.93333pt}}}$}$\hfil\cr\hfil$\scriptscriptstyle\Theta$\hfil\cr}}}}{\widehat{\Theta}}{\widehat{\Theta}}$,
$\mathsf{f}\in\Sigma$,

  3. 3.

$o(t)=o(s)$.

Then, $t=s$ whenever $t\mathrel{\mathcal{B}}s$.

######  Proof 7.5 (Proof Sketch).

It suffices to show that $\mathcal{B}$ is a coalgebraic bisimulation. The
claim is then a consequence of strong extensionality of the final coalgebra
$T_{\nu}X$. Let us spell out what it means for $\mathcal{B}$ to be a
coalgebraic bisimulation. Given $t$ and $t^{\prime}$, such that
$t\mathrel{\mathcal{B}}t^{\prime}$, and assuming representations

$\displaystyle t=$ $\displaystyle\;\sum_{i\in
I}g_{i}.\,\mathsf{f}_{i}(t_{i,1},\ldots,t_{i,n_{i}})+\sum_{i\in
J}g_{i}.\,x_{i},$ $\displaystyle t^{\prime}=$ $\displaystyle\;\sum_{i\in
I^{\prime}}g_{i}.\,\mathsf{f}_{i}(t_{i,1},\ldots,t_{i,n_{i}})+\sum_{i\in
J^{\prime}}g_{i}.\,x_{i}$

where the $g_{i}$ range over $\Gamma^{\Theta}$, the sums $\sum_{i\in
J}g_{i}.\,x_{i}$ and $\sum_{i\in J^{\prime}}g_{i}.\,x_{i}$ must be equal, and
there must exist a set $K$ and surjections $e\colon K\to I$, $e^{\prime}\colon
K\to I^{\prime}$, such that for every $k\in K$, $g_{e(k)}=g_{e^{\prime}(k)}$,
$\mathsf{f}_{e(k)}=\mathsf{f}_{e^{\prime}(k)}$ and
$t_{e(k),1}\mathrel{\mathcal{B}}t_{e^{\prime}(k),1},\ldots,t_{e(k),m}\mathrel{\mathcal{B}}t_{e^{\prime}(k),m}$
where $m$ is the arity of $\mathsf{f}_{e(k)}$. This is indeed true for
$\mathcal{B}$. The reason for it is that $t$ and $t^{\prime}$ can be
represented as

$\displaystyle t=$ $\displaystyle\;\sum_{n\in{\rm Nature}}\sum_{i\in
I,|g_{i}|=n}g_{i}.\,\mathsf{f}_{i}(t_{i,1},\ldots,t_{i,n_{i}})+\sum_{n\in{\rm
Nature}}\sum_{i\in J,|g_{i}|=n}g_{i}.\,x_{i},$ $\displaystyle t^{\prime}=$
$\displaystyle\;\sum_{n\in{\rm Nature}}\sum_{i\in
I^{\prime},|g_{i}|=n}g_{i}.\,\mathsf{f}_{i}(t_{i,1}^{\prime},\ldots,t_{i,n_{i}}^{\prime})+\sum_{n\in{\rm
Nature}}\sum_{i\in J^{\prime},|g_{i}|=n}g_{i}.\,x_{i}$

and we can derive the requisite properties for inner sums by induction on $n$
from the assumptions.

###  7.3 Rational Trees

In what follows, we identify every $n\in{\rm Nature}$ with the set
$\\{0,\ldots,n-1\\}$, and select binary coproducts in $\mathbf{Set}$ so that
$n\oplus
m=\\{0,\ldots,n-1\\}\oplus\\{0,\ldots,m-1\\}=\\{0,\ldots,n+m-1\\}=n+m$. The
inclusion of $n$ to $m\geq n$ is then a coproduct injection, which we refer to
as $\operatorname{\mathsf{in}}_{n}^{m}$.

######  Definition 7.6 (Prefinite, Flat, (Non-)Guarded, Rational, Definable).

  1. 1.

The set of _prefinite_ elements of $T_{\nu}X$ is defined by induction: $t\in
T_{\nu}X$ of the form (10) is _prefinite_ if the involved sums contain
finitely many distinct elements and all the ${t_{i},t_{i,j}\in T_{\nu}X}$ are
prefinite.

  2. 2.

A prefinite $t\in T_{\nu}X$ of the form (10) is _flat_ if ${t_{i},t_{i,j}\in
X}$.

  3. 3.

An element $t\in T_{\nu}X$ of the form (10) is _guarded_ if $K=\emptyset$.

  4. 4.

An element $t\in T_{\nu}X$ of the form (10) is _non-guarded_ if $I\cup
J=\emptyset$.

  5. 5.

An element $t\in T_{\nu}X$ is _rational_ if $\mathfrak{D}(t)$ is finite and
$t$ depends on a finite subset of $\Sigma\cup\Gamma$.

A map $t\colon Y\to T_{\nu}X$ is prefinite/flat/guarded/non-guarded if
correspondingly for every $x\in X$, every $t(x)$ is
prefinite/flat/guarded/non-guarded. Finally:

  1. 6.

A map $t\colon k\to T_{\nu}n$ (with $k,n\in{\rm Nature}$) is _definable_ if
for some $m\geq k$ there is flat guarded $s\colon m\to T_{\nu}m$ and non-
guarded $r\colon m\to T_{\nu}n$, such that
$t=\operatorname{\mathsf{in}}_{k}^{m}\mspace{4.0mu};\mspace{2.0mu}s^{\ast}\mspace{4.0mu};\mspace{2.0mu}r^{\sharp}$.

Using 7.3, one can show

######  Lemma 7.7.

Sum, composition and Kleene iteration of rational maps are again rational.

The following property is a form of Kleene theorem, originally stating the
equivalence of regular and recognizable languages [38]. In our setting it is
proven with the help of 7.4.

######  Proposition 7.8.

Given $n,k\in{\rm Nature}$, a map $n\to T_{\nu}k$ is rational iff it is
definable.

Let $\mathfrak{F}=\mathfrak{F}_{\Sigma,\Gamma,\Theta}$ be the (non-full)
subcategory of $\mathbf{Set}_{{\bm{\mathsf{T}}}_{\nu}}$, identified as
follows:

  * •

the objects of $\mathfrak{F}$ are positive natural numbers,

  * •

the morphisms in $\mathfrak{F}(n,k)$ are rational maps $f\colon n\to T_{\nu}k$
(equivalently: (co)tuples $[t_{0},\ldots,t_{n-1}]$ of rational elements of
$T_{\nu}k$).

Let the wide subcategory of tame morphisms $\overline{\mathfrak{F}}$ consist
of such tuples $[t_{0},\ldots,t_{n-1}]$ that ${t_{i}\in Tk}$ for all $i$, and
let $\mathfrak{F}^{?}$ consist of those maps in $\overline{\mathfrak{F}}$ that
do not involve symbols from $\Gamma$. This defines a KiCT essentially due to
the closure properties from 7.7.

Given an interpretation
$\llbracket\operatorname{-\\!-}\rrbracket\colon(\Sigma,\Gamma,\Theta)\to\mathbf{C}$,
let us extend it to flat elements first via

$\displaystyle\llbracket 0\rrbracket=0,\quad\leavevmode\nobreak\ \llbracket
t+s\rrbracket=\llbracket t\rrbracket+\llbracket
s\rrbracket,\quad\leavevmode\nobreak\
\llbracket\eta^{\ast}\rrbracket=\llbracket
1\rrbracket^{\ast},\quad\leavevmode\nobreak\ \llbracket
t\mspace{4.0mu};\mspace{2.0mu}s^{\sharp}\rrbracket=\llbracket
t\rrbracket\mspace{4.0mu};\mspace{2.0mu}\llbracket
s\rrbracket,\quad\leavevmode\nobreak\ \llbracket
k\rrbracket=\operatorname{\mathsf{in}}_{k}\leavevmode\nobreak\ (k\in n)$

where $\eta^{\ast}$ stands for a tuple of infinite sum $[\sum_{i\in{\rm
Nature}}\\{\\}.0,\ldots,\sum_{i\in{\rm Nature}}\\{\\}.(n-1)]$, and is the
interpretation of $\eta^{\star}$ in $\mathfrak{F}$. The clause for
$\eta^{\ast}$ in necessary to cater for infinite sums that can occur in
prefinite elements. Such sums can only contain finitely many distinct
elements, and thus can be expressed via finite sums and composition with
$\eta^{\ast}$. Next, define
${\llbracket\operatorname{-\\!-}\rrbracket_{\shortuparrow}\colon\mathfrak{F}\to\mathbf{C}}$

  * •

on objects via $\llbracket n\rrbracket_{\shortuparrow}=\llbracket
1\rrbracket\oplus\ldots\oplus\llbracket 1\rrbracket$ ($\llbracket 1\rrbracket$
repeated $n$ times),

  * •

on morphisms, via $\llbracket
t\rrbracket_{\shortuparrow}=\operatorname{\mathsf{in}}_{n,m}\mspace{4.0mu};\mspace{2.0mu}\llbracket
s\rrbracket^{\ast}\mspace{4.0mu};\mspace{2.0mu}\llbracket r\rrbracket$, where
$t=\operatorname{\mathsf{in}}_{n,m}\mspace{4.0mu};\mspace{2.0mu}t^{\ast}\mspace{4.0mu};\mspace{2.0mu}r^{\sharp}$,
for a guarded flat $s\colon m\to T_{\nu}m$, and a non-guarded $r\colon m\to
T_{\nu}k$, computed with 7.8.

######  Theorem 7.9.

$\mathfrak{F}_{\Sigma,\Gamma,\Theta}$ is a free KiCT over
$\Sigma,\Gamma,\Theta$.

The following property is instrumental for proving this result:

######  Lemma 7.10.

Let $(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$ and
$(\mathbf{D},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{D}})$ be two KiCs,
and let $F$ be the following map, acting on objects and on morphisms:
$FX\in|\mathbf{D}|$ for every $X\in|\mathbf{C}|$, $Fp\in\mathbf{D}(FX,FY)$ for
every $p\in\mathbf{C}(X,Y)$. Suppose that $F$ preserves coproducts,
$Fp\in\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{D}}(FX,FY)$ for all
$p\in\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}(X,Y)$. $F$ is a KiC-
functor if the following further preservation properties hold

$\displaystyle Fp^{\ast}=(Fp)^{\ast},\quad
F(p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}})=Fp\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}},\quad
F(p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}})=Fp\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}},\quad
F(p\mspace{4.0mu};\mspace{2.0mu}[0,1])=Fp\mspace{4.0mu};\mspace{2.0mu}[0,1].$

Let us briefly outline a potential application of Theorem 7.9 to may-diverge
Kleene algebras, which we informally described in the introduction. Let us now
define them formally:

######  Definition 7.11 (May-Diverge Kleene Algebra).

A _may-diverge Kleene algebra_ is an idempotent semiring
$(S,\operatorname{}\linebreak[1]0,\operatorname{}\linebreak[1]1,\operatorname{}\linebreak[1]+,\operatorname{}\linebreak[1]\,\mspace{4.0mu};\mspace{2.0mu})$
equipped with an iteration operator $(\operatorname{-\\!-})^{\ast}\colon S\to
S$ satisfying the laws:

$\displaystyle
p^{\ast}=1+p\mspace{4.0mu};\mspace{2.0mu}p^{\ast}\qquad(p+q)^{\ast}=p^{\ast}\mspace{4.0mu};\mspace{2.0mu}(q\mspace{4.0mu};\mspace{2.0mu}p^{\ast})^{\ast}\qquad\vbox{$r\mspace{4.0mu};\mspace{2.0mu}p^{\ast}=q^{\ast}\mspace{4.0mu};\mspace{2.0mu}rr\mspace{4.0mu};\mspace{2.0mu}p=q\mspace{4.0mu};\mspace{2.0mu}r$}$

Thus, may-diverge Kleene algebras are very close to KiCs of the form
$(\mathbf{C},\mathbf{C})$ with $|\mathbf{C}|=1$, except that in our present
treatment all KiCs come with binary coproducts as an additional structure. We
conjecture though that any may-diverge Kleene algebra, viewed as a category,
can be embedded to a KiC $(\mathbf{C},\mathbf{C})$ with
$|\mathbf{C}|=\\{1,2,\ldots\\}$. Theorem 7.9 will then entail a
characterization of the free may-diverge Kleene algebra on $\Gamma$ as the
full subcategory induced by the single object $1$ of the Kleisli category of
the monad $TX=\mathcal{R}(\Gamma^{\star}\times X)$. In other words, the free
may-diverge Kleene algebra is carried (up-to-isomorphism) by rational elements
of $\mathcal{R}(\Gamma^{\star})$, similarly to that how the free Kleene
algebra is carried by rational elements of ${\mathcal{P}}(\Gamma^{\star})$.

##  8 Conclusions and Further Work

We developed a general and robust categorical notion of Kleene iteration –
KiC(T) (=Kleene-iteration category (with tests)) – inspired by Kleene algebra
(with tests) and its numerous cousins. We attested this notion with various
yardsticks: stability under the generalized coalgebraic resumption monad
transformer (hence under the exception transformer, as its degenerate case),
equivalence to the classical notion of Conway iteration and to a suitably
axiomatized theory of while-loops, but most remarkably, we established an
explicit description of the ensuing free model, as a category of certain
nondeterministic rational trees, playing the same role for our theory as the
algebra of regular events for Kleene algebra. However, in our case, the free
model is much more intricate and difficult to construct, as the iteration
operator of it is neither a least fixpoint nor a unique fixpoint. A salient
feature of our notion, mirrored in the structure of the free model, is that it
can mediate between linear time and branching time semantics via corresponding
specified classes of morphisms.

Given the abstract nature of our results, we expect them be be reusable for
varying and enriching the core notion of Kleene iteration with other features.
For example, our underlying notion of nondeterminism is that of idempotent
grove category. General grove categories are a natural base for probabilistic
or graded semantics, and we expect that most of our results, including
completeness can be adapted to this case. Yet more generally, a relevant
ingredient of our construction is monad $\mathcal{R}$, currently capturing the
effect of nondeterminism, but which can potentially be varied to obtain other
flavors of linear behavior.

An important open problem that remains for future work is that of defining
KiCTs without coproducts, potentially providing a bridge to relevant algebraic
structures as single-object categories. Now that the free KiCT with coproduct
is identified, the free KiCT without coproducts is expected to be complete
over the same model. Identifying such a notion is hard, because it would
simultaneously encompass independent axiomatizations of iterative behavior,
e.g. branching time and linear time. As of now, such axiomatizations are built
on hard-to-reconcile approaches to iteration as either a least or a unique
fixpoint.

## References

  * [1] Luca Aceto, Arnaud Carayol, Zoltán Ésik, and Anna Ingólfsdóttir.  Algebraic synchronization trees and processes.  In Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer, editors, Proc. of 39th Int. Coll on Automata, Languages, and Programming, ICALP 2012, Part 2, volume 7392 of Lect. Notes in Comput. Sci., pages 30–41. Springer, 2012.
  * [2] Michael A. Arbib and Ernest G. Manes.  Partially additive categories and flow-diagram semantics.  J. Algebra, 62(1):203–227, 1980.
  * [3] Steve Awodey.  Category Theory.  Oxford University Press, 2nd edition, 2010.
  * [4] David B. Benson and Jerzy Tiuryn.  Fixed points in free process algebras, part I.  Theor. Comput. Sci., 63(3):275–294, 1989.
  * [5] S.L. Bloom, Z. Esik, and D. Taubner.  Iteration theories of synchronization trees.  Information and Computation, 102(1):1–55, 1993.
  * [6] Stephen L. Bloom and Zoltán Ésik.  Iteration Theories: The Equational Logic of Iterative Processes.  Springer, 1993.
  * [7] Janusz A. Brzozowski.  Derivatives of regular expressions.  J. ACM, 11(4):481–494, 1964.
  * [8] Kenta Cho.  Total and partial computation in categorical quantum foundations.  In Chris Heunen, Peter Selinger, and Jamie Vicary, editors, Proc. of 12th Int. Workshop on Quantum Physics and Logic, QPL 2015, volume 195 of Electron. Proc. in Theor. Comput. Sci., pages 116–135. Open Publishing Assoc., 2015.
  * [9] Robin Cockett.  Itegories & PCAs, 2007.  Slides from Fields Institute Meeting on Traces (Ottawa, 2007).
  * [10] Robin Cockett and Stephen Lack.  Restriction categories III: colimits, partial limits and extensivity.  Math. Struct Comput. Sci., 17(4):775–817, 2007.
  * [11] Manfred Droste and Werner Kuich.  Semirings and Formal Power Series, pages 3–28.  Springer, 2009.
  * [12] Calvin Elgot.  Monadic computation and iterative algebraic theories.  In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium 1973, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 175–230. Elsevier, 1975.
  * [13] Zoltán Ésik.  Equational properties of fixed-point operations in cartesian categories: An overview.  Math. Struct. Comput. Sci., 29(6):909–925, 2019.
  * [14] Wan J. Fokkink and Hans Zantema.  Basic process algebra with iteration: Completeness of its equational axioms.  Comput. J., 37(4):259–268, 1994.
  * [15] Leandro Gomes, Alexandre Madeira, and Luís S. Barbosa.  On Kleene algebras for weighted computation.  In Simone Cavalheiro and José Fiadeiro, editors, Formal Methods: Foundations and Applications, volume 10623 of Lect. Notes in Comput. Sci., pages 271–286. Springer, 2017.
  * [16] Sergey Goncharov.  Shades of iteration: From Elgot to Kleene.  In Alexandre Madeira and Manuel A. Martins, editors, Revised Selected Papers from 26th IFIP WG 1.3 Int. Workshop on Recent Trends in Algebraic Development Techniques, WADT 2022, volume 13710 of Lect. Notes in Comput. Sci., pages 100–120. Springer, 2023.
  * [17] Sergey Goncharov, Christoph Rauch, and Lutz Schröder.  Unguarded recursion on coinductive resumptions.  Electron. Notes Theor. Comput. Sci., 319:183–198, 2015.
  * [18] Sergey Goncharov, Lutz Schröder, and Till Mossakowski.  Kleene monads: Handling iteration in a framework of generic effects.  In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Proc. of 3rd Int. Conf. Algebra and Coalgebra in Computer Science, CALCO 2009, volume 5728 of Lect. Notes in Comput. Sci., pages 18–33. Springer, 2009.
  * [19] Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Julian Jakob.  Unguarded recursion on coinductive resumptions.  Log. Methods in Comput. Sci., 14(3):10:1–10:47, 2018.
  * [20] Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Maciej Piróg.  Guarded and unguarded iteration for generalized processes.  Log. Methods Comput. Sci., 15(3):1:1–1:47, 2019.
  * [21] Clemens Grabmayer.  Milner’s proof system for regular expressions modulo bisimilarity is complete: Crystallization: Near-collapsing process graph interpretations of regular expressions.  In Proc. of 37th Ann. ACM/IEEE Symp. on Logic in Computer Science, LICS ’22, pages 34:1–34:13, New York, 2022.
  * [22] Niels Grathwohl, Dexter Kozen, and Konstantinos Mamouras.  KAT + B!  In Proc. of 23rd EACL Ann. Conf. on Computer Science Logic and 29th Ann. ACM/IEEE Symp. on Logic in Computer Science, CSL-LICS 2014, pages 44:1–44:10. ACM, 2014.
  * [23] Bart Jacobs.  New directions in categorical logic, for classical, probabilistic and quantum logic.  CoRR, abs/1205.3940, 2015.
  * [24] S. C. Kleene.  Representation of events in nerve nets and finite automata.  In Claude Shannon and John McCarthy, editors, Automata Studies, pages 3–41. Princeton University Press, 1956.
  * [25] Dexter Kozen.  A completeness theorem for Kleene algebras and the algebra of regular events.  Inf. Comput., 110(2):366–390, 1994.
  * [26] Dexter Kozen.  Kleene algebra with tests.  ACM Trans. Program. Lang. Syst., 19(3):427–443, 1997.
  * [27] Dexter Kozen and Konstantinos Mamouras.  Kleene algebra with products and iteration theories.  In Simona Ronchi Della Rocca, editor, Proc. of 22nd EACSL Ann. Conf. on Computer Science Logic, CSL 2013, volume 23 of Leibniz Int. Proc. in Inform., pages 415–431. Dagstuhl Publishing, 2013.
  * [28] Dexter Kozen and Frederick Smith.  Kleene algebra with tests: Completeness and decidability.  In Dirk van Dalen and Marc Bezem, editors, Selected Papers from 10th Int. Workshop Computer Science Logic, CSL ’96, volume 1258 of Lect. Notes in Comput. Sci., pages 244–259. Springer, 1997.
  * [29] Saunders Mac Lane.  Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics.  Springer, 1971.
  * [30] Annabelle McIver, Tahiry M. Rabehaja, and Georg Struth.  On probabilistic Kleene algebras, automata and simulations.  In Harrie de Swart, editor, Proc. of 12th Int. Conf. on Relational and Algebraic Methods in Computer Science, RAMICS 2011, volume 6663 of Lect. Notes in Comput. Sci., pages 264–279. Springer, 2011.
  * [31] Robin Milner.  A Calculus of Communicating Systems, volume 92 of Lect. Notes in Comput. Sci. Springer, 1980.
  * [32] Robin Milner.  A complete inference system for a class of regular behaviours.  J. Comput. Syst. Sci., 28(3):439–466, 1984.
  * [33] Eugenio Moggi.  Notions of computation and monads.  Inf. Comput., 93(1):55–92, 1991.
  * [34] Bernhard Möller.  Kleene getting lazy.  Sci. Comput. Program., 65(2):195–214, 2007.
  * [35] Maciej Piróg and Jeremy Gibbons.  Monads for behaviour.  Electron. Notes Theor. Comput. Sci., 298:309–324, 2013.
  * [36] Gordon D. Plotkin.  A powerdomain construction.  SIAM J. Comput., 5(3):452–487, 1976.
  * [37] J.J.M.M. Rutten.  Behavioural differential equations: A coinductive calculus of streams, automata, and power series.  Theor. Comput. Sci., 308(1):1–53, 2003.
  * [38] Jacques Sakarovitch.  Elements of Automata Theory.  Cambridge University Press, 2009.
  * [39] Alex Simpson and Gordon Plotkin.  Complete axioms for categorical fixed-point operators.  In Proc. of 15th Ann. IEEE Symp. on Logic in Computer Science, LICS ’00, pages 30–41. IEEE, 2000.
  * [40] Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva.  Guarded Kleene algebra with tests: Verification of uninterpreted programs in nearly linear time.  Proc. ACM Program. Lang., 4(POPL), 2020.
  * [41] Daniele Turi and Jan Rutten.  On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces.  Math. Struct. Comput. Sci., 8(5):481–540, 1998.
  * [42] Tarmo Uustalu.  Generalizing substitution.  Theor. Inform. Appl., 37(4):315–336, 2003.

## Appendix: Selected Proof Details

###  I. Proof of 4.3

Suppose that $d$ is linear. Then

$\displaystyle\operatorname{\mathsf{\underline{if}}}\mathbin{}d\operatorname{\mathsf{\underline{then}}}\mathbin{}p\operatorname{\mathsf{\underline{else}}}\mathbin{\,}q$
$\displaystyle\;=d\mspace{4.0mu};\mspace{2.0mu}[q,p]$
$\displaystyle\;=d\mspace{4.0mu};\mspace{2.0mu}([q,0]+[0,p])$
$\displaystyle\;=d\mspace{4.0mu};\mspace{2.0mu}[q,0]+d\mspace{4.0mu};\mspace{2.0mu}[0,p]$
$\displaystyle\;=d\mspace{4.0mu};\mspace{2.0mu}[1,0]\mspace{4.0mu};\mspace{2.0mu}q+d\mspace{4.0mu};\mspace{2.0mu}[0,1]\mspace{4.0mu};\mspace{2.0mu}p$
$\displaystyle\;=\operatorname{\mathsf{if}}\mathbin{}d?\operatorname{\mathsf{then}}\mathbin{}p\operatorname{\mathsf{else}}\mathbin{}q.$

###  II. Proof of 4.4

The necessity is obvious. Let us show sufficiency. For every
$b\in\mathbf{C}^{?}(X)$, let us fix some choice of
$\bar{b}\in\mathbf{C}^{?}(X)$, for which the pair $(b,\bar{b})$ satisfies
contradiction and excluded middle, and show that $\mathbf{C}^{?}(X)$ forms a
Boolean algebra, i.e. $\mathbf{C}^{?}(X)$ is a complemented distributive
lattice. Complementation precisely amounts to the assumed identities, and we
are left to show the laws of distributive lattices. Since complements are
uniquely defined in Boolean algebras, it will follow that $\bar{b}$ is
uniquely determined by $b$. Of course, this is not used in the subsequent
proof.

It follows by definition that $(\mathbf{C}^{?}(X),0,+)$ and
$(\mathbf{C}^{?}(X),1,\mspace{4.0mu};\mspace{2.0mu})$ are monoids. Showing
that they are idempotent and commutative (hence, are semilattices) amounts to
showing that $b\mspace{4.0mu};\mspace{2.0mu}b=b$ and
$b\mspace{4.0mu};\mspace{2.0mu}c=c\mspace{4.0mu};\mspace{2.0mu}b$ for all
$b,c\in\mathbf{C}^{?}(X)$. The first identity is shown as follows, using
linearity and the assumed identities:

$\displaystyle b=$ $\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}1$
$\displaystyle=$ $\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}(b+\bar{b})$
$\displaystyle=$
$\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}b+b\mspace{4.0mu};\mspace{2.0mu}\bar{b}$
$\displaystyle=$ $\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}b+0$
$\displaystyle=$ $\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}b.$ For the
second one, note that $1=b+\bar{b}=b+b+\bar{b}=b+1$, and then $\displaystyle
b\mspace{4.0mu};\mspace{2.0mu}c=$
$\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}1$
$\displaystyle=$
$\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}(b+1)$
$\displaystyle=$
$\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}b+b\mspace{4.0mu};\mspace{2.0mu}c$
$\displaystyle=$
$\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}b+b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}b\mspace{4.0mu};\mspace{2.0mu}c$
$\displaystyle=$
$\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}b\mspace{4.0mu};\mspace{2.0mu}(1+c)$
$\displaystyle=$
$\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}b,$

where we used the instance of idempotence
$b\mspace{4.0mu};\mspace{2.0mu}c=b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}b\mspace{4.0mu};\mspace{2.0mu}c$
that we just established. Analogously,
$c\mspace{4.0mu};\mspace{2.0mu}b=b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}b$,
and hence $b\mspace{4.0mu};\mspace{2.0mu}c=c\mspace{4.0mu};\mspace{2.0mu}b$.

Finally, distributivity amounts to
$(a+b)\mspace{4.0mu};\mspace{2.0mu}c=a\mspace{4.0mu};\mspace{2.0mu}c+b\mspace{4.0mu};\mspace{2.0mu}c$
and
$a+b\mspace{4.0mu};\mspace{2.0mu}c=(a+b)\mspace{4.0mu};\mspace{2.0mu}(a+c)$
for all $a,b,c\in\mathbf{C}^{?}(X)$. The first identity is an axiom of
idempotent grove categories. The second one is obtained as follows:

$\displaystyle(a+b)\mspace{4.0mu};\mspace{2.0mu}(a+c)=$
$\displaystyle\;a\mspace{4.0mu};\mspace{2.0mu}a+a\mspace{4.0mu};\mspace{2.0mu}c+b\mspace{4.0mu};\mspace{2.0mu}a+b\mspace{4.0mu};\mspace{2.0mu}c\qquad$
$\displaystyle=$
$\displaystyle\;a+a\mspace{4.0mu};\mspace{2.0mu}c+a\mspace{4.0mu};\mspace{2.0mu}b+b\mspace{4.0mu};\mspace{2.0mu}c$
$\displaystyle=$
$\displaystyle\;a\mspace{4.0mu};\mspace{2.0mu}(1+c+b)+b\mspace{4.0mu};\mspace{2.0mu}c$
$\displaystyle=$
$\displaystyle\;a\mspace{4.0mu};\mspace{2.0mu}1+b\mspace{4.0mu};\mspace{2.0mu}c$
$\displaystyle=$ $\displaystyle\;a+b\mspace{4.0mu};\mspace{2.0mu}c$ ∎

###  III. Proof of 4.6

Negation is defined as follows:

$\displaystyle\bar{0}=$ $\displaystyle\;1,$
$\displaystyle\overline{[\operatorname{\mathsf{in_{0}}},0]}=$
$\displaystyle\;[0,\operatorname{\mathsf{in_{1}}}],$
$\displaystyle\overline{b+c}=$
$\displaystyle\;\bar{b}\mspace{4.0mu};\mspace{2.0mu}\bar{c},$
$\displaystyle\bar{1}=$ $\displaystyle\;0,$
$\displaystyle\overline{[0,\operatorname{\mathsf{in_{1}}}]}=$
$\displaystyle\;[\operatorname{\mathsf{in_{0}}},0],$
$\displaystyle\overline{b\mspace{4.0mu};\mspace{2.0mu}c}=$
$\displaystyle\;\bar{b}+\bar{c}.$

For every $X$, let $\mathbf{C}^{?}(X)$ be the smallest subset of
$\mathbf{C}(X,X)$ that contains $0$, $1$, $[\operatorname{\mathsf{in_{0}}},0]$
and $[0,\operatorname{\mathsf{in_{1}}}]$, and closed under $+$ and
$\\!\mspace{4.0mu};\mspace{2.0mu}$. By 4.4, we need to show that every
$b\in\mathbf{C}^{?}(X)$ is linear and satisfies
$b\mspace{4.0mu};\mspace{2.0mu}\bar{b}=0$, $b+\bar{b}=1$, which we do by
induction. Let us strengthen the induction invariant by also adding
$\bar{b}\mspace{4.0mu};\mspace{2.0mu}b=0$. Note that the above equations do
not uniquely define complement, e.g.
$\overline{[\operatorname{\mathsf{in_{0}}},0]}=\;[0,\operatorname{\mathsf{in_{1}}}]$
refers to a particular decomposition of $X$ as $X_{1}\oplus X_{2}$, while
another decomposition could theoretically produce a different result. Thus,
more precisely, we use the fact that every element of $\mathbf{C}^{?}(X)$ has
a representation in the free algebra of terms over $0$, $1$,
$[\operatorname{\mathsf{in_{0}}},0]$, $[0,\operatorname{\mathsf{in_{1}}}]$,
$+$ and $\mspace{4.0mu};\mspace{2.0mu}$, and we run induction over this
representation.

_Induction Base._ If $b=0$ or $b=1$, the verification is trivial. Consider
$b=[\operatorname{\mathsf{in_{0}}},0]$. Then

$\displaystyle b\mspace{4.0mu};\mspace{2.0mu}0=$
$\displaystyle\;[\operatorname{\mathsf{in_{0}}},0]\mspace{4.0mu};\mspace{2.0mu}0$
$\displaystyle=$
$\displaystyle\;[\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}0,0]$
$\displaystyle=$ $\displaystyle\;0,$ $\displaystyle
b\mspace{4.0mu};\mspace{2.0mu}(p+q)=$
$\displaystyle\;[\operatorname{\mathsf{in_{0}}},0]\mspace{4.0mu};\mspace{2.0mu}(p+q)$
$\displaystyle=$
$\displaystyle\;[\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}p+\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}q,0]$
$\displaystyle=$
$\displaystyle\;[\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}p,0]+[\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}q,0]$
$\displaystyle=$
$\displaystyle\;b\mspace{4.0mu};\mspace{2.0mu}p+b\mspace{4.0mu};\mspace{2.0mu}q,$
for any suitably typed $p$ and $q$; analogously
$\bar{b}\mspace{4.0mu};\mspace{2.0mu}0=0$,
$\bar{b}\mspace{4.0mu};\mspace{2.0mu}(p+q)=\bar{b}\mspace{4.0mu};\mspace{2.0mu}p+\bar{b}\mspace{4.0mu};\mspace{2.0mu}q$.
Moreover, $\displaystyle b\mspace{4.0mu};\mspace{2.0mu}\bar{b}=$
$\displaystyle\;[\operatorname{\mathsf{in_{0}}},0]\mspace{4.0mu};\mspace{2.0mu}[0,\operatorname{\mathsf{in_{1}}}]$
$\displaystyle=$
$\displaystyle\;[\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}[0,\operatorname{\mathsf{in_{1}}}],0\mspace{4.0mu};\mspace{2.0mu}[0,\operatorname{\mathsf{in_{1}}}]]$
$\displaystyle=$ $\displaystyle\;0,$ $\displaystyle b+\bar{b}=$
$\displaystyle\;[\operatorname{\mathsf{in_{0}}},0]+[0,\operatorname{\mathsf{in_{1}}}]$
$\displaystyle=$
$\displaystyle\;[\operatorname{\mathsf{in_{0}}}+0,0+\operatorname{\mathsf{in_{1}}}]$
$\displaystyle=$ $\displaystyle\;1.$

The identity $\bar{b}\mspace{4.0mu};\mspace{2.0mu}b=0$ is shown analogously to
$b\mspace{4.0mu};\mspace{2.0mu}\bar{b}=0$.

_Induction Step._ Suppose that the induction hypothesis holds for some
${b,c\in\mathbf{C}^{?}(X)}$ and show that $b\mspace{4.0mu};\mspace{2.0mu}c$,
$b+c$ are both linear and satisfy equations:

$\displaystyle
b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}(\bar{b}+\bar{c})=$
$\displaystyle\;0,$
$\displaystyle(\bar{b}+\bar{c})\mspace{4.0mu};\mspace{2.0mu}b\mspace{4.0mu};\mspace{2.0mu}c=$
$\displaystyle\;0,$ $\displaystyle
b\mspace{4.0mu};\mspace{2.0mu}c+(\bar{b}+\bar{c})=$ $\displaystyle\;1,$ (11)
$\displaystyle(b+c)\mspace{4.0mu};\mspace{2.0mu}\bar{b}\mspace{4.0mu};\mspace{2.0mu}\bar{c}=$
$\displaystyle\;0,$
$\displaystyle\bar{b}\mspace{4.0mu};\mspace{2.0mu}\bar{c}\mspace{4.0mu};\mspace{2.0mu}(b+c)=$
$\displaystyle\;0,$
$\displaystyle(b+c)+\bar{b}\mspace{4.0mu};\mspace{2.0mu}\bar{c}=$
$\displaystyle\;1.$ (12) _Linearity of $(b\mspace{4.0mu};\mspace{2.0mu}c)$:_
$\displaystyle b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}0$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}0$ $\displaystyle\;=0,$
$\displaystyle
b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}(p+q)$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}(b\mspace{4.0mu};\mspace{2.0mu}p+c\mspace{4.0mu};\mspace{2.0mu}q)$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}p+b\mspace{4.0mu};\mspace{2.0mu}b\mspace{4.0mu};\mspace{2.0mu}q.$
_Linearity of $(b+c)$:_ $\displaystyle(b+c)\mspace{4.0mu};\mspace{2.0mu}0$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}0+c\mspace{4.0mu};\mspace{2.0mu}0$
$\displaystyle\;=0,$ $\displaystyle(b+c)\mspace{4.0mu};\mspace{2.0mu}(p+q)$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}(p+q)+c\mspace{4.0mu};\mspace{2.0mu}(p+q)$
$\displaystyle\;=(b\mspace{4.0mu};\mspace{2.0mu}p+b\mspace{4.0mu};\mspace{2.0mu}q)+(c\mspace{4.0mu};\mspace{2.0mu}p+c\mspace{4.0mu};\mspace{2.0mu}q)$
$\displaystyle\;=(b+c)\mspace{4.0mu};\mspace{2.0mu}p+(b+c)\mspace{4.0mu};\mspace{2.0mu}q.$
Finally, we prove two equations from the list (11)–(12) – the rest is
analogous. Note that $c+1=c+c+\bar{c}=c+\bar{c}=1$, $\displaystyle
b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}(\bar{b}+\bar{c})$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}\bar{b}+b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}\bar{c}$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}\bar{b}+b\mspace{4.0mu};\mspace{2.0mu}0$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}\bar{b}$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}c\mspace{4.0mu};\mspace{2.0mu}\bar{b}+b\mspace{4.0mu};\mspace{2.0mu}\bar{b}$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}(c+1)\mspace{4.0mu};\mspace{2.0mu}\bar{b}$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}1\mspace{4.0mu};\mspace{2.0mu}\bar{b}$
$\displaystyle\;=0.$ $\displaystyle
b\mspace{4.0mu};\mspace{2.0mu}c+(\bar{b}+\bar{c})$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}c+\bar{b}\mspace{4.0mu};\mspace{2.0mu}1+1\mspace{4.0mu};\mspace{2.0mu}\bar{c}$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}c+\bar{b}\mspace{4.0mu};\mspace{2.0mu}(c+\bar{c})+(b+\bar{b})\mspace{4.0mu};\mspace{2.0mu}\bar{c}$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}c+\bar{b}\mspace{4.0mu};\mspace{2.0mu}c+\bar{b}\mspace{4.0mu};\mspace{2.0mu}\bar{c}+b\mspace{4.0mu};\mspace{2.0mu}\bar{c}+\bar{b}\mspace{4.0mu};\mspace{2.0mu}\bar{c}$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}(c+\bar{c})+\bar{b}\mspace{4.0mu};\mspace{2.0mu}(c+\bar{c})$
$\displaystyle\;=(b+\bar{b})\mspace{4.0mu};\mspace{2.0mu}(c+\bar{c})$
$\displaystyle\;=1\mspace{4.0mu};\mspace{2.0mu}1$ $\displaystyle\;=1.$ ∎

###  IV. Proof of 4.7

Clause 1 is shown as follows:

$\displaystyle(\mathinner{\raisebox{-1.0pt}{\scalebox{1.35}{$\diamond$}}}b)?$
$\displaystyle\;=(\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}})\mspace{4.0mu};\mspace{2.0mu}[0,1]$
$\displaystyle\;=\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}[0,1]+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}\mspace{4.0mu};\mspace{2.0mu}[0,1]$
$\displaystyle\;=\bar{b}\mspace{4.0mu};\mspace{2.0mu}0+b$ $\displaystyle\;=b.$
We proceed with Clause 2. To that end, fix some $d$ from the image of
$\mathinner{\raisebox{-1.0pt}{\scalebox{1.35}{$\diamond$}}}$, i.e. assume that
$d=\mathinner{\raisebox{-1.0pt}{\scalebox{1.35}{$\diamond$}}}b=\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}$
for some $b\in\mathbf{C}^{?}(X)$. Then
$\displaystyle(\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}})\mspace{4.0mu};\mspace{2.0mu}0$
$\displaystyle\;=\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}0+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}\mspace{4.0mu};\mspace{2.0mu}0$
$\displaystyle\;=\bar{b}\mspace{4.0mu};\mspace{2.0mu}0+b\mspace{4.0mu};\mspace{2.0mu}0$
$\displaystyle\;=0,$
$\displaystyle(\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}})\mspace{4.0mu};\mspace{2.0mu}(g+h)$
$\displaystyle\;=\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}(g+h)+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}\mspace{4.0mu};\mspace{2.0mu}(g+h)$
$\displaystyle\;=\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}g+\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}h+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}\mspace{4.0mu};\mspace{2.0mu}g+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}\mspace{4.0mu};\mspace{2.0mu}h$
$\displaystyle\;=(\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}})\mspace{4.0mu};\mspace{2.0mu}g+(\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}})\mspace{4.0mu};\mspace{2.0mu}h,$
$\displaystyle(\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}})\mspace{4.0mu};\mspace{2.0mu}\nabla$
$\displaystyle\;=b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}\nabla+\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}\mspace{4.0mu};\mspace{2.0mu}\nabla$
$\displaystyle\;=b+\bar{b}$ $\displaystyle\;=1,$
$\displaystyle(\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}})$
$\displaystyle\mspace{4.0mu};\mspace{2.0mu}[\operatorname{\mathsf{in_{0}}},\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}]$
$\displaystyle\;=\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}$
$\displaystyle\;=\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}},$
as desired. The dual equation
$d=d\mspace{4.0mu};\mspace{2.0mu}[d,\operatorname{\mathsf{in_{1}}}]$ is shown
analogously. Finally, Clause 3 is shown as follows:
$\displaystyle(e\mspace{4.0mu};\mspace{2.0mu}[d,\operatorname{\mathsf{in_{1}}}])?$
$\displaystyle\;=(e\mspace{4.0mu};\mspace{2.0mu}[d,\operatorname{\mathsf{in_{1}}}])\mspace{4.0mu};\mspace{2.0mu}[0,1]$
$\displaystyle\;=e\mspace{4.0mu};\mspace{2.0mu}[d\mspace{4.0mu};\mspace{2.0mu}[0,1],1]$
$\displaystyle\;=e\mspace{4.0mu};\mspace{2.0mu}[d\mspace{4.0mu};\mspace{2.0mu}[0,1]+0,d\mspace{4.0mu};\mspace{2.0mu}[0,1]+1]$
$\displaystyle\;=e\mspace{4.0mu};\mspace{2.0mu}[d\mspace{4.0mu};\mspace{2.0mu}[0,1],d\mspace{4.0mu};\mspace{2.0mu}[0,1]]+e\mspace{4.0mu};\mspace{2.0mu}[0,1]$
$\displaystyle\;=d\mspace{4.0mu};\mspace{2.0mu}[0,1]+e\mspace{4.0mu};\mspace{2.0mu}[0,1]$
$\displaystyle\;=d?+e?.$
$\displaystyle(e\mspace{4.0mu};\mspace{2.0mu}[\operatorname{\mathsf{in_{0}}},d])?$
$\displaystyle\;=(e\mspace{4.0mu};\mspace{2.0mu}[\operatorname{\mathsf{in_{0}}},d])\mspace{4.0mu};\mspace{2.0mu}[0,1]$
$\displaystyle\;=e\mspace{4.0mu};\mspace{2.0mu}[0,d\mspace{4.0mu};\mspace{2.0mu}[0,1]]$
$\displaystyle\;=e\mspace{4.0mu};\mspace{2.0mu}[0,1]\mspace{4.0mu};\mspace{2.0mu}d\mspace{4.0mu};\mspace{2.0mu}[0,1]$
$\displaystyle\;=e?\mspace{4.0mu};\mspace{2.0mu}d?.$ Finally, for Clause 4,
let
$d=\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}$.
Then
$\displaystyle(d\mspace{4.0mu};\mspace{2.0mu}[\operatorname{\mathsf{in_{1}}},\operatorname{\mathsf{in_{0}}}])?$
$\displaystyle\;=(\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}})\mspace{4.0mu};\mspace{2.0mu}[\operatorname{\mathsf{in_{1}}},\operatorname{\mathsf{in_{0}}}]\mspace{4.0mu};\mspace{2.0mu}[0,1]$
$\displaystyle\;=\bar{b}+b\mspace{4.0mu};\mspace{2.0mu}0$
$\displaystyle\;=\bar{b}$
$\displaystyle\;=\overline{\bar{b}\mspace{4.0mu};\mspace{2.0mu}0+b}$
$\displaystyle\;=\overline{(\bar{b}\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+b\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}})\mspace{4.0mu};\mspace{2.0mu}[0,1]}$
$\displaystyle\;=\overline{d?}$ ∎

###  V. Proof to 5.6

We will prove the following auxiliary identity:

$\displaystyle[p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}},p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}]^{\ast}=(1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}])\mspace{4.0mu};\mspace{2.0mu}([p,p]\mspace{4.0mu};\mspace{2.0mu}(\operatorname{\mathsf{in_{1}}}+p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}))^{\ast},$
(13)

from which the goal follows. Indeed, note the identities:

$\displaystyle[p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}},p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}]\mspace{4.0mu};\mspace{2.0mu}\nabla=$
$\displaystyle\;\nabla\mspace{4.0mu};\mspace{2.0mu}p,$
$\displaystyle[p,p]\mspace{4.0mu};\mspace{2.0mu}(\operatorname{\mathsf{in_{1}}}+p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}})\mspace{4.0mu};\mspace{2.0mu}\nabla=$
$\displaystyle\;\nabla\mspace{4.0mu};\mspace{2.0mu}p\mspace{4.0mu};\mspace{2.0mu}(1+p),$

compose both sides of (13) with $\operatorname{\mathsf{in_{0}}}$ on the left
and $\nabla$ on the right, and simplify the result; notice that
$\nabla=[1;1]\in\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}(X\oplus X,X)$:

$\displaystyle p^{\ast}=$
$\displaystyle\;\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}\nabla\mspace{4.0mu};\mspace{2.0mu}p^{\ast}$
$\displaystyle=$
$\displaystyle\;\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}[p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}},p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}+p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}]^{\ast}\mspace{4.0mu};\mspace{2.0mu}\nabla$
// $\ast$-Uni $\displaystyle=$
$\displaystyle\;\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}(1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}])\mspace{4.0mu};\mspace{2.0mu}([p,p]\mspace{4.0mu};\mspace{2.0mu}(\operatorname{\mathsf{in_{1}}}+p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}))^{\ast}\mspace{4.0mu};\mspace{2.0mu}\nabla$
// (13) $\displaystyle=$
$\displaystyle\;\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}(1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}])\mspace{4.0mu};\mspace{2.0mu}\nabla\mspace{4.0mu};\mspace{2.0mu}(p\mspace{4.0mu};\mspace{2.0mu}(1+p))^{\ast}$
// $\ast$-Uni $\displaystyle=$
$\displaystyle\;(p\mspace{4.0mu};\mspace{2.0mu}(1+p))^{\ast}.$ Now, to show
(13), note that
$\displaystyle[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}]^{\ast}=$
$\displaystyle\;1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}]\mspace{4.0mu};\mspace{2.0mu}[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}]^{\ast}$
// $\ast$-Fix $\displaystyle=$
$\displaystyle\;1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}]^{\ast}]$
$\displaystyle=$
$\displaystyle\;1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}(1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}]\mspace{4.0mu};\mspace{2.0mu}[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}]^{\ast})]$
// $\ast$-Fix $\displaystyle=$
$\displaystyle\;1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}].$
Then
$\displaystyle[p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}},p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}$
$\displaystyle+p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}]^{\ast}$
$\displaystyle=$
$\displaystyle\;([0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}]+[p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}},p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}])^{\ast}$
$\displaystyle=$
$\displaystyle\;[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}]^{\ast}\mspace{4.0mu};\mspace{2.0mu}([p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}},p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}]\mspace{4.0mu};\mspace{2.0mu}[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}]^{\ast})^{\ast}$
// $\ast$-Sum $\displaystyle=$
$\displaystyle\;(1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}])\mspace{4.0mu};\mspace{2.0mu}([p,p]\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{1}}}\mspace{4.0mu};\mspace{2.0mu}(1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}]))^{\ast}$
$\displaystyle=$
$\displaystyle\;(1+[0,p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}])\mspace{4.0mu};\mspace{2.0mu}([p,p]\mspace{4.0mu};\mspace{2.0mu}(\operatorname{\mathsf{in_{1}}}+p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{in_{0}}}))^{\ast},$

and we are done.∎

###  VI. Proof of Theorem 5.9

Note that the assumptions imply that $T$ is a KiC-functor, in particular,
$T0=0$ and $T(p+q)=Tp+Tq$, by .3. The laws of grove categories are easy to
check. Indeed, the equations (3) interpreted in
$\mathbf{C}_{{\bm{\mathsf{T}}}}$ turn into

$\displaystyle\qquad\qquad 0\mspace{4.0mu};\mspace{2.0mu}p^{\sharp}=$
$\displaystyle\;0,$
$\displaystyle(q+r)\mspace{4.0mu};\mspace{2.0mu}p^{\sharp}=$
$\displaystyle\;q\mspace{4.0mu};\mspace{2.0mu}p^{\sharp}+r\mspace{4.0mu};\mspace{2.0mu}p^{\sharp},$

and clearly follow from assumptions. Linearity of left injections in
$\mathbf{C}_{{\bm{\mathsf{T}}}}$ reads as

$\displaystyle\qquad\qquad\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}\eta\mspace{4.0mu};\mspace{2.0mu}0^{\sharp}=$
$\displaystyle\;0,$
$\displaystyle\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}\eta\mspace{4.0mu};\mspace{2.0mu}(q+r)^{\sharp}=$
$\displaystyle\;\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}\eta\mspace{4.0mu};\mspace{2.0mu}q^{\sharp}+\operatorname{\mathsf{in_{0}}}\mspace{4.0mu};\mspace{2.0mu}\eta\mspace{4.0mu};\mspace{2.0mu}r^{\sharp},$

and follows from the assumption that $\operatorname{\mathsf{in_{0}}}$ is
linear in $\mathbf{C}$ – analogously for $\operatorname{\mathsf{in_{1}}}$.

Let us check that the morphisms from
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}_{\bm{\mathsf{T}}}$ are all
linear. To that end, take some $p$ from
$\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}}_{\bm{\mathsf{T}}}$, and show

$\displaystyle\qquad\qquad p\mspace{4.0mu};\mspace{2.0mu}0^{\sharp}=$
$\displaystyle\;0,$ $\displaystyle
p\mspace{4.0mu};\mspace{2.0mu}(q+r)^{\sharp}=$
$\displaystyle\;p\mspace{4.0mu};\mspace{2.0mu}q^{\sharp}+p\mspace{4.0mu};\mspace{2.0mu}r^{\sharp}$

Using the assumptions,
$p\mspace{4.0mu};\mspace{2.0mu}0^{\sharp}=p\mspace{4.0mu};\mspace{2.0mu}T0\mspace{4.0mu};\mspace{2.0mu}\mu=p\mspace{4.0mu};\mspace{2.0mu}0\mspace{4.0mu};\mspace{2.0mu}\mu=0\mspace{4.0mu};\mspace{2.0mu}\mu=0$
where $\mu=1^{\sharp}$ is multiplication of ${\bm{\mathsf{T}}}$. The second
equation is shown analogously.

Finally, we proceed to verify the laws of iteration. To that end, we record
some auxiliary properties:

$\displaystyle(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp}$
$\displaystyle=(p^{\sharp})^{\ast},$ (14)
$\displaystyle\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp}+q^{\sharp})$
$\displaystyle=p+q.$ (15)

For the first identity, note that

$\displaystyle
Tp^{\sharp}\mspace{4.0mu};\mspace{2.0mu}\mu=TTp\mspace{4.0mu};\mspace{2.0mu}T\mu\mspace{4.0mu};\mspace{2.0mu}\mu$
$\displaystyle=TTp\mspace{4.0mu};\mspace{2.0mu}\mu\mspace{4.0mu};\mspace{2.0mu}\mu=\mu\mspace{4.0mu};\mspace{2.0mu}Tp\mspace{4.0mu};\mspace{2.0mu}\mu=\mu\mspace{4.0mu};\mspace{2.0mu}p^{\sharp}.$
By assumption, $\mu=1^{\sharp}$ is tame, hence, by $\ast$-Uni,
$\displaystyle(Tp^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}\mu$
$\displaystyle=\mu\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}.$ We then
have
$\displaystyle(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp}$
$\displaystyle=T\eta\mspace{4.0mu};\mspace{2.0mu}T(p^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}\mu$
$\displaystyle=T\eta\mspace{4.0mu};\mspace{2.0mu}(Tp^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}\mu$
$\displaystyle=T\eta\mspace{4.0mu};\mspace{2.0mu}\mu\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}$
$\displaystyle=(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp}.$
The second identity is shown as follows:
$\displaystyle\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp}+q^{\sharp})$
$\displaystyle=\eta\mspace{4.0mu};\mspace{2.0mu}(Tp\mspace{4.0mu};\mspace{2.0mu}\mu+Tq\mspace{4.0mu};\mspace{2.0mu}\mu)$
$\displaystyle=\eta\mspace{4.0mu};\mspace{2.0mu}(Tp+Tq)\mspace{4.0mu};\mspace{2.0mu}\mu$
$\displaystyle=\eta\mspace{4.0mu};\mspace{2.0mu}T(p+q)\mspace{4.0mu};\mspace{2.0mu}\mu$
$\displaystyle=(p+q)\mspace{4.0mu};\mspace{2.0mu}\eta\mspace{4.0mu};\mspace{2.0mu}\mu$
$\displaystyle=p+q.$

Now, the laws of KiCs are shown as follows:

$\ast$-Fix: We need to show
$\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}=\eta+p\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp}$.
Indeed,

$\displaystyle\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}$
$\displaystyle\;=\eta\mspace{4.0mu};\mspace{2.0mu}(1+p^{\sharp}\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})$
$\displaystyle\;=\eta\mspace{4.0mu};\mspace{2.0mu}(1+p^{\sharp}\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp})$
// (14)
$\displaystyle\;=\eta\mspace{4.0mu};\mspace{2.0mu}(\eta^{\sharp}+(p\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp})^{\sharp})$
$\displaystyle\;=\eta+p\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp}.$
// (15)

$\ast$-Sum: We need to show
$\eta\mspace{4.0mu};\mspace{2.0mu}((p+q)^{\sharp})^{\ast}=\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(q\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp})^{\ast})^{\sharp}$.
This is essentially obtained from $\ast$-Sum for
$(\mathbf{C},\accentset{\rule{3.85002pt}{0.6pt}}{\mathbf{C}})$ by repeated use
of (15):

$\displaystyle\eta\mspace{4.0mu};\mspace{2.0mu}((p+q)^{\sharp})^{\ast}$
$\displaystyle\;=\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp}+q^{\sharp})^{\ast}$
$\displaystyle\;=\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}(q^{\sharp}\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\ast}$
$\displaystyle\;=\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}(q^{\sharp}\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp})^{\ast}$
$\displaystyle\;=\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}((q\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp})^{\sharp})^{\ast}$
$\displaystyle\;=\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(q\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp})^{\ast})^{\sharp}.$

$\ast$-Uni: Suppose that
$u\mspace{4.0mu};\mspace{2.0mu}p^{\sharp}=q\mspace{4.0mu};\mspace{2.0mu}u^{\sharp}$
for some tame $u$. We need to show
$u\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp}=\eta\mspace{4.0mu};\mspace{2.0mu}(q^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}u^{\sharp}$.
By applying Kleisli lifting to both sides of the assumption, we obtain
$u^{\sharp}\mspace{4.0mu};\mspace{2.0mu}p^{\sharp}=q^{\sharp}\mspace{4.0mu};\mspace{2.0mu}u^{\sharp}$,
which by $\ast$-Uni yields
$u^{\sharp}\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}=(q^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}u^{\sharp}$.
Then

$\displaystyle
u\mspace{4.0mu};\mspace{2.0mu}(\eta\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast})^{\sharp}$
$\displaystyle\;=u\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}$ // (15)
$\displaystyle\;=\eta\mspace{4.0mu};\mspace{2.0mu}u^{\sharp}\mspace{4.0mu};\mspace{2.0mu}(p^{\sharp})^{\ast}$
$\displaystyle\;=\eta\mspace{4.0mu};\mspace{2.0mu}(q^{\sharp})^{\ast}\mspace{4.0mu};\mspace{2.0mu}u^{\sharp},$

and we are done. ∎

###  VII. Proof of Theorem 6.2

The present construction is an improvement of a previous one [16, Theorem 18],
which we partially reuse here. Two important changes are responsible for
redesigning the previous argument: here we redefine DW-And, and make it an
axiom (instead of a rule, as before), and we restrict the use of DW-Uni, by
making more conservative assumptions about the subcategory $\mathbf{D}$.

The requisite mutual translations are as follows:

$\displaystyle\operatorname{\mathsf{\underline{while}}}\mathbin{\,}d\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}p=$
$\displaystyle\;(\operatorname{\mathsf{\underline{if}}}\mathbin{}d\operatorname{\mathsf{\underline{then}}}\mathbin{}p\mspace{4.0mu};\mspace{2.0mu}\operatorname{\mathsf{t\kern-0.45ptt}}\operatorname{\mathsf{\underline{else}}}\mathbin{\,}\operatorname{\mathsf{f\kern-0.78ptf}})^{\dagger},$
(16) $\displaystyle p^{\dagger}=$
$\displaystyle\;\operatorname{\mathsf{in_{1}}}\mspace{4.0mu};\mspace{2.0mu}(\operatorname{\mathsf{\underline{while}}}\mathbin{\,}(\operatorname{\mathsf{in_{0}}}\oplus\operatorname{\mathsf{in_{1}}})\mathbin{}\operatorname{\mathsf{\underline{do}}}\mathbin{\,}[\operatorname{\mathsf{in_{0}}},p])\mspace{4.0mu};\mspace{2.0mu}[1,\delta]$
(17)

where $\delta=\operatorname{\mathsf{in_{1}}}^{\dagger}$.

First, we show that the indicated translations are mutually inverse.

(i)
$(\operatorname{-\\!-})^{\dagger}\to\underline{\operatorname{\mathsf{while}}}\to(\operatorname{-\\!-})^{\dagger}$:
We need to show that