1–LABEL:LastPageOct. 12, 2017Sep. 05, 2018

This is the extended version of an article presented at MFPS XXXIII [16],
extended with proofs that previously appeared in the appendix, as well as new
sections on soundness, adequacy, and full abstraction.

# A categorical foundation for structured reversible flowchart languages:
Soundness and adequacy

Robert Glück  DIKU, Department of Computer Science, University of Copenhagen,
Denmark<EMAIL_ADDRESS>and  Robin Kaarsgaard<EMAIL_ADDRESS>
###### Abstract.

Structured reversible flowchart languages is a class of imperative reversible
programming languages allowing for a simple diagrammatic representation of
control flow built from a limited set of control flow structures. This class
includes the reversible programming language Janus (without recursion), as
well as more recently developed reversible programming languages such as
R-CORE and R-WHILE.

In the present paper, we develop a categorical foundation for this class of
languages based on inverse categories with joins. We generalize the notion of
extensivity of restriction categories to one that may be accommodated by
inverse categories, and use the resulting _decisions_ to give a reversible
representation of predicates and assertions. This leads to a categorical
semantics for structured reversible flowcharts, which we show to be
computationally sound and adequate, as well as equationally fully abstract
with respect to the operational semantics under certain conditions.

###### Key words and phrases:

Reversible computing, flowchart languages, structured programming, categorical
semantics, category theory

###### 1991 Mathematics Subject Classification:

D.3.1, F.3.2

The authors acknowledge the support given by _COST Action IC1405 Reversible
computation: Extending horizons of computing._ We also thank the anonymous
reviewers of MFPS XXXIII for their thoughtful and detailed comments on a
previous version of this paper.

##  1\. Introduction

Reversible computing is an emerging paradigm that adopts a physical principle
of reality into a _computation model without information erasure_. Reversible
computing extends the standard forward-only mode of computation with the
ability to execute in reverse as easily as forward. Reversible computing is a
necessity in the context of quantum computing and some bio-inspired
computation models. Regardless of the physical motivation, bidirectional
determinism is interesting in its own right. The potential benefits include
the design of innovative reversible architectures (e.g., [34, 33, 37]), new
programming models and techniques (e.g., [40, 17, 28]), and the enhancement of
software with reversibility (e.g., [8]).

Today the semantics of reversible programming languages are usually formalized
using traditional metalanguages, such as structural operational semantics or
denotational semantics based on complete partial orders (e.g., [19, 40]).
However, these metalanguages were introduced for the definition of
conventional (irreversible) programming languages. The fundamental properties
of a reversible language, such as the required backward determinism and the
invertibility of object language programs, are not naturally captured by these
metalanguages. As a result, these properties are to be shown for each semantic
definition. This unsatisfying state of affairs is not surprising, however, as
these properties have been rarely required for more than half a century of
mainstream language development. The recent advances in the area of reversible
computing have changed this situation.

This paper provides a new categorical foundation specifically for formalizing
reversible programming languages, in particular the semantics of reversible
structured flowchart languages [36, 39], which are the reversible counterpart
of the structured high-level programming languages used today. This
formalization is based on join inverse categories with a developed notion of
_extensivity_ for inverse categories, which gives rise to natural
representations of predicates and assertions, and consequently to models of
reversible structured flowcharts. It provides a framework for modelling
reversible languages, such that the reversible semantic properties of the
object language are naturally ensured by the metalanguage.

The semantic framework we are going to present in this paper covers the
reversible structured languages regardless of their concrete formation, such
as atomic operations, elementary predicates, and value domains. State of the
art reversible programming languages that are concretizations of this
computation model include the well-known imperative language Janus [40]
without recursion, the while languages R-WHILE and R-CORE with dynamic data
structures [19, 20], and the structured reversible language SRL with stacks
and arrays [39]. Structured control-flow is also a defining element of
reversible object-oriented languages [22]. Further, unstructured reversible
flowchart languages, such as reversible assembly languages with jumps [14, 4]
and the unstructured reversible language RL [39], can be transformed into
structured ones thanks to the structured reversible program theorem [36].

The main contribution of this paper is to provide a metalanguage formalism
based on join inverse categories that is geared to formalize the reversible
flowchart languages. The languages formalized in this framework are ensured to
have the defining reversible language properties, including backward
determinism and local invertibility. Another main property of the formalism is
that every reversible structured language that is syntactically closed under
inversion of its elementary operations is also closed under inversion of
reversible control-flow operators. This is particularly useful, as it is
sufficient to check this property for elementary constructs to ensure the
correctness of the associated program inverter. Key to our formalism are
decisions, which provide a particularly advantageous reversible representation
of predicates and their corresponding assertions. This insight may guide the
design of reversible constructs that are often quite involved to model in a
reversible setting, such as pattern matching.

The results in this paper are illustrated by introducing a family of small
reversible flowchart languages $\mathtt{RINT}_{k}$ for reversible computing
with integer data, a reversible counterpart of the family of classic counter
languages used for theoretical investigations into irreversible languages. The
family introduced here may well serve the same purpose in a reversible
context.

_Overview:_ In Section 2, we give an introduction to structured reversible
flowchart languages, while Section 3 describes the restriction and inverse
category theory used as backdrop in later sections. In Section 4, we warm up
by developing a notion of extensivity for inverse categories, based on
extensive restriction categories and its associated concept of _decisions_.
Then, in Section 5, we put it all to use by showing how decisions may be used
to model predicates and ultimately also reversible flowcharts, and we show
that these are computationally sound and adequate with respect to the
operational semantics in Section 6. In Section 7, we extend the previous
theorems by giving a sufficient condition for equational full abstraction. In
Section 8, we show how to verify program inversion using the categorical
semantics, develop a small language to exemplify our framework, and discuss
other applications in reversible programming. Section 9 offers some concluding
remarks.

##  2\. Reversible structured flowcharts

Structured reversible flowcharts [36, 39] naturally model the control flow
behavior of reversible (imperative) programming languages in a simple
diagrammatic representation, as classical flowcharts do for conventional
languages. A crucial difference is that atomic steps are limited to _partial
injective functions_ and they require an additional _assertion_ , an explicit
orthogonalizing condition, at join points in the control flow.

A structured reversible flowchart $F$ is built from four blocks (Figure 1): An
_atomic step_ that performs an elementary operation on a domain $X$ specified
by a partial injective function $a:X\rightharpoonup X$; a _while loop_ over a
block $B$ with entry assertion $p_{1}:X\rightarrow\mathit{Bool}$ and exit test
$p_{2}:X\rightarrow\mathit{Bool}$; a _selection_ of block $B_{1}$ or $B_{2}$
with entry test $p_{1}:X\rightarrow\mathit{Bool}$ and exit assertion
$p_{2}:X\rightarrow\mathit{Bool}$; and a _sequence_ of blocks $B_{1}$ and
$B_{2}$.

$a$

$p_{1}$ $\mathbf{t}$$\mathbf{f}$ $p_{2}$ $\mathbf{t}$$\mathbf{f}$25. $B$

$p_{1}$ $\mathbf{t}$$\mathbf{f}$25. $B_{1}$ $p_{2}$
$\mathbf{t}$$\mathbf{f}$25. $B_{2}$

25. $B_{1}$ 25. $B_{2}$

(a) Step

(b) While loop

(c) Selection

(d) Sequence

Figure 1. Structured reversible flowcharts.

A structured reversible flowchart $F$ consists of one main block. Blocks have
unique entry and exit points, and can be nested any number of times to form
more complex flowcharts. The interpretation of $F$ consists of a given domain
$X$ (typically of stores or states, which we shall denote by $\sigma$) and a
finite set of partial injective functions $a$ and predicates
$p:X\rightarrow\mathit{Bool}$. Computation starts at the entry point of $F$ in
an initial $x_{0}$ (the input), proceeds sequentially through the edges of
$F$, and ends at the exit point of $F$ in a final $x_{n}$ (the output), if $F$
is defined on the given input. Though the specific set of predicates depend on
the flowchart language, they are often (as we will do here) assumed to be
closed under Boolean operators, in particular conjunction and negation. The
operational semantics for these, shown in Figure 2, are the same as in the
irreversible case (see, e.g., [35]): We use the judgment form $\sigma\vdash
p\rightsquigarrow b$ here to mean that the predicate $p$ evaluated on the
state $\sigma$ results in the Boolean value $b$.

$\sigma\vdash p\rightsquigarrow b$

$\begin{gathered}\frac{}{\sigma\vdash\mathit{tt}\rightsquigarrow\mathit{tt}}\\\\[6.0pt]
\frac{\sigma\vdash
p\rightsquigarrow\mathit{tt}}{\sigma\vdash\mathbf{not}~{}p\rightsquigarrow\mathit{ff}}\\\\[6.0pt]
\frac{\sigma\vdash p\rightsquigarrow\mathit{tt}\qquad\sigma\vdash
q\rightsquigarrow\mathit{tt}}{\sigma\vdash
p~{}\mathbf{and}~{}q\rightsquigarrow\mathit{tt}}\\\\[6.0pt] \frac{\sigma\vdash
p\rightsquigarrow\mathit{ff}\qquad\sigma\vdash
q\rightsquigarrow\mathit{tt}}{\sigma\vdash
p~{}\mathbf{and}~{}q\rightsquigarrow\mathit{ff}}\end{gathered}\qquad\enspace\begin{gathered}\frac{}{\sigma\vdash\mathit{ff}\rightsquigarrow\mathit{ff}}\\\\[6.0pt]
\frac{\sigma\vdash
p\rightsquigarrow\mathit{ff}}{\sigma\vdash\mathbf{not}~{}p\rightsquigarrow\mathit{tt}}\\\\[6.0pt]
\frac{\sigma\vdash p\rightsquigarrow\mathit{tt}\qquad\sigma\vdash
q\rightsquigarrow\mathit{ff}}{\sigma\vdash
p~{}\mathbf{and}~{}q\rightsquigarrow\mathit{ff}}\\\\[6.0pt] \frac{\sigma\vdash
p\rightsquigarrow\mathit{ff}\qquad\sigma\vdash
q\rightsquigarrow\mathit{ff}}{\sigma\vdash
p~{}\mathbf{and}~{}q\rightsquigarrow\mathit{ff}}\end{gathered}$

Figure 2. Operational semantics for Boolean predicates.

The assertion $p_{1}$ in a reversible while loop (marked by a circle, as
introduced in [40]) is a new flowchart operator: the predicate $p_{1}$ must be
_true_ when the control flow reaches the assertion along the
$\mathbf{t}$-edge, and _false_ when it reaches the assertion along the
$\mathbf{f}$-edge; otherwise, the loop is undefined. The test $p_{2}$ (marked
by a diamond) has the usual semantics. This means that $B$ in a loop is
repeated as long as $p_{1}$ and $p_{2}$ are _false_.

The selection has an assertion $p_{2}$, which must be _true_ when the control
flow reaches the assertion from $B_{1}$, and _false_ when the control flow
reaches the assertion from $B_{2}$; otherwise, the selection is undefined. As
usual, the test $p_{1}$ selects $B_{1}$ or $B_{2}$. The assertion makes the
selection reversible.

Despite their simplicity, reversible structured flowcharts are _reversibly
universal_ [3], which means that they are computationally as powerful as any
reversible programming language can be. Given a suitable domain $X$ for finite
sets of atomic operations and predicates, there exists, for every injective
computable function $f:X\rightarrow Y$, a reversible flowchart $F$ that
computes $f$.

Reversible structured flowcharts (Figure 1) have a straightforward
representation as program texts defined by the grammar

$\begin{array}[t]{lclclclcl}B&::=&a&|&\mathbf{from}~{}p~{}\mathbf{loop}~{}B~{}\mathbf{until}~{}p&|&\mathbf{if}~{}p~{}\mathbf{then}~{}B~{}\mathbf{else}~{}B~{}\mathbf{fi}~{}p&|&B~{}\mathtt{;}~{}B\end{array}$

It is often assumed, as we will do here, that the set of atomic steps contains
a step $\mathbf{skip}$ that acts as the identity. The operational semantics
for these flowchart structures (or simply _commands_) are shown in Figure 3.
Here, the judgment form $\sigma\vdash c\downarrow\sigma^{\prime}$ is used and
taken to mean that the command $c$ converges in the state $\sigma$ resulting
in a new state $\sigma^{\prime}$. Note the use of the meta-command
$\mathit{\underline{loop}}[p,c,q]$: This does not represent any reversible
flowchart structure (and is thus not a syntactically valid command), but is
rather a piece of internal syntax used to give meaning to loops. This is
required since the role of the entry assertion in a reversible while loop
changes after the first iteration: When entering the loop from the outside
(_i.e._ , before any iterations have occured), the entry assertion must be
true, but when entering from the inside (_i.e._ , one or more iterations), the
entry assertion must be false.

$\sigma\vdash c\downarrow\sigma^{\prime}$

$\displaystyle\begin{gathered}\frac{\phantom{\vdash\downarrow}}{\sigma\vdash\mathbf{skip}\downarrow\sigma}\\\\[6.0pt]
\frac{\sigma\vdash p\rightsquigarrow\mathit{tt}\quad\enspace\sigma\vdash
c_{1}\downarrow\sigma^{\prime}\quad\enspace\sigma^{\prime}\vdash
q\rightsquigarrow\mathit{tt}}{\sigma\vdash\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\downarrow\sigma^{\prime}}\\\\[6.0pt]
\frac{\sigma\vdash p\rightsquigarrow\mathit{tt}\quad\enspace\sigma\vdash
q\rightsquigarrow\mathit{tt}}{\sigma\vdash\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}q\downarrow\sigma}\end{gathered}\qquad\enspace\begin{gathered}\frac{\sigma\vdash
c_{1}\downarrow\sigma^{\prime}\qquad\sigma^{\prime}\vdash
c_{2}\downarrow\sigma^{\prime\prime}}{\sigma\vdash
c_{1}~{}\mathtt{;}~{}c_{2}\downarrow\sigma^{\prime\prime}}\\\\[6.0pt]
\frac{\sigma\vdash p\rightsquigarrow\mathit{ff}\quad\enspace\sigma\vdash
c_{2}\downarrow\sigma^{\prime}\quad\enspace\sigma^{\prime}\vdash
q\rightsquigarrow\mathit{ff}}{\sigma\vdash\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\downarrow\sigma^{\prime}}\\\\[6.0pt]
\frac{\sigma\vdash p\rightsquigarrow\mathit{ff}\quad\enspace\sigma\vdash
q\rightsquigarrow\mathit{tt}}{\sigma\vdash\mathit{\underline{loop}}[p,c,q]\downarrow\sigma}\end{gathered}$
$\displaystyle\frac{\sigma\vdash
p\rightsquigarrow\mathit{ff}\quad\enspace\sigma\vdash
q\rightsquigarrow\mathit{ff}\quad\enspace\sigma\vdash
c\downarrow\sigma^{\prime}\quad\enspace\sigma^{\prime}\vdash\mathit{\underline{loop}}[p,c,q]\downarrow\sigma^{\prime\prime}}{\sigma\vdash\mathit{\underline{loop}}[p,c,q]\downarrow\sigma^{\prime\prime}}$
$\displaystyle\frac{\sigma\vdash
p\rightsquigarrow\mathit{tt}\quad\enspace\sigma\vdash
q\rightsquigarrow\mathit{ff}\quad\enspace\sigma\vdash
c\downarrow\sigma^{\prime}\quad\enspace\sigma^{\prime}\vdash\mathit{\underline{loop}}[p,c,q]\downarrow\sigma^{\prime\prime}}{\sigma\vdash\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}q\downarrow\sigma^{\prime\prime}}$

Figure 3. Operational semantics for the reversible flowchart structures.

The reversible structured flowcharts defined above corresponds to the
reversible language R-WHILE [19], but their value domain, atomic functions and
predicates are unspecified. As a minimum, a reversible flowchart needs blocks
(a), (b), and (d) from Figure 1, because selection can be simulated by
combining while loops that conditionally skip the body block or execute it
once. R-CORE [20] is an example of such a minimal language.

##  3\. Restriction and inverse categories

The following section contains the background on restriction and inverse
category theory necessary for our later developments. Unless otherwise
specified, the definitions and results presented in this section can be found
in introductory texts on the subject (e.g., [15, 21, 10, 11, 12]).

Restriction categories [10, 11, 12] axiomatize categories of partial maps.
This is done by assigning to each morphism $f$ a _restriction idempotent_
$\overline{f}$, which we think of as a partial identity defined precisely
where $f$ is. Formally, restriction categories are defined as follows. A
_restriction category_ is a category $\mathscr{C}$ equipped with a combinator
mapping each morphism $A\xrightarrow{f}B$ to a morphism
$A\xrightarrow{\overline{f}}A$ satisfying

  1. (i)

$f\overline{f}=f$,

  2. (ii)

$\overline{g}\overline{f}=\overline{f}\overline{g}$,

  3. (iii)

$\overline{f\overline{g}}=\overline{f}\overline{g}$, and

  4. (iv)

$\overline{g}f=f\overline{gf}$

for all suitable $g$. As an example, the category $\mathbf{Pfn}$ of sets and
partial functions is a restriction category, with $\overline{f}(x)=x$ if $f$
is defined at $x$, and undefined otherwise. Note that being a restriction
category is a structure, not a property; a category may be a restriction
category in several different ways (e.g., assigning $\overline{f}=\text{id}$
for each morphism $f$ gives a trivial restriction structure to any category).

In restriction categories, we say that a morphism $A\xrightarrow{f}B$ is
_total_ if $\overline{f}=\text{id}_{A}$, and a _partial isomorphism_ if there
exists a (necessarily unique) _partial inverse_ $B\xrightarrow{f^{\dagger}}A$
such that $f^{\dagger}f=\overline{f}$ and
$ff^{\dagger}=\overline{f^{\dagger}}$. Isomorphisms are then simply the total
partial isomorphisms with total partial inverses. An inverse category can then
be defined as a special kind of restriction category111This is a rather modern
definition due to [10]. Originally, inverse categories were defined as the
categorical extensions of inverse semigroups; see [27].. An _inverse category_
is a restriction category where each morphism is a partial isomorphism. Every
restriction category $\mathscr{C}$ gives rise to an inverse category
$\operatorname{Inv}(\mathscr{C})$ (the _cofree_ inverse category of
$\mathscr{C}$, see [26]), which has as objects all objects of $\mathscr{C}$,
and as morphisms all of the partial isomorphisms of $\mathscr{C}$. As such,
since partial isomorphisms in $\mathbf{Pfn}$ are partial injective functions,
a canonical example of an inverse category is the category
$\operatorname{Inv}(\mathbf{Pfn})\cong\mathbf{PInj}$ of sets and partial
injective functions.

Since each morphism in an inverse category has a unique partial inverse, as
also suggested by our notation this makes inverse categories canonically
_dagger categories_ [30], in the sense that they come equipped with a
contravariant endofunctor $(-)^{\dagger}$ satisfying $f=f^{\dagger\dagger}$
and $\text{id}_{A}^{\dagger}=\text{id}_{A}$ for each morphism $f$ and object
$A$.

Given two restriction categories $\mathscr{C}$ and $\mathscr{D}$, the well-
behaved functors between them are _restriction functors_ , _i.e._ , functors
$F$ satisfying $F(\overline{f})=\overline{F(f)}$. Analogous to how regular
semigroup homomorphisms preserve partial inverses in inverse semigroups, when
$\mathscr{C}$ and $\mathscr{D}$ are inverse categories, all functors between
them are restriction functors; specifically they preserve the canonical
dagger, _i.e._ , $F(f^{\dagger})=F(f)^{\dagger}$.

Before we move on, we show some basic facts about restriction idempotents in
restriction (and inverse) categories that will become useful later (see also,
e.g., [10, 15]).

######  Lemma 1.

In any restriction category, it is the case that

  1. (i)

$\overline{\text{id}}=\text{id}$,

  2. (ii)

$\overline{\overline{f}}=\overline{f}$,

  3. (iii)

$\overline{gf}~{}\overline{f}=\overline{gf}$,

  4. (iv)

$\overline{\overline{g}f}=\overline{gf}$,

  5. (v)

if $g$ is total then $\overline{gf}=\overline{f}$, and

  6. (vi)

if $gf$ is total then so is $f$.

for all morphisms $X\xrightarrow{f}Y$ and $Y\xrightarrow{g}Z$.

######  Proof 3.1.

For (i) $\text{id}=\text{id}~{}\overline{\text{id}}=\overline{\text{id}}$, and
(ii) by
$\overline{\overline{f}}=\overline{\text{id}\overline{f}}=\overline{\text{id}}~{}\overline{f}=\text{id}\overline{f}=\overline{f}$
using (i). For (iii) we have
$\overline{gf}~{}\overline{f}=\overline{gf\overline{f}}=\overline{gf}$, while
(iv) follows by
$\overline{\overline{g}f}=\overline{f\overline{gf}}=\overline{f}~{}\overline{gf}=\overline{gf}~{}\overline{f}=\overline{gf}$
using (iii). A special case of (iv) is (v) since $g$ total means that
$\overline{g}=\text{id}$, and so
$\overline{gf}=\overline{\overline{g}f}=\overline{\text{id}f}=\overline{f}$.
Finally, (vi) follows by $gf$ total means that $\overline{gf}=\text{id}$, so
by this and (iii),
$\text{id}=\overline{gf}=\overline{gf}~{}\overline{f}=\text{id}\overline{f}=\overline{f}$,
so $f$ is total as well.

###  3.1. Partial order enrichment and joins

A consequence of how restriction (and inverse) categories are defined is that
hom sets $\mathscr{C}(A,B)$ may be equipped with a partial order given by
$f\leq g$ iff $g\overline{f}=f$ (this extends to an enrichment in the category
of partial orders and monotone functions). Intuitively, this states that $f$
is below $g$ iff $g$ behaves exactly like $f$ when restricted to the points
where $f$ is defined. Notice that any morphism $e$ below an identity
$\text{id}_{X}$ is a restriction idempotent under this definition, since
$e\leq\text{id}_{X}$ iff $\text{id}_{X}\overline{e}=e$, _i.e._ , iff
$\overline{e}=e$.

A sufficient condition for each $\mathscr{C}(A,B)$ to have a least element is
that $\mathscr{C}$ has a _restriction zero_ ; a zero object $0$ in the usual
sense which additionally satisfies
$A\xrightarrow{0_{A,A}}A=A\xrightarrow{\overline{0_{A,A}}}A$ for each endo-
zero map $0_{A,A}$. One may now wonder when $\mathscr{C}(A,B)$ has joins as a
partial order. Unfortunately, $\mathscr{C}(A,B)$ has joins of all morphisms
only in very degenerate cases. However, if instead of considering arbitrary
joins we consider joins of maps that are somehow compatible, this becomes much
more viable. In a restriction category, say that morphisms $X\xrightarrow{f}Y$
and $X\xrightarrow{g}Y$ are _disjoint_ iff $f\overline{g}=0$; and _compatible_
iff $f\overline{g}=g\overline{f}$. It can be shown that disjointness implies
compatibility, as disjointness is expectedly symmetric. Further, we may extend
this to say that a set of parallel morphisms is disjoint iff each pair of
morphisms is disjoint, and likewise for compatibility. This gives suitable
notions of _join restriction categories_. A restriction category $\mathscr{C}$
has compatible (disjoint) joins if it has a restriction zero, and satisfies
that for each compatible (disjoint) subset $S$ of any hom set
$\mathscr{C}(A,B)$, there exists a morphism $\bigvee_{s\in S}s$ such that

  1. (i)

$s\leq\bigvee_{s\in S}s$ for all $s\in S$, and $s\leq t$ for all $s\in S$
implies $\bigvee_{s\in S}s\leq t$;

  2. (ii)

$\overline{\bigvee_{s\in S}s}=\bigvee_{s\in S}\overline{s}$;

  3. (iii)

$f\left(\bigvee_{s\in S}s\right)=\bigvee_{s\in S}(fs)$ for all $f:B\to X$; and

  4. (iv)

$\left(\bigvee_{s\in S}s\right)g=\bigvee_{s\in S}(sg)$ for all $g:Y\to A$.

For inverse categories, the situation is a bit more tricky, as the join of two
compatible partial isomorphisms may not be a partial isomorphism. To ensure
this, we need stronger relations: In an inverse category, say that parallel
maps $f$ and $g$ are _disjoint_ iff $f\overline{g}=0$ and
$f^{\dagger}\overline{g^{\dagger}}=0$; and _compatible_ iff
$f\overline{g}=g\overline{f}$ and
$f^{\dagger}\overline{g^{\dagger}}=g^{\dagger}\overline{f^{\dagger}}$. We may
now extend this to notions of disjoint sets and compatible sets of morphisms
in inverse categories as before. This finally gives notions of _join inverse
categories_ : An inverse category $\mathscr{C}$ has compatible (disjoint)
joins if it has a restriction zero and satisfies that for all compatible
(disjoint) subsets $S$ of all hom sets $\mathscr{C}(A,B)$, there exists a
morphism $\vee_{s\in S}s$ satisfying (i) – (iv) of Definition 3.1. An example
of a join inverse category is $\mathbf{PInj}$ of sets and partial injective
functions. Here, $\bigvee_{f\in S}f$ for a set of compatible partial injective
functions $S$ is constructed as the function with graph the union of the
graphs of all $f\in S$; or equivalently as the function

$\left(\bigvee_{f\in S}f\right)(x)=\left\\{\begin{array}[]{ll}g(x)&\text{if
there exists $g\in S$ such that $g(x)$ is defined}\\\
\text{undefined}&\text{otherwise}\end{array}\right.$

Similarly, the category $\mathbf{PHom}$ of topological spaces and partial
homeomorphisms (_i.e._ , partial injective functions which are open and
continuous in their domain of definition) is an inverse category with joins
constructed in the same way. Further, for any join restriction category
$\mathscr{C}$, the cofree inverse category $\operatorname{Inv}(\mathscr{C})$
of $\mathscr{C}$ is a join inverse category as well [21, Lemma 3.1.27], and
joins on both restriction and inverse categories can be freely adjoined [21,
Sec. 3.1]. A functor $F$ between restriction (or inverse) categories with
joins is said to be join-preserving when $F(\bigvee_{s\in S}s)=\bigvee_{s\in
S}F(s)$.

###  3.2. Restriction coproducts, extensivity, and related concepts

While a restriction category may very well have coproducts, these are
ultimately only well-behaved when the coproduct injections
$A\xrightarrow{\kappa_{1}}A+B$ and $B\xrightarrow{\kappa_{2}}A+B$ are total;
if this is the case, we say that the restriction category has _restriction
coproducts_. If a restriction category has all finite restriction coproducts,
it also has a restriction zero serving as unit. Note that in restriction
categories with restriction coproducts, the coproduct injections $\kappa_{1}$
(respectively $\kappa_{2}$) are partial isomorphisms with partial inverse
$\kappa_{1}^{\dagger}=A+B\xrightarrow{[\text{id}_{A},0_{B,A}]}A$ (respectively
$\kappa_{2}^{\dagger}=A+B\xrightarrow{[0_{A,B},\text{id}_{B}]}A$).

In [12], it is shown that the existence of certain maps, called _decisions_ ,
in a restriction category $\mathscr{C}$ with restriction coproducts leads to
the subcategory $\operatorname{Total}(\mathscr{C})$ of total maps being
extensive (in the sense of, e.g., [7]). This leads to the definition of an
_extensive restriction category_ 222The name is admittedly mildly confusing,
as an extensive restriction category is not extensive in the usual sense.
Nevertheless, we stay with the established terminology.. A restriction
category is said to be _extensive_ (as a restriction category) if it has
restriction coproducts and a restriction zero, and for each map
$A\xrightarrow{f}B+C$ there is a unique _decision_ $A\xrightarrow{\langle
f\rangle}A+A$ satisfying

(D.1):

$\nabla\langle f\rangle=\overline{f}$ and

(D.2):

$(f+f)\langle f\rangle=(\kappa_{1}+\kappa_{2})f$.

In the above, $\nabla$ denotes the codiagonal $[\text{id},\text{id}]$. A
consequence of these axioms is that each decision is a partial isomorphism;
one can show that $\langle f\rangle$ must be partial inverse to
$[\overline{\kappa_{1}^{\dagger}f},\overline{\kappa_{2}^{\dagger}f}]$ (see
[12]). Further, when a restriction category with restriction coproducts has
finite joins, it is also extensive with $\langle
f\rangle=(\kappa_{1}\overline{\kappa_{1}^{\dagger}f})\vee(\kappa_{2}\overline{\kappa_{2}^{\dagger}f})$.
As an example, $\mathbf{Pfn}$ is extensive with $A\xrightarrow{\langle
f\rangle}A+A$ for $A\xrightarrow{f}B+C$ given by

$\langle f\rangle(x)=\left\\{\begin{array}[]{ll}\kappa_{1}(x)&\text{if
$f(x)=\kappa_{1}(y)$ for some $y\in B$}\\\ \kappa_{2}(x)&\text{if
$f(x)=\kappa_{2}(z)$ for some $z\in C$}\\\ \text{undefined}&\text{if $f(x)$ is
undefined}\end{array}\right..$

While inverse categories only have coproducts (much less restriction
coproducts) in very degenerate cases (see [15]), they may very well be
equipped with a more general sum-like symmetric monoidal tensor, a
disjointness tensor.

A _disjointness tensor_ on a restriction category is a symmetric monoidal
restriction functor $-\oplus-$ satisfying that its unit is the restriction
zero, and that the canonical maps

$\amalg_{1}=A\xrightarrow{\rho^{-1}}A\oplus
0\xrightarrow{\text{id}\oplus\text{0}}A\oplus
B\qquad\qquad\amalg_{2}=B\xrightarrow{\lambda^{-1}}0\oplus
B\xrightarrow{\text{0}\oplus\text{id}}A\oplus B$

are jointly epic, where $\rho$ respectively $\lambda$ is the left respectively
right unitor of the monoidal functor $-\oplus-$.

It can be straightforwardly shown that any restriction coproduct gives rise to
a disjointness tensor. A useful interaction between compatible joins and a
join-preserving disjointness tensor in inverse categories was shown in [5,
26], namely that it leads to a $\dagger$-trace (in the sense of [24, 31]):

######  Proposition 2.

Let $\mathscr{C}$ be an inverse category with (at least countable) compatible
joins and a join-preserving disjointness tensor. Then $\mathscr{C}$ has a
trace operator given by

$\operatorname{Tr}_{A,B}^{U}(f)=f_{11}\vee\bigvee_{n\in\omega}f_{21}f_{22}^{n}f_{12}$

satisfying
$\operatorname{Tr}_{A,B}^{U}(f)^{\dagger}=\operatorname{Tr}_{A,B}^{U}(f^{\dagger})$,
where $f_{ij}=\amalg_{j}^{\dagger}f\amalg_{i}$.

##  4\. Extensivity of inverse categories

As discussed earlier, extensivity of restriction categories hinges on the
existence of certain partial isomorphisms – decisions – yet their
axiomatization relies on the presence of a map that is not a partial
isomorphism, the codiagonal.

In this section, we tweak the axiomatization of extensivity of restriction
categories to one that is equivalent, but additionally transports more easily
to inverse categories. We then give a definition of extensitivity for inverse
categories, from which it follows that $\operatorname{Inv}(\mathscr{C})$ is an
extensive inverse category when $\mathscr{C}$ is an extensive restriction
category.

Recall that decisions satisfy the following two axioms:

(D.1):

$\nabla\langle f\rangle=\overline{f}$ and

(D.2):

$(f+f)\langle f\rangle=(\kappa_{1}+\kappa_{2})f$

As mentioned previously, an immediate problem with this is the reliance on the
codiagonal. However, intuitively, what (D.1) states is simply that the
decision $\langle f\rangle$ cannot do anything besides to tag its inputs
appropriately. Using a disjoint join, we reformulate this axiom to the
following:

(D’.1):

$(\kappa_{1}^{\dagger}\langle f\rangle)\vee(\kappa_{2}^{\dagger}\langle
f\rangle)=\overline{f}$

Note that this axiom also subtly states that disjoint joins of the given form
always exist.

Say that a restriction category is _pre-extensive_ if it has restriction
coproducts, a restriction zero, and a combinator mapping each map
$A\xrightarrow{f}B+C$ to a _pre-decision_ $A\xrightarrow{\langle f\rangle}A+A$
(with no additional requirements). We can then show the following:

######  Theorem 3.

Let $\mathscr{C}$ be a pre-extensive restriction category. The following are
equivalent:

  1. (i)

$\mathscr{C}$ is an extensive restriction category.

  2. (ii)

Every pre-decision of $\mathscr{C}$ satisfies (D.1) and (D.2).

  3. (iii)

Every pre-decision of $\mathscr{C}$ satisfies (D’.1) and (D.2).

To show this theorem, we will need the following lemma:

######  Lemma 4.

In an extensive restriction category, joins of the form $(f+0)\vee(0+g)$ exist
for all maps $A\xrightarrow{f}B$ and $C\xrightarrow{g}D$ and are equal to
$f+g$.

######  Proof 4.1.

By [9], for any map $A\xrightarrow{h}B+C$ in an extensive restriction
category,
$h=(\overline{\kappa_{1}^{\dagger}}~{}h)\vee(\overline{\kappa_{2}^{\dagger}}~{}h)$.
But then
$f+g=(\overline{\kappa_{1}^{\dagger}}(f+g))\vee(\overline{\kappa_{2}^{\dagger}}(f+g))=((\text{id}+\text{0})(f+g))\vee((\text{0}+\text{id})(f+g))=(f+\text{0})\vee(\text{0}+g)$.

We can now continue with the proof.

######  Proof 4.2.

The equivalence between (i) and (ii) was given in [12]. That (ii) and (iii)
are equivalent follows by

$\displaystyle(\kappa_{1}^{\dagger}\langle
f\rangle)\vee(\kappa_{2}^{\dagger}\langle f\rangle)$
$\displaystyle=([\text{id},\text{0}]\langle
f\rangle)\vee([\text{0},\text{id}]\langle f\rangle)$
$\displaystyle=(\nabla(\text{id}+\text{0})\langle
f\rangle)\vee(\nabla(\text{0}+\text{id})\langle f\rangle)$
$\displaystyle=\nabla((\text{id}+\text{0})\vee(\text{0}+\text{id}))\langle
f\rangle$ $\displaystyle=\nabla(\text{id}+\text{id})\langle
f\rangle=\nabla\langle f\rangle$

where we note that the join $(\text{id}+\text{0})\vee(\text{0}+\text{id})$
exists and equals $\text{id}+\text{id}$ when every pre-decision satisfies
(D.1) and (D.2) by Lemma 4. That the join also exists when every pre-decision
satisfies (D’.1) and (D.2) follows as well, since the universal mapping
property for coproducts guarantees that the only map $g$ satisfying
$((\kappa_{1}+\kappa_{2})+(\kappa_{1}+\kappa_{2}))g=(\kappa_{1}+\kappa_{2})(\kappa_{1}+\kappa_{2})$
is $\kappa_{1}+\kappa_{2}$ itself, so we must have
$\langle\kappa_{1}+\kappa_{2}\rangle=\kappa_{1}+\kappa_{2}$, and

$\displaystyle(\text{id}+\text{0})\vee(\text{0}+\text{id})$
$\displaystyle=\overline{\kappa_{1}^{\dagger}}\vee\overline{\kappa_{2}^{\dagger}}=(\kappa_{1}\kappa_{1}^{\dagger})\vee(\kappa_{2}\kappa_{2}^{\dagger})$
$\displaystyle=(\kappa_{1}^{\dagger}(\kappa_{1}+\kappa_{2}))\vee(\kappa_{2}^{\dagger}(\kappa_{1}+\kappa_{2}))$
$\displaystyle=\overline{\kappa_{1}+\kappa_{2}}=\text{id}+\text{id}$

which was what we wanted.

Another subtle consequence of our amended first rule is that
$\kappa_{1}^{\dagger}\langle f\rangle$ is its own restriction idempotent (and
likewise for $\kappa_{2}^{\dagger}\langle f\rangle$) since
$\kappa_{1}^{\dagger}\langle f\rangle\leq(\kappa_{1}^{\dagger}\langle
f\rangle)\vee(\kappa_{2}^{\dagger}\langle
f\rangle)=\overline{f}\leq\text{id}$, as the maps below identity are precisely
the restriction idempotents.

Our next snag in transporting this definition to inverse categories has to do
with the restriction coproducts themselves, as it is observed in [15] that any
inverse category with restriction coproducts is a preorder. Intuitively, the
problem is not that unicity of coproduct maps cannot be guaranteed in non-
preorder inverse categories, but rather that the coproduct map
$A+B\xrightarrow{[f,g]}C$ in a restriction category is not guaranteed to be a
partial isomorphism when $f$ and $g$ are.

For this reason, we will consider the more general disjointness tensor for
sum-like constructions rather than full-on restriction coproducts, as inverse
categories may very well have a disjointness tensor without it leading to
immediate degeneracy. Notably, $\mathbf{PInj}$ has a disjointness tensor,
constructed on objects as the disjoint union of sets (precisely as the
restriction coproduct in $\mathbf{Pfn}$, but without the requirement of a
universal mapping property). This leads us to the following definition:

An inverse category with a disjointness tensor is said to be _extensive_ when
each map $A\xrightarrow{f}B\oplus C$ has a unique decision
$A\xrightarrow{\langle f\rangle}A\oplus A$ satisfying

(D’.1):

$(\amalg_{1}^{\dagger}\langle f\rangle)\vee(\amalg_{2}^{\dagger}\langle
f\rangle)=\overline{f}$

(D’.2):

$(f\oplus f)\langle f\rangle=(\amalg_{1}\oplus\amalg_{2})f$.

As an example, $\mathbf{PInj}$ is an extensive inverse category with the
unique decision $A\xrightarrow{\langle f\rangle}A\oplus A$ for a partial
injection $A\xrightarrow{f}B\oplus C$ given by

$\langle f\rangle(x)=\left\\{\begin{array}[]{ll}\amalg_{1}(x)&\text{if}\
f(x)=\amalg_{1}(y)\ \text{for some $y\in B$}\\\ \amalg_{2}(x)&\text{if}\
f(x)=\amalg_{2}(z)\ \text{for some $z\in C$}\\\ \text{undefined}&\text{if
$f(x)$ is undefined}\end{array}\right.\enspace.$

Aside from a shift from coproduct injections to the quasi-injections of the
disjointness tensor, a subtle change here is the notion of join. That is, for
restriction categories with disjoint joins, any pair of maps $f,g$ with
$f\overline{g}=0$ has a join – but for inverse categories, we additionally
require that their _inverses_ are disjoint as well, _i.e._ , that
$f^{\dagger}\overline{g^{\dagger}}=0$, for the join to exist. In this case,
however, there is no difference between the two. As previously discussed, a
direct consequence of this axiom is that each $\amalg_{i}^{\dagger}\langle
f\rangle$ must be its own restriction idempotent. Since restriction
idempotents are self-adjoint (_i.e._ , satisfy $f=f^{\dagger}$), they are
disjoint iff their inverses are disjoint.

Since restriction coproducts give rise to a disjointness tensor, we may
straightforwardly show the following theorem.

######  Theorem 5.

When $\mathscr{C}$ is an extensive restriction category,
$\operatorname{Inv}(\mathscr{C})$ is an extensive inverse category.

Further, constructing the decision $\langle f\rangle$ as
$(\amalg_{1}\overline{\amalg_{1}^{\dagger}f})\vee(\amalg_{2}\overline{\amalg_{2}^{\dagger}f})$
(_i.e._ , mirroring the construction of decisions in restriction categories
with disjoint joins), we may show the following.

######  Theorem 6.

Let $\mathscr{C}$ be an inverse category with a disjointness tensor, a
restriction zero, and finite disjoint joins which are further preserved by the
disjointness tensor. Then $\mathscr{C}$ is extensive as an inverse category.

Before we proceed, we show two small lemmas regarding decisions and the (join
preserving) disjointness tensor (for the latter, see also [15]).

######  Lemma 7.

In any inverse category with a disjointness tensor, it is the case that

  1. (i)

$\overline{\amalg_{1}}=\overline{\amalg_{2}}=\text{id}$,

  2. (ii)

$\overline{\amalg_{1}^{\dagger}}=\text{id}\oplus 0$ and
$\overline{\amalg_{2}^{\dagger}}=0\oplus\text{id}$,

  3. (iii)

$\amalg_{j}^{\dagger}\amalg_{i}=\text{id}$ if $i=j$ and
$\amalg_{j}^{\dagger}\amalg_{i}=0$ otherwise.

######  Proof 4.3.

For (i), adding subscripts on identities and zero maps for clarity,

$\displaystyle\overline{\amalg_{1}}$
$\displaystyle=\overline{(\text{id}_{X}\oplus
0_{0,Y})\rho^{-1}}=\overline{\overline{(\text{id}_{X}\oplus
0_{0,Y})}\rho^{-1}}=\overline{(\overline{\text{id}_{X}}\oplus\overline{0_{0,Y}})\rho^{-1}}=\overline{(\text{id}_{X}\oplus
0_{0,0})\rho^{-1}}$
$\displaystyle=\overline{(\text{id}_{X}\oplus\text{id}_{0})\rho^{-1}}=\overline{\text{id}_{X\oplus
0}~{}\rho^{-1}}=\overline{\rho^{-1}}=\text{id}_{X}$

and analogously for $\overline{\amalg_{2}}$. For (ii),

$\overline{\amalg_{1}^{\dagger}}=\overline{((\text{id}\oplus
0)\rho^{-1})^{\dagger}}=\overline{\rho(\text{id}^{\dagger}\oplus
0^{\dagger})}=\overline{\overline{\rho}(\text{id}\oplus
0)}=\overline{\text{id}~{}(\text{id}\oplus 0)}=\overline{\text{id}\oplus
0}=\text{id}\oplus 0$

and again, the proof for $\amalg_{2}$ is analogous. To show (iii) when $i=j$

$\displaystyle\amalg_{1}^{\dagger}\amalg_{1}$
$\displaystyle=\rho(\text{id}_{X}\oplus 0_{Y,0})(\text{id}_{X}\oplus
0_{0,Y})\rho^{-1}=\rho(\text{id}_{X}\oplus
0_{0,0})\rho^{-1}=\rho(\text{id}_{X}\oplus\text{id}_{0})\rho^{-1}$
$\displaystyle=\rho~{}\text{id}_{X\oplus
0}~{}\rho^{-1}=\rho\rho^{-1}=\text{id}_{X}$

and similarly for $\amalg_{2}^{\dagger}\amalg_{2}=\text{id}$ (noting that
$0_{Y,0}0_{0,Y}=0_{0,0}=\text{id}_{0}$ follows by the universal mapping
property of the zero object $0$). For $i\neq j$, we proceed with the case
where $i=1$ and $j=2$, yielding

$\displaystyle\amalg_{2}^{\dagger}\amalg_{1}=\rho(0_{X,0}\oplus\text{id}_{Y})(\text{id}_{X}\oplus
0_{0,Y})\rho^{-1}=\rho(0_{X,0}\oplus 0_{0,Y})\rho^{-1}=\rho~{}0_{X\oplus
0,0\oplus Y}~{}\rho^{-1}=0_{X,Y}$

where $0_{X,0}\oplus 0_{0,Y}=0_{X\oplus 0,0\oplus Y}$ follows by the fact that
$0_{X,0}\oplus 0_{0,Y}$ factors through $0\oplus 0$ (by the universal mapping
property of $0$) and the fact that $0\oplus 0\cong 0$ (since $0$ serves as
unit for $-\oplus-$), so $0_{X,0}\oplus 0_{0,Y}$ factors through $0$ as well.
The case where $i=2$ and $j=1$ is entirely analogous.

######  Lemma 8.

In any extensive inverse category, it is the case that

  1. (i)

$\overline{\amalg_{1}^{\dagger}\langle f\rangle}=\amalg_{1}^{\dagger}\langle
f\rangle$,

  2. (ii)

$\overline{\amalg_{1}^{\dagger}}\vee\overline{\amalg_{2}^{\dagger}}=\text{id}$,

  3. (iii)

$\langle f\rangle=(\amalg_{1}\overline{\amalg_{1}^{\dagger}\langle
f\rangle})\vee(\amalg_{2}\overline{\amalg_{2}^{\dagger}\langle f\rangle})$,
and

  4. (iv)

$\overline{f}=\overline{\langle f\rangle}$.

######  Proof 4.4.

To show (i), we have by definition of the join that
$\amalg_{1}^{\dagger}\langle f\rangle\leq(\amalg_{1}^{\dagger}\langle
f\rangle)\vee(\amalg_{2}^{\dagger}\langle f\rangle)=\overline{f}$, where the
equality follows precisely by the first axiom of decisions. Since
$\overline{f}\leq\text{id}$ by $\text{id}\overline{\overline{f}}=\overline{f}$
(since $\overline{\overline{f}}=\overline{f}$ by Lemma 1), it follows by
transitivity of $-\leq-$ (since it is a partial order) that
$\amalg_{1}^{\dagger}\langle f\rangle\leq\text{id}$. But since $f\leq g$ iff
$g\overline{f}=f$, it follows from $\amalg_{1}^{\dagger}\langle
f\rangle\leq\text{id}$ that $\overline{\amalg_{1}^{\dagger}\langle
f\rangle}=\text{id}~{}\overline{\amalg_{1}^{\dagger}\langle
f\rangle}=\amalg_{1}^{\dagger}\langle f\rangle$.

For (ii), using Lemma 7 we start by noting that

$\overline{\amalg_{1}^{\dagger}(\amalg_{1}\oplus\amalg_{2})}=\overline{\overline{\amalg_{1}^{\dagger}}(\amalg_{1}\oplus\amalg_{2})}=\overline{(\text{id}\oplus
0)(\amalg_{1}\oplus\amalg_{2})}=\overline{\amalg_{1}\oplus
0}=\overline{\amalg_{1}}\oplus\overline{0}=\text{id}\oplus
0=\overline{\amalg_{1}^{\dagger}}$

and similarly

$\overline{\amalg_{2}^{\dagger}(\amalg_{1}\oplus\amalg_{2})}=\overline{\overline{\amalg_{2}^{\dagger}}(\amalg_{1}\oplus\amalg_{2})}=\overline{(0\oplus\text{id})(\amalg_{1}\oplus\amalg_{2})}=\overline{0\oplus\amalg_{2}}=\overline{0}\oplus\overline{\amalg_{2}}=0\oplus\text{id}=\overline{\amalg_{2}^{\dagger}}$

and since
$\langle\amalg_{1}\oplus\amalg_{2}\rangle=\amalg_{1}\oplus\amalg_{2}$, we have

$\displaystyle\overline{\amalg_{1}^{\dagger}}\vee\overline{\amalg_{2}^{\dagger}}$
$\displaystyle=\overline{\amalg_{1}^{\dagger}(\amalg_{1}\oplus\amalg_{2})}\vee\overline{\amalg_{2}^{\dagger}(\amalg_{1}\oplus\amalg_{2})}=\overline{\amalg_{1}^{\dagger}\langle\amalg_{1}\oplus\amalg_{2}\rangle}\vee\overline{\amalg_{2}^{\dagger}\langle\amalg_{1}\oplus\amalg_{2}\rangle}$
$\displaystyle=\overline{\overline{\amalg_{1}\oplus\amalg_{2}}}=\overline{\amalg_{1}\oplus\amalg_{2}}=\overline{\amalg_{1}}\oplus\overline{\amalg_{2}}=\text{id}\oplus\text{id}=\text{id}.$

Using this, we may prove (iii) (and later (iv)) as follows:

$\displaystyle\langle f\rangle$ $\displaystyle=\text{id}\langle
f\rangle=(\overline{\amalg_{1}^{\dagger}}\vee\overline{\amalg_{2}^{\dagger}})\langle
f\rangle=(\overline{\amalg_{1}^{\dagger}}\langle
f\rangle)\vee(\overline{\amalg_{2}^{\dagger}}\langle
f\rangle)=(\amalg_{1}\amalg_{1}^{\dagger}\langle
f\rangle)\vee(\amalg_{2}\amalg_{2}^{\dagger}\langle f\rangle)$
$\displaystyle=(\amalg_{1}\overline{\amalg_{1}^{\dagger}\langle
f\rangle})\vee(\amalg_{2}\overline{\amalg_{2}^{\dagger}\langle f\rangle})$

where $\amalg_{1}^{\dagger}\langle
f\rangle=\overline{\amalg_{1}^{\dagger}\langle f\rangle}$ follows by (i).
Using these again, we show (iv) by

$\displaystyle\overline{f}$ $\displaystyle=(\amalg_{1}^{\dagger}\langle
f\rangle)\vee(\amalg_{2}^{\dagger}\langle
f\rangle)=\overline{\amalg_{1}^{\dagger}\langle
f\rangle}\vee\overline{\amalg_{2}^{\dagger}\langle
f\rangle}=\overline{\overline{\amalg_{1}^{\dagger}}\langle
f\rangle}\vee\overline{\overline{\amalg_{2}^{\dagger}}\langle
f\rangle}=\overline{(\overline{\amalg_{1}^{\dagger}}\langle
f\rangle)\vee(\overline{\amalg_{2}^{\dagger}}\langle f\rangle)}$
$\displaystyle=\overline{(\overline{\amalg_{1}^{\dagger}}\vee\overline{\amalg_{2}^{\dagger}})\langle
f\rangle)}=\overline{\text{id}\langle f\rangle}=\overline{\langle f\rangle}$

which was what we wanted.

##  5\. Modelling structured reversible flowcharts

In the following, let $\mathscr{C}$ be an inverse category with (at least
countable) compatible joins and a join-preserving disjointness tensor. As
disjoint joins are compatible, it follows that $\mathscr{C}$ is an extensive
inverse category with a (uniform) $\dagger$-trace operator.

In this section, we will show how this framework can be used model reversible
structured flowchart languages. First, we will show how decisions in extensive
inverse categories can be used to model predicates, and then how this
representation extends to give very natural semantics to reversible flowcharts
corresponding to conditionals and loops.

###  5.1. Predicates as decisions

In suitably equipped categories, one naturally considers predicates on an
object $A$ as given by maps $A\to 1+1$. In inverse categories, however, the
mere idea of a predicate as a map of the form $A\to 1\oplus 1$ is problematic,
as only very degenerate maps of this form are partial isomorphisms. In the
following, we show how decisions give rise to an unconventional yet ultimately
useful representation of predicates. To our knowledge this representation is
novel, motivated here by the necessity to model predicates in a reversible
fashion, as decisions are always partial isomorphisms.

The simplest useful predicates are the predicates that are always true
(respectively always false). By convention, we represent these by the left
(respectively right) injection (which are both their own decisions),

$\displaystyle\left\llbracket\mathit{tt}\right\rrbracket$
$\displaystyle=\amalg_{1}$
$\displaystyle\left\llbracket\mathit{ff}\right\rrbracket$
$\displaystyle=\amalg_{2}.$

Semantically, we may think of decisions as a separation of an object $A$ into
_witnesses_ and _counterexamples_ of the predicate it represents. In a certain
sense, the axioms of decisions say that there is nothing more to a decision
than how it behaves when postcomposed with $\amalg_{1}^{\dagger}$ or
$\amalg_{2}^{\dagger}$. As such, given the convention above, we think of
$\amalg_{1}^{\dagger}\langle p\rangle$ as the witnesses of the predicate
represented by the decision $\langle p\rangle$, and
$\amalg_{2}^{\dagger}\langle p\rangle$ as its counterexamples.

With this in mind, we turn to boolean combinators. The negation of a
predicate-as-a-decision must simply swap witnesses for counterexamples (and
vice versa). In other words, we obtain the negation of a decision by
postcomposing with the commutator $\gamma$ of the disjointness tensor,

$\left\llbracket\mathbf{not}~{}p\right\rrbracket=\gamma\left\llbracket
p\right\rrbracket.$

With this, it is straightforward to verify that, e.g.,
$\left\llbracket\mathbf{not}~{}\mathit{tt}\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket$,
as

$\left\llbracket\mathbf{not}~{}\mathit{tt}\right\rrbracket=\gamma\amalg_{1}=\gamma(\text{id}\oplus\text{0})\rho^{-1}=(\text{0}\oplus\text{id})\gamma\rho^{-1}=(\text{0}\oplus\text{id})\lambda^{-1}=\amalg_{2}=\left\llbracket\mathit{ff}\right\rrbracket.$

For conjunction, we exploit that our category has (specifically) finite
disjoint joins, and define the conjunction of predicates-as-decisions
$\left\llbracket p\right\rrbracket$ and $\left\llbracket q\right\rrbracket$ by

$\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket=\left((\amalg_{1}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket})\vee(\amalg_{2}(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket}))\right)\overline{\left\llbracket
p\right\rrbracket}~{}\overline{\left\llbracket q\right\rrbracket}.$

The intuition behind this definition is that the witnesses of a conjunction of
predicates is given by the meet of the witnesses of the each predicate, while
the counterexamples of a conjunction of predicates is the join of the
counterexamples of each predicate. Note that this is then precomposed with
$\overline{\left\llbracket p\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket}$ to ensure that the result is only defined where both $p$
and $q$ are; this gives

Noting that the meet of two restriction idempotents is given by their
composition, this is precisely what this definition states. Similarly we
define the disjunction of $\left\llbracket p\right\rrbracket$ and
$\left\llbracket q\right\rrbracket$ by

$\left\llbracket
p~{}\mathbf{or}~{}q\right\rrbracket=\left((\amalg_{1}(\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}\vee\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket}))\vee(\amalg_{2}\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}~{}\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket})\right)\overline{\left\llbracket
p\right\rrbracket}~{}\overline{\left\llbracket q\right\rrbracket},$

as $\left\llbracket p~{}\mathbf{or}~{}q\right\rrbracket$ then has as witnesses
the join of the witnesses of $\left\llbracket p\right\rrbracket$ and
$\left\llbracket q\right\rrbracket$, and as counterexamples the meet of the
counterexamples of $\left\llbracket p\right\rrbracket$ and $\left\llbracket
q\right\rrbracket$. With these definitions, it can be shown that, e.g., the De
Morgan laws are satisfied. However, since we can thus construct this from
conjunctions and negations, we will leave disjunctions as syntactic sugar.

That all of these are indeed decisions can be shown straightforwardly, as
summarized in the following closure theorem.

######  Theorem 9.

Decisions in $\mathscr{C}$ are closed under Boolean negation, conjunction, and
disjunction.

###  5.2. Reversible structured flowcharts, categorically

To give a categorical account of structured reversible flowchart languages, we
assume the existence of a suitable distinguished object $\Sigma$ of stores,
which we think of as the _domain of computation_ , such that we may give
denotations to structured reversible flowcharts as morphisms
$\Sigma\to\Sigma$.

Since atomic steps (corresponding to elementary operations, e.g., store
updates) may vary from language to language, we assume that each such atomic
step in our language has a denotation as a morphism $\Sigma\to\Sigma$. In the
realm of reversible flowcharts, these atomic steps are required to be partial
injective functions; here, we abstract this to require that their denotation
is a partial isomorphism (though this is a trivial requirement in inverse
categories).

Likewise, elementary predicates (e.g., comparison of values in a store) may
vary from language to language, so we assume that such elementary predicates
have denotations as well as decisions $\Sigma\to\Sigma\oplus\Sigma$. If
necessary (as is the case for Janus [40]), we may then close these elementary
predicates under boolean combinations as discussed in the previous section.

To start, we note how sequencing of flowcharts may be modelled trivially by
means of composition, _i.e._ ,

$\left\llbracket c_{1}~{}\mathtt{;}~{}c_{2}\right\rrbracket=\left\llbracket
c_{2}\right\rrbracket\left\llbracket c_{1}\right\rrbracket$

or, using the diagrammatic notation of flowcharts and the string diagrams for
monoidal categories in the style of [31] (read left-to-right and bottom-to-
top),

$\left\llbracket\begin{picture}(17.0,2.0)(0.0,-0.5)\put(0.0,0.0){\line(1,0){2.0}}
\put(2.0,0.0){\vector(1,0){1.0}}
\put(3.0,-1.5){25.\dashbox(0.0)(4.0,3.0)[c]{\shortstack[c]{ \small$c_{1}$ }}}
\put(7.0,0.0){\line(1,0){2.0}} \put(9.0,0.0){\vector(1,0){1.0}}
\put(10.0,-1.5){25.\dashbox(0.0)(4.0,3.0)[c]{\shortstack[c]{ \small$c_{2}$ }}}
\put(14.0,0.0){\vector(1,0){3.0}}
\end{picture}\right\rrbracket\enspace=\enspace\leavevmode\hbox
to106.81pt{\vbox to17.47pt{\pgfpicture\makeatletter\hbox{\hskip
32.35175pt\lower-5.89038pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{-13.2904pt}{-5.69038pt}{26.58081pt}{17.07166pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.9574pt}{0.59544pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$\left\llbracket
c_{1}\right\rrbracket$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{29.38873pt}{-5.69038pt}{26.58081pt}{17.07166pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{32.72174pt}{0.59544pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$\left\llbracket
c_{2}\right\rrbracket$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\par{}{{}}{} {}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{{
{\pgfsys@beginscope\pgfsys@setlinewidth{0.32pt}\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{}
{}{}{} {}{}{}
\pgfsys@moveto{-1.19998pt}{1.59998pt}\pgfsys@curveto{-1.09998pt}{0.99998pt}{0.0pt}{0.09999pt}{0.29999pt}{0.0pt}\pgfsys@curveto{0.0pt}{-0.09999pt}{-1.09998pt}{-0.99998pt}{-1.19998pt}{-1.59998pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{-32.15175pt}{2.84544pt}\pgfsys@lineto{-21.79956pt}{2.84544pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-21.79956pt}{2.84544pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.74567pt}{6.37845pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{-21.62393pt}{2.84544pt}\pgfsys@lineto{-10.81218pt}{2.84544pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.21806pt}{6.37845pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{11.09656pt}{2.84544pt}\pgfsys@lineto{22.30229pt}{2.84544pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.30229pt}{2.84544pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.92941pt}{6.37845pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{22.47748pt}{2.84544pt}\pgfsys@lineto{31.58257pt}{2.84544pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{27.03001pt}{6.37845pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{53.49132pt}{2.84544pt}\pgfsys@lineto{63.70111pt}{2.84544pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{63.70111pt}{2.84544pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{58.8262pt}{6.37845pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{63.73433pt}{2.84544pt}\pgfsys@lineto{74.2617pt}{2.84544pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{68.99802pt}{6.37845pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
Intuitively, a decision separates an object into witnesses (in the first
component) and counterexamples (in the second). As such, the partial inverse
to a decision must be defined only on witnesses in the first component, and
only on counterexamples in the second. But then, where decisions model
_predicates_ , codecisions (_i.e._ , partial inverses to decisions) model
_assertions_.

With this in mind, we achieve a denotation of reversible conditionals as

$\left\llbracket\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\left\llbracket p\right\rrbracket$

or, as diagrams

$\left\llbracket\begin{picture}(18.0,6.5)(0.0,-0.5)\put(0.0,0.0){\line(1,0){2.0}}
\put(2.0,0.0){\vector(1,0){1.0}} \put(3.0,0.0){\line(1,1){2.0}}
\put(3.0,0.0){\line(1,-1){2.0}} \put(7.0,0.0){\line(-1,-1){2.0}}
\put(7.0,0.0){\line(-1,1){2.0}}
\put(3.0,-2.0){\makebox(4.0,4.0)[c]{\shortstack[c]{ \small$p$ }}}
\put(5.6,3.2){\makebox(0.0,0.0)[lt]{{\tiny{$\mathbf{t}$}}}}
\put(5.6,-3.2){\makebox(0.0,0.0)[lb]{{\tiny{$\mathbf{f}$}}}}
\put(5.0,2.0){\line(0,1){2.0}} \put(5.0,4.0){\line(1,0){1.0}}
\put(6.0,4.0){\vector(1,0){1.0}}
\put(7.0,2.5){25.\dashbox(0.0)(4.0,3.0)[c]{\shortstack[c]{ \small$c_{2}$ }}}
\put(11.0,4.0){\line(1,0){2.0}} \put(13.0,4.0){\line(0,-1){1.0}}
\put(13.0,3.0){\vector(0,-1){1.0}} \put(13.0,0.0){\oval(4.0,4.0)}
\put(11.0,-2.0){\makebox(4.0,4.0)[c]{\shortstack[c]{ \small$q$ }}}
\put(13.7,3.2){\makebox(0.0,0.0)[lt]{{\tiny{$\mathbf{t}$}}}}
\put(13.7,-3.2){\makebox(0.0,0.0)[lb]{{\tiny{$\mathbf{f}$}}}}
\put(15.0,0.0){\vector(1,0){3.0}} \put(5.0,-2.0){\line(0,-1){2.0}}
\put(5.0,-4.0){\line(1,0){1.0}} \put(6.0,-4.0){\vector(1,0){1.0}}
\put(7.0,-5.5){25.\dashbox(0.0)(4.0,3.0)[c]{\shortstack[c]{ \small$c_{1}$ }}}
\put(11.0,-4.0){\line(1,0){2.0}} \put(13.0,-4.0){\vector(0,1){2.0}}
\end{picture}\right\rrbracket\enspace=\enspace\leavevmode\hbox
to142.66pt{\vbox to44.5pt{\pgfpicture\makeatletter\hbox{\hskip
28.65276pt\lower-22.25105pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{-12.34706pt}{-21.33955pt}{24.69412pt}{42.67911pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.01405pt}{-2.25pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$\left\llbracket
p\right\rrbracket$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{29.38873pt}{4.9794pt}{26.58081pt}{17.07166pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{32.72174pt}{11.26523pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$\left\llbracket
c_{2}\right\rrbracket$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{29.38873pt}{-22.05106pt}{26.58081pt}{17.07166pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{32.72174pt}{-15.76523pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$\left\llbracket
c_{1}\right\rrbracket$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{71.98495pt}{-21.33955pt}{26.74664pt}{42.67911pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{75.31796pt}{-3.125pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$\left\llbracket
q\right\rrbracket^{\dagger}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\par{}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{-28.45276pt}{-13.51523pt}\pgfsys@lineto{-18.9541pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-18.9541pt}{-13.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.47343pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{-18.77892pt}{-13.51523pt}\pgfsys@lineto{-9.10509pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.942pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{9.24706pt}{13.51523pt}\pgfsys@lineto{22.30229pt}{13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.30229pt}{13.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.00467pt}{17.04823pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{ {}{}{}}
{{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{22.47748pt}{13.51523pt}\pgfsys@lineto{29.18874pt}{13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.8331pt}{17.04823pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{9.24706pt}{-13.51523pt}\pgfsys@lineto{22.30229pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.30229pt}{-13.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.00467pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{ {}{}{}}
{{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{22.47748pt}{-13.51523pt}\pgfsys@lineto{29.18874pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.8331pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{} {}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{56.16954pt}{13.51523pt}\pgfsys@lineto{63.55872pt}{13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{63.55872pt}{13.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{60.09412pt}{17.04823pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{63.73433pt}{13.51523pt}\pgfsys@lineto{74.54608pt}{13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{69.1402pt}{17.04823pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{} {}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{56.16954pt}{-13.51523pt}\pgfsys@lineto{63.55872pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{63.55872pt}{-13.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{60.09412pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{63.73433pt}{-13.51523pt}\pgfsys@lineto{74.54608pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{69.1402pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{96.17046pt}{-13.51523pt}\pgfsys@lineto{104.53075pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{104.53075pt}{-13.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{100.5806pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{104.70593pt}{-13.51523pt}\pgfsys@lineto{113.81104pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{109.25848pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
To give the denotation of reversible loops, we use the $\dagger$-trace
operator. Defining a shorthand for the body of the loop as

$\beta[p,c,q]=(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}$

we obtain the denotation

$\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}q\right\rrbracket=\operatorname{Tr}_{\Sigma,\Sigma}^{\Sigma}(\beta[p,c,q])=\operatorname{Tr}_{\Sigma,\Sigma}^{\Sigma}((\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger})$

or diagrammatically

$\left\llbracket\begin{picture}(18.0,5.2)(0.0,-1.7)\put(0.0,0.0){\line(1,0){2.0}}
\put(2.0,0.0){\vector(1,0){1.0}} \put(5.0,0.0){\oval(4.0,4.0)}
\put(3.0,-2.0){\makebox(4.0,4.0)[c]{\shortstack[c]{\small$p$}}}
\put(2.0,1.1){\makebox(0.0,0.0)[rt]{{\tiny{$\mathbf{t}$}}}}
\put(5.7,-3.2){\makebox(0.0,0.0)[lb]{{\tiny{$\mathbf{f}$}}}}
\put(7.0,0.0){\vector(1,0){4.0}} \put(11.0,0.0){\line(1,1){2.0}}
\put(11.0,0.0){\line(1,-1){2.0}} \put(15.0,0.0){\line(-1,-1){2.0}}
\put(15.0,0.0){\line(-1,1){2.0}}
\put(11.0,-2.0){\makebox(4.0,4.0)[c]{\shortstack[c]{\small$q$}}}
\put(15.5,1.1){\makebox(0.0,0.0)[lt]{{\tiny{$\mathbf{t}$}}}}
\put(13.6,-3.2){\makebox(0.0,0.0)[lb]{{\tiny{$\mathbf{f}$}}}}
\put(13.0,-2.0){\line(0,-1){2.0}} \put(13.0,-4.0){\line(-1,0){1.0}}
\put(12.0,-4.0){\vector(-1,0){1.0}}
\put(7.0,-5.5){25.\dashbox(0.0)(4.0,3.0)[c]{\shortstack[c]{\small$c$}}}
\put(7.0,-4.0){\line(-1,0){2.0}} \put(5.0,-4.0){\vector(0,1){2.0}}
\put(15.0,0.0){\vector(1,0){3.0}}
\end{picture}\right\rrbracket\enspace=\enspace\leavevmode\hbox
to142.66pt{\vbox to57.5pt{\pgfpicture\makeatletter\hbox{\hskip
28.65276pt\lower-21.53955pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{-13.46707pt}{-21.33955pt}{26.93414pt}{42.67911pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.13406pt}{-3.125pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$\left\llbracket
p\right\rrbracket^{\dagger}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{30.42583pt}{-21.33955pt}{24.50662pt}{42.67911pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{33.75883pt}{-2.25pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$\left\llbracket
q\right\rrbracket$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{73.32787pt}{4.9794pt}{24.06082pt}{17.07166pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{76.66087pt}{11.26523pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$\left\llbracket
c\right\rrbracket$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{-19.91684pt}{13.51523pt}\pgfsys@lineto{-10.81218pt}{13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.36452pt}{17.04823pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{-28.45276pt}{-13.51523pt}\pgfsys@lineto{-19.2389pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.2389pt}{-13.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.61584pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{-19.0633pt}{-13.51523pt}\pgfsys@lineto{-10.81218pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-14.93774pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{10.81218pt}{-13.51523pt}\pgfsys@lineto{21.73312pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{21.73312pt}{-13.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.50264pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{21.90874pt}{-13.51523pt}\pgfsys@lineto{33.57404pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{27.74138pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{51.78423pt}{13.51523pt}\pgfsys@lineto{63.84308pt}{13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{63.84308pt}{13.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{58.04364pt}{17.04823pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{64.0187pt}{13.51523pt}\pgfsys@lineto{76.82236pt}{13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{70.42053pt}{17.04823pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{51.78423pt}{-13.51523pt}\pgfsys@lineto{80.9149pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{80.9149pt}{-13.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{66.57956pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{81.09053pt}{-13.51523pt}\pgfsys@lineto{113.81104pt}{-13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{97.45078pt}{-9.98222pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{93.89418pt}{13.51523pt}\pgfsys@lineto{103.19812pt}{13.51523pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{98.54614pt}{17.04823pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{102.99884pt}{13.51523pt}\pgfsys@lineto{102.99884pt}{35.76521pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{99.46584pt}{24.64021pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{102.99884pt}{35.56595pt}\pgfsys@lineto{43.13913pt}{35.56595pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{43.13913pt}{35.56595pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{72.83899pt}{32.03294pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{45.52458pt}{35.56595pt}\pgfsys@lineto{-20.11612pt}{35.56595pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.70424pt}{32.03294pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{-19.91684pt}{35.56595pt}\pgfsys@lineto{-19.91684pt}{13.31595pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{$\mathit{}$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-16.38383pt}{24.44095pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
That this has the desired operational behavior follows from the fact that the
$\dagger$-trace operator is canonically constructed in join inverse categories
as

$\operatorname{Tr}_{X,Y}^{U}(f)=f_{11}\vee\bigvee_{n\in\omega}f_{21}f_{22}^{n}f_{12}\enspace.$

Recall that $f_{ij}=\amalg_{j}^{\dagger}f\amalg_{i}$. As such, for our loop
construct defined above, the $f_{11}$-cases correpond to cases where a given
state bypasses the loop entirely; $f_{21}f_{12}$ (that is, for $n=0$) to cases
where exactly one iteration is performed by a given state before exiting the
loop; $f_{21}f_{22}f_{12}$ to cases where two iterations are performed before
exiting; and so on. In this way, the given trace semantics contain all
successive loop unrollings, as desired. We will make this more formal in the
following section, where we show computational soundness and adequacy for
these with respect to the operational semantics.

In order to be able to provide a correspondence between categorical and
operational semantics, we also need an interpretation of the meta-command
$\underline{\mathit{loop}}$. While it may not be so clear at the present, it
turns out that the appropriate one is

$\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket=\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n}\enspace.$

While it may seem like a small point, the mere existence of a categorical
semantics in inverse categories for a reversible programming language has some
immediate benefits. In particular, that a programming language is reversible
can be rather complicated to show by means of operational semantics (see,
e.g., [40, Sec. 2.3]), yet it follows directly in our categorical semantics,
as it is compositional and all morphisms in inverse categories have a unique
partial inverse.

##  6\. Computational soundness and adequacy

Computational soundness and adequacy (see, e.g., [13]) are the two fundamental
properties of operational semantics with respect to their denotational
counterparts, as soundness and completeness are for proof systems with respect
to their semantics. In brief, computational soundness and adequacy state that
the respective notions of _convergence_ of the operational and denotational
semantics are in agreement.

In the operational semantics, the notion of convergence seems straightforward:
a program $c$ converges in a state $\sigma$ if there exists another state
$\sigma^{\prime}$ such that $\sigma\vdash c\downarrow\sigma^{\prime}$. On the
denotational side, it seems less obvious what a proper notion of convergence
is.

An idea (used by, e.g., Fiore [13]) is to let values (in this case, states) be
interpreted as _total_ morphisms from some sufficiently simple object $I$ into
an appropriate object $V$ (here, we will use our object $\Sigma$ of states).
In this context, the notion of convergence for a program $p$ in a state
$\sigma$ is then that the resulting morphism $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ is, again, (the
denotation of) a state – _i.e._ , it is total. Naturally, this approach
requires machinery to separate total maps from partial ones. As luck would
have it inverse categories fit the bill perfectly, as they can be regarded as
special instances of restriction categories.

To make this idea more clear in the current context, and to allow us to use
the established formulations of computational soundness and adequacy, we
define a model of a structured reversible flowchart language to be the
following:

A model of a structured reversible flowchart language $\mathcal{L}$ consists
of a join inverse category $\mathscr{C}$ with a disjointness tensor, further
equipped with distinguished objects $I$ and $\Sigma$ satisfying

  1. (i)

the identity and zero maps on $I$ are distinct, _i.e._ , $\text{id}_{I}\neq
0_{I,I}$,

  2. (ii)

if $I\xrightarrow{e}I$ is a restriction idempotent then $e=\text{id}_{I}$ or
$e=0_{I,I}$, and

  3. (iii)

each $\mathcal{L}$-state $\sigma$ is interpreted as a _total_ morphism
$I\xrightarrow{\left\llbracket\sigma\right\rrbracket}\Sigma$.

Here, we think of $I$ as the _indexing object_ , and $\Sigma$ as the _object
of states_. In irreversible programming languages, the first two conditions in
the definition above are often left out, as the indexing object is typically
chosen to be the terminal object $1$. However, terminal objects are degenerate
in inverse categories, as they always coincide with the initial object when
they exist – that is, they are zero objects. For this reason, we require
instead the existence of a sufficiently simple indexing object, as described
by these two properties. For example, in $\mathbf{PInj}$, any one-element set
will satisfy these conditions.

Even further, the third condition is typically proven rather than assumed. We
include it here as an assumption since structured reversible flowchart
languages may take many different forms, and we have no way of knowing how the
concrete states are formed. As such, rather than limiting ourselves to
languages where states take a certain form in order to show totality of
interpretation, we instead assume it to be able to show properties about more
programming languages.

This also leads us to another important point: We are only able to show
computational soundness and adequacy for the operational semantics as they are
stated, _i.e._ , we are not able to take into account the specific atomic
steps (besides $\mathbf{skip}$) or elementary predicates of the language.

As such, computational soundness and adequacy (and what may follow from that)
should be understood _conditionally_ : If a structured reversible flowchart
language has a model of the form above _and_ it is computationally sound and
adequate with respect to its atomic steps and elementary predicates, then the
entire interpretation is sound and adequate as well.

We begin by recalling the definition of the denotation of predicates and
commands in a model of a structured reversible flowchart language from Section
5.

Recall the interpretation of predicates in $\mathcal{L}$ as decisions in
$\mathscr{C}$:

  1. (i)

$\left\llbracket\mathit{tt}\right\rrbracket=\amalg_{1}$,

  2. (ii)

$\left\llbracket\mathit{ff}\right\rrbracket=\amalg_{2}$,

  3. (iii)

$\left\llbracket\mathbf{not}~{}p\right\rrbracket=\gamma\left\llbracket
p\right\rrbracket$,

  4. (iv)

$\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket=\left((\amalg_{1}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket})\vee(\amalg_{2}(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket}))\right)\overline{\left\llbracket
p\right\rrbracket}~{}\overline{\left\llbracket q\right\rrbracket}$.

Recall the interpretation of commands in $\mathcal{L}$ (and the meta-command
$\underline{\mathit{loop}}$) as morphisms $\Sigma\to\Sigma$ in $\mathscr{C}$:

  1. (i)

$\left\llbracket\mathbf{skip}\right\rrbracket=\text{id}_{\Sigma}$,

  2. (ii)

$\left\llbracket c_{1}~{}\mathtt{;}~{}c_{2}\right\rrbracket=\left\llbracket
c_{2}\right\rrbracket\left\llbracket c_{1}\right\rrbracket$,

  3. (iii)

$\left\llbracket\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\left\llbracket p\right\rrbracket$,

  4. (iv)

$\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}q\right\rrbracket=\operatorname{Tr}_{\Sigma,\Sigma}^{\Sigma}(\beta[p,c,q])$,
and

  5. (v)

$\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket=\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n}$

where $\beta[p,c,q]=(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}:\Sigma\oplus\Sigma\to\Sigma\oplus\Sigma$. Note
also that $f_{ij}=\amalg_{j}^{\dagger}f\amalg_{i}$.

The overall strategy we will use to show computational soundness and
computational adequacy for programs is to start by showing it for predicates.
To begin to tackle this, we first need a lemma regarding the totality of
predicates.

######  Lemma 10.

Let $p$ and $q$ be $\mathcal{L}$-predicates. It is the case that

  1. (i)

$I\xrightarrow{\left\llbracket\sigma\right\rrbracket}\Sigma\xrightarrow{\left\llbracket\mathit{tt}\right\rrbracket}\Sigma\oplus\Sigma$
and
$I\xrightarrow{\left\llbracket\sigma\right\rrbracket}\Sigma\xrightarrow{\left\llbracket\mathit{ff}\right\rrbracket}\Sigma\oplus\Sigma$
are total,

  2. (ii)

$I\xrightarrow{\left\llbracket\sigma\right\rrbracket}\Sigma\xrightarrow{\left\llbracket\mathbf{not}~{}p\right\rrbracket}\Sigma\oplus\Sigma$
is total iff
$I\xrightarrow{\left\llbracket\sigma\right\rrbracket}\Sigma\xrightarrow{\left\llbracket
p\right\rrbracket}\Sigma\oplus\Sigma$ is, and

  3. (iii)

$I\xrightarrow{\left\llbracket\sigma\right\rrbracket}\Sigma\xrightarrow{\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket}\Sigma\oplus\Sigma$ is total iff
$I\xrightarrow{\left\llbracket\sigma\right\rrbracket}\Sigma\xrightarrow{\left\llbracket
p\right\rrbracket}\Sigma\oplus\Sigma$ and
$I\xrightarrow{\left\llbracket\sigma\right\rrbracket}\Sigma\xrightarrow{\left\llbracket
q\right\rrbracket}\Sigma\oplus\Sigma$ both are.

######  Proof 6.1.

For (i), it follows that

$\overline{\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{\amalg_{1}\left\llbracket\sigma\right\rrbracket}=\overline{\overline{\amalg_{1}}\left\llbracket\sigma\right\rrbracket}=\overline{\text{id}_{\Sigma}\left\llbracket\sigma\right\rrbracket}=\overline{\left\llbracket\sigma\right\rrbracket}=\text{id}_{I},$

where the final equality follows by the definition of a model. The case for
$\mathit{ff}$ is entirely analogous.

For (ii), we have that

$\overline{\left\llbracket\mathbf{not}~{}p\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{\gamma\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{\overline{\gamma}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{\text{id}_{\Sigma\oplus\Sigma}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$

which implies directly that
$I\xrightarrow{\left\llbracket\sigma\right\rrbracket}\Sigma\xrightarrow{\left\llbracket\mathbf{not}~{}p\right\rrbracket}\Sigma\oplus\Sigma$
is total iff
$I\xrightarrow{\left\llbracket\sigma\right\rrbracket}\Sigma\xrightarrow{\left\llbracket
p\right\rrbracket}\Sigma\oplus\Sigma$ is.

For (iii), it suffices to show that $\overline{\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}$, since
$\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\text{id}_{I}$ then
yields $\overline{\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\text{id}_{I}\text{id}_{I}=\text{id}_{I}$
directly; the other direction follows by the fact that if
$\overline{g}\overline{f}=\text{id}$ then
$\text{id}=\overline{g}\overline{f}=\overline{g}\overline{f}~{}\overline{f}=\text{id}\overline{f}=\overline{f}$
(and analogously for $g$).

We start by observing that

$\displaystyle\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$
$\displaystyle=\overline{((\amalg_{1}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket})\vee(\amalg_{2}\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}))\left\llbracket\sigma\right\rrbracket}$ (1)
$\displaystyle=\overline{(\amalg_{1}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}\left\llbracket\sigma\right\rrbracket)\vee(\amalg_{2}\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}\left\llbracket\sigma\right\rrbracket)}$ (2)
$\displaystyle=\overline{(\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket})\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket})}$ (3)
$\displaystyle=\overline{(\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket})}\vee\overline{(\amalg_{2}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket})}$ (4)
$\displaystyle=\overline{(\overline{\amalg_{1}\left\llbracket\sigma\right\rrbracket}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket})}\vee\overline{(\overline{\amalg_{2}\left\llbracket\sigma\right\rrbracket}\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket})}$ (5)
$\displaystyle=\overline{\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}}\vee\overline{\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}}$ (6)
$\displaystyle=\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ (7)

where (1) follows by Lemma 8, (2) by distributivity of composition of joins,
(3) by the fourth axiom of restriction categories (see Definition 3), (4) by
distributivity of restriction over joins (see Definition 3.1), (5) by Lemma 1,
(6) since
$\overline{\amalg_{1}\left\llbracket\sigma\right\rrbracket}=\overline{\amalg_{2}\left\llbracket\sigma\right\rrbracket}=\text{id}_{I}$
follows by (i), and (7) by Lemma 1. We may establish by analogous argument
that

$\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}$

as well. In the following, let $\sigma_{p}=\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ and
$\sigma_{q}=\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket$. We start by computing

$\displaystyle\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=((\amalg_{1}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket})\vee(\amalg_{2}(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket})))\overline{\left\llbracket
p\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket}\left\llbracket\sigma\right\rrbracket$ (8)
$\displaystyle=((\amalg_{1}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket})\vee(\amalg_{2}(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket})))\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ (9)
$\displaystyle=((\amalg_{1}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket}\left\llbracket\sigma\right\rrbracket)\vee(\amalg_{2}(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket})\left\llbracket\sigma\right\rrbracket))\overline{\sigma_{p}}~{}\overline{\sigma_{q}}$
(10)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket})\vee$
$\displaystyle\qquad(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket})))\overline{\sigma_{p}}~{}\overline{\sigma_{q}}$
(11)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\sigma_{p}}\vee\overline{\amalg_{2}^{\dagger}\sigma_{q}})))\overline{\sigma_{p}}~{}\overline{\sigma_{q}}$
(12)

where (8) follows by the definition of $\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket$ (see Definition 6), (9) by two
applications of the fourth axiom of restriction categories (see Definition 3),
(10) by distributivity of composition over joins (see Definition 3.1) and the
definitions of $\sigma_{p}$ and $\sigma_{q}$, (11) by repeated applications of
the fourth axiom of restriction categories, and (12) by definition of
$\sigma_{p}$ and $\sigma_{q}$. But then we have

$\displaystyle\overline{\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket}$
$\displaystyle=\overline{((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\sigma_{p}}\vee\overline{\amalg_{2}^{\dagger}\sigma_{q}})))\overline{\sigma_{p}}~{}\overline{\sigma_{q}}}$
(13)
$\displaystyle=\overline{\overline{((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\sigma_{p}}\vee\overline{\amalg_{2}^{\dagger}\sigma_{q}})))}\overline{\sigma_{p}}~{}\overline{\sigma_{q}}}$
(14)
$\displaystyle=\overline{\overline{((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})}\vee\overline{(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\sigma_{p}}\vee\overline{\amalg_{2}^{\dagger}\sigma_{q}})))}\overline{\sigma_{p}}~{}\overline{\sigma_{q}}}$
(15)
$\displaystyle=\overline{((\overline{\amalg_{1}\left\llbracket\sigma\right\rrbracket}\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\overline{\amalg_{2}\left\llbracket\sigma\right\rrbracket}(\overline{\amalg_{2}^{\dagger}\sigma_{p}}\vee\overline{\amalg_{2}^{\dagger}\sigma_{q}})))\overline{\sigma_{p}}~{}\overline{\sigma_{q}}}$
(16)
$\displaystyle=((\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{p}}\vee\overline{\amalg_{2}^{\dagger}\sigma_{q}}))\overline{\sigma_{p}}~{}\overline{\sigma_{q}}$
(17)
$\displaystyle=(\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}}~{}\overline{\sigma_{p}}~{}\overline{\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{p}}~{}\overline{\sigma_{p}}~{}\overline{\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{q}}~{}\overline{\sigma_{p}}~{}\overline{\sigma_{q}})$
(18)
$\displaystyle=(\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}}~{}\overline{\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{p}}~{}\overline{\sigma_{p}}~{}\overline{\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{q}}~{}\overline{\sigma_{q}}~{}\overline{\sigma_{p}})$
(19)
$\displaystyle=(\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{p}}~{}\overline{\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{q}}~{}\overline{\sigma_{p}})$
(20)
$\displaystyle=(\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{p}}(\overline{\amalg_{1}^{\dagger}\sigma_{q}}\vee\overline{\amalg_{2}^{\dagger}\sigma_{q}}))\vee(\overline{\amalg_{2}^{\dagger}\sigma_{q}}(\overline{\amalg_{1}^{\dagger}\sigma_{p}}\vee\overline{\amalg_{2}^{\dagger}\sigma_{p}}))$
(21)
$\displaystyle=(\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{2}^{\dagger}\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{q}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{p}})\vee$
$\displaystyle\qquad(\overline{\amalg_{2}^{\dagger}\sigma_{q}}~{}\overline{\amalg_{2}^{\dagger}\sigma_{p}})$
(22)
$\displaystyle=(\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\overline{\amalg_{1}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{2}^{\dagger}\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{1}^{\dagger}\sigma_{q}})\vee(\overline{\amalg_{2}^{\dagger}\sigma_{p}}~{}\overline{\amalg_{2}^{\dagger}\sigma_{q}})$
(23)
$\displaystyle=(\overline{\amalg_{1}^{\dagger}\sigma_{p}}\vee\overline{\amalg_{2}^{\dagger}\sigma_{p}})(\overline{\amalg_{1}^{\dagger}\sigma_{q}}\vee\overline{\amalg_{2}^{\dagger}\sigma_{q}})=\overline{\sigma_{p}}~{}\overline{\sigma_{q}}$
(24)

Here, (13) follows by (8)–(12), (14) by Lemma 1, (15) by distributivity of
restriction over joins, (16) by the third axiom of restriction categories,
(17) follows by (i), (18) by distributivity of composition over joins, (19) by
commutativity of restriction idempotents (see Definition 3), (20) by Lemma 1,
(21) by Lemma 8, (22) by distributivity of composition over joins, (23) by
idempotence of joins, and (24) by distributivity of composition over joins and
definition of $\sigma_{p}$ and $\sigma_{q}$.

A common way to show computational soundness (see, e.g., [13]) is to show a
kind of preservation property; that interpretations are, in a sense, preserved
across evaluation in the operational semantics. This is shown for predicates
in the following lemma:

######  Lemma 11.

If $\sigma\vdash p\rightsquigarrow b$ then $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
b\right\rrbracket\left\llbracket\sigma\right\rrbracket$.

######  Proof 6.2.

By induction on the structure of the derivation $\mathcal{D}$ of $\sigma\vdash
p\rightsquigarrow b$.

  * •

Case
$\mathcal{D}=\dfrac{}{\sigma\vdash\mathit{tt}\rightsquigarrow\mathit{tt}}$. We
trivially have
$\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma\right\rrbracket$.

  * •

Case
$\mathcal{D}=\dfrac{}{\sigma\vdash\mathit{ff}\rightsquigarrow\mathit{ff}}$.
Again, we trivially have
$\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket$.

  * •

Case $\mathcal{D}=\dfrac{\sigma\vdash
p\rightsquigarrow\mathit{tt}}{\sigma\vdash\mathbf{not}~{}p\rightsquigarrow\mathit{ff}}$.
By induction we have that $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$.
But then
$\left\llbracket\mathbf{not}~{}p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\gamma\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\gamma\amalg_{1}\left\llbracket\sigma\right\rrbracket=\amalg_{2}\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket$.

  * •

Case $\mathcal{D}=\dfrac{\sigma\vdash
p\rightsquigarrow\mathit{ff}}{\sigma\vdash\mathbf{not}~{}p\rightsquigarrow\mathit{tt}}$.
By induction we have that $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{2}\left\llbracket\sigma\right\rrbracket$.
Thus
$\left\llbracket\mathbf{not}~{}p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\gamma\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\gamma\amalg_{2}\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma\right\rrbracket$.

  * •

Case $\mathcal{D}=\dfrac{\sigma\vdash
p\rightsquigarrow\mathit{tt}\qquad\sigma\vdash
q\rightsquigarrow\mathit{tt}}{\sigma\vdash
p~{}\mathbf{and}~{}q\rightsquigarrow\mathit{tt}}$.
By induction $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$
and $\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$.
We compute

$\displaystyle\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=((\amalg_{1}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket})\vee(\amalg_{2}(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket})))\overline{\left\llbracket
p\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket}\left\llbracket\sigma\right\rrbracket$ (25)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket})\vee$
$\displaystyle\qquad(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket})))\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ (26)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket})\vee$
$\displaystyle\qquad(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket})))\overline{\amalg_{1}\left\llbracket\sigma\right\rrbracket}~{}\overline{\amalg_{1}\left\llbracket\sigma\right\rrbracket}$
(27)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket\sigma\right\rrbracket})\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{0_{\Sigma,\Sigma}\left\llbracket\sigma\right\rrbracket}\vee\overline{0_{\Sigma,\Sigma}\left\llbracket\sigma\right\rrbracket})))\overline{\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket\sigma\right\rrbracket}$
(28)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket\sigma\right\rrbracket})\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket\overline{0_{\Sigma,\Sigma}\left\llbracket\sigma\right\rrbracket}))\overline{\left\llbracket\sigma\right\rrbracket}$
(29)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket)\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket\overline{0_{I,\Sigma}}))\overline{\left\llbracket\sigma\right\rrbracket}$
(30)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket)\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket
0_{I,I}))\overline{\left\llbracket\sigma\right\rrbracket}$ (31)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket)\vee
0_{I,\Sigma\oplus\Sigma})\overline{\left\llbracket\sigma\right\rrbracket}$
(32)
$\displaystyle=\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket\sigma\right\rrbracket}=\amalg_{1}\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma\right\rrbracket.$
(33)

where (25) is the definition of $\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket$, (26) follows by (8) – (11), (27) by
$\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$,
(28) by Lemma 7, (29) by Lemma 1 and idempotence of joins, (30) by the first
axiom of restriction categories and the universal mapping property of the zero
object, (31) by the zero object a restriction zero, (32) once again by the
universal mapping property of the zero object, and (33) by the first axiom of
restriction categories and the definition of
$\left\llbracket\mathit{tt}\right\rrbracket$.

  * •

Case $\mathcal{D}=\dfrac{\sigma\vdash
p\rightsquigarrow\mathit{ff}\qquad\sigma\vdash
q\rightsquigarrow\mathit{tt}}{\sigma\vdash
p~{}\mathbf{and}~{}q\rightsquigarrow\mathit{ff}}$.
By induction $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{2}\left\llbracket\sigma\right\rrbracket$
and $\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$.

$\displaystyle\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=((\amalg_{1}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket})\vee(\amalg_{2}(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket})))\overline{\left\llbracket
p\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket}\left\llbracket\sigma\right\rrbracket$ (34)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket})\vee$
$\displaystyle\qquad(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket})))\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ (35)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\amalg_{2}\left\llbracket\sigma\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket})\vee$
$\displaystyle\qquad(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\amalg_{2}\left\llbracket\sigma\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket})))\overline{\amalg_{2}\left\llbracket\sigma\right\rrbracket}~{}\overline{\amalg_{1}\left\llbracket\sigma\right\rrbracket}$
(36)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{0_{\Sigma,\Sigma}\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket\sigma\right\rrbracket})\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\left\llbracket\sigma\right\rrbracket}\vee\overline{0_{\Sigma,\Sigma}\left\llbracket\sigma\right\rrbracket})))\overline{\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket\sigma\right\rrbracket}$
(37) $\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket
0_{I,I}~{}\overline{\left\llbracket\sigma\right\rrbracket})\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\left\llbracket\sigma\right\rrbracket}\vee
0_{I,I})))\overline{\left\llbracket\sigma\right\rrbracket}$ (38)
$\displaystyle=(0_{I,\Sigma\oplus\Sigma}\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket\sigma\right\rrbracket}))\overline{\left\llbracket\sigma\right\rrbracket}$
(39)
$\displaystyle=\amalg_{2}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket\sigma\right\rrbracket}=\amalg_{2}\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket$
(40)

where (34) is the definition of $\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket$, (35) follows by (8) – (11), (36) by
$\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{2}\left\llbracket\sigma\right\rrbracket$
and $\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$,
(37) by Lemma 7, (38) by the first axiom of restriction categories as well as
the universal mapping property of the zero object and the fact that it is a
restriction zero, (39) by the universal mapping property of the zero object
and the fact that zero maps are unit for joins, (40) by zero maps units for
joins, the first axiom of restriction categories, and the definition of
$\left\llbracket\mathit{ff}\right\rrbracket$.

  * •

Case $\mathcal{D}=\dfrac{\sigma\vdash
p\rightsquigarrow\mathit{tt}\qquad\sigma\vdash
q\rightsquigarrow\mathit{ff}}{\sigma\vdash
p~{}\mathbf{and}~{}q\rightsquigarrow\mathit{ff}}$, similar to the previous
case.

  * •

Case $\mathcal{D}=\dfrac{\sigma\vdash
p\rightsquigarrow\mathit{ff}\qquad\sigma\vdash
q\rightsquigarrow\mathit{ff}}{\sigma\vdash
p~{}\mathbf{and}~{}q\rightsquigarrow\mathit{ff}}$.
By induction $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{2}\left\llbracket\sigma\right\rrbracket$
and $\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{2}\left\llbracket\sigma\right\rrbracket$.

$\displaystyle\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=((\amalg_{1}\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket})\vee(\amalg_{2}(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket})))\overline{\left\llbracket
p\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket}\left\llbracket\sigma\right\rrbracket$ (41)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket})\vee$
$\displaystyle\qquad(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket})))\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ (42)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\amalg_{2}\left\llbracket\sigma\right\rrbracket}~{}\overline{\amalg_{1}^{\dagger}\amalg_{2}\left\llbracket\sigma\right\rrbracket})\vee$
$\displaystyle\qquad(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\amalg_{2}^{\dagger}\amalg_{2}\left\llbracket\sigma\right\rrbracket}\vee\overline{\amalg_{2}^{\dagger}\amalg_{2}\left\llbracket\sigma\right\rrbracket})))\overline{\amalg_{2}\left\llbracket\sigma\right\rrbracket}~{}\overline{\amalg_{2}\left\llbracket\sigma\right\rrbracket}$
(43)
$\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{0_{\Sigma,\Sigma}\left\llbracket\sigma\right\rrbracket}~{}\overline{0_{\Sigma,\Sigma}\left\llbracket\sigma\right\rrbracket})\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket(\overline{\left\llbracket\sigma\right\rrbracket}\vee\overline{\left\llbracket\sigma\right\rrbracket})))\overline{\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket\sigma\right\rrbracket}$
(44) $\displaystyle=((\amalg_{1}\left\llbracket\sigma\right\rrbracket
0_{I,I})\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket\sigma\right\rrbracket}))\overline{\left\llbracket\sigma\right\rrbracket}$
(45)
$\displaystyle=(0_{I,\Sigma\oplus\Sigma}\vee(\amalg_{2}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket\sigma\right\rrbracket}))\overline{\left\llbracket\sigma\right\rrbracket}$
(46)
$\displaystyle=\amalg_{2}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket\sigma\right\rrbracket}=\amalg_{2}\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket$
(47)

where (41) is the definition of $\left\llbracket
p~{}\mathbf{and}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket$,
(42) follows by (8) – (11), (43) by $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{2}\left\llbracket\sigma\right\rrbracket$,
(44) by Lemma 7, (45) by idempotence of restriction idempotents and joins,
(46) by the universal mapping property of the zero object, and (47) by the
first axiom of restriction categories and the definition of
$\left\llbracket\mathit{ff}\right\rrbracket$.

With this done, the computational soundness lemma for predicates follows
readily.

######  Lemma 12.

If there exists $b$ such that $\sigma\vdash p\rightsquigarrow b$ then
$\left\llbracket p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ is
total.

######  Proof 6.3.

Suppose there exists $b$ such that $\sigma\vdash p\rightsquigarrow b$ by some
derivation. It follows by the operational semantics that $b$ must be either
$\mathit{tt}$ or $\mathit{ff}$, and in either case it follows by Lemma 10 (i)
that $\left\llbracket b\right\rrbracket\left\llbracket\sigma\right\rrbracket$
is total, _i.e._ , $\overline{\left\llbracket
b\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\text{id}_{I}$.
Applying the derivation of $\sigma\vdash p\rightsquigarrow b$ to Lemma 11
yields that $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
b\right\rrbracket\left\llbracket\sigma\right\rrbracket$, so specifically
$\overline{\left\llbracket