p\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{\left\llbracket
b\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\text{id}_{I}$, as
desired.

Adequacy for predicates can then be shown by induction on the structure of the
predicate, and by letting Lemma 10 (regarding the totality of predicates) do
much of the heavy lifting.

######  Lemma 13.

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

######  Proof 6.4.

By induction on the structure of $p$.

  * •

Case $p=\mathit{tt}$. Then
$\sigma\vdash\mathit{tt}\rightsquigarrow\mathit{tt}$ by
$\dfrac{}{\sigma\vdash\mathit{tt}\rightsquigarrow\mathit{tt}}$.

  * •

Case $p=\mathit{ff}$. Then
$\sigma\vdash\mathit{ff}\rightsquigarrow\mathit{ff}$ by
$\dfrac{}{\sigma\vdash\mathit{ff}\rightsquigarrow\mathit{ff}}$.

  * •

Case $p=\mathbf{not}~{}p^{\prime}$. Since
$\left\llbracket\mathbf{not}~{}p^{\prime}\right\rrbracket\left\llbracket\sigma\right\rrbracket$
is total, it follows by Lemma 10 that $\left\llbracket
p^{\prime}\right\rrbracket\left\llbracket\sigma\right\rrbracket$ is total as
well, so by induction, there exists $b$ such that $\sigma\vdash
p^{\prime}\rightsquigarrow b$ by some derivation $\mathcal{D}$. We have two
cases to consider: If $b=\mathit{tt}$, $\mathcal{D}$ is a derivation of
$\sigma\vdash p^{\prime}\rightsquigarrow\mathit{tt}$, and so we may derive
$\sigma\vdash\mathbf{not}~{}p^{\prime}\rightsquigarrow\mathit{ff}$ by

$\dfrac{\overset{\mathcal{D}}{\sigma\vdash
p^{\prime}\rightsquigarrow\mathit{tt}}}{\sigma\vdash\mathbf{not}~{}p^{\prime}\rightsquigarrow\mathit{ff}}$

If on the other hand $b=\mathit{ff}$, $\mathcal{D}$ is a derivation of
$\sigma\vdash p^{\prime}\rightsquigarrow\mathit{ff}$, and we may use the other
$\mathbf{not}$-rule with $\mathcal{D}$ to derive

$\dfrac{\overset{\mathcal{D}}{\sigma\vdash
p^{\prime}\rightsquigarrow\mathit{ff}}}{\sigma\vdash\mathbf{not}~{}p^{\prime}\rightsquigarrow\mathit{tt}}\enspace.$

  * •

Case $p=q~{}\mathbf{and}~{}r$. Since we have that $\left\llbracket
q~{}\mathbf{and}~{}r\right\rrbracket\left\llbracket\sigma\right\rrbracket$ is
total, by Lemma 10, so are $\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket$ and $\left\llbracket
r\right\rrbracket\left\llbracket\sigma\right\rrbracket$. Thus, it follows by
induction that there exist $b_{1}$ and $b_{2}$ such that $\sigma\vdash
q\rightsquigarrow b_{1}$ respectively $\sigma\vdash r\rightsquigarrow b_{2}$
by derivations $\mathcal{D}_{1}$ respectively $\mathcal{D}_{2}$. This gives us
four cases depending on what $b_{1}$ and $b_{2}$ are. Luckily, these four
cases match precisely the four different rules we have for $\mathbf{and}$: For
example, if $b_{1}=\mathit{tt}$ and $b_{2}=\mathit{ff}$, we may derive
$\sigma\vdash q~{}\mathbf{and}~{}r\rightsquigarrow\mathit{ff}$ by

$\dfrac{\overset{\mathcal{D}_{1}}{\sigma\vdash
q\rightsquigarrow\mathit{tt}}\qquad\overset{\mathcal{D}_{2}}{\sigma\vdash
r\rightsquigarrow\mathit{ff}}}{\sigma\vdash
q~{}\mathbf{and}~{}r\rightsquigarrow\mathit{ff}},$

and so on.

With computational soundness and adequacy done for the predicates, we turn our
attention to commands. Before we can show computational soundness, we will
need a technical lemma regarding the denotational behaviour of loop bodies in
states $\sigma$ when the relevant predicates are either true or false (see
Definition 6 for the definition of the loop body $\beta[p,c,q]$).

######  Lemma 14.

Let $\sigma$ be a state, and $p$ and $q$ be predicates. Then

  1. (1)

If $\sigma\vdash p\rightsquigarrow\mathit{tt}$ and $\sigma\vdash
q\rightsquigarrow\mathit{tt}$ then
$\beta[p,c,q]_{11}\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma\right\rrbracket$,

  2. (2)

If $\sigma\vdash p\rightsquigarrow\mathit{ff}$ and $\sigma\vdash
q\rightsquigarrow\mathit{tt}$ then
$\beta[p,c,q]_{21}\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma\right\rrbracket$,

  3. (3)

If $\sigma\vdash p\rightsquigarrow\mathit{tt}$ and $\sigma\vdash
q\rightsquigarrow\mathit{ff}$ then
$\beta[p,c,q]_{12}\left\llbracket\sigma\right\rrbracket=\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$, and

  4. (4)

If $\sigma\vdash p\rightsquigarrow\mathit{ff}$ and $\sigma\vdash
q\rightsquigarrow\mathit{ff}$ then
$\beta[p,c,q]_{22}\left\llbracket\sigma\right\rrbracket=\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$.

Further, in each case, for all other choices of $i$ and $j$,
$\beta[p,c,q]_{ij}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$.

######  Proof 6.5.

For (1), suppose $\sigma\vdash p\rightsquigarrow\mathit{tt}$ and $\sigma\vdash
q\rightsquigarrow\mathit{tt}$, so by Lemma 11, $\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 have

$\displaystyle\beta[p,c,q]_{11}\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ (48)
$\displaystyle=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\overline{\left\llbracket
p\right\rrbracket}\left\llbracket\sigma\right\rrbracket=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ (49)
$\displaystyle=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}\left\llbracket\sigma\right\rrbracket}=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\amalg_{1}\left\llbracket\sigma\right\rrbracket$ (50)
$\displaystyle=\amalg_{1}^{\dagger}\amalg_{1}\text{id}_{\Sigma}\left\llbracket\sigma\right\rrbracket=\overline{\amalg_{1}}\left\llbracket\sigma\right\rrbracket=\text{id}_{\Sigma}\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma\right\rrbracket$
(51)

where (48) follows by definition of $\beta[p,c,q]_{11}$ and $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$,
(49) by $\left\llbracket p\right\rrbracket$ a partial isomorphism and the
fourth axiom of restriction categories, (50) 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$
and the first axiom of restriction categories, and (51) by naturality and
totality of $\amalg_{1}$.

The proof of (2) is analogous to that of (1).

For (3), suppose $\sigma\vdash p\rightsquigarrow\mathit{tt}$ and $\sigma\vdash
q\rightsquigarrow\mathit{ff}$, so by Lemma 11, $\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{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{2}\left\llbracket\sigma\right\rrbracket$.
We compute

$\displaystyle\beta[p,c,q]_{12}\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ (52)
$\displaystyle=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\overline{\left\llbracket
p\right\rrbracket}\left\llbracket\sigma\right\rrbracket=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ (53)
$\displaystyle=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\amalg_{2}\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}\left\llbracket\sigma\right\rrbracket}=\amalg_{2}^{\dagger}\amalg_{2}\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\overline{\amalg_{1}}\left\llbracket\sigma\right\rrbracket}$
(54) $\displaystyle=\overline{\amalg_{2}}\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\text{id}_{\Sigma}\left\llbracket\sigma\right\rrbracket}=\text{id}_{\Sigma}\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket\sigma\right\rrbracket}=\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$ (55)

where (52) follows by definition of $\beta[p,c,q]_{12}$ and $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$,
(53) by $\left\llbracket p\right\rrbracket$ a partial isomorphism and the
fourth axiom of restriction categories, (54) by $\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{2}\left\llbracket\sigma\right\rrbracket$,
naturality of $\amalg_{2}$ and Lemma 1, and (55) by totality of $\amalg_{2}$
and the first axiom of restriction categories.

The proof of (4) is analogous.

To see that in each case, for all other choices of $i,j$,
$\beta[p,c,q]_{ij}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$, we show
a few of the cases where $\sigma\vdash p\rightsquigarrow\mathit{tt}$ and
$\sigma\vdash q\rightsquigarrow\mathit{tt}$. The rest follow by the same line
of reasoning. Recall that when $\sigma\vdash p\rightsquigarrow\mathit{tt}$ and
$\sigma\vdash q\rightsquigarrow\mathit{tt}$ we have $\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$.

$\displaystyle\beta[p,c,q]_{12}\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ (56)
$\displaystyle=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\overline{\left\llbracket
p\right\rrbracket}\left\llbracket\sigma\right\rrbracket=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ (57)
$\displaystyle=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\amalg_{1}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\amalg_{2}^{\dagger}\amalg_{1}\text{id}_{\Sigma}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ (58)
$\displaystyle=0_{\Sigma,\Sigma}\text{id}_{\Sigma}\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}=0_{I,\Sigma}$ (59)

where (56) and (57) follow as in (52) and (53), (58) by $\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$
and naturality of $\amalg_{1}$, and (59) by Lemma 7 and the universal mapping
property of the zero object.

Finally, for $\beta[p,c,q]_{21}$ we have

$\displaystyle\beta[p,c,q]_{21}\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\amalg_{2}\left\llbracket\sigma\right\rrbracket=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\gamma\amalg_{1}\left\llbracket\sigma\right\rrbracket$
(60)
$\displaystyle=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\gamma\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\left\llbracket\mathbf{not}~{}p\right\rrbracket\left\llbracket\sigma\right\rrbracket$
(61)
$\displaystyle=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket)\left\llbracket q\right\rrbracket
0_{\Sigma,\Sigma}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$ (62)

where (60) follows by definition of $\beta[p,c,q]_{21}$ and
$\gamma\amalg_{1}=\amalg_{2}$, (61) by $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$
and definition of $\left\llbracket\mathbf{not}~{}p\right\rrbracket$, and (62)
by $\left\llbracket
p\right\rrbracket^{\dagger}\left\llbracket\mathbf{not}~{}p\right\rrbracket=0_{\Sigma,\Sigma}$
and the universal mapping property of the zero object.

With this lemma done, we turn our attention to the preservation lemma for
commands in order to show computational soundness.

######  Lemma 15.

If $\sigma\vdash c\downarrow\sigma^{\prime}$ then $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$.

######  Proof 6.6.

By induction on the structure of the derivation $\mathcal{D}$ of $\sigma\vdash
c\downarrow\sigma^{\prime}$.

  * •

Case $\mathcal{D}=\dfrac{}{\sigma\vdash\mathbf{skip}\downarrow\sigma}$. We
have
$\left\llbracket\mathbf{skip}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\text{id}_{\Sigma}\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma\right\rrbracket$.

  * •

Case $\mathcal{D}=\dfrac{\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}}$.
By induction, $\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$
and $\left\llbracket
c_{2}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime\prime}\right\rrbracket$.
But then

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

as desired.

  * •

Case $\mathcal{D}=\dfrac{\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}}$.
By induction, $\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$,
and by Lemma 11, $\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^{\prime}\right\rrbracket=\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\amalg_{1}\left\llbracket\sigma^{\prime}\right\rrbracket$.
We compute:

$\displaystyle\left\llbracket\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left\llbracket q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ (63)
$\displaystyle=\left\llbracket q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\amalg_{1}\left\llbracket\sigma\right\rrbracket$ (64)
$\displaystyle=\left\llbracket
q\right\rrbracket^{\dagger}\amalg_{1}\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}\amalg_{1}\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ (65)
$\displaystyle=\overline{\left\llbracket
q\right\rrbracket}\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{1}\left\llbracket\sigma^{\prime}\right\rrbracket}$
(66)
$\displaystyle=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\overline{\amalg_{1}}\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\text{id}_{\Sigma}\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket$
(67)

where (63) follows by definition of
$\left\llbracket\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\right\rrbracket$;
(64) by $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\amalg_{1}\left\llbracket\sigma\right\rrbracket$;
(65) by naturality of $\amalg_{1}$, $\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$,
and $\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\amalg_{1}\left\llbracket\sigma^{\prime}\right\rrbracket$;
(66) by $\left\llbracket q\right\rrbracket$ a partial isomorphism, the fourth
axiom of restriction categories, and $\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\amalg_{1}\left\llbracket\sigma^{\prime}\right\rrbracket$;
and (67) by Lemmas 1 and 7 and the first axiom of restriction categories.

  * •

Case $\mathcal{D}=\dfrac{\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}}$.
By induction, $\left\llbracket
c_{2}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$,
and by Lemma 11, $\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^{\prime}\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\amalg_{2}\left\llbracket\sigma^{\prime}\right\rrbracket$.
We have

$\displaystyle\left\llbracket\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left\llbracket q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ (68)
$\displaystyle=\left\llbracket q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\amalg_{2}\left\llbracket\sigma\right\rrbracket$ (69)
$\displaystyle=\left\llbracket
q\right\rrbracket^{\dagger}\amalg_{2}\left\llbracket
c_{2}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}\amalg_{2}\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ (70)
$\displaystyle=\overline{\left\llbracket
q\right\rrbracket}\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{2}\left\llbracket\sigma^{\prime}\right\rrbracket}$
(71)
$\displaystyle=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\overline{\amalg_{2}}\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\text{id}_{\Sigma}\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket.$
(72)

which follows by similar arguments as in (63) – (67).

  * •

Case $\mathcal{D}=\dfrac{\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}$.
Since $\sigma\vdash p\rightsquigarrow\mathit{tt}$ and $\sigma\vdash
q\rightsquigarrow\mathit{tt}$, by Lemma 14 we get
$\beta[p,c,q]_{11}\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma\right\rrbracket$
and $\beta[p,c,q]_{12}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$, and
so

$\displaystyle\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\operatorname{Tr}_{\Sigma,\Sigma}^{\Sigma}(\beta[p,c,q])$
(73)
$\displaystyle\qquad=\left(\beta[p,c,q]_{11}\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}~{}\beta[p,c,q]_{22}^{n}~{}\beta[p,c,q]_{12}\right)\left\llbracket\sigma\right\rrbracket$
(74)
$\displaystyle\qquad=\left(\left(\beta[p,c,q]_{11}\left\llbracket\sigma\right\rrbracket\right)\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}~{}\beta[p,c,q]_{22}^{n}~{}\beta[p,c,q]_{12}\left\llbracket\sigma\right\rrbracket\right)$
(75)
$\displaystyle\qquad=\left\llbracket\sigma\right\rrbracket\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}~{}\beta[p,c,q]_{22}^{n}~{}0_{I,\Sigma}=\left\llbracket\sigma\right\rrbracket\vee
0_{I,\Sigma}=\left\llbracket\sigma\right\rrbracket$ (76)

where (73) follows by definition of
$\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}q\right\rrbracket$,
(74) by definition of the canonical trace in join inverse categories (see
Proposition 2), (75) by distributivity of composition over joins, and (76) by
$\beta[p,c,q]_{11}\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma\right\rrbracket$,
$\beta[p,c,q]_{12}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$, the
universal mapping property of the zero object, and the fact that zero maps are
units for joins.

  * •

Case $\mathcal{D}=\dfrac{\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}}$.
By induction, $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$
and
$\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime\prime}\right\rrbracket$,
and since $\sigma\vdash p\rightsquigarrow\mathit{tt}$ and $\sigma\vdash
q\rightsquigarrow\mathit{ff}$, by Lemma 14 we get
$\beta[p,c,q]_{11}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$ and
$\beta[p,c,q]_{12}\left\llbracket\sigma\right\rrbracket=\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$. Thus

$\displaystyle\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\operatorname{Tr}_{\Sigma,\Sigma}^{\Sigma}(\beta[p,c,q])\left\llbracket\sigma\right\rrbracket$
(77)
$\displaystyle\qquad=\left(\beta[p,c,q]_{11}\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}~{}\beta[p,c,q]_{22}^{n}~{}\beta[p,c,q]_{12}\right)\left\llbracket\sigma\right\rrbracket$
(78)
$\displaystyle\qquad=\left(\left(\beta[p,c,q]_{11}\left\llbracket\sigma\right\rrbracket\right)\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}~{}\beta[p,c,q]_{22}^{n}~{}\beta[p,c,q]_{12}\left\llbracket\sigma\right\rrbracket\right)$
(79)
$\displaystyle\qquad=\left(0_{I,\Sigma}\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}~{}\beta[p,c,q]_{22}^{n}~{}\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket\right)$ (80)
$\displaystyle\qquad=\bigvee_{n\in\omega}\beta[p,c,q]_{21}~{}\beta[p,c,q]_{22}^{n}~{}\left\llbracket\sigma^{\prime}\right\rrbracket$
(81)
$\displaystyle\qquad=\left(\bigvee_{n\in\omega}\beta[p,c,q]_{21}~{}\beta[p,c,q]_{22}^{n}\right)\left\llbracket\sigma^{\prime}\right\rrbracket$
(82)
$\displaystyle\qquad=\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime\prime}\right\rrbracket$
(83)

where (77) follows by the definition of
$\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}q\right\rrbracket$,
(78) by the definition of the canonical trace (Proposition 2), (79) by
distributivity of composition over joins, (80) by
$\beta[p,c,q]_{11}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$ and
$\beta[p,c,q]_{12}\left\llbracket\sigma\right\rrbracket=\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$, (81) by
$\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$ and the fact that zero
maps are units for joins, (82) by distributivity of composition over joins,
and (83) by definition of
$\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket$ and
$\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime\prime}\right\rrbracket$.

  * •

Case $\mathcal{D}=\dfrac{\sigma\vdash
p\rightsquigarrow\mathit{ff}\quad\enspace\sigma\vdash
q\rightsquigarrow\mathit{tt}}{\sigma\vdash\mathit{\underline{loop}}[p,c,q]\downarrow\sigma}$.
Since $\sigma\vdash p\rightsquigarrow\mathit{ff}$ and $\sigma\vdash
q\rightsquigarrow\mathit{tt}$, by Lemma 14 we get
$\beta[p,c,q]_{22}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$ and
$\beta[p,c,q]_{21}\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma\right\rrbracket$.
This gives us

$\displaystyle\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left(\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n}\right)\left\llbracket\sigma\right\rrbracket$
(84)
$\displaystyle=\left(\beta[p,c,q]_{21}\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n+1}\right)\left\llbracket\sigma\right\rrbracket$
(85)
$\displaystyle=\left(\left(\beta[p,c,q]_{21}\left\llbracket\sigma\right\rrbracket\right)\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n+1}\left\llbracket\sigma\right\rrbracket\right)$
(86)
$\displaystyle=\left(\left\llbracket\sigma\right\rrbracket\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n}\beta[p,c,q]_{22}\left\llbracket\sigma\right\rrbracket\right)$
(87)
$\displaystyle=\left(\left\llbracket\sigma\right\rrbracket\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n}0_{I,\Sigma}\right)$
(88) $\displaystyle=\left\llbracket\sigma\right\rrbracket\vee
0_{I,\Sigma}=\left\llbracket\sigma\right\rrbracket$ (89)

where (84) follows by definition of
$\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket$, (85) by
unrolling the case for $n=0$, (86) by distributivity of composition over
joins, (87) by
$\beta[p,c,q]_{21}\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma\right\rrbracket$
and unrolling of the $n+1$-ary composition, (88) by
$\beta[p,c,q]_{22}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$, and
(89) by the universal mapping property of the zero object and the fact that
zero maps are units for joins.

  * •

Case $\mathcal{D}=\dfrac{\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}}$.
By induction, $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$
and
$\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime\prime}\right\rrbracket$,
and since ${\sigma\vdash p\rightsquigarrow\mathit{ff}}$ and $\sigma\vdash
q\rightsquigarrow\mathit{ff}$, it follows by Lemma 14 that
$\beta[p,c,q]_{22}\left\llbracket\sigma\right\rrbracket=\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$ and
$\beta[p,c,q]_{21}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$. We then
have

$\displaystyle\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left(\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n}\right)\left\llbracket\sigma\right\rrbracket$
(90)
$\displaystyle=\left(\beta[p,c,q]_{21}\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n+1}\right)\left\llbracket\sigma\right\rrbracket$
(91)
$\displaystyle=\left(\left(\beta[p,c,q]_{21}\left\llbracket\sigma\right\rrbracket\right)\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n+1}\left\llbracket\sigma\right\rrbracket\right)$
(92)
$\displaystyle=0_{I,\Sigma}\vee\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n+1}\left\llbracket\sigma\right\rrbracket$
(93)
$\displaystyle=\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n}\beta[p,c,q]_{22}\left\llbracket\sigma\right\rrbracket$
(94)
$\displaystyle=\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n}\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$ (95)
$\displaystyle=\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n}\left\llbracket\sigma^{\prime}\right\rrbracket$
(96)
$\displaystyle=\left(\bigvee_{n\in\omega}\beta[p,c,q]_{21}\beta[p,c,q]_{22}^{n}\right)\left\llbracket\sigma^{\prime}\right\rrbracket$
(97)
$\displaystyle=\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime\prime}\right\rrbracket$
(98)

where (90) follows by definition of
$\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket$, (91) by
unrolling the case for $n=0$, (92) by distributivity of composition over
joins, (93) by
$\beta[p,c,q]_{21}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$, (94) by
zero maps units for joins and unrolling of the $n+1$-ary composition, (95) by
$\beta[p,c,q]_{22}\left\llbracket\sigma\right\rrbracket=\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$, (96) by
$\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$,
(97) by distributivity of composition over joins, and finally (98) by
definition of
$\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket$ and
$\left\llbracket\mathit{\underline{loop}}[p,c,q]\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime\prime}\right\rrbracket$.

This finally allows us to show the computational soundness theorem for
commands – and so, for programs – in a straightforward manner.

######  Theorem 16 (Computational soundness).

If there exists $\sigma^{\prime}$ such that $\sigma\vdash
c\downarrow\sigma^{\prime}$ then $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$ is total.

######  Proof 6.7.

Suppose there exists $\sigma^{\prime}$ such that $\sigma\vdash
c\downarrow\sigma^{\prime}$. By Lemma 15, $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$,
and since the interpretation of _any_ state is assumed to be total, it follows
that $\overline{\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{\left\llbracket\sigma^{\prime}\right\rrbracket}=\text{id}_{I}$,
which was what we wanted.

With computational soundness done, we only have computational adequacy left to
prove. Adequacy is much simpler than usual in our case, as we have no higher
order data to deal with, and as such, it can be shown by plain structural
induction rather than by the assistance of logical relations. Nevertheless, we
require two technical lemmas in order to succeed.

######  Lemma 17.

Let $f:A\oplus U\to B\oplus U$ and $s:I\to A$ be morphisms. If
$\operatorname{Tr}^{U}_{A,B}(f)s$ is total, either
$\operatorname{Tr}^{U}_{A,B}(f)s=f_{11}s$, or there exists $n\in\omega$ such
that $\operatorname{Tr}^{U}_{A,B}(f)s=f_{21}f_{22}^{n}f_{12}s$.

######  Proof 6.8.

Since the trace is canonically constructed, it takes the form

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

Further, in the proof of Theorem 20 in [26], it is shown that this join not
only exists but is a _disjoint_ join, _i.e._ , for any choice of $n\in\omega$,

$f_{11}\overline{f_{21}f_{22}^{n}f_{12}}=\left(f_{21}f_{22}^{n}f_{12}\right)\overline{f_{11}}=0_{A,B}$

and for all $n,m\in\omega$ with $n\neq m$,

$\overline{f_{21}f_{22}^{n}f_{12}}f_{21}f_{22}^{m}f_{12}=\overline{f_{21}f_{22}^{m}f_{12}}f_{21}f_{22}^{n}f_{12}=0_{A,B}.$

But then,

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

Since all of the morphisms $\overline{f_{11}s}$ and
$\overline{f_{21}f_{22}^{n}f_{12}s}$ for any $n\in\omega$ are restriction
idempotents $I\to I$, it follows for each of them that they are either equal
to $\text{id}_{I}$ or to $0_{I,I}$. Suppose that none of these are equal to
the identity $\text{id}_{I}$. Then they must all be $0_{I,I}$, and so
$\overline{\operatorname{Tr}^{U}_{A,B}(f)s}=0_{I,I}\neq\text{id}_{I}$,
contradicting totality. On the other hand, suppose that there exists an
identity among these. Then, it follows by the disjointness property above that
the rest must be $0_{I,I}$.

With these done, we are finally ready to tackle the adequacy theorem.

######  Theorem 18 (Computational adequacy).

If $\left\llbracket c\right\rrbracket\left\llbracket\sigma\right\rrbracket$ is
total then there exists $\sigma^{\prime}$ such that ${\sigma\vdash
c\downarrow\sigma^{\prime}}$.

######  Proof 6.9.

By induction on the structure of $c$.

  * •

Case $c=\mathbf{skip}$. Then $\sigma\vdash\mathbf{skip}\downarrow\sigma$ by
$\dfrac{}{\sigma\vdash\mathbf{skip}\downarrow\sigma}$.

  * •

Case $c=c_{1}~{}\mathtt{;}~{}c_{2}$.
In this case, $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
c_{1}~{}\mathtt{;}~{}c_{2}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
c_{2}\right\rrbracket\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket$. Since this is
total, so is $\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket$ by Lemma 1. But
then, by induction, there exists $\sigma^{\prime}$ such that $\sigma\vdash
c_{1}\downarrow\sigma^{\prime}$ by some derivation $\mathcal{D}_{1}$, and by
Lemma 15, $\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$.
But then $\left\llbracket c_{2}\right\rrbracket\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
c_{2}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$, so by
induction there exists $\sigma^{\prime\prime}$ such that
$\sigma^{\prime}\vdash c_{2}\downarrow\sigma^{\prime\prime}$ by some
derivation $\mathcal{D}_{2}$. But then $\sigma\vdash
c_{1}~{}\mathtt{;}~{}c_{2}\downarrow\sigma^{\prime\prime}$ by

$\dfrac{\overset{\mathcal{D}_{1}}{\sigma\vdash
c_{1}\downarrow\sigma^{\prime}}\qquad\enspace\overset{\mathcal{D}_{2}}{\sigma^{\prime}\vdash
c_{2}\downarrow\sigma^{\prime\prime}}}{\sigma\vdash
c_{1}~{}\mathtt{;}~{}c_{2}\downarrow\sigma^{\prime\prime}}\enspace.$

  * •

Case
$c=\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q$.
Thus, $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\right\rrbracket\left\llbracket\sigma\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\left\llbracket\sigma\right\rrbracket$, and since this is
total, $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ is total as well by
analogous argument to the previous case. It then follows by Lemma 13 that
there exists $b$ such that $\sigma\vdash p\rightsquigarrow b$ by some
derivation $\mathcal{D}_{1}$, and by Lemma 11, $\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
b\right\rrbracket\left\llbracket\sigma\right\rrbracket$. We have two cases
depending on what $b$ is.

When $b=\mathit{tt}$ we have

$\displaystyle\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left\llbracket q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left\llbracket q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\amalg_{1}\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}\amalg_{1}\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket$

by $\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 naturality of $\amalg_{1}$. Since this is total, $\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket$ must be total as
well by Lemma 1. But then, by induction, there exists $\sigma^{\prime}$ such
that $\sigma\vdash c_{1}\downarrow\sigma^{\prime}$ by some derivation
$\mathcal{D}_{2}$, and by Lemma 15, $\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$.
Continuing the computation, we get

$\displaystyle\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left\llbracket
q\right\rrbracket^{\dagger}\amalg_{1}\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}\amalg_{1}\left\llbracket\sigma^{\prime}\right\rrbracket=(\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket)^{\dagger}\left\llbracket\sigma^{\prime}\right\rrbracket=\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket}^{\dagger}\left\llbracket\sigma^{\prime}\right\rrbracket$
$\displaystyle=\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket}\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}$

where we exploit that $\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$
as well as the fact that $\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket=\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket}$ (by Lemma 8) and the fact that restriction idempotents are
their own partial inverses. But then $\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}$ must be
total, in turn meaning that $\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ must be
total. But then by Lemma 13, there must exist $b^{\prime}$ such that
$\sigma^{\prime}\vdash q\rightsquigarrow b^{\prime}$ by some derivation
$\mathcal{D}_{3}$, with $\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket
b^{\prime}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ by
Lemma 11. Again, we have two cases depending on $b^{\prime}$. If
$b^{\prime}=\mathit{tt}$, we derive
$\sigma\vdash\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\downarrow\sigma^{\prime}$
by

$\dfrac{\overset{\mathcal{D}_{1}}{\sigma\vdash
p\rightsquigarrow\mathit{tt}}\qquad\enspace\overset{\mathcal{D}_{2}}{\sigma\vdash
c_{1}\downarrow\sigma^{\prime}}\qquad\enspace\overset{\mathcal{D}_{3}}{\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}}$

On the other hand, when $b^{\prime}=\mathit{ff}$, we have

$\displaystyle\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{1}^{\dagger}\amalg_{2}\left\llbracket\sigma^{\prime}\right\rrbracket}$
$\displaystyle=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{0_{\Sigma,\Sigma}\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{0_{I,\Sigma}}=\left\llbracket\sigma^{\prime}\right\rrbracket
0_{I,I}=0_{I,\Sigma}$

using $\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\amalg_{2}\left\llbracket\sigma^{\prime}\right\rrbracket$
and $\amalg_{1}^{\dagger}\amalg_{2}=0_{\Sigma,\Sigma}$ by Lemma 7. But then
$\overline{\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket}=0_{I,I}$,
contradicting $\overline{\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\text{id}_{I}$ since
$0_{I,I}\neq\text{id}_{I}$ by definition of a model. Thus there exists
$\sigma^{\prime}$ such that
$\sigma\vdash\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\downarrow\sigma^{\prime}$.

To show the case when $b=\mathit{ff}$, we proceed as before. We then have

$\displaystyle\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left\llbracket q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\left\llbracket\mathit{ff}\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left\llbracket q\right\rrbracket^{\dagger}(\left\llbracket
c_{1}\right\rrbracket\oplus\left\llbracket
c_{2}\right\rrbracket)\amalg_{2}\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}\amalg_{2}\left\llbracket
c_{2}\right\rrbracket\left\llbracket\sigma\right\rrbracket$

using the fact 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$
and naturality of $\amalg_{2}$. Thus $\left\llbracket
c_{2}\right\rrbracket\left\llbracket\sigma\right\rrbracket$ must be total by
Lemma 1, which means that by induction there exists $\sigma^{\prime}$ such
that $\sigma\vdash c_{2}\downarrow\sigma^{\prime}$ by a derivation
$\mathcal{D}_{2}$, and by Lemma 15, $\left\llbracket
c_{2}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$.
Continuing as before, we obtain now that

$\displaystyle\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left\llbracket
q\right\rrbracket^{\dagger}\amalg_{2}\left\llbracket
c_{2}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket^{\dagger}\amalg_{2}\left\llbracket\sigma^{\prime}\right\rrbracket=(\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket)^{\dagger}\left\llbracket\sigma^{\prime}\right\rrbracket=\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket}^{\dagger}\left\llbracket\sigma^{\prime}\right\rrbracket$
$\displaystyle=\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket}\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}$

and so $\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ must be total
in this case as well (by arguments analogous to the corresponding case for
$b=\mathit{tt}$), so by Lemma 13 there must exist $b^{\prime}$ such that
$\sigma^{\prime}\vdash q\rightsquigarrow b^{\prime}$ by some derivation
$\mathcal{D}_{3}$, and $\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket
b^{\prime}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ by
Lemma 11. Again, we do a case analysis depending on the value of $b^{\prime}$.

If $b^{\prime}=\mathit{tt}$, we have

$\displaystyle\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{2}^{\dagger}\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{2}^{\dagger}\left\llbracket\mathit{tt}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{\amalg_{2}^{\dagger}\amalg_{1}\left\llbracket\sigma^{\prime}\right\rrbracket}$
$\displaystyle=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{0_{\Sigma,\Sigma}\left\llbracket\sigma^{\prime}\right\rrbracket}=\left\llbracket\sigma^{\prime}\right\rrbracket\overline{0_{I,\Sigma}}=\left\llbracket\sigma^{\prime}\right\rrbracket
0_{I,I}=0_{I,\Sigma}$

by arguments analogous to the corresponding case where $b=\mathit{tt}$. This
contradicts the totality of $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$ by
$\overline{\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket}=\overline{0_{I,\Sigma}}=0_{I,I}\neq\text{id}_{I}$,
and we get by contradiction that there exists $\sigma^{\prime}$ such that
$\sigma\vdash\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\downarrow\sigma^{\prime}$.

If $b^{\prime}=\mathit{ff}$, we derive
$\sigma\vdash\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q\downarrow\sigma^{\prime}$
by

$\dfrac{\overset{\mathcal{D}_{1}}{\sigma\vdash
p\rightsquigarrow\mathit{ff}}\qquad\enspace\overset{\mathcal{D}_{2}}{\sigma\vdash
c_{2}\downarrow\sigma^{\prime}}\qquad\enspace\overset{\mathcal{D}_{3}}{\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}}\enspace.$

  * •

Case $c=\mathbf{from}~{}p~{}\mathbf{loop}~{}c_{1}~{}\mathbf{until}~{}q$.
In this case, $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c_{1}~{}\mathbf{until}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\operatorname{Tr}^{\Sigma}_{\Sigma,\Sigma}(\beta[p,c_{1},q])\left\llbracket\sigma\right\rrbracket$.
Since this is total and $\left\llbracket\sigma\right\rrbracket:I\to\Sigma$, it
follows by Lemma 17 that either

$\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c_{1}~{}\mathbf{until}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\beta[p,c_{1},q]_{11}\left\llbracket\sigma\right\rrbracket$

or there exists $n\in\omega$ such that

$\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c_{1}~{}\mathbf{until}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\beta[p,c_{1},q]_{12}\left\llbracket\sigma\right\rrbracket.$

If
$\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c_{1}~{}\mathbf{until}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\beta[p,c_{1},q]_{11}\left\llbracket\sigma\right\rrbracket$,
we have

$\displaystyle\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c_{1}~{}\mathbf{until}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\beta[p,c_{1},q]_{11}\left\llbracket\sigma\right\rrbracket=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c_{1}\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c_{1}\right\rrbracket)\left\llbracket
q\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c_{1}\right\rrbracket)\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$
$\displaystyle=\amalg_{1}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c_{1}\right\rrbracket)\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}~{}\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$

using the trick from previously that $\left\llbracket
p\right\rrbracket^{\dagger}\amalg_{1}=(\left\llbracket
p\right\rrbracket^{\dagger}\amalg_{1})^{\dagger\dagger}=(\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket)^{\dagger}=\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}^{\dagger}=\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}$, $\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}$, the fourth axiom of
restriction idempotents and commutativity of restriction idempotents to obtain
this. It follows by the totality of $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket$ that
$\overline{\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ and
$\overline{\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket}$ must be total, so
$\left\llbracket p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ and
$\left\llbracket q\right\rrbracket\left\llbracket\sigma\right\rrbracket$ must
be total as well. It then follows by Lemma 13 that there exist $b_{1}$ and
$b_{2}$ such that $\sigma\vdash p\rightsquigarrow b_{1}$ and $\sigma\vdash
q\rightsquigarrow b_{2}$ by derivations $\mathcal{D}_{1}$ respectively
$\mathcal{D}_{2}$. But then it follows by Lemma 14 that
$b_{1}=b_{2}=\mathit{tt}$, as we would otherwise have $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\beta[p,c_{1},q]_{11}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$,
contradicting totality. Thus we may derive
$\sigma\vdash\mathbf{from}~{}p~{}\mathbf{loop}~{}c_{1}~{}\mathbf{until}~{}q\downarrow\sigma$
by

$\dfrac{\overset{\mathcal{D}_{1}}{\sigma\vdash
p\rightsquigarrow\mathit{tt}}\qquad\enspace\overset{\mathcal{D}_{2}}{\sigma\vdash
q\rightsquigarrow\mathit{tt}}}{\sigma\vdash\mathbf{from}~{}p~{}\mathbf{loop}~{}c_{1}~{}\mathbf{until}~{}q\downarrow\sigma}.$

On the other hand, suppose that there exists $n\in\omega$ such that

$\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c_{1}~{}\mathbf{until}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket=\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\beta[p,c_{1},q]_{12}\left\llbracket\sigma\right\rrbracket.$

Since this is total, by Lemma 1
$\beta[p,c_{1},q]_{12}\left\llbracket\sigma\right\rrbracket$ is total as well,
and

$\displaystyle\beta[p,c_{1},q]_{12}\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c_{1}\right\rrbracket)\left\llbracket q\right\rrbracket\left\llbracket
p\right\rrbracket^{\dagger}\amalg_{1}\left\llbracket\sigma\right\rrbracket=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c_{1}\right\rrbracket)\left\llbracket
q\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket}\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c_{1}\right\rrbracket)\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\right\rrbracket\left\llbracket\sigma\right\rrbracket}$
$\displaystyle=\amalg_{2}^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c_{1}\right\rrbracket)\left\llbracket
q\right\rrbracket\left\llbracket\sigma\right\rrbracket\overline{\amalg_{1}^{\dagger}\left\llbracket
p\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}$

which follows by arguments analogous to the previous case. But then
$\left\llbracket p\right\rrbracket\left\llbracket\sigma\right\rrbracket$ and
$\left\llbracket q\right\rrbracket\left\llbracket\sigma\right\rrbracket$ must
be total as well, so by Lemma 13 there exist $b_{1}$ and $b_{2}$ such that
$\sigma\vdash p\rightsquigarrow b_{1}$ and $\sigma\vdash q\rightsquigarrow
b_{2}$ by derivations $\mathcal{D}_{1}$ respectively $\mathcal{D}_{2}$. Since
$\beta[p,c_{1},q]_{12}\left\llbracket\sigma\right\rrbracket$ is total, it
further follows by Lemma 14 that $b_{1}=\mathit{tt}$ and $b_{2}=\mathit{ff}$,
as we would otherwise have
$\beta[p,c_{1},q]_{12}\left\llbracket\sigma\right\rrbracket=0_{I,\Sigma}$.
Further,
$\beta[p,c_{1},q]_{12}\left\llbracket\sigma\right\rrbracket=\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket$, and since this is
total, by induction there exists $\sigma^{\prime}$ such that $\sigma\vdash
c_{1}\downarrow\sigma^{\prime}$ by some derivation $\mathcal{D}_{3}$, with
$\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$
by Lemma 15.

To summarize, we have now that

$\displaystyle\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c_{1}~{}\mathbf{until}~{}q\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\beta[p,c_{1},q]_{12}\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma\right\rrbracket$
$\displaystyle=\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\left\llbracket\sigma^{\prime}\right\rrbracket$

is total, and we have derivations $\mathcal{D}_{1}$ of $\sigma\vdash
p\rightsquigarrow\mathit{tt}$, $\mathcal{D}_{2}$ of $\sigma\vdash
q\rightsquigarrow\mathit{ff}$, and $\mathcal{D}_{3}$ of $\sigma\vdash
c_{1}\downarrow\sigma^{\prime}$. To finish the proof, we show by induction on
$n$ that if
$\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\left\llbracket\sigma^{\prime}\right\rrbracket$
is total for any state $\sigma^{\prime}$, there exists a state
$\sigma^{\prime\prime}$ such that
$\sigma^{\prime}\vdash\mathit{\underline{loop}}[p,c_{1},q]\downarrow\sigma^{\prime\prime}$
by some derivation $\mathcal{D}_{4}$.

    * –

In the base case $n=0$, so
$\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\left\llbracket\sigma^{\prime}\right\rrbracket=\beta[p,c_{1},q]_{21}\left\llbracket\sigma^{\prime}\right\rrbracket$.
By proof analogous to previous cases, we have that $\left\llbracket
p\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ and
$\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ must be
total, so by Lemma 13 there exist $b^{\prime}_{1}$ and $b^{\prime}_{2}$ such
that $\sigma^{\prime}\vdash p\rightsquigarrow b^{\prime}_{1}$ and
$\sigma^{\prime}\vdash q\rightsquigarrow b^{\prime}_{1}$ by derivations
$\mathcal{D}^{\prime}_{1}$ respectively $\mathcal{D}^{\prime}_{2}$. Further,
by totality, it follows by Lemma 14 that we must have
$b_{1}^{\prime}=\mathit{ff}$, $b_{2}^{\prime}=\mathit{tt}$. Thus we may
produce our derivation $\mathcal{D}_{4}$ of
$\sigma^{\prime}\vdash\mathit{\underline{loop}}[p,c_{1},q]\downarrow\sigma^{\prime}$
by

$\dfrac{\overset{\mathcal{D}_{1}^{\prime}}{\sigma^{\prime}\vdash
p\rightsquigarrow\mathit{ff}}\quad\enspace\overset{\mathcal{D}_{2}^{\prime}}{\sigma^{\prime}\vdash
q\rightsquigarrow\mathit{tt}}}{\sigma^{\prime}\vdash\mathit{\underline{loop}}[p,c,q]\downarrow\sigma^{\prime}}$

    * –

In the inductive case, we have that

$\displaystyle\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n+1}\left\llbracket\sigma^{\prime}\right\rrbracket=\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\beta[p,c_{1},q]_{22}\left\llbracket\sigma^{\prime}\right\rrbracket$

and since this is assumed to be total, it follows by Lemma 1 that
$\beta[p,c_{1},q]_{22}\left\llbracket\sigma^{\prime}\right\rrbracket$ is total
as well. Again, by argument analogous to previous cases, this implies that
$\left\llbracket
p\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ and
$\left\llbracket
q\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ are both
total, so by Lemma 13 there exist $b_{1}^{\prime}$ and $b_{2}^{\prime}$ such
that $\sigma^{\prime}\vdash p\rightsquigarrow b_{1}^{\prime}$ and
$\sigma^{\prime}\vdash q\rightsquigarrow b_{2}^{\prime}$ by derivations
$\mathcal{D}^{\prime}_{1}$ respectively $\mathcal{D}^{\prime}_{2}$. Likewise,
it then follows by Lemma 14 that since this is total, we must have
$b_{1}^{\prime}=b_{2}^{\prime}=\mathit{ff}$, and so
$\beta[p,c_{1},q]_{22}\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$, again by
Lemma 14. Since $\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$ is total,
by the outer induction hypothesis there exists a derivation
$\mathcal{D}_{3}^{\prime}$ of $\sigma^{\prime}\vdash
c_{1}\downarrow\sigma^{\prime\prime}$ for some $\sigma^{\prime\prime}$, and so
$\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket\sigma^{\prime\prime}\right\rrbracket$
by Lemma 15. But then

$\displaystyle\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n+1}\left\llbracket\sigma^{\prime}\right\rrbracket$
$\displaystyle=\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\beta[p,c_{1},q]_{22}\left\llbracket\sigma^{\prime}\right\rrbracket$
$\displaystyle=\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\left\llbracket
c_{1}\right\rrbracket\left\llbracket\sigma^{\prime}\right\rrbracket$
$\displaystyle=\beta[p,c_{1},q]_{21}\beta[p,c_{1},q]_{22}^{n}\left\llbracket\sigma^{\prime\prime}\right\rrbracket$

since this is total, by (inner) induction there exists a derivation
$\mathcal{D}_{4}^{\prime}$ of
$\sigma^{\prime\prime}\vdash\mathit{\underline{loop}}[p,c_{1},q]\downarrow\sigma^{\prime\prime\prime}$.
Thus, we may produce our derivation $\mathcal{D}_{4}$ as

$\dfrac{\overset{\mathcal{D}^{\prime}_{1}}{\sigma^{\prime}\vdash
p\rightsquigarrow\mathit{ff}}\quad\enspace\overset{\mathcal{D}^{\prime}_{2}}{\sigma^{\prime}\vdash
q\rightsquigarrow\mathit{ff}}\quad\enspace\overset{\mathcal{D}^{\prime}_{3}}{\sigma^{\prime}\vdash
c_{1}\downarrow\sigma^{\prime\prime}}\quad\enspace\overset{\mathcal{D}^{\prime}_{4}}{\sigma^{\prime\prime}\vdash\mathit{\underline{loop}}[p,c,q]\downarrow\sigma^{\prime\prime\prime}}}{\sigma^{\prime}\vdash\mathit{\underline{loop}}[p,c_{1},q]\downarrow\sigma^{\prime\prime\prime}}$

concluding the internal lemma.

Since this is the case, we may finally show
$\sigma\vdash\mathbf{from}~{}p~{}\mathbf{loop}~{}q~{}\mathbf{until}~{}c\downarrow\sigma^{\prime}$
by

$\dfrac{\overset{\mathcal{D}_{1}}{\sigma\vdash
p\rightsquigarrow\mathit{tt}}\quad\enspace\overset{\mathcal{D}_{2}}{\sigma\vdash
q\rightsquigarrow\mathit{ff}}\quad\enspace\overset{\mathcal{D}_{3}}{\sigma\vdash
c\downarrow\sigma^{\prime}}\quad\enspace\overset{\mathcal{D}_{4}}{\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}},$

which concludes the proof.

##  7\. Full abstraction

Where computational soundness and adequacy state an agreement in the notions
of convergence between the operational and denotational semantics, full
abstraction deals with their respective notions of equivalence (see, e.g.,
[32, 29]). Unlike the case for computational soundness and computational
adequacy, where defining a proper notion of convergence required more work on
the categorical side, the tables have turned when it comes to program
equivalence. In the categorical semantics, program equivalence is clear –
equality of interpretations. Operationally, however, there is nothing
immediately corresponding to equality of behaviour at runtime.

To produce this, we consider how two programs may behave when executed from
the same start state. If they always produce the same result, we say that they
are operationally equivalent. Formally, we define this as follows:

Say that programs $p_{1}$ and $p_{2}$ are _operationally equivalent_ , denoted
$p_{1}\approx p_{2}$, if for all states $\sigma$, $\sigma\vdash
p_{1}\downarrow\sigma^{\prime}$ if and only if $\sigma\vdash
p_{2}\downarrow\sigma^{\prime}$.

A model is said to be _equationally fully abstract_ (see, e.g., [32]) if these
two notions of program equivalence are in agreement. In the present section,
we will show a sufficient condition for equational full abstraction of models
of structured reversible flowchart languages. This condition will be that the
given model additionally has the properties of being $I$-_well pointed_ and
_bijective on states_.

Say that a model of a structured reversible flowchart language is $I$-_well
pointed_ if, for all parallel morphisms $f,g:A\to B$, $f=g$ precisely when
$fp=gp$ for all $p:I\to A$.

Say that a model $\mathscr{C}$ of a structured reversible flowchart language
$\mathcal{L}$ is _bijective on states_ if there is a bijective correspondence
between states of $\mathcal{L}$ and _total_ morphisms $I\to\Sigma$ of
$\mathscr{C}$.

If a computationally sound and adequate model of a structured reversible
flowchart language is bijective on states, we can show a stronger version of
Lemma 15.

######  Lemma 19.

If $\mathscr{C}$ be a sound and adequate model of a structured reversible
flowchart language which is bijective on states. Then $\sigma\vdash
c\downarrow\sigma^{\prime}$ iff $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$
and this is total.

######  Proof 7.1.

By Lemma 15 and Theorem 16, we only need to show that $\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$
implies $\sigma\vdash c\downarrow\sigma^{\prime}$. Assume that
$\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime}\right\rrbracket$
and that this is total. By Theorem 18, there exists $\sigma^{\prime\prime}$
such that $\sigma\vdash c\downarrow\sigma^{\prime\prime}$, so by Lemma 15,
$\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime\prime}\right\rrbracket$.
Thus $\left\llbracket\sigma^{\prime}\right\rrbracket=\left\llbracket
c\right\rrbracket\left\llbracket\sigma\right\rrbracket=\left\llbracket\sigma^{\prime\prime}\right\rrbracket$,
so $\sigma^{\prime}=\sigma^{\prime\prime}$ by bijectivity on states.

With this, we can show equational full abstraction.

######  Theorem 20 (Equational full abstraction).

Let $\mathscr{C}$ be a sound and adequate model of a structured reversible
flowchart language that is furthermore $I$-well pointed and bijective on
states. Then $\mathscr{C}$ is equationally fully abstract, _i.e._ ,
$p_{1}\approx p_{2}$ if and only if $\left\llbracket
p_{1}\right\rrbracket=\left\llbracket p_{2}\right\rrbracket$.

######  Proof 7.2.

Suppose $p_{1}\approx p_{2}$, _i.e._ , for all $\sigma$, $\sigma\vdash
p_{1}\downarrow\sigma^{\prime}$ if and only if $\sigma\vdash
p_{2}\downarrow\sigma^{\prime}$. Let $s:I\to\Sigma$ be a morphism. Since
$\mathscr{C}$ is a model of a structured reversible flowchart language, it
follows that either $\overline{s}=\text{id}_{I}$ or $\overline{s}=0_{I,I}$
where $\text{id}_{I}\neq 0_{I,I}$.

If $\overline{s}=0_{I,I}$, we have $\left\llbracket p_{1}\right\rrbracket
s=\left\llbracket p_{2}\right\rrbracket s=0_{I,\Sigma}$ by unicity of the zero
map.

On the other hand, if $\overline{s}=\text{id}_{I}$, by bijectivity on states
there exists $\sigma_{0}$ such that
$s=\left\llbracket\sigma_{0}\right\rrbracket$. Consider now $\left\llbracket
p_{1}\right\rrbracket s=\left\llbracket
p_{1}\right\rrbracket\left\llbracket\sigma_{0}\right\rrbracket$. If this is
total, by Theorem 18 there exists $\sigma_{0}^{\prime}$ such that
$\sigma_{0}\vdash p_{1}\downarrow\sigma_{0}^{\prime}$, and by $p_{1}\approx
p_{2}$, $\sigma_{0}\vdash p_{2}\downarrow\sigma_{0}^{\prime}$ as well. But
then, applying Lemma 15 on both yields that

$\left\llbracket p_{1}\right\rrbracket s=\left\llbracket
p_{1}\right\rrbracket\left\llbracket\sigma_{0}\right\rrbracket=\left\llbracket\sigma_{0}^{\prime}\right\rrbracket=\left\llbracket
p_{2}\right\rrbracket\left\llbracket\sigma_{0}\right\rrbracket=\left\llbracket
p_{2}\right\rrbracket s\enspace.$

If, on the other hand, $\left\llbracket p_{1}\right\rrbracket s$ is not total,
by the contrapositive to Theorem 16, there exists _no_ $\sigma_{0}^{\prime}$
such that $\sigma_{0}\vdash p_{1}\downarrow\sigma_{0}^{\prime}$, so by
$p_{1}\approx p_{2}$ there exists no $\sigma_{0}^{\prime\prime}$ such that
$\sigma_{0}\vdash p_{1}\downarrow\sigma_{0}^{\prime\prime}$. But then, by the
contrapositive of Theorem 18 and the fact that restriction idempotents on $I$
are either $\text{id}_{I}$ or $0_{I,I}$, it follows that

$\left\llbracket p_{1}\right\rrbracket s=\left\llbracket
p_{1}\right\rrbracket\left\llbracket\sigma_{0}\right\rrbracket=0_{I,\Sigma}=\left\llbracket
p_{2}\right\rrbracket\left\llbracket\sigma_{0}\right\rrbracket=\left\llbracket
p_{2}\right\rrbracket s.$

Since $s$ was chosen arbitrarily and $\left\llbracket p_{1}\right\rrbracket
s=\left\llbracket p_{2}\right\rrbracket s$ in all cases, it follows by
$I$-well pointedness that $\left\llbracket
p_{1}\right\rrbracket=\left\llbracket p_{2}\right\rrbracket$.

In the other direction, suppose $\left\llbracket
p_{1}\right\rrbracket=\left\llbracket p_{2}\right\rrbracket$, let $\sigma_{0}$
be a state, and suppose that there exists $\sigma_{0}^{\prime}$ such that
$\sigma_{0}\vdash p_{1}\downarrow\sigma_{0}^{\prime}$. By Lemma 15,
$\left\llbracket
p_{1}\right\rrbracket\left\llbracket\sigma_{0}\right\rrbracket=\left\llbracket\sigma_{0}^{\prime}\right\rrbracket$,
and by Theorem 16 this is total. But then, by $\left\llbracket
p_{1}\right\rrbracket=\left\llbracket p_{2}\right\rrbracket$, $\left\llbracket
p_{2}\right\rrbracket\left\llbracket\sigma_{0}\right\rrbracket=\left\llbracket
p_{1}\right\rrbracket\left\llbracket\sigma_{0}\right\rrbracket=\left\llbracket\sigma_{0}^{\prime}\right\rrbracket$,
so by Lemma 19, $\sigma_{0}\vdash p_{2}\downarrow\sigma_{0}^{\prime}$. The
other direction follows similarly.

##  8\. Applications

In this section, we briefly cover some applications of the developed theory:
We show how the usual program invertion rules can be verified using the
semantics; introduce a small reversible flowchart language, and use the
results from the previous sections to give it semantics; and discuss how
decisions may be used as a programming technique to naturally represent
predicates in a reversible functional language.

###  8.1. Verifying program inversion

A desirable syntactic property for reversible programming languages is to be
closed under program inversion, in the sense that for each program $p$, there
is another program $\mathcal{I}[p]$ such that
$\left\llbracket\mathcal{I}[p]\right\rrbracket=\left\llbracket
p\right\rrbracket^{\dagger}$. Janus, R-WHILE, and R-CORE [40, 19, 20] are all
examples of reversible programming languages with this property. This is
typically witnessed by a _program inverter_ [1, 2], that is, a procedure
mapping the program text of a program to the program text of its inverse
program333While semantic inverses _are_ unique, their program texts generally
are not. As such, a programming language may have many different sound and
complete program inverters, though they will all be equivalent up to program
semantics..

Program inversion of irreversible languages is inherently difficult because of
their backwards nondeterminism and the elimination of nondeterminism requires
advanced machinery (e.g., LR-based parsing methods [18]). Constructing program
inversion for reversible languages is typically straightforward because of
their backward determinism, but exploting this object language property, e.g.,
for proving program inverters correct, is severly hindered by the fact that
conventional metalanguages do not naturally capture these object-language
properties. On the other hand, the categorical foundation considered here
leads to a very concise theorem regarding program inversion for all reversible
flowchart languages.

Suppose that we are given a language where elementary operations are closed
under program inversion (_i.e._ , where each elementary operation $b$ has an
inverse $\mathcal{I}[b]$ such that
$\left\llbracket\mathcal{I}[b]\right\rrbracket=\left\llbracket
b\right\rrbracket^{\dagger}$). We can use the semantics to verify the usual
program inversion rules for $\mathbf{skip}$, sequencing, reversible
conditionals and loops as follows, by structural induction on $c$ with the
hypothesis that $\left\llbracket\mathcal{I}[c]\right\rrbracket=\left\llbracket
c\right\rrbracket^{\dagger}$. For $\mathbf{skip}$, we have

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

thus justifying the inversion rule $\mathcal{I}[\mathbf{skip}]=\mathbf{skip}$.
Likewise for sequences,

$\left\llbracket
c_{1}~{}\mathtt{;}~{}c_{2}\right\rrbracket^{\dagger}=(\left\llbracket
c_{2}\right\rrbracket\left\llbracket
c_{1}\right\rrbracket)^{\dagger}=\left\llbracket
c_{1}\right\rrbracket^{\dagger}\left\llbracket
c_{2}\right\rrbracket^{\dagger}=\left\llbracket\mathcal{I}[c_{1}]\right\rrbracket\left\llbracket\mathcal{I}[c_{2}]\right\rrbracket=\left\llbracket\mathcal{I}[c_{2}]~{}\mathtt{;}~{}\mathcal{I}[c_{1}]\right\rrbracket$

which verifies the inversion rule

$\mathcal{I}[c_{1}~{}\mathtt{;}~{}c_{2}]=\mathcal{I}[c_{2}]~{}\mathtt{;}~{}\mathcal{I}[c_{1}]\enspace.$

Our approach becomes more interesting when we come to conditionals. Given some
conditional statement
$\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q$,
we notice that

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

which verifies the correctness of usual the inversion rule (see, e.g., [19,
20])

$\mathcal{I}[\mathbf{if}~{}p~{}\mathbf{then}~{}c_{1}~{}\mathbf{else}~{}c_{2}~{}\mathbf{fi}~{}q]=\mathbf{if}~{}q~{}\mathbf{then}~{}\mathcal{I}[c_{1}]~{}\mathbf{else}~{}\mathcal{I}[c_{2}]~{}\mathbf{fi}~{}p.$

Finally, for reversible loops, we have

$\displaystyle\left\llbracket\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}q\right\rrbracket^{\dagger}$
$\displaystyle=\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})^{\dagger}$
$\displaystyle=\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})^{\dagger})$
$\displaystyle=\operatorname{Tr}_{\Sigma,\Sigma}^{\Sigma}(\left\llbracket
p\right\rrbracket\left\llbracket
q\right\rrbracket^{\dagger}(\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket^{\dagger}))$
$\displaystyle=\operatorname{Tr}_{\Sigma,\Sigma}^{\Sigma}((\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket^{\dagger})\left\llbracket p\right\rrbracket\left\llbracket
q\right\rrbracket^{\dagger})$
$\displaystyle=\operatorname{Tr}_{\Sigma,\Sigma}^{\Sigma}((\text{id}_{\Sigma}\oplus\left\llbracket\mathcal{I}[c]\right\rrbracket)\left\llbracket
p\right\rrbracket\left\llbracket q\right\rrbracket^{\dagger})$
$\displaystyle=\left\llbracket\mathbf{from}~{}q~{}\mathbf{loop}~{}\mathcal{I}[c]~{}\mathbf{until}~{}p\right\rrbracket$

where the fact that it is a $\dagger$-trace allows us to move the dagger
inside the trace, and dinaturality of the trace in the second component allows
us to move $\text{id}_{\Sigma}\oplus\left\llbracket
c\right\rrbracket^{\dagger}$ from the very right to the very left. This brief
argument verifies the correctness of the inversion rule (see [20])

$\mathcal{I}[\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}q]=\mathbf{from}~{}q~{}\mathbf{loop}~{}\mathcal{I}[c]~{}\mathbf{until}~{}p$

We summarize this in the following theorem:

######  Theorem 21.

If a reversible structured flowchart language is syntactically closed under
inversion of elementary operations, it is also closed under inversion of
reversible sequencing, conditionals, and loops.

###  8.2. Example: A reversible flowchart language

Consider the following family of (neither particularly useful nor particularly
useless) reversible flowchart languages for reversible computing with integer
data, $\mathtt{RINT}_{k}$. $\mathtt{RINT}_{k}$ has precisely $k$ variables
available for storage, denoted $\mathtt{x_{1}}$ through $\mathtt{x_{k}}$ (of
which $\mathtt{x_{1}}$ is designated by convention as the input/output
variable), and its only atomic operations are addition and subtraction of
variables, as well as addition with a constant. Variables are used as
elementary predicates, with zero designating truth and non-zero values all
designating falsehood. For control structures we have reversible conditionals
and loops, and sequencing as usual. This gives the syntax:

$\displaystyle p$
$\displaystyle::=\mathit{tt}\mid\mathit{ff}\mid\mathtt{x_{i}}\mid
p~{}\mathbf{and}~{}p\mid\mathbf{not}~{}p$ (Tests) $\displaystyle c$
$\displaystyle::=c~{}\mathtt{;}~{}c\mid\mathtt{x_{i}}\mathrel{+\\!\\!=}\mathtt{x_{j}}\mid\mathtt{x_{i}}\mathrel{-\\!\\!=}\mathtt{x_{j}}\mid\mathtt{x_{i}}\mathrel{+\\!\\!=}\overline{n}$
$\displaystyle\mid\mathbf{if}~{}p~{}\mathbf{then}~{}c~{}\mathbf{else}~{}c~{}\mathbf{fi}~{}p$
$\displaystyle\mid\mathbf{from}~{}p~{}\mathbf{loop}~{}c~{}\mathbf{until}~{}p$
(Commands)

Here, $\overline{n}$ is the syntactic representation of an integer $n$. In the
cases for addition and subtraction, we impose the additional syntactic
constraints that $1\leq i\leq k$, $1\leq j\leq k$, and $i\neq j$, the latter
to guarantee reversibility. Subtraction by a constant is not included as it
may be derived straightforwardly from addition with a constant. A program in
$\mathtt{RINT}_{k}$ is then simply a command.

We may now give semantics to this language in our framework. For a concrete
model, we select the category $\mathbf{PInj}$ of sets and partial injections,
which is a join inverse category with a join-preserving disjointness tensor
(given on objects by the disjoint union of sets), so it is extensive in the
sense of Definition 4 by Theorem 6. By our developments previously in this
section, to give a full semantics to $\mathtt{RINT}_{k}$ in $\mathbf{PInj}$,
it suffices to provide an object (_i.e._ , a set) of stores $\Sigma$,
denotations of our three classes of elementary operations (addition by a
variable, addition by a constant, and subtraction by a variable) as morphisms
(_i.e._ , partial injective functions) $\Sigma\to\Sigma$, and denotations of
our class of elementary predicates (here, testing whether a variable is zero
or not) as decisions $\Sigma\to\Sigma\oplus\Sigma$. These are all shown in
Figure 4.

$\displaystyle\Sigma$ $\displaystyle=\mathbb{Z}^{k}$
$\displaystyle\left\llbracket\mathtt{x_{i}}\right\rrbracket(a_{1},\dots,a_{k})$
$\displaystyle=\left\\{\begin{array}[]{ll}\amalg_{1}(a_{1},\dots,a_{k})&\quad\text{if
}a_{i}=0\\\
\amalg_{2}(a_{1},\dots,a_{k})&\quad\text{otherwise}\end{array}\right.$
$\displaystyle\left\llbracket\mathtt{x_{i}}\mathrel{+\\!\\!=}\mathtt{x_{j}}\right\rrbracket(a_{1},\dots,a_{k})$
$\displaystyle=(a_{1},\dots,a_{i-1},a_{i}+a_{j},\dots,a_{k})$
$\displaystyle\left\llbracket\mathtt{x_{i}}\mathrel{+\\!\\!=}\overline{n}\right\rrbracket(a_{1},\dots,a_{k})$
$\displaystyle=(a_{1},\dots,a_{i-1},a_{i}+n,\dots,a_{k})$
$\displaystyle\left\llbracket\mathtt{x_{i}}\mathrel{-\\!\\!=}\mathtt{x_{j}}\right\rrbracket(a_{1},\dots,a_{k})$
$\displaystyle=(a_{1},\dots,a_{i-1},a_{i}-a_{j},\dots,a_{k})$ Figure 4. The
object of stores and semantics of elementary operations and predicates of
$\mathtt{RINT}_{k}$ in $\mathbf{PInj}$.

It is uncomplicated to show that all of these are partial injective functions,
and that the denotation of each predicate
$\left\llbracket\mathtt{x_{i}}\right\rrbracket$ is a decision, so that this
is, in fact, a model of $\mathtt{RINT}_{k}$ in $\mathbf{PInj}$.

We can now reap the benefits in the form of a reversibility theorem for free.
Operationally, semantic reversibility of a program is taken to mean that it is
_locally_ forward and backward deterministic; roughly, that any execution of
any subpart of that program is performed in a way that is both forward and
backward deterministic (see, e.g., [6]). Denotationally (see [25, Sec. 1.1]),
the semantic reversibility of a program becomes the property that all of its
meaningful subprograms (including itself) have denotations as partial
isomorphisms. Since every meaningful $\mathtt{RINT}_{k}$ program fragment
takes its semantics in an inverse category, reversibility follows directly.

######  Theorem 22 (Reversibility).

Every $\mathtt{RINT}_{k}$ program is semantically reversible.

Further, since we can straightforwardly show that
$\left\llbracket\mathtt{x_{i}}\mathrel{+\\!\\!=}\mathtt{x_{j}}\right\rrbracket^{\dagger}=\left\llbracket\mathtt{x_{i}}\mathrel{-\\!\\!=}\mathtt{x_{j}}\right\rrbracket$
and
$\left\llbracket\mathtt{x_{i}}\mathrel{+\\!\\!=}\overline{n}\right\rrbracket^{\dagger}=\left\llbracket\mathtt{x_{i}}\mathrel{+\\!\\!=}\overline{-n}~{}\\!\right\rrbracket$,
we can use the technique from Sec. 8.1 to obtain a sound and complete program
inverter.

######  Theorem 23 (Program inversion).

$\mathtt{RINT}_{k}$ has a (sound and complete) program inverter. In
particular, for every $\mathtt{RINT}_{k}$ program $p$ there exists a program
$\mathcal{I}[p]$ such that
$\left\llbracket\mathcal{I}[p]\right\rrbracket=\left\llbracket
p\right\rrbracket^{\dagger}$.

###  8.3. Decisions as a programming technique

Decisions offer a solution to the awkwardness in representing predicates
reversibly, as the usual representations of predicates on $X$ as maps
$\mathit{{}X\mskip 4.0mu plus 1.0mu\to Bool}$ fail to be reversible in all but
the most trivial cases. On the programming side, the reversible
_duplication/equality operator_ $\lfloor\cdot\rfloor$ (see [17, 38]), defined
on lists as

$\displaystyle\lfloor\langle x\rangle\rfloor$ $\displaystyle=\langle
x,x\rangle$ $\displaystyle\lfloor\langle x,y\rangle\rfloor$
$\displaystyle=\left\\{\begin{array}[]{ll}\langle x\rangle&\text{if $x=y$}\\\
\langle x,y\rangle&\text{if $x\neq y$}\end{array}\right.\enspace,$

can be seen as a distant ancestor to this idea of predicates as decisions, in
that it provides an ad-hoc solution to the problem of checking whether two
values are equal in a reversible manner.

Decisions offer a more systematic approach: They suggest that one ought to
define Boolean values in reversible functional programming not in the usual
way, but rather by means of the polymorphic datatype
$\mathit{{}\mathbf{data}\mskip 4.0mu plus 1.0muPBool\mskip 4.0mu plus
1.0mu\alpha\mskip 4.0mu plus 1.0mu=\mskip 4.0mu plus 1.0mu\mskip 4.0mu plus
1.0muTrue\mskip 4.0mu plus 1.0mu\alpha\mskip 4.0mu plus 1.0mu\mid\mskip 4.0mu
plus 1.0mu\mskip 4.0mu plus 1.0muFalse\mskip 4.0mu plus 1.0mu\alpha}$ storing
not only the _result_ , but also _what_ was tested to begin with. With this
definition, negation on these polymorphic Booleans ($\mathit{{}pnot}$) may be
defined straightforwardly as shown in Figure 5. In turn, this allows for more
complex predicates to be expressed in a largely familiar way. For example, the
decision for testing whether a natural number is even ($\mathit{{}peven}$) is
also shown in Figure 5, with $\mathit{{}fmap}$ given in the straightforward
way on polymorphic Booleans, _i.e._ $\mathit{{}fmap\mskip 4.0mu plus 1.0mu}$
$\mathit{{}{}::{}}$ $\mathit{{}{}(\alpha\mskip 4.0mu plus
1.0mu\leftrightarrow\mskip 4.0mu plus 1.0mu\beta)\mskip 4.0mu plus
1.0mu\to\mskip 4.0mu plus 1.0mu(PBool\mskip 4.0mu plus 1.0mu\alpha\mskip 4.0mu
plus 1.0mu\leftrightarrow\mskip 4.0mu plus 1.0mu\mskip 4.0mu plus
1.0muPBool\mskip 4.0mu plus 1.0mu\beta)\mskip 4.0mu plus 1.0mu}$
$\mathit{{}fmap\mskip 4.0mu plus 1.0muf\mskip 4.0mu plus 1.0mu(True\mskip
4.0mu plus 1.0mux)\mskip 4.0mu plus 1.0mu}$ $\mathit{{}{}={}}$
$\mathit{{}{}True\mskip 4.0mu plus 1.0mu(f\mskip 4.0mu plus 1.0mux)\mskip
4.0mu plus 1.0mu}$ $\mathit{{}fmap\mskip 4.0mu plus 1.0muf\mskip 4.0mu plus
1.0mu(False\mskip 4.0mu plus 1.0mux)\mskip 4.0mu plus 1.0mu}$
$\mathit{{}{}={}}$ $\mathit{{}{}False\mskip 4.0mu plus 1.0mu(f\mskip 4.0mu
plus 1.0mux)\mskip 4.0mu plus 1.0mu\enspace.}$ For comparison with the
$\mathit{{}peven}$ function shown in Figure 5, the corresponding irreversible
predicate is typically defined as follows, with $\mathit{{}not}$ the usual
negation of Booleans  $\mathit{{}even\mskip 4.0mu plus 1.0mu}$
$\mathit{{}{}::{}}$ $\mathit{{}{}Nat\mskip 4.0mu plus 1.0mu\to\mskip 4.0mu
plus 1.0muBool\mskip 4.0mu plus 1.0mu}$ $\mathit{{}even\mskip 4.0mu plus
1.0mu0\mskip 4.0mu plus 1.0mu}$ $\mathit{{}{}={}}$ $\mathit{{}{}True\mskip
4.0mu plus 1.0mu}$ $\mathit{{}even\mskip 4.0mu plus 1.0mu(n+1)\mskip 4.0mu
plus 1.0mu}$ $\mathit{{}{}={}}$ $\mathit{{}{}not\mskip 4.0mu plus
1.0mu(even\mskip 4.0mu plus 1.0mun)\mskip 4.0mu plus 1.0mu\enspace.}$ As such,
the reversible implementation as a decision is nearly identical, the only
difference being the use of $\mathit{{}fmap}$ in the definition of
$\mathit{{}peven}$ to recover the input value once the branch has been
decided.

$\mathit{{}pnot\mskip 4.0mu plus 1.0mu}$ | $\mathit{{}{}::{}}$ | $\mathit{{}{}PBool\mskip 4.0mu plus 1.0mu\alpha\mskip 4.0mu plus 1.0mu\leftrightarrow\mskip 4.0mu plus 1.0muPBool\mskip 4.0mu plus 1.0mu\alpha\mskip 4.0mu plus 1.0mu}$
---|---|---
$\mathit{{}pnot\mskip 4.0mu plus 1.0mu(True\mskip 4.0mu plus 1.0mux)\mskip 4.0mu plus 1.0mu}$ | $\mathit{{}{}={}}$ | $\mathit{{}{}False\mskip 4.0mu plus 1.0mux\mskip 4.0mu plus 1.0mu}$
$\mathit{{}pnot\mskip 4.0mu plus 1.0mu(False\mskip 4.0mu plus 1.0mux)\mskip 4.0mu plus 1.0mu}$ | $\mathit{{}{}={}}$ | $\mathit{{}{}True\mskip 4.0mu plus 1.0mux}$

$\mathit{{}peven\mskip 4.0mu plus 1.0mu}$ | $\mathit{{}{}::{}}$ | $\mathit{{}{}Nat\mskip 4.0mu plus 1.0mu\leftrightarrow\mskip 4.0mu plus 1.0muPBool\mskip 4.0mu plus 1.0muNat\mskip 4.0mu plus 1.0mu}$
---|---|---
$\mathit{{}peven\mskip 4.0mu plus 1.0mu0\mskip 4.0mu plus 1.0mu}$ | $\mathit{{}{}={}}$ | $\mathit{{}{}True\mskip 4.0mu plus 1.0mu0\mskip 4.0mu plus 1.0mu}$
$\mathit{{}peven\mskip 4.0mu plus 1.0mu(n+1)\mskip 4.0mu plus 1.0mu}$ | $\mathit{{}{}={}}$ | $\mathit{{}{}fmap\mskip 4.0mu plus 1.0mu(+1)\mskip 4.0mu plus 1.0mu(pnot\mskip 4.0mu plus 1.0mu(peven\mskip 4.0mu plus 1.0mun))}$

Figure 5. The definition of the $\mathit{even}$-predicate as a decision on
natural numbers.

##  9\. Concluding remarks

In the present paper, we have built on the work on extensive restriction
categories [10, 11, 12] to derive a related concept of extensivity for inverse
categories. We have used this concept to give a novel reversible
representation of predicates and their corresponding assertions in
(specifically extensive) join inverse categories with a disjointness tensor,
and in turn used these to model the fundamental control structures of
reversible loops and conditionals in structured reversible flowchart
languages. We have shown that these categorical semantics are computationally
sound and adequate with respect to the operational semantics, and given a
sufficient condition for equational full abstraction.

Further, this approach also allowed us to derive a program inversion theorem
for structured reversible flowchart languages, and we illustrated our approach
by developing a family of structured reversible flowchart languages and using
our framework to give it denotational semantics, with theorems regarding
reversibility and program inversion for free.

The idea to represent predicates by decisions was inspired by the
_instruments_ associated with predicates in Effectus theory [23]. Given that
_side effect free_ instruments $\iota$ in Effectus theory satisfy a similar
rule as decisions in extensive restriction categories, namely
$\nabla\iota=\text{id}$, and that Boolean effecti are extensive, it could be
interesting to explore the connections between extensive restriction
categories and Boolean effecti, especially as regards their internal logic.

Finally, on the programming language side, it could be interesting to further
explore how decisions can be used in reversible programming, e.g., to do the
heavy lifting involved in pattern matching and branch joining. As our focus
has been on the representation of predicates, our approach may be easily
adapted to other reversible flowchart structures, e.g., Janus-style loops
[40].

## References

  * [1] Abramov, S. M. and R. Glück, _The universal resolving algorithm: inverse computation in a functional language_ , in: R. Backhouse and J. N. Oliveira, editors, _Mathematics of Program Construction. Proceedings_ , Lecture Notes in Computer Science 1837 (2000), pp. 187–212.
  * [2] Abramov, S. M. and R. Glück, _The universal resolving algorithm and its correctness: inverse computation in a functional language_ , Science of Computer Programming 43 (2002), pp. 193–229.
  * [3] Axelsen, H. B. and R. Glück, _What do reversible programs compute?_ , in: M. Hofmann, editor, _Foundations of Software Science and Computation Structures. Proceedings_ , Lecture Notes in Computer Science 6604 (2011), pp. 42–56.
  * [4] Axelsen, H. B., R. Glück and T. Yokoyama, _Reversible machine code and its abstract processor architecture_ , in: V. Diekert, M. V. Volkov and A. Voronkov, editors, _Computer Science – Theory and Applications. Proceedings_ , Lecture Notes in Computer Science 4649 (2007), pp. 56–69.
  * [5] Axelsen, H. B. and R. Kaarsgaard, _Join inverse categories as models of reversible recursion_ , in: B. Jacobs and C. Löding, editors, _FOSSACS 2016, Proceedings_ , number 9634 in Lecture Notes in Computer Science (2016), pp. 73–90.
  * [6] Bennett, C. H., _Logical reversibility of computation_ , IBM Journal of Research and Development 17 (1973), pp. 525–532.
  * [7] Carboni, A., S. Lack and R. F. C. Walters, _Introduction to extensive and distributive categories_ , Journal of Pure and Applied Algebra 84 (1993), pp. 145 – 158.
  * [8] Carothers, C. D., K. S. Perumalla and R. M. Fujimoto, _Efficient optimistic parallel simulations using reverse computation_ , ACM Trans. Model. Comput. Simul. 9 (1999), pp. 224–253.
  * [9] Cockett, J. R. B., _Itegories & PCAs_ (2007), slides from talk at FMCS 2007\.
  * [10] Cockett, J. R. B. and S. Lack, _Restriction categories I: Categories of partial maps_ , Theoretical Computer Science 270 (2002), pp. 223–259.
  * [11] Cockett, J. R. B. and S. Lack, _Restriction categories II: Partial map classification_ , Theoretical Computer Science 294 (2003), pp. 61–102.
  * [12] Cockett, R. and S. Lack, _Restriction categories III: Colimits, partial limits and extensivity_ , Mathematical Structures in Computer Science 17 (2007), pp. 775–817.
  * [13] Fiore, M. P., “Axiomatic Domain Theory in Categories of Partial Maps,” Ph.D. thesis, University of Edinburgh (1994).
  * [14] Frank, M. P., “Reversibility for efficient computing,” Ph.D. thesis, EECS Dept., Massachusetts Institute of Technology (1999).
  * [15] Giles, B. G., “An Investigation of some Theoretical Aspects of Reversible Computing,” Ph.D. thesis, University of Calgary (2014).
  * [16] Glück, R. and R. Kaarsgaard, _A categorical foundation for structured reversible flowchart languages_ , in: A. Silva, editor, _Proceedings of the 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII)_ , Electronic Notes in Theoretical Computer Science 336 (2017), pp. 155–171.
  * [17] Glück, R. and M. Kawabe, _A program inverter for a functional language with equality and constructors_ , in: A. Ohori, editor, _Programming Languages and Systems. Proceedings_ , Lecture Notes in Computer Science 2895 (2003), pp. 246–264.
  * [18] Glück, R. and M. Kawabe, _A method for automatic program inversion based on LR(0) parsing_ , Fundamenta Informaticae 66 (2005), pp. 367–395.
  * [19] Glück, R. and T. Yokoyama, _A linear-time self-interpreter of a reversible imperative language_ , Computer Software 33 (2016), pp. 108–128.
  * [20] Glück, R. and T. Yokoyama, _A minimalist’s reversible while language_ , IEICE Transactions on Information and Systems E100-D (2017), pp. 1026–1034.
  * [21] Guo, X., “Products, Joins, Meets, and Ranges in Restriction Categories,” Ph.D. thesis, University of Calgary (2012).
  * [22] Haulund, T., T. Mogensen and R. Glück, _Implementing reversible object-oriented language features on reversible machines_ , in: I. Phillips and H. Rahaman, editors, _Reversible Computation. Proceedings_ , Lecture Notes in Computer Science 10301, 2017, pp. 66–73.
  * [23] Jacobs, B., _New directions in categorical logic, for classical, probabilistic and quantum logic_ , Logical Methods in Computer Science 11 (2015), pp. 1–76.
  * [24] Joyal, A., R. Street and D. Verity, _Traced monoidal categories_ , Mathematical Proceedings of the Cambridge Philosophical Society 119 (1996), pp. 447–468.
  * [25] Kaarsgaard, R., “The Logic of Reversible Computing – Theory and Practice,” Ph.D. thesis, University of Copenhagen (2018).
  * [26] Kaarsgaard, R., H. B. Axelsen and R. Glück, _Join inverse categories and reversible recursion_ , Journal of Logical and Algebraic Methods in Programming 87 (2017), pp. 33–50.
  * [27] Kastl, J., _Inverse categories_ , in: H.-J. Hoehnke, editor, _Algebraische Modelle, Kategorien und Gruppoide_ , Studien zur Algebra und ihre Anwendungen 7, Akademie-Verlag, 1979 pp. 51–60.
  * [28] Mogensen, T. Æ., _Partial evaluation of the reversible language Janus_ , in: _Partial Evaluation and Program Manipulation. Proceedings_ (2011), pp. 23–32.
  * [29] Plotkin, G., _Full abstraction, totality and PCF_ , Mathematical Structures in Computer Science 9 (1999), pp. 1–20.
  * [30] Selinger, P., _Dagger compact closed categories and completely positive maps_ , Electronic Notes in Theoretical Computer Science 170 (2007), pp. 139–163.
  * [31] Selinger, P., _A survey of graphical languages for monoidal categories_ , in: B. Coecke, editor, _New Structures for Physics_ , Lecture Notes in Physics 813 (2011), pp. 289–355.
  * [32] Stoughton, A., “Fully Abstract Models of Programming Languages,” Pitman Publishing, Inc., 1988.
  * [33] Thomsen, M. K., H. B. Axelsen and R. Glück, _A reversible processor architecture and its reversible logic design_ , in: A. De Vos and R. Wille, editors, _Reversible Computation. Proceedings_ , Lecture Notes in Computer Science 7165 (2012), pp. 30–42.
  * [34] Thomsen, M. K., R. Glück and H. B. Axelsen, _Reversible arithmetic logic unit for quantum arithmetic_ , Journal of Physics A: Mathematical and Theoretical 43 (2010), p. 382002.
  * [35] Winskel, G., “The Formal Semantics of Programming Languages: An Introduction,” MIT Press, 1993.
  * [36] Yokoyama, T., H. B. Axelsen and R. Glück, _Reversible flowchart languages and the structured reversible program theorem_ , in: L. Aceto, I. Damgård, L. A. Goldberg, M. M. Halldórsson, A. Ingólfsdóttir and I. Walukiewicz, editors, _International Colloquium on Automata, Languages and Programming. Proceedings_ , Lecture Notes in Computer Science 5126 (2008), pp. 258–270.
  * [37] Yokoyama, T., H. B. Axelsen and R. Glück, _Optimizing reversible simulation of injective functions_ , Journal of Multiple-Valued Logic and Soft Computing 18 (2012), pp. 5–24.
  * [38] Yokoyama, T., H. B. Axelsen and R. Glück, _Towards a reversible functional language_ , in: A. De Vos and R. Wille, editors, _RC 2011_ , Lecture Notes in Computer Science 7165 (2012), pp. 14–29.
  * [39] Yokoyama, T., H. B. Axelsen and R. Glück, _Fundamentals of reversible flowchart languages_ , Theoretical Computer Science 611 (2016), pp. 87–115.
  * [40] Yokoyama, T. and R. Glück, _A reversible programming language and its invertible self-interpreter_ , in: _Partial Evaluation and Semantics-Based Program Manipulation. Proceedings_ (2007), pp. 144–153.