A CATEGORICAL FOUNDATION FOR STRUCTURED REVERSIBLE
FLOWCHART LANGUAGES: SOUNDNESS AND ADEQUACY
ROBERT GLÜCK AND ROBIN KAARSGAARD

arXiv:1710.03666v1 [] 10 Oct 2017

DIKU, Department of Computer Science, University of Copenhagen, Denmark
e-mail address: glueck@acm.org
DIKU, Department of Computer Science, University of Copenhagen, Denmark
e-mail address: robin@di.ku.dk
Abstract. Structured reversible flowchart languages is a class of imperative reversible
programming languages allowing for a simple diagrammatic representation of control flow
built from a limited set of control flow structures. This class includes the reversible
programming language Janus (without recursion), as well as more recently developed reversible programming languages such as R-CORE and R-WHILE.
In the present paper, we develop a categorical foundation for this class of languages
based on inverse categories with joins. We generalize the notion of extensivity of restriction
categories to one that may be accommodated by inverse categories, and use the resulting
decision maps to give a reversible representation of predicates and assertions. This leads
to a categorical semantics for structured reversible flowcharts, which we show to be both
sound, adequate, and fully abstract with respect to the operational semantics under certain
conditions.

1. Introduction
Reversible computing is an emerging paradigm that adopts a physical principle of reality
into a computation model without information erasure. Reversible computing extends the
standard forward-only mode of computation with the ability to execute in reverse as easily as forward. Reversible computing is a necessity in the context of quantum computing
and some bio-inspired computation models. Regardless of the physical motivation, bidirectional determinism is interesting in its own right. The potential benefits include the
design of innovative reversible architectures (e.g., [28, 27, 30]), new programming models
1998 ACM Subject Classification: D.3.1, F.3.2.
Key words and phrases: Reversible computing, flowchart languages, structured programming, categorical
semantics, category theory.
This is the extended version of an article presented at MFPS XXXIII [14], extended with proofs that
previously appeared in the appendix, as well as new sections on soundness, adequacy, and full abstraction.
The authors acknowledge the support given by COST Action IC1405 Reversible computation: Extending
horizons of computing. We also thank the anonymous reviewers of MFPS XXXIII for their thoughtful and
detailed comments on a previous version of this paper.

LOGICAL METHODS
IN COMPUTER SCIENCE

DOI:10.2168/LMCS-???

1

c Glück and Kaarsgaard
Creative Commons

2

GLÜCK AND KAARSGAARD

and techniques (e.g., [32, 15, 23]), and the enhancement of software with reversibility (e.g.,
[6]).
The semantics of reversible programming languages are usually formalized using traditional metalanguages such as structural operational semantics or denotational semantics
based on complete partial orders. However, these are geared towards the definition of conventional programming languages. The fundamental properties of a reversible language
are not naturally captured by these metalanguages and are to be shown individually for
each semantic definition, such as the required backward determinism and the invertibility
of object language programs.
This paper aims at providing a new categorical foundation specifically for formalizing
reversible programming languages, in particular the semantics of reversible structured flowchart languages [29], which are the reversible counterpart of the structured programming
languages used today. This formalization is based on join inverse categories with a developed notion of extensivity for inverse categories, which gives rise to natural representations
of predicates and assertions, and consequently to models of reversible structured flowcharts.
The goal is to provide a framework for modelling these languages, such that the reversible
semantic properties of the object language are naturally ensured by the meta language.
The semantic framework we are going to present in this paper covers the reversible structured languages regardless of their concrete formation, such as atomic operations, elementary predicates, and value domains. Reversible programming languages that are instances of
this computation model include the imperative language Janus [32] without recursion, and
the while languages R-WHILE and R-CORE with dynamic data structures [16, 17]. Further,
unstructured reversible flowchart languages, such as reversible assembly languages with
jumps [12, 3], can be transformed into structured ones thanks to the structured reversible
program theorem [29].
Overview: In Section 2, we give an introduction to structured reversible flowchart languages, while Section 3 describes the restriction and inverse category theory used as backdrop in later sections. In Section 4, we warm up by developing a notion of extensivity for
inverse categories, based on extensive restriction categories and its associated concept of
decisions. Then, in Section 5, we put it all to use by showing how decisions may be used
to model predicates and ultimately also reversible flowcharts, and we show that these are
sound and adequate with respect to the operational semantics in Section 6. In Section 7,
we extend the previous theorems by giving a sufficient condition for full abstraction. In Section 8, we show how to extract a program inverter from the categorical semantics, develop
a small language to exemplify our framework, and discuss other applications in reversible
programming. Section 9 offers some concluding remarks.
2. Reversible structured flowcharts
Structured reversible flowcharts naturally model the control flow behavior of reversible
(imperative) programming languages in a simple diagrammatic representation, as classical
flowcharts do for conventional languages. A crucial difference is that atomic steps are
limited to partial injective functions and they require an additional assertion, an explicit
orthogonalizing condition, at join points in the control flow.
A structured reversible flowchart F is built from four blocks (Figure 1): An atomic
step that performs an elementary operation on a domain X specified by a partial injective
function a : X ⇀ X; a while loop over a block B with entry assertion p1 : X → Bool and

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

✲ a

✲

(a) Step

✓✏
t✲
t
✲
✲ p❅
p1
2
✒✑❅
f
f
✻
B ✛
(b) While loop

3

✲ B1

t
t ✏
❄
✓
✲ p❅
p2 ✲
1
❅
✒✑
f
f
✻
✲
B2

(c) Selection

✲ B1

✲ B2

✲

(d) Sequence

Figure 1: Structured reversible flowcharts.
exit test p2 : X → Bool ; a selection of block B1 or B2 with entry test p1 : X → Bool
and exit assertion p2 : X → Bool ; and a sequence of blocks B1 and B2 . The operational
semantics of these are shown in Figure 2.
A structured reversible flowchart F consists of one main block. Blocks have unique entry
and exit points, and can be nested any number of times to form more complex flowcharts.
The interpretation of F consists of a given domain X (typically, a store) and a finite set of
partial injective functions a and predicates p : X → Bool . Computation starts at the entry
point of F in an initial x0 (the input), proceeds sequentially through the edges of F , and
ends at the exit point of F in a final xn (the output), if F is defined on the given input.
Though the specific set of predicates depend on the flowchart language, they are often (as
we will do here) assumed to be closed under Boolean operators, in particular conjunction
and negation. The operational semantics for these are the same as in the irreversible case;
see Figure 3.
The assertion p1 in a reversible while loop (marked by the circle [32]) is a new flowchart
operator: the predicate p1 must be true when the control flow reaches the assertion along
the t-edge, and false when it reaches the assertion along the f -edge; otherwise, the loop is
undefined. The test p2 (marked by a diamond) has the usual semantics. This means that
B in a loop is repeated as long as p1 and p2 are false.
The selection has an assertion p2 , which must be true when the control flow reaches the
assertion from B1 , and false when the control flow reaches the assertion from B2 ; otherwise,
the selection is undefined. As usual, the test p1 selects B1 or B2 . The assertion makes the
selection reversible.
Despite their simplicity, reversible structured flowcharts are reversibly universal [2],
which means that they are computationally as powerful as any reversible programming
language can be. Given a suitable domain X for finite sets of atomic operations and
predicates, there exists, for every injective computable function f : X → Y , a reversible
flowchart F that computes f .
Reversible structured flowcharts (Figure 1) have a straightforward representation as
program texts defined by the grammar
B ::= a | from p loop B until p | if p then B else B fi p | B ; B
It is often assumed, as we will do here, that the set of atomic steps contains a step skip
that acts as the identity. Reversible structured flowcharts defined above corresponds to the
reversible language R-WHILE [16], but their value domain, atomic functions and predicates
are unspecified. As a minimum, a reversible flowchart needs blocks (a,b,d) because selection
(c) can be simulated by combining while loops that conditionally skip the body block or
execute it once. R-CORE [17] is an example of such a minimal language.

4

GLÜCK AND KAARSGAARD

σ ⊢ p ↓ σ′
σ ⊢ skip ↓ σ

σ ⊢ c1 ↓ σ ′
σ ′ ⊢ c2 ↓ σ ′′
σ ⊢ c1 ; c2 ↓ σ ′′

σ ⊢ p ↓ tt
σ ⊢ c1 ↓ σ ′
σ ′ ⊢ q ↓ tt
σ ⊢ if p then c1 else c2 fi q ↓ σ ′

σ ⊢ p ↓ ff
σ ⊢ c2 ↓ σ ′
σ ′ ⊢ q ↓ ff
σ ⊢ if p then c1 else c2 fi q ↓ σ ′

σ ⊢ p ↓ tt
σ ⊢ q ↓ tt
σ ⊢ from p loop c until q ↓ σ

σ ⊢ p ↓ ff
σ ⊢ q ↓ tt
σ ⊢ loop[p, c, q] ↓ σ

σ ⊢ p ↓ ff

σ ⊢ q ↓ ff
σ ⊢ c ↓ σ′
σ ′ ⊢ loop[p, c, q] ↓ σ ′′
σ ⊢ loop[p, c, q] ↓ σ ′′

σ ⊢ p ↓ tt

σ ⊢ q ↓ ff
σ ⊢ c ↓ σ′
σ ′ ⊢ loop[p, c, q] ↓ σ ′′
σ ⊢ from p loop c until q ↓ σ ′′

Figure 2: Operational semantics for the reversible flowchart structures.
σ⊢p↓b
σ ⊢ tt ↓ tt

σ ⊢ ff ↓ ff

σ ⊢ p ↓ tt
σ ⊢ not p ↓ ff

σ ⊢ p ↓ ff
σ ⊢ not p ↓ tt

σ ⊢ p ↓ tt
σ ⊢ q ↓ tt
σ ⊢ p and q ↓ tt

σ ⊢ p ↓ tt
σ ⊢ q ↓ ff
σ ⊢ p and q ↓ ff

σ ⊢ p ↓ ff
σ ⊢ q ↓ tt
σ ⊢ p and q ↓ ff

σ ⊢ p ↓ ff
σ ⊢ q ↓ ff
σ ⊢ p and q ↓ ff

Figure 3: Operational semantics for Boolean predicates.
3. Restriction and inverse categories
The following section contains the background on restriction and inverse category theory
necessary for our later developments. Unless otherwise specified, the definitions and results
presented in this section can be found in introductory texts on the subject (e.g., [13, 18, 8,
9, 10]).
Restriction categories [8, 9, 10] axiomatize categories of partial maps. This is done by
assigning to each morphism f a restriction idempotent f , which we think of as a partial
identity defined precisely where f is. Formally, restriction categories are defined as follows.
Definition 1. A restriction category is a category C equipped with a combinator mapping
f

f

each morphism A −
→ B to a morphism A −
→ A satisfying

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

5

(iii) f g = f g, and
(iv) gf = f gf

(i) f f = f ,
(ii) gf = f g,
for all suitable g.

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

In restriction categories, we say that a morphism A −
→ B is total if f = idA , and a
f†

partial isomorphism if there exists a (necessarily unique) partial inverse B −→ A such that
f † f = f and f f † = f † . Isomorphisms are then simply the total partial isomorphisms with
total partial inverses. An inverse category can then be defined as a special kind of restriction
category1.
Definition 2. An inverse category is a restriction category where each morphism is a partial
isomorphism.
Every restriction category C gives rise to an inverse category Inv(C ), which has as
objects all objects of C , and as morphisms all of the partial isomorphisms of C . As such,
since partial isomorphisms in Pfn are partial injective functions, a canonical example of an
inverse category is the category Inv(Pfn) ∼
= PInj of sets and partial injective functions.
Since each morphism in an inverse category has a unique partial inverse, as also suggested by our notation this makes inverse categories canonically dagger categories [25], in
the sense that they come equipped with a contravariant endofunctor (−)† satisfying f = f ††
and id†A = idA for each morphism f and object A.
Given two restriction categories C and D, the well-behaved functors between them are
restriction functors, i.e., functors F satisfying F (f ) = F (f ). Analogous to how regular
semigroup homomorphisms preserve partial inverses in inverse semigroups, when C and D
are inverse categories, all functors between them are restriction functors; specifically they
preserve the canonical dagger, i.e., F (f † ) = F (f )† .
3.1. Partial order enrichment and joins. A consequence of how restriction (and inverse)
categories are defined is that hom sets C (A, B) may be equipped with a partial order given
by f ≤ g iff gf = f (this extends to an enrichment in the category of partial orders and
monotone functions). Intuitively, this states that f is below g iff g behaves exactly like f
when restricted to the points where f is defined. A sufficient condition for each C (A, B)
to have a least element is that C has a restriction zero; a zero object 0 in the usual sense
0A,A

0A,A

which additionally satisfies A −−−→ A = A −−−→ A for each endo-zero map 0A,A .
One may now wonder when C (A, B) has joins as a partial order. Unfortunately, C (A, B)
has joins of all morphisms only in very degenerate cases. However, if instead of considering
arbitrary joins we consider joins of maps that are somehow compatible, this becomes much
more viable.
1This is a rather modern definition due to [8]. Originally, inverse categories were defined as the categorical

extensions of inverse semigroups; see [22].

6

GLÜCK AND KAARSGAARD

Definition 3. In a restriction category, say that parallel maps f and g are disjoint iff
f g = 0; and compatible iff f g = gf .
It can be shown that disjointness implies compatibility, as disjointness is expectedly
symmetric. Further, we may extend this to say that a set of parallel morphisms is disjoint
iff each pair of morphisms is disjoint, and likewise for compatibility. This gives suitable
notions of join restriction categories.
Definition 4. A restriction category C has compatible (disjoint) joins if it has a restriction
zero, and satisfies that
W for each compatible (disjoint) subset S of any hom set C (A, B), there
exists a morphism s∈S s such that
W
W
(i) s ≤ s∈S s for all s ∈ S, and s ≤ t for all s ∈ S implies s∈S s ≤ t;
W
W
(ii) s∈S s =  s∈S s;
W
W
(iii) f
s = s∈S (f s) for all f : B → X; and
W s∈S
W
(iv)
s∈S s g =
s∈S (sg) for all g : Y → A.

For inverse categories, the situation is a bit more tricky, as the join of two compatible
partial isomorphisms may not be a partial isomorphism. To ensure this, we need stronger
relations:
Definition 5. In an inverse category, say that parallel maps f and g are disjoint iff f g = 0
and f † g † = 0; and compatible iff f g = gf and f † g† = g † f † .
We may now extend this to notions of disjoint sets and compatible sets of morphisms
in inverse categories as before. This finally gives notions of join inverse categories:
Definition 6. An inverse category C has compatible (disjoint) joins if it has a restriction
zero and satisfies that for all compatible (disjoint) subsets S of all hom sets C (A, B), there
exists a morphism ∨s∈S s satisfying (i) – (iv) of Definition 4.
A functor F between
restriction
(or inverse) categories with joins is said to be joinW
W
preserving when F ( s∈S s) = s∈S F (s).

3.2. Restriction coproducts, extensivity, and related concepts. While a restriction
category may very well have coproducts, these are ultimately only well-behaved when all
coproduct injections are total; if this is the case, we say that the restriction category has
restriction coproducts. If a restriction category has all finite restriction coproducts, it also
has a restriction zero serving as unit.
In [10], it is shown that the existence of certain maps, called decisions, in a restriction
category C with restriction coproducts leads to the subcategory Total(C ) of total maps
being extensive (in the sense of, e.g., [5]). This leads to the definition of an extensive
restriction category 2.

Definition 7. A restriction category is said to be extensive (as a restriction category) if it
f

has restriction coproducts and a restriction zero, and for each map A −
→ B + C there is a
hf i

unique decision A −−→ A + A satisfying

2The name is admittedly mildly confusing, as an extensive restriction category is not extensive in the

usual sense. Nevertheless, we stay with the established terminology.

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

(D.1): ∇hf i = f and

7

(D.2): (f + f )hf i = (κ1 + κ2 )f .

In the above, ∇ denotes the codiagonal [id, id]. A consequence of these axioms is that
each decision is a partial isomorphism; one can show that hf i must be partial inverse to
[κ†1 f , κ†2 f ] (see [10]). Further, when a restriction category with restriction coproducts has
finite joins, it is also extensive with hf i = κ1 κ†1 f ∨ κ2 κ†2 f . As an example, Pfn is extensive
hf i

f

with A −−→ A + A for A −
→ B + C given by

if f (x) = κ1 (y) for some y ∈ B
 κ1 (x)
κ2 (x)
if f (x) = κ2 (z) for some z ∈ C .
hf i(x) =

undefined if f (x) is undefined

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

Definition 8. A disjointness tensor on a restriction category is a symmetric monoidal
restriction functor −⊕− satisfying that its unit is the restriction zero, and that the canonical
maps
ρ−1

id⊕0

∐1 = A −−→ A ⊕ 0 −−−→ A ⊕ B

λ−1

0⊕id

∐2 = B −−→ 0 ⊕ B −−−→ A ⊕ B

are jointly epic, where ρ respectively λ is the left respectively right unitor of the monoidal
functor − ⊕ −.
It can be straightforwardly shown that any restriction coproduct gives rise to a disjointness tensor. A useful interaction between compatible joins and a join-preserving disjointness
tensor in inverse categories was shown in [4, 21], namely that it leads to a †-trace (in the
sense of [20, 26]):
Proposition 1. Let C be an inverse category with (at least countable) compatible joins and
a join-preserving disjointness tensor. Then C has a trace operator given by
_
TrU
f21 f22 f12
A,B (f ) = f11 ∨
n∈ω

satisfying

†
TrU
A,B (f )

=

†
TrU
A,B (f ),

where fij = ∐†j f ∐i .

4. Extensivity of inverse categories
As discussed earlier, extensivity of restriction categories hinges on the existence of certain
partial isomorphisms – decisions – yet their axiomatization relies on the presence of a map
that is not a partial isomorphism, the codiagonal.
In this section, we tweak the axiomatization of extensivity of restriction categories to
one that is equivalent, but additionally transports more easily to inverse categories. We then
give a definition of extensitivity for inverse categories, from which it follows that Inv(C ) is
an extensive inverse category when C is an extensive restriction category.
Recall that decisions satisfy the following two axioms:

8

GLÜCK AND KAARSGAARD

(D.1): ∇hf i = f and

(D.2): (f + f )hf i = (κ1 + κ2 )f

As mentioned previously, an immediate problem with this is the reliance on the codiagonal. However, intuitively, what (D.1) states is simply that the decision hf i cannot do
anything besides to tag its inputs appropriately. Using a disjoint join, we reformulate this
axiom to the following:
(D’.1): (κ†1 hf i) ∨ (κ†2 hf i) = f
Note that this axiom also subtly states that disjoint joins of the given form always exist.
Say that a restriction category is pre-extensive if it has restriction coproducts, a restricf

hf i

tion zero, and a combinator mapping each map A −
→ B + C to a pre-decision A −−→ A + A
(with no additional requirements). We can then show the following:
Theorem 4.1. Let C be a pre-extensive restriction category. The following are equivalent:
(i) C is an extensive restriction category.
(ii) Every pre-decision of C satisfies (D.1) and (D.2).
(iii) Every pre-decision of C satisfies (D’.1) and (D.2).
To show this theorem, we will need the following lemma:
Lemma 4.2. In an extensive restriction category, joins of the form (f + 0) ∨ (0 + g) exist
f

g

for all maps A −
→ B and C −
→ D and are equal to f + g.
h

Proof. By [7], for any map A −
→ B +C in an extensive restriction category, h = (κ†1 h)∨(κ†2 h).
But then f + g = (κ†1 f + g) ∨ (κ†2 f + g) = (id + 0f + g) ∨ (0 + idf + g) = (f + 0) ∨ (0 + g).
We can now continue with the proof.
Proof. The equivalence between (i) and (ii) was given in [10]. That (ii) and (iii) are equivalent follows by
(κ†1 hf i) ∨ (κ†2 hf i) = ([id, 0]hf i) ∨ ([0, id]hf i)
= (∇id + 0hf i) ∨ (∇0 + idhf i)
= ∇(id + 0 ∨ 0 + id)hf i
= ∇(id + id)hf i = ∇hf i
where we note that the join id + 0 ∨ 0 + id exists and equals id + id when every predecision satisfies (D.1) and (D.2) by Lemma 4.2. That the join also exists when every predecision satisfies (D’.1) and (D.2) follows as well, since the universal mapping property for
coproducts guarantees that the only map g satisfying (κ1 +κ2 )+(κ1 +κ2 )g = (κ1 +κ2 )(κ1 +κ2 )
is κ1 + κ2 itself, so we must have hκ1 + κ2 i = κ1 + κ2 , and
(id + 0) ∨ (0 + id) = κ†1 ∨ κ†2 = (κ1 κ†1 ) ∨ (κ2 κ†2 )
= (κ†1 (κ1 + κ2 )) ∨ κ†2 (κ1 + κ2 ))
= κ1 + κ2 = id + id
which was what we wanted.

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

9

Another subtle consequence of our amended first rule is that κ†1 hf i is its own restriction
idempotent (and likewise for κ†2 ) since κ†1 hf i ≤ (κ†1 hf i) ∨ (κ†2 hf i) = f ≤ id, as the maps
below identity are precisely the restriction idempotents.
Our next snag in transporting this definition to inverse categories has to do with the
restriction coproducts themselves, as it is observed in [13] that any inverse category with
restriction coproducts is a preorder. Intuitively, the problem is not that unicity of coproduct
maps cannot be guaranteed in non-preorder inverse categories, but rather that the coproduct
[f,g]

map A + B −−→ C in a restriction category is not guaranteed to be a partial isomorphism
when f and g are.
For this reason, we will consider the more general disjointness tensor for sum-like constructions rather than full-on restriction coproducts, as inverse categories may very well
have a disjointness tensor without it leading to immediate degeneracy. Notably, PInj has
a disjointness tensor, constructed on objects as the disjoint union of sets (precisely as the
restriction coproduct in Pfn, but without the requirement of a universal mapping property).
This leads us to the following definition:
Definition 9. An inverse category with a disjointness tensor is said to be extensive when
hf i

f

each map A −
→ B ⊕ C has a unique decision A −−→ A ⊕ A satisfying
(D’.1): (∐†1 hf i) ∨ (∐†2 hf i) = f
(D’.2): (f ⊕ f )hf i = (∐1 ⊕ ∐2 )f .
hf i

As an example, PInj is an extensive inverse category with the unique decision A −−→
f

A ⊕ A for a partial injection A −
→ B ⊕ C given by

if f (x) = ∐1 (y) for some y ∈ B
 ∐1 (x)
∐2 (x)
if f (x) = ∐2 (z) for some z ∈ C
hf i(x) =

undefined if f (x) is undefined

.

Aside from a shift from coproduct injections to the quasi-injections of the disjointness tensor,
a subtle change here is the notion of join. That is, for restriction categories with disjoint
joins, any pair of maps f, g with f g = 0 has a join – but for inverse categories, we additionally
require that their inverses are disjoint as well, i.e., that f † g † = 0, for the join to exist. In
this case, however, there is no difference between the two. As previously discussed, a direct
consequence of this axiom is that each ∐†i hf i must be its own restriction idempotent. Since
restriction idempotents are self-adjoint (i.e., satisfy f = f † ), they are disjoint iff their
inverses are disjoint.
Since restriction coproducts give rise to a disjointness tensor, we may straightforwardly
show the following theorem.
Theorem 4.3. When C is an extensive restriction category, Inv(C ) is an extensive inverse
category.
Further, constructing the decision hf i as (∐1 ∐†1 f ) ∨ (∐2 ∐†2 f ) (i.e., mirroring the construction of decisions in restriction categories with disjoint joins), we may show the following.
Theorem 4.4. Let C be an inverse category with a disjointness tensor, a restriction zero,
and finite disjoint joins. Then C is extensive as an inverse category.

10

GLÜCK AND KAARSGAARD

5. Modelling structured reversible flowcharts
In the following, let C be an inverse category with (at least countable) compatible joins and
a join-preserving disjointness tensor. As disjoint joins are compatible, it follows that C is
an extensive inverse category with a (uniform) †-trace operator.
In this section, we will show how this framework can be used model reversible structured
flowchart languages. First, we will show how decisions in extensive inverse categories can
be used to model predicates, and how this representation extends to give very natural
semantics to reversible flowcharts corresponding to conditionals and loops. Then we will
use the “internal program inverter” given by the canonical dagger functor on C to extract
a program inverter for reversible flowcharts.
5.1. Predicates as decisions. In suitably equipped categories, one naturally considers
predicates on an object A as given by maps A → 1 + 1. In inverse categories, however,
the mere idea of a predicate as a map of the form A → 1 ⊕ 1 is problematic, as only very
degenerate maps of this form are partial isomorphisms. In the following, we show how
decisions give rise to an unconventional yet ultimately useful representation of predicates.
To our knowledge this representation is novel, motivated here by the necessity to model
predicates in a reversible fashion, as decisions are always partial isomorphisms.
The simplest useful predicates are the predicates that are always true respectively always false. By convention, we represent these by the left respectively right injection (which
are both their own decisions),
JttK = ∐1

Jff K = ∐2 .

Semantically, we may think of decisions as a separation of an object A into witnesses and
counterexamples of the predicate it represents. In a certain sense, the axioms of decisions
say that there is nothing more to a decision than how it behaves when postcomposed with
∐†1 or ∐†2 . As such, given the convention above, we think of ∐†1 hpi as the witnesses of the
predicate represented by the decision hpi, and ∐†2 hpi as its counterexamples.
With this in mind, we turn to boolean combinators. The negation of a predicateas-a-decision must simply swap witnesses for counterexamples (and vice versa). In other
words, we obtain the negation of a decision by postcomposing with the commutator γ of
the disjointness tensor,
Jnot pK = γ JpK .
With this, it is straightforward to verify that, e.g., Jnot ttK = Jff K, as
Jnot ttK = γ∐1 = γid ⊕ 0ρ−1 = 0 ⊕ idγρ−1 = 0 ⊕ idλ−1 = ∐2 = Jff K .

For conjunction, we exploit that our category has (specifically) finite disjoint joins, and
define the conjunction of predicates-as-decisions JpK and JqK by
Jp and qK = (∐1 ∐†1 JpK ∐†1 JqK) ∨ (∐2 (∐†2 JpK ∨ ∐†2 JqK))JpK JqK.

The intuition behind this definition is that the witnesses of a conjunction of predicates is
given by the meet of the witnesses of the each predicate, while the counterexamples of a
conjunction of predicates is the join of the counterexamples of each predicate. Note that
this is then precomposed with JpK JqK to ensure that the result is only defined where both
p and q are; this gives

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

11

Noting that the meet of two restriction idempotents is given by their composition, this
is precisely what this definition states. Similarly we define the disjunction of JpK and JqK by
Jp or qK = (∐1 (∐†1 JpK ∨ ∐†1 JqK)) ∨ (∐2 (∐†2 JpK ∐†2 JqK))JpK JqK,

as Jp or qK then has as witnesses the join of the witnesses of JpK and JqK, and as counterexamples the meet of the counterexamples of JpK and JqK. With these definitions, it can be
shown that, e.g., the De Morgan laws are satisfied. However, since we can thus construct
this from conjunctions and negations, we will leave disjunctions as syntactic sugar.
That all of these are indeed decisions can be shown straightforwardly, as summarized
in the following closure theorem.
Theorem 5.1. Decisions in C are closed under Boolean negation, conjunction, and disjunction.
5.2. Reversible structured flowcharts, categorically. To give a categorical account of
structured reversible flowchart languages, we assume the existence of a suitable distinguished
object Σ of stores, which we think of as the domain of computation, such that we may give
denotations to structured reversible flowcharts as morphisms Σ → Σ.
Since atomic steps (corresponding to elementary operations, e.g., store updates) may
vary from language to language, we assume that each such atomic step in our language has
a denotation as a morphism Σ → Σ. In the realm of reversible flowcharts, these atomic
steps are required to be partial injective functions; here, we abstract this to require that
their denotation is a partial isomorphism (though this is a trivial requirement in inverse
categories).
Likewise, elementary predicates (e.g., comparison of values in a store) may vary from
language to language, so we assume that such elementary predicates have denotations as
well as decisions Σ → Σ ⊕ Σ. If necessary (as is the case for Janus [32]), we may then
close these elementary predicates under boolean combinations as discussed in the previous
section.
To start, we note how sequencing of flowcharts may be modelled trivially by means of
composition, i.e.,
Jc1 ; c2 K = Jc2 K Jc1 K
or, using the diagrammatic notation of flowcharts and the string diagrams for monoidal
categories in the style of [26] (read left-to-right and bottom-to-top),
y
q
✲ c1 ✲ c2 ✲ =
Jc1 K
Jc2 K
.

To extend this elementary model to one that additionally models reversible conditionals,
we observe that the partial inverse to a decision is precisely its corresponding assertion.
Intuitively, a decision separates an object into witnesses (in the first component) and counterexamples (in the second). As such, the partial inverse to a decision must be defined only
on witnesses in the first component, and only on counterexamples in the second.
With this in mind, we achieve a denotation of reversible conditionals as
Jif p then c1 else c2 fi qK = JqK† Jc1 K ⊕ Jc2 K JpK

12

GLÜCK AND KAARSGAARD

or, as diagrams
u

✲ c1

w
t
w
❅
w ✲ p
w ❅
v
f

✲ c2

}


t ✏
❄
✓

q ✲ =
✒ ✑
~
f
✻

JpK

Jc2 K
Jc1 K

JqK

†

.

For reversible loops, we use the †-trace operator to obtain the denotation
†
Jfrom p loop c until qK = TrΣ
Σ,Σ (idΣ ⊕ JcK JqK JpK )

or diagrammatically
u

}

✓✏
t
✲ p❅ t✲
q
w ✲
v ✒✑❅
~ =
f
f
✻
c ✛

JqK

†

JpK

JcK

.

That this has the desired operational behavior follows from the fact that the †-trace operator
is canonically constructed in join inverse categories as
_
n
TrU
f21 f22
f12 .
X,Y (f ) = f11 ∨
n∈ω

∐†j f ∐i .

As such, for our loop construct defined above, the f11 -cases
Recall that fij =
correpond to cases where a given state bypasses the loop entirely; f21 f12 (that is, for n = 0)
to cases where exactly one iteration is performed by a given state before exiting the loop;
f21 f22 f12 to cases where two iterations are performed before exiting; and so on. In this way,
the given trace semantics contain all successive loop unrollings, as desired. We will make
this more formal in the following section, where we show soundness and adequacy for these
with respect to the operational semantics.
In order to be able to provide a correspondence between categorical and operational
semantics, we also need an interpretation of the meta-command loop. While it may not be
so clear at the present, it turns out that the appropriate one is
_
q
y
loop[p, c, q] =
β[p, c, q]21 β[p, c, q]n22
n∈ω

where β[p, c, q] = idΣ ⊕JcK JqK JpK† , i.e., the inner part of the interpretation of the from-loop.
While it may seem like a small point, the mere existence of a categorical semantics in
inverse categories for a reversible programming language has some immediate benefits. In
particular, that a programming language is reversible can be rather complicated to show
by means of operational semantics (see, e.g., [32, Sec. 2.3]), yet it follows directly in our
categorical semantics, as all morphisms in inverse categories have a unique partial inverse.
6. Soundness and adequacy
Soundness and adequacy (see, e.g., [11]) are the two fundamental properties of operational
semantics with respect to their denotational counterparts, as soundness and completeness
are for proof systems with respect to their semantics. In brief, soundness and adequacy state
that the respective notions of convergence of the operational and denotational semantics
are in agreement.

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

13

In the operational semantics, the notion of convergence seems straightforward: a program p converges in a state σ if there exists another state σ ′ such that σ ⊢ p ↓ σ ′ . On the
denotational side, it seems less obvious what a proper notion of convergence is.
An idea (used by, e.g., Fiore [11]) is to let values (in this case, states) be interpreted as
total morphisms from some sufficiently simple object I into an appropriate object V (here,
we will use our object Σ of states). In this context, the notion of convergence for a program
p in a state σ is then that the resulting value (state) JpK JσK is again, a state – i.e., it is
total. Naturally, this approach requires machinery to separate total maps from partial ones.
As luck would have it, inverse categories fit the bill perfectly, as they can be regarded as
special instances of restriction categories.
To make this idea more clear in the current context, and to allow us to use the established formulations of soundness and adequacy, we define a model of a structured reversible
flowchart language to be the following:
Definition 10. A model of a structured reversible flowchart language L consists of a join
inverse category C with a disjointness tensor, further equipped with distinguished objects
I and Σ satisfying
(i) the identity and zero maps on I are distinct, i.e., idI 6= 0I,I ,
e
(ii) if I −
→ I is a restriction idempotent then e = idI or e = 0I,I , and
JσK

(iii) each L-state σ is interpreted as a total morphism I −−→ Σ.
Here, we think of I as the indexing object, and Σ as the object of states. In irreversible
programming languages, the first two conditions in the definition above are often left out,
as the indexing object is typically chosen to be the terminal object 1. However, terminal
objects are degenerate in inverse categories, as they always coincide with the initial object
when they exist – that is, they are zero objects. For this reason, we require instead the
existence of a sufficiently simple indexing object, as described by these two properties. For
example, in PInj, any one-element set will satisfy these conditions.
Even further, the third condition is typically proven rather than assumed. We include
it here as an assumption since structured reversible flowchart languages may take many
different forms, and we have no way of knowing how the concrete states are formed. As
such, rather than limiting ourselves to languages where states take a certain form in order
to show totality of interpretation, we instead assume it to be able to show properties about
more programming languages.
This also leads us to another important point: We are only able to show soundness and
adequacy for the operational semantics as they are stated, i.e., we are not able to take into
account the specific atomic steps (besides skip) or elementary predicates of the language.
As such, soundness and adequacy (and what may follow from that) should be understood conditionally: If a structured reversible flowchart language has a model of the form
above and it is sound and adequate with respect to its atomic steps and elementary predicates, then the entire interpretation is sound and adequate as well.
We begin by recalling the definition of the denotation of predicates and commands in
a model of a structured reversible flowchart language from Section 5.
Definition 11. Recall the interpretation of predicates in L as decisions in C :
(i) JttK = ∐1 ,
(ii) Jff K = ∐2 ,
(iii) Jnot pK = γ JpK,

14

GLÜCK AND KAARSGAARD

  


(iv) Jp and qK = ∐1 ∐†1 JpK ∐†1 JqK ∨ ∐2 ∐†2 JpK ∨ ∐†2 JqK JpK JqK.

Definition 12. Recall the interpretation of commands in L (and the meta-command loop)
as morphisms Σ → Σ in C :
(i) JskipK = idΣ ,
(ii) Jc1 ; c2 K = Jc2 K Jc1 K,
(iii) Jif p then c1 else c2 fi qK = JqK† (Jc1 K ⊕ Jc2 K) JpK,
(iv) Jfrom p loop c until qK = TrΣ
Σ,Σ (β[p, c, q]), and
q
y W
(v) loop[p, c, q] = n∈ω β[p, c, q]21 β[p, c, q]n22

where β[p, c, q] = (idΣ ⊕ JcK) JqK JpK† : Σ ⊕ Σ → Σ ⊕ Σ. Note also that fij = ∐†j f ∐i .

The overall strategy we will use to show soundness and adequacy for programs is to
start by showing it for predicates. To begin to tackle this, we first need a lemma regarding
the totality of predicates.
Lemma 6.1. Let p and q be L-predicates. It is the case that
JσK

JttK

JσK

JσK

Jnot pK

JσK

Jp and qK

Jff K

(i) I −−→ Σ −−→ Σ ⊕ Σ and I −−→ Σ −−→ Σ ⊕ Σ are total,
JσK

JpK

(ii) I −−→ Σ −−−−−→ Σ ⊕ Σ is total iff I −−→ Σ −−→ Σ ⊕ Σ is, and
JσK

JpK

JσK

JqK

(iii) I −−→ Σ −−−−−−→ Σ ⊕ Σ is total iff I −−→ Σ −−→ Σ ⊕ Σ and I −−→ Σ −−→ Σ ⊕ Σ both
are.
Proof. For (i), it follows that
JttK JσK = ∐1 JσK = ∐1 JσK = idΣ JσK = JσK = idI ,

where the final equality follows by the definition of a model. The case for ff is entirely
analogous.
For (ii), we have that
Jnot pK JσK = γ JpK JσK = γ JpK JσK = idΣ⊕Σ JpK JσK = JpK JσK
JσK

Jnot pK

JσK

JpK

which implies directly that I −−→ Σ −−−−−→ Σ ⊕ Σ is total iff I −−→ Σ −−→ Σ ⊕ Σ is.
For (iii), it suffices to show that Jp and qK JσK = JpK JσKJqK JσK, since JpK JσK = JqK JσK =
idI then yields Jp and qK JσK = idI idI = idI directly; the other direction follows by the fact
that if gf = id then id = gf = gf f = idf = f (and analogously for g).
We start by observing that
JpK JσK = ((∐1 ∐†1 JpK) ∨ (∐2 ∐†2 JpK)) JσK

= ((∐1 ∐†1 JpK JσK) ∨ (∐2 ∐†2 JpK JσK))

= ((∐1 JσK ∐†1 JpK JσK) ∨ (∐2 JσK ∐†2 JpK JσK))

= ((∐1 JσK ∐†1 JpK JσK) ∨ (∐2 JσK ∐†2 JpK JσK))
= ((∐1 JσK∐†1 JpK JσK) ∨ (∐2 JσK∐†2 JpK JσK))
= ∐†1 JpK JσK ∨ ∐†2 JpK JσK

= ∐†1 JpK JσK ∨ ∐†2 JpK JσK

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

15

where ∐1 JσK = ∐2 JσK = idI follows by (i), and ∐†1 JpK = ∐†1 JpK and ∐†2 JpK = ∐†2 JpK follow
by JpK a decision. We may establish by analogous argument that
JqK JσK = ∐†1 JqK JσK ∨ ∐†2 JqK JσK

as well. In the following, let σp = JpK JσK and σq = JqK JσK. We have

 

Jp and qK JσK = ∐†1 JpK JσK ∐†1 JqK JσK ∨ ∐†2 JpK JσK ∨ ∐†2 JqK JσK JpK JσK JqK JσK

 

= ∐†1 σp ∐†1 σq ∨ ∐†2 σp ∨ ∐†2 σq σp σq



= ∐†1 σp ∐†1 σq ∨ ∐†2 σp ∨ ∐†2 σq σp σq

 
 

= ∐†1 σp ∐†1 σq σp σq ∨ ∐†2 σp σp σq ∨ ∐†2 σq σp σq
 
 


= ∐†1 σp σp ∐†1 σq σq ∨ ∐†2 σp σp σq ∨ ∐†2 σq σq σp

 
 

= ∐†1 σp ∐†1 σq ∨ ∐†2 σp σq ∨ ∐†2 σq σp
 

 



= ∐†1 σp ∐†1 σq ∨ ∐†2 σp ∐†1 σq ∨ ∐†2 σq ∨ ∐†2 σq ∐†1 σp ∨ ∐†2 σp
 
 
 
 


= ∐†1 σp ∐†1 σq ∨ ∐†2 σp ∐†1 σq ∨ ∐†2 σp ∐†2 σq ∨ ∐†2 σq ∐†1 σp ∨ ∐†2 σq ∐†2 σp

 
 
 

= ∐†1 σp ∐†1 σq ∨ ∐†1 σp ∐†2 σq ∨ ∐†2 σp ∐†1 σq ∨ ∐†2 σp ∐†2 σq



= ∐†1 σp ∨ ∐†2 σp ∐†1 σq ∨ ∐†2 σq = σp σq

which was what we wanted.

A common way to show soundness (see, e.g., [11]) is to show a kind of preservation
property; that interpretations are, in a sense, preserved across evaluation in the operational
semantics. This is shown in the following lemma:
Lemma 6.2. If σ ⊢ p ↓ b then JpK JσK = JbK JσK.

Proof. By induction on the structure of the derivation D of σ ⊢ p ↓ b.
. We trivially have JttK JσK = JttK JσK.
• Case D =
σ ⊢ tt ↓ tt
• Case D =
. Again, we trivially have Jff K JσK = Jff K JσK.
σ ⊢ ff ↓ ff
σ ⊢ p ↓ tt
.
• Case D =
σ ⊢ not p ↓ ff
By induction we have that JpK JσK = JttK JσK = ∐1 JσK. But then Jnot pK JσK =
γ JpK JσK = γ ∐1 JσK = ∐2 JσK = Jff K JσK.
σ ⊢ p ↓ ff
.
• Case D =
σ ⊢ not p ↓ tt
By induction we have that JpK JσK = Jff K JσK = ∐2 JσK.
γ JpK JσK = γ ∐2 JσK = ∐1 JσK = JttK JσK.
σ ⊢ p ↓ tt
σ ⊢ q ↓ tt
.
• Case D =
σ ⊢ p and q ↓ tt

Thus Jnot pK JσK =

16

GLÜCK AND KAARSGAARD

By induction JpK JσK = JttK JσK = ∐1 JσK and JqK JσK = JttK JσK = ∐1 JσK. We
compute
  


Jp and qK JσK = ∐1 ∐†1 JpK ∐†1 JqK ∨ ∐2 ∐†2 JpK ∨ ∐†2 JqK JpK JqK JσK
 



= ∐1 JσK ∐†1 JpK JσK ∐†1 JqK JσK ∨ ∐2 JσK ∐†2 JpK JσK ∨ ∐†2 JqK JσK


JpK JσK JqK JσK

 


= ∐1 JσK ∐†1 ∐1 JσK ∐†1 ∐1 JσK ∨ ∐2 JσK ∐†2 ∐1 JσK ∨ ∐†2 ∐1 JσK

∐1 JσK ∐1 JσK
 


= ∐1 JσK JσK JσK ∨ ∐2 JσK 0Σ,Σ JσK ∨ 0Σ,Σ JσK JσK JσK


= (∐1 JσK) ∨ (∐2 JσK (0I,I ∨ 0I,I )) JσK
= (∐1 JσK) ∨ (∐2 JσK 0I,I ) JσK

= ((∐1 JσK) ∨ 0I,Σ⊕Σ )JσK
• Case D =

= ∐1 JσK JσK = ∐1 JσK = Jtt K JσK .
σ ⊢ p ↓ ff
σ ⊢ q ↓ tt
.
σ ⊢ p and q ↓ ff

By induction JpK JσK = Jff K JσK = ∐2 JσK and JqK JσK = JttK JσK = ∐1 JσK.


  

Jp and qK JσK = ∐1 ∐†1 JpK ∐†1 JqK ∨ ∐2 ∐†2 JpK ∨ ∐†2 JqK JpK JqK JσK
 



= ∐1 JσK ∐†1 JpK JσK ∐†1 JqK JσK ∨ ∐2 JσK ∐†2 JpK JσK ∨ ∐†2 JqK JσK


JpK JσK JqK JσK

 


= ∐1 JσK ∐†1 ∐2 JσK ∐†1 ∐1 JσK ∨ ∐2 JσK ∐†2 ∐2 JσK ∨ ∐†2 ∐1 JσK
∐2 JσK ∐1 JσK

 


= ∐1 JσK 0Σ,Σ JσK JσK ∨ ∐2 JσK JσK ∨ 0Σ,Σ JσK JσK JσK


 

= ∐1 JσK 0I,I JσK ∨ ∐2 JσK JσK ∨ 0I,I JσK



= 0I,Σ⊕Σ ∨ ∐2 JσK JσK JσK


= ∐2 JσK JσK JσK = ∐2 JσK = Jff K JσK

σ ⊢ p ↓ tt
σ ⊢ q ↓ ff
, similar to the previous case.
σ ⊢ p and q ↓ ff
σ ⊢ p ↓ ff
σ ⊢ q ↓ ff
.
• Case D =
σ ⊢ p and q ↓ ff
• Case D =

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

17

By induction JpK JσK = Jff K JσK = ∐2 JσK and JqK JσK = Jff K JσK = ∐2 JσK.
  


Jp and qK JσK = ∐1 ∐†1 JpK ∐†1 JqK ∨ ∐2 ∐†2 JpK ∨ ∐†2 JqK JpK JqK JσK

 


= ∐1 JσK ∐†1 JpK JσK ∐†1 JqK JσK ∨ ∐2 JσK ∐†2 JpK JσK ∨ ∐†2 JqK JσK
JpK JσK JqK JσK

 


= ∐1 JσK ∐†1 ∐2 JσK ∐†1 ∐2 JσK ∨ ∐2 JσK ∐†2 ∐2 JσK ∨ ∐†2 ∐2 JσK


∐2 JσK ∐2 JσK

 


= ∐1 JσK 0Σ,Σ JσK 0Σ,Σ JσK ∨ ∐2 JσK JσK ∨ JσK JσK JσK


= (∐1 JσK 0I,I ) ∨ ∐2 JσK JσK JσK



= 0I,Σ⊕Σ ∨ ∐2 JσK JσK JσK


= ∐2 JσK JσK JσK = ∐2 JσK = Jff K JσK .

With this done, the soundness lemma for predicates follows readily.
Lemma 6.3. If there exists b such that σ ⊢ p ↓ b then JpK JσK is total.

Proof. Suppose there exists b such that σ ⊢ p ↓ b by some derivation. It follows by the operational semantics that b must be either tt or ff , and in either case it follows by Lemma 6.1 (i)
that JbK JσK is total, i.e., JbK JσK = idI . Applying the derivation of σ ⊢ p ↓ b to Lemma 6.2
yields that JpK JσK = JbK JσK, so specifically JpK JσK = JbK JσK = idI , as desired.

Adequacy for predicates can then be shown by induction on the structure of the predicate, and by letting Lemma 6.1 (regarding the totality of predicates) do much of the heavy
lifting.
Lemma 6.4. If JpK JσK is total then there exists b such that σ ⊢ p ↓ b.

Proof. By induction on the structure of p.
.
• Case p = tt. Then σ ⊢ tt ↓ tt by
σ ⊢ tt ↓ tt
• Case p = ff . Then σ ⊢ ff ↓ ff by
.
σ ⊢ ff ↓ ff
• Case p = not p′ . Since Jnot p′ K JσK is total, it follows by Lemma 6.1 that Jp′ K JσK is
total as well, so by induction, there exists b such that σ ⊢ p′ ↓ b by some derivation
D. We have two cases to consider: If b = tt, D is a derivation of σ ⊢ p′ ↓ tt, and so
we may derive σ ⊢ not p′ ↓ ff by
D

σ ⊢ p′ ↓ tt
σ ⊢ not p′ ↓ ff
If on the other hand b = ff , D is a derivation of σ ⊢ p′ ↓ ff , and we may use the
other not-rule with D to derive
D

σ ⊢ p′ ↓ ff
.
σ ⊢ not p′ ↓ tt

18

GLÜCK AND KAARSGAARD

• Case p = q and r. Since we have that Jq and rK JσK is total, by Lemma 6.1, so are
JqK JσK and JrK JσK. Thus, it follows by induction that there exist b1 and b2 such that
σ ⊢ q ↓ b1 respectively σ ⊢ r ↓ b2 by derivations D1 respectively D2 . This gives us
four cases depending on what b1 and b2 are. Luckily, these four cases match precisely
the four different rules we have for and: For example, if b1 = tt and b2 = ff , we
may derive σ ⊢ q and r ↓ ff by
D1

D2

σ ⊢ q ↓ tt
σ ⊢ r ↓ ff
,
σ ⊢ q and r ↓ ff
and so on.
With soundness and adequacy done for the predicates, we turn our attention to commands. Before we can show soundness, we will need a technical lemma regarding the
denotational behaviour of loop bodies in states σ when the relevant predicates are either
true or false (see Definition 12 for the definition of the loop body β[p, c, q]).
Lemma 6.5. Let σ be a state, and p and q be predicates. Then
(1) If σ ⊢ p ↓ tt and σ ⊢ q ↓ tt then β[p, c, q]11 JσK = JσK,
(2) If σ ⊢ p ↓ ff and σ ⊢ q ↓ tt then β[p, c, q]21 JσK = JσK,
(3) If σ ⊢ p ↓ tt and σ ⊢ q ↓ ff then β[p, c, q]12 JσK = JcK JσK, and
(4) If σ ⊢ p ↓ ff and σ ⊢ q ↓ ff then β[p, c, q]22 JσK = JcK JσK.
Further, in each case, for all other choices of i and j, β[p, c, q]ij JσK = 0I,Σ .

Proof. For (1), suppose σ ⊢ p ↓ tt and σ ⊢ q ↓ tt, so by Lemma 6.2, JpK JσK = JttK JσK =
∐1 JσK and JqK JσK = JttK JσK = ∐1 JσK. We have
β[p, c, q]11 JσK = ∐†1 (idΣ ⊕ JcK) JqK JpK† ∐1 JσK = ∐†1 (idΣ ⊕ JcK) JqK JpK† JpK JσK
= ∐†1 (idΣ ⊕ JcK) JqK JpK JσK = ∐†1 (idΣ ⊕ JcK) JqK JσK JpK JσK

= ∐†1 (idΣ ⊕ JcK) ∐1 JσK ∐1 JσK = ∐†1 (idΣ ⊕ JcK) ∐1 JσK
= ∐†1 ∐1 idΣ JσK = ∐1 JσK = idΣ JσK = JσK .

The proof of (2) is analogous to that of (1).
For (3), suppose σ ⊢ p ↓ tt and σ ⊢ q ↓ ff , so by Lemma 6.2, JpK JσK = JttK JσK = ∐1 JσK
and JqK JσK = Jff K JσK = ∐2 JσK. We compute
β[p, c, q]12 JσK = ∐†2 (idΣ ⊕ JcK) JqK JpK† ∐1 JσK = ∐†2 (idΣ ⊕ JcK) JqK JpK† JpK JσK
= ∐†2 (idΣ ⊕ JcK) JqK JpK JσK = ∐†2 (idΣ ⊕ JcK) JqK JσK JpK JσK
= ∐†2 (idΣ ⊕ JcK) ∐2 JσK ∐1 JσK = ∐†2 ∐2 JcK JσK ∐1 JσK
= ∐2 JcK JσK idΣ JσK = idΣ JcK JσK JσK = JcK JσK

The proof of (4) is analogous.
To see that in each case, for all other choices of i, j, β[p, c, q]ij JσK = 0I,Σ , we show a
few of the cases where σ ⊢ p ↓ tt and σ ⊢ q ↓ tt. The rest follow by the same line of
reasoning. Recall that when σ ⊢ p ↓ tt and σ ⊢ q ↓ tt we have JpK JσK = JttK JσK = ∐1 JσK

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

19

and JqK JσK = JttK JσK = ∐1 JσK.

β[p, c, q]12 JσK = ∐†2 (idΣ ⊕ JcK) JqK JpK† ∐1 JσK = ∐†2 (idΣ ⊕ JcK) JqK JpK† JpK JσK
= ∐†2 (idΣ ⊕ JcK) JqK JpK JσK = ∐†2 (idΣ ⊕ JcK) JqK JσK JpK JσK
= ∐†2 (idΣ ⊕ JcK) ∐1 JσK JpK JσK = ∐†2 ∐1 idΣ JσK JpK JσK
= 0Σ,Σ idΣ JσK JpK JσK = 0I,Σ .

For β[p, c, q]21 , we have

β[p, c, q]21 JσK = ∐†1 (idΣ ⊕ JcK) JqK JpK† ∐2 JσK = ∐†1 (idΣ ⊕ JcK) JqK JpK† γ ∐1 JσK

= ∐†1 (idΣ ⊕ JcK) JqK JpK† γ JpK JσK = ∐†1 (idΣ ⊕ JcK) JqK JpK† Jnot pK JσK

and so on.

= ∐†1 (idΣ ⊕ JcK) JqK 0Σ,Σ JσK = 0I,Σ ,

With this lemma done, we turn our attention to the preservation lemma for commands
in order to show soundness.
Lemma 6.6. If σ ⊢ c ↓ σ ′ then JcK JσK = Jσ ′ K.

Proof. By induction on the structure of the derivation D of σ ⊢ c ↓ σ ′ .
• Case D =
. We have JskipK JσK = idΣ JσK = JσK.
σ ⊢ skip ↓ σ
′
σ ⊢ c1 ↓ σ
σ ′ ⊢ c2 ↓ σ ′′
.
• Case D =
σ ⊢ c1 ; c2 ↓ σ ′′
By induction, Jc1 K JσK = Jσ ′ K and Jc2 K Jσ ′ K = Jσ ′′ K. But then
q y q y
Jc1 ; c2 K JσK = Jc2 K Jc1 K JσK = Jc2 K σ ′ = σ ′′

as desired.
• Case D =

σ ⊢ p ↓ tt
σ ⊢ c1 ↓ σ ′
σ ′ ⊢ q ↓ tt
.
σ ⊢ if p then c1 else c2 fi q ↓ σ ′

By induction, Jc1 K JσK = Jσ ′ K, and by Lemma 6.2, JpK JσK = JttK JσK = ∐1 JσK and
JqK Jσ ′ K = JttK Jσ ′ K = ∐1 Jσ ′ K. We compute:

Jif p then c1 else c2 fi qK JσK = JqK† (Jc1 K ⊕ Jc2 K) JpK JσK = JqK† (Jc1 K ⊕ Jc2 K) ∐1 JσK
q y
q y
= JqK† ∐1 Jc1 K JσK = JqK† ∐1 σ ′ = JqK† JqK σ ′
q y q y
q y
= JqK σ ′ = σ ′ JqK Jσ ′ K = σ ′ ∐1 Jσ ′ K
q y
q y
q y
q y
= σ ′ ∐1 Jσ ′ K = σ ′ idΣ Jσ ′ K = σ ′ Jσ ′ K = σ ′ .
• Case D =

σ ⊢ p ↓ ff
σ ⊢ c2 ↓ σ ′
σ ′ ⊢ q ↓ ff
.
σ ⊢ if p then c1 else c2 fi q ↓ σ ′

By induction, Jc2 K JσK = Jσ ′ K, and by Lemma 6.2, JpK JσK = Jff K JσK = ∐2 JσK and

20

GLÜCK AND KAARSGAARD

JqK Jσ ′ K = Jff K Jσ ′ K = ∐2 Jσ ′ K. We have

Jif p then c1 else c2 fi qK JσK = JqK† (Jc1 K ⊕ Jc2 K) JpK JσK = JqK† (Jc1 K ⊕ Jc2 K) ∐2 JσK
q y
q y
= JqK† ∐2 Jc2 K JσK = JqK† ∐2 σ ′ = JqK† JqK σ ′
q y q y
q y
= JqK σ ′ = σ ′ JqK Jσ ′ K = σ ′ ∐2 Jσ ′ K
q y
q y
q y
q y
= σ ′ ∐2 Jσ ′ K = σ ′ idΣ Jσ ′ K = σ ′ Jσ ′ K = σ ′ .
• Case D =

σ ⊢ p ↓ tt
σ ⊢ q ↓ tt
.
σ ⊢ from p loop c until q ↓ σ

Since σ ⊢ p ↓ tt and σ ⊢ q ↓ tt, by Lemma 6.5 we get β[p, c, q]11 JσK = JσK and
β[p, c, q]12 JσK = 0I,Σ , and so
Jfrom p loop c until qK JσK = TrΣ
Σ,Σ (β[p, c, q])
=

β[p, c, q]11 ∨

_

β[p, c, q]21 β[p, c, q]n22

β[p, c, q]12

n∈ω

=

(β[p, c, q]11 JσK) ∨

= JσK ∨

_

n∈ω

_

β[p, c, q]21 β[p, c, q]n22

n∈ω

!

JσK

β[p, c, q]12 JσK

!

β[p, c, q]21 β[p, c, q]n22 0I,Σ = JσK ∨ 0I,Σ = JσK .

σ ⊢ q ↓ ff
σ ⊢ c ↓ σ′
σ ′ ⊢ loop[p, c, q] ↓ σ ′′
.
σ ⊢ from p loop c until q ↓ σ ′′
y
q
By induction, JcK JσK = Jσ ′ K and loop[p, c, q] Jσ ′ K = Jσ ′′ K, and since σ ⊢ p ↓ tt and
σ ⊢ q ↓ ff , by Lemma 6.5 we get β[p, c, q]11 JσK = 0I,Σ and β[p, c, q]12 JσK = JcK JσK.
Thus

• Case D =

σ ⊢ p ↓ tt

Jfrom p loop c until qK JσK = TrΣ
Σ,Σ (β[p, c, q])
=

β[p, c, q]11 ∨

_

β[p, c, q]21 β[p, c, q]n22 β[p, c, q]12

n∈ω

=

(β[p, c, q]11 JσK) ∨

=

0I,Σ ∨

_

_

n∈ω

=

β[p, c, q]21 β[p, c, q]n22

β[p, c, q]21 β[p, c, q]n22

n∈ω

=
q

_

q ′y
σ

β[p, c, q]21 β[p, c, q]n22

n∈ω

!

yq y q y
= loop[p, c, q] σ ′ = σ ′′ .
• Case D =

σ ⊢ p ↓ ff
σ ⊢ q ↓ tt
.
σ ⊢ loop[p, c, q] ↓ σ

JσK

β[p, c, q]21 β[p, c, q]n22 β[p, c, q]12 JσK

n∈ω

_

!

q ′y
σ

JcK JσK

!

!

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

21

Since σ ⊢ p ↓ ff and σ ⊢ q ↓ tt, by Lemma 6.5 we get β[p, c, q]22 JσK = 0I,Σ and
β[p, c, q]21 JσK = JσK. This gives us
!
_
y
q
n
β[p, c, q]21 β[p, c, q]22 JσK
loop[p, c, q] JσK =
n∈ω

=

β[p, c, q]21 ∨

_

β[p, c, q]21 β[p, c, q]n+1
22

n∈ω

=

(β[p, c, q]21 JσK) ∨

=

JσK ∨

=

JσK ∨

_

!

JσK

β[p, c, q]21 β[p, c, q]n+1
22

n∈ω

_

β[p, c, q]21 β[p, c, q]n22 β[p, c, q]22 JσK

_

β[p, c, q]21 β[p, c, q]n22 0I,Σ

n∈ω

n∈ω

!

JσK

!

!

= JσK ∨ 0I,Σ = JσK

σ ⊢ q ↓ ff
σ ⊢ c ↓ σ′
σ ′ ⊢ loop[p, c, q] ↓ σ ′′
.
σ ⊢ loop[p, c, q] ↓ σ ′′
q
y
By induction, JcK JσK = Jσ ′ K and loop[p, c, q] Jσ ′ K = Jσ ′′ K, and since σ ⊢ p ↓ ff and
σ ⊢ q ↓ ff , it follows by Lemma 6.5 that β[p, c, q]22 JσK = JcK JσK and β[p, c, q]21 JσK =
0I,Σ . We then have
!
_
y
q
β[p, c, q]21 β[p, c, q]n22 JσK
loop[p, c, q] JσK =

• Case D =

σ ⊢ p ↓ ff

n∈ω

=

β[p, c, q]21 ∨

_

β[p, c, q]21 β[p, c, q]n+1
22

n∈ω

=

(β[p, c, q]21 JσK) ∨

= 0I,Σ ∨

_

n∈ω

=

_

n∈ω

=

_

n∈ω

=

_

n∈ω

=
q

_

n∈ω

β[p, c, q]21 β[p, c, q]n+1
22 JσK

β[p, c, q]21 β[p, c, q]n22 JcK JσK

q y
β[p, c, q]21 β[p, c, q]n22 σ ′

n∈ω

JσK

!

β[p, c, q]21 β[p, c, q]n+1
22 JσK

β[p, c, q]21 β[p, c, q]n22 β[p, c, q]22 JσK

_

!

β[p, c, q]21 β[p, c, q]n22

!

yq y q y
= loop[p, c, q] σ ′ = σ ′′

q ′y
σ

22

GLÜCK AND KAARSGAARD

which was what we wanted.
This finally allows us to show the soundness theorem for commands – and so, for
programs – in a straightforward manner.
Theorem 6.7 (Soundness). If there exists σ ′ such that σ ⊢ c ↓ σ ′ then JcK JσK is total.

Proof. Suppose there exists σ ′ such that σ ⊢ c ↓ σ ′ . By Lemma 6.6, JcK JσK = Jσ ′ K, and since
the interpretation of any state is assumed to be total, it follows that JcK JσK = Jσ ′ K = idI ,
which was what we wanted.
With soundness done, we only have 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 6.8. If gf is total, so is f .
Proof. Let f : A → B and g : B → C be morphisms such that gf = idA . Then f = idA f =
gf f = gf f = gf = idA , so f is total as well.

Lemma 6.9. Let f : A ⊕ U → B ⊕ U and s : I → A be morphisms. If TrU
A,B (f )s is total,
U
U
n
either TrA,B (f )s = f11 s, or there exists n ∈ ω such that TrA,B (f )s = f21 f22 f12 s.
Proof. Since the trace is canonically constructed, it takes the form
_
n
TrU
(f
)
=
f
∨
f21 f22
f12 .
11
A,B
n∈ω

Further, in the proof of Theorem 20 in [21], it is shown that this join not only exists but is
a disjoint join, i.e., for any choice of n ∈ ω,
n
nf
f11 f21 f22
12 = (f21 f22 f12 ) f11 = 0A,B

and for all n, m ∈ ω with n 6= m,
n f f f mf = f f mf f f n f = 0
f21 f22
21 22 12 21 22 12
12 21 22 12
A,B .

But then,
TrU
A,B (f )s =

f11 ∨

_

nf
f21 f22
12 s

n∈ω

= (f11 s) ∨

!

_

n f s)
(f21 f22
12

n∈ω

= f11 s ∨

_

n f s.
f21 f22
12

n∈ω
n f s for any n ∈ ω are restriction idempotents
Since all of the morphisms f11 s and f21 f22
12
I → I, it follows for each of them that they are either equal to idI or to 0I,I . Suppose that
none of these are equal to the identity idI . Then they must all be 0I,I , and so TrU
A,B (f )s =
0I,I 6= idI , 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
0I,I .

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

23

With these done, we are finally ready to tackle the adequacy theorem.
Theorem 6.10 (Adequacy). If JcK JσK is total then there exists σ ′ such that σ ⊢ c ↓ σ ′ .
Proof. By induction on the structure of c.
• Case c = skip. Then σ ⊢ skip ↓ σ by
• Case c = c1 ; c2 .

σ ⊢ skip ↓ σ

.

In this case, JcK JσK = Jc1 ; c2 K JσK = Jc2 K Jc1 K JσK. Since this is total, so is Jc1 K JσK
by Lemma 6.8. But then, by induction, there exists σ ′ such that σ ⊢ c1 ↓ σ ′ by some
derivation D1 , and by Lemma 6.6, Jc1 K JσK = Jσ ′ K. But then Jc2 K Jc1 K JσK = Jc2 K Jσ ′ K,
so by induction there exists σ ′′ such that σ ′ ⊢ c2 ↓ σ ′′ by some derivation D2 . But
then σ ⊢ c1 ; c2 ↓ σ ′′ by
D1

D2

σ ⊢ c1 ↓ σ ′
σ ′ ⊢ c2 ↓ σ ′′
.
σ ⊢ c1 ; c2 ↓ σ ′′
• Case c = if p then c1 else c2 fi q.
Thus, JcK JσK = Jif p then c1 else c2 fi qK JσK = JqK† (Jc1 K ⊕ Jc2 K) JpK JσK, and since
this is total, JpK JσK is total as well by analogous argument to the previous case. It
then follows by Lemma 6.4 that there exists b such that σ ⊢ p ↓ b by some derivation
D1 , and by Lemma 6.2, JpK JσK = JbK JσK. We have two cases depending on what b
is.
When b = tt we have
JcK JσK = JqK† (Jc1 K ⊕ Jc2 K) JpK JσK = JqK† (Jc1 K ⊕ Jc2 K) JttK JσK
= JqK† (Jc1 K ⊕ Jc2 K) ∐1 JσK = JqK† ∐1 Jc1 K JσK

so since this is total, Jc1 K JσK must be total as well by Lemma 6.8. But then, by
induction, there exists σ ′ such that σ ⊢ c1 ↓ σ ′ by some derivation D2 , and by
Lemma 6.6, Jc1 K JσK = Jσ ′ K. Continuing the computation, we get
†q y
q y
q y
JcK JσK = JqK† ∐1 Jc1 K JσK = JqK† ∐1 σ ′ = (∐†1 JqK)† σ ′ = ∐†1 JqK σ ′
q y q y
q y
= ∐†1 JqK σ ′ = σ ′ ∐†1 JqK Jσ ′ K = σ ′ ∐†1 JqK Jσ ′ K JqK Jσ ′ K

so JqK Jσ ′ K must be total, in turn meaning that JqK Jσ ′ K must be total. But then by
Lemma 6.4, there must exist b′ such that σ ′ ⊢ q ↓ b′ by some derivation D3 , with
JqK Jσ ′ K = Jb′ K Jσ ′ K by Lemma 6.2. Again, we have two cases depending on b′ . If
b′ = tt, we derive σ ⊢ if p then c1 else c2 fi q ↓ σ ′ by
D1

D2

D3

σ ⊢ c1 ↓ σ ′
σ ′ ⊢ q ↓ tt
σ ⊢ p ↓ tt
σ ⊢ if p then c1 else c2 fi q ↓ σ ′
On the other hand, when b′ = ff , we have
q y
q y
q y
JcK JσK = σ ′ ∐†1 JqK Jσ ′ K = σ ′ ∐†1 Jff K Jσ ′ K = σ ′ ∐†1 ∐2 Jσ ′ K
q y
q y
q y
= σ ′ 0Σ,Σ Jσ ′ K = σ ′ 0I,Σ = σ ′ 0I,I = 0I,Σ

so JcK JσK = 0I,I , contradicting JcK JσK = idI since 0I,I 6= idI by definition of a model.
Thus there exists σ ′ such that σ ⊢ if p then c1 else c2 fi q ↓ σ ′ .

24

GLÜCK AND KAARSGAARD

To show the case when b = ff , we proceed as before. We then have
JcK JσK = JqK† (Jc1 K ⊕ Jc2 K) JpK JσK = JqK† (Jc1 K ⊕ Jc2 K) Jff K JσK
= JqK† (Jc1 K ⊕ Jc2 K) ∐2 JσK = JqK† ∐2 Jc2 K JσK

So Jc2 K JσK must be total by Lemma 6.8, which means that by induction there exists
σ ′ such that σ ⊢ c2 ↓ σ ′ by a derivation D2 , and by Lemma 6.6, Jc2 K JσK = Jσ ′ K.
Continuing as before, we obtain now that
†q y
q y
q y
JcK JσK = JqK† ∐2 Jc2 K JσK = JqK† ∐2 σ ′ = (∐†2 JqK)† σ ′ = ∐†2 JqK σ ′
q y q y
q y
= ∐†2 JqK σ ′ = σ ′ ∐†2 JqK Jσ ′ K = σ ′ ∐†2 JqK Jσ ′ K JqK Jσ ′ K

and so JqK Jσ ′ K must be total in this case as well, so by Lemma 6.4 there must exist
b′ such that σ ′ ⊢ q ↓ b′ by some derivation D3 , and JqK Jσ ′ K = Jb′ K Jσ ′ K by Lemma 6.2.
Again, we do a case analysis depending on the value of b′ .
If b′ = tt, we have
q y
q y
q y
JcK JσK = σ ′ ∐†2 JqK Jσ ′ K = σ ′ ∐†2 JttK Jσ ′ K = σ ′ ∐†2 ∐1 Jσ ′ K
q y
q y
q y
= σ ′ 0Σ,Σ Jσ ′ K = σ ′ 0I,Σ = σ ′ 0I,I = 0I,Σ

which contradicts the totality of JcK JσK by JcK JσK = 0I,Σ = 0I,I 6= idI , and we get
by contradiction that there exists σ ′ such that σ ⊢ if p then c1 else c2 fi q ↓ σ ′ .
If b′ = ff , we derive σ ⊢ if p then c1 else c2 fi q ↓ σ ′ by
D2

D1

D3

σ ⊢ p ↓ ff
σ ⊢ c2 ↓ σ ′
σ ′ ⊢ q ↓ ff
.
σ ⊢ if p then c1 else c2 fi q ↓ σ ′
• Case c = from p loop c1 until q.
In this case, JcK JσK = Jfrom p loop c1 until qK JσK = TrΣ
Σ,Σ (β[p, c1 , q]) JσK. Since
this is total and JσK : I → Σ, it follows by Lemma 6.9 that either
Jfrom p loop c1 until qK JσK = β[p, c1 , q]11 JσK

or there exists n ∈ ω such that

Jfrom p loop c1 until qK JσK = β[p, c1 , q]21 β[p, c1 , q]n22 β[p, c1 , q]12 JσK .

If Jfrom p loop c1 until qK JσK = β[p, c1 , q]11 JσK, we have

Jfrom p loop c1 until qK JσK = β[p, c1 , q]11 JσK = ∐†1 (idΣ ⊕ Jc1 K) JqK JpK† ∐1 JσK
= ∐†1 (idΣ ⊕ Jc1 K) JqK ∐†1 JpK JσK

= ∐†1 (idΣ ⊕ Jc1 K) JqK JσK ∐†1 JpK JσK

= ∐†1 (idΣ ⊕ Jc1 K) JqK JσK ∐†1 JpK JσK JqK JσK JpK JσK

so it follows by totality of JcK JσK that JpK JσK and JqK JσK must be total, so JpK JσK
and JqK JσK must be total as well. It then follows by Lemma 6.4 that there exist
b1 and b2 such that σ ⊢ p ↓ b1 and σ ⊢ q ↓ b2 by derivations D1 respectively
D2 . But then it follows by Lemma 6.5 that b1 = b2 = tt, as we would otherwise

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

25

have JcK JσK = β[p, c1 , q]11 JσK = 0I,Σ , contradicting totality. Thus we may derive
σ ⊢ from p loop c1 until q ↓ σ by
D1

D2

σ ⊢ p ↓ tt
σ ⊢ q ↓ tt
.
σ ⊢ from p loop c1 until q ↓ σ
On the other hand, suppose that there exists n ∈ ω such that
JcK JσK = Jfrom p loop c1 until qK JσK = β[p, c1 , q]21 β[p, c1 , q]n22 β[p, c1 , q]12 JσK .
Since this is total, by Lemma 6.8 β[p, c1 , q]12 JσK is total as well, and

β[p, c1 , q]12 JσK = ∐†2 (idΣ ⊕ Jc1 K) JqK JpK† ∐1 JσK = ∐†2 (idΣ ⊕ Jc1 K) JqK ∐†1 JpK JσK
= ∐†2 (idΣ ⊕ Jc1 K) JqK JσK ∐†1 JpK JσK

= ∐†2 (idΣ ⊕ Jc1 K) JqK JσK ∐†1 JpK JσKJpK JσK JqK JσK

But then JpK JσK and JqK JσK must be total as well, so by Lemma 6.4 there exist b1
and b2 such that σ ⊢ p ↓ b1 and σ ⊢ q ↓ b2 by derivations D1 respectively D2 . Since
β[p, c1 , q]12 JσK is total, it further follows by Lemma 6.5 that b1 = tt and b2 = ff , as
we would otherwise have β[p, c1 , q]12 JσK = 0I,Σ . Further, β[p, c1 , q]12 JσK = Jc1 K JσK,
and since this is total, by induction there exists σ ′ such that σ ⊢ c1 ↓ σ ′ by some
derivation D3 , with Jc1 K JσK = Jσ ′ K by Lemma 6.6.
To summarize, we have now that
Jfrom p loop c1 until qK JσK = β[p, c1 , q]21 β[p, c1 , q]n22 β[p, c1 , q]12 JσK
= β[p, c1 , q]21 β[p, c1 , q]n22 Jc1 K JσK
q y
= β[p, c1 , q]21 β[p, c1 , q]n22 σ ′

is total, and we have derivations D1 of σ ⊢ p ↓ tt, D2 of σ ⊢ q ↓ ff , and D3 of σ ⊢ c1 ↓
σ ′ . To finish the proof, we show by induction on n that if β[p, c1 , q]21 β[p, c1 , q]n22 Jσ ′ K
is total for any state σ ′ , there exists a state σ ′′ such that σ ′ ⊢ loop[p, c1 , q] ↓ σ ′′ by
some derivation D4 .
– In the base case n = 0, so β[p, c1 , q]21 β[p, c1 , q]n22 Jσ ′ K = β[p, c1 , q]21 Jσ ′ K. By
proof analogous to previous cases, we have that JpK Jσ ′ K and JqK Jσ ′ K must be
total, so by Lemma 6.4 there exist b′1 and b′2 such that σ ′ ⊢ p ↓ b′1 and σ ′ ⊢ q ↓ b′1
by derivations D1′ respectively D2′ . Further, by totality, it follows by Lemma 6.5
that we must have b′1 = ff , b′2 = tt. Thus we may produce our derivation D4 of
σ ′ ⊢ loop[p, c1 , q] ↓ σ ′ by
σ′

D1′

σ′

D2′

⊢ p ↓ ff
⊢ q ↓ tt
σ ′ ⊢ loop[p, c, q] ↓ σ ′

– In the inductive case, we have that
q ′y
q y
σ = β[p, c1 , q]21 β[p, c1 , q]n22 β[p, c1 , q]22 σ ′
β[p, c1 , q]21 β[p, c1 , q]n+1
22

and since this is assumed to be total, it follows by Lemma 6.8 that β[p, c1 , q]22 Jσ ′ K
is total as well. Again, by argument analogous to previous cases, this implies
that JpK Jσ ′ K and JqK Jσ ′ K are both total, so by Lemma 6.4 there exist b′1 and
b′2 such that σ ′ ⊢ p ↓ b′1 and σ ′ ⊢ q ↓ b′2 by derivations D1′ respectively D2′ .

26

GLÜCK AND KAARSGAARD

Likewise, it then follows by Lemma 6.5 that since this is total, we must have
b′1 = b′2 = ff , and so β[p, c1 , q]22 Jσ ′ K = Jc1 K Jσ ′ K, again by Lemma 6.5. Since
Jc1 K Jσ ′ K is total, by the outer induction hypothesis there exists a derivation D3′
of σ ′ ⊢ c1 ↓ σ ′′ for some σ ′′ , and so Jc1 K Jσ ′ K = Jσ ′′ K by Lemma 6.6. But then
q y
q ′y
β[p, c1 , q]21 β[p, c1 , q]n+1
σ = β[p, c1 , q]21 β[p, c1 , q]n22 β[p, c1 , q]22 σ ′
22
q y
= β[p, c1 , q]21 β[p, c1 , q]n22 Jc1 K σ ′
q y
= β[p, c1 , q]21 β[p, c1 , q]n22 σ ′′
since this is total, by (inner) induction there exists a derivation D4′ of σ ′′ ⊢
loop[p, c1 , q] ↓ σ ′′′ . Thus, we may produce our derivation D4 as
σ′

D1′

⊢ p ↓ ff

σ′

D2′

σ′

D3′

σ ′′

σ ′′

⊢ q ↓ ff
⊢ c1 ↓
′
σ ⊢ loop[p, c1 , q] ↓ σ ′′′

D4′

⊢ loop[p, c, q] ↓ σ ′′′

concluding the internal lemma.
Since this is the case, we may finally show σ ⊢ from p loop q until c ↓ σ ′ by
D1

D2

D3

D4

σ ⊢ c ↓ σ′
σ ′ ⊢ loop[p, c, q] ↓ σ ′′
σ ⊢ q ↓ ff
,
σ ⊢ from p loop c until q ↓ σ ′′
which concludes the proof.
σ ⊢ p ↓ tt

7. Full abstraction
Where 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., [24]). Unlike the case for soundness and 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 observationally
equivalent. Formally, we define this as follows:
Definition 13. Say that programs p1 and p2 are observationally equivalent, denoted p1 ≈ p2 ,
if for all states σ, σ ⊢ p1 ↓ σ ′ if and only if σ ⊢ p2 ↓ σ ′ .
A model is said to be fully abstract if these two notions of program equivalence are in
agreement. In the present section, we will show a sufficient condition for 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.
Definition 14. Say that a model of a structured reversible flowchart language is I-well
pointed if, for all parallel morphisms f, g : A → B, f = g precisely when f p = gp for all
p : I → A.

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

27

Definition 15. Say that a model C of a structured reversible flowchart language L is bijective on states if there is a bijective correspondence between states of L and total morphisms
I → Σ of C .
If a sound and adequate model of a structured reversible flowchart language is bijective
on states, we can show a stronger version of Lemma 6.6.
Lemma 7.1. If C be a sound and adequate model of a structured reversible flowchart
language which is bijective on states. Then σ ⊢ c ↓ σ ′ iff JcK JσK = Jσ ′ K and this is total.

Proof. By Lemma 6.6 and Theorem 6.7, we only need to show that JcK JσK = Jσ ′ K implies
σ ⊢ c ↓ σ ′ . Assume that JcK JσK = Jσ ′ K and that this is total. By Theorem 6.10, there exists
σ ′′ such that σ ⊢ c ↓ σ ′′ , so by Lemma 6.6, JcK JσK = Jσ ′′ K. Thus Jσ ′ K = JcK JσK = Jσ ′′ K, so
σ ′ = σ ′′ by bijectivity on states.
With this, we can show full abstraction.

Theorem 7.2 (Full abstraction). Let C be a sound and adequate model of a structured
reversible flowchart language that is furthermore I-well pointed and bijective on states. Then
C is fully abstract, i.e., p1 ≈ p2 if and only if Jp1 K = Jp2 K.

Proof. Suppose p1 ≈ p2 , i.e., for all σ, σ ⊢ p1 ↓ σ ′ if and only if σ ⊢ p2 ↓ σ ′ . Let s : I → Σ
be a morphism. Since C is a model of a structured reversible flowchart language, it follows
that either s = idI or s = 0I,I where idI 6= 0I,I .
If s = 0I,I , we have Jp1 K s = Jp2 K s = 0I,Σ by unicity of the zero map.
On the other hand, if s = idI , by bijectivity on states there exists σ0 such that s = Jσ0 K.
Consider now Jp1 K s = Jp1 K Jσ0 K. If this is total, by Theorem 6.10 there exists σ0′ such that
σ0 ⊢ p1 ↓ σ0′ , and by p1 ≈ p2 , σ0 ⊢ p2 ↓ σ0′ as well. But then, applying Lemma 6.6 on both
yields that
q y
Jp1 K s = Jp1 K Jσ0 K = σ0′ = Jp2 K Jσ0 K = Jp2 K s .
If, on the other hand, Jp1 K s is not total, by the contrapositive to Theorem 6.7, there exists
no σ0′ such that σ0 ⊢ p1 ↓ σ0′ , so by p1 ≈ p2 there exists no σ0′′ such that σ0 ⊢ p1 ↓ σ0′′ . But
then, by the contrapositive of Theorem 6.10 and the fact that restriction idempotents on I
are either idI or 0I,I , it follows that
Jp1 K s = Jp1 K Jσ0 K = 0I,Σ = Jp2 K Jσ0 K = Jp1 K s.

Since s was chosen arbitrarily and Jp1 K s = Jp2 K s in all cases, it follows by I-well pointedness
that Jp1 K = Jp2 K.
In the other direction, suppose Jp1 K = Jp2 K, let σ0 be a state, and suppose that there
exists σ0′ such that σ0 ⊢ p1 ↓ σ0′ . By Lemma 6.6, Jp1 K Jσ0 K = Jσ0′ K, and by Theorem 6.7
this is total. But then, by Jp1 K = Jp2 K, Jp2 K Jσ0 K = Jp1 K Jσ0 K = Jσ0′ K, so by Lemma 7.1,
σ0 ⊢ p2 ↓ σ0′ . The other direction follows similarly.
8. Applications
In this section, we briefly cover some applications of the developed theory: We show how a
program inverter can be derived from 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.

28

GLÜCK AND KAARSGAARD

8.1. Extracting a program inverter. 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 I[p] such that JI[p]K = JpK† . Janus, R-WHILE, and
R-CORE [32, 16, 17] are all examples of reversible programming languages with this property.
This is typically witnessed by a program inverter [1], that is, a procedure mapping the
program text of a program to the program text of its inverse program3.
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 I[b] such that
JI[b]K = JbK† ). We can extend this to a program inverter for skip, sequencing, reversible
conditionals and loops as follows, by structural induction with the hypothesis that JI[c]K =
JcK† . For skip, we have
JskipK† = id†Σ = idΣ = JskipK
giving us the usual inversion rule of I[skip] = skip. Likewise for sequences,
Jc1 ; c2 K† = (Jc2 K Jc1 K)† = Jc1 K† Jc2 K† = JI[c1 ]K JI[c2 ]K = JI[c2 ] ; I[c1 ]K

giving us the inversion rule

I[c1 ; c2 ] = I[c2 ] ; I[c1 ] .
Our approach becomes more interesting when we come to conditionals. Given some
conditional statement if p then c1 else c2 fi q, we notice that
Jif p then c1 else c2 fi qK† = (JqK† Jc1 K ⊕ Jc2 K JpK)†

= JpK† Jc1 K† ⊕ Jc2 K† JqK††
= JpK† Jc1 K† ⊕ Jc2 K† JqK

= JpK† JI[c1 ]K ⊕ JI[c2 ]K JqK

which yields the inversion rule

= Jif q then I[c1 ] else I[c2 ] fi pK

I[if p then c1 else c2 fi q] = if q then I[c1 ] else I[c2 ] fi p].
Fortunately, this is precisely the usual inversion rule for reversible conditionals (see, e.g.,
[16, 17]). For reversible loops, we have
† †
Jfrom p loop c until qK† = TrΣ
Σ,Σ (idΣ ⊕ JcK JqK JpK )

† †
= TrΣ
Σ,Σ ((idΣ ⊕ JcK JqK JpK ) )

†
†
= TrΣ
Σ,Σ (JpK JqK idΣ ⊕ JcK )

†
†
= TrΣ
Σ,Σ (idΣ ⊕ JcK JpK JqK )

†
= TrΣ
Σ,Σ (idΣ ⊕ JI[c]K JpK JqK )

= Jfrom q loop I[c] until pK

3While 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.

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

29

where the fact that it is a †-trace allows us to move the dagger inside the trace, and
dinaturality of the trace in the second component allows us to move idΣ ⊕ JcK† from the
very right to the very left. This gives us the inversion rule
I[from p loop c until q] = from q loop I[c] until p
which matches the usual inversion rule for reversible loops [17]. We summarize this in the
following theorem:
Theorem 8.1. If a reversible structured flowchart language is syntactically closed under
inversion of elementary operations, it is also closed under inversion of reversible 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, RINTk . RINTk has precisely k variables available for storage,
denoted x1 through xk (of which x1 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:
p ::= tt | ff | xi | p and p | not p

(Tests)

c ::= c ; c | xi += xj | xi −= xj | xi += n
| if p then c else c fi p
| from p loop c until p

(Commands)

Here, n is the syntactic representation of an integer n. In the cases for addition and
subtraction, we impose the additional syntactic constraints that 1 ≤ i ≤ k, 1 ≤ j ≤ k, and
i 6= 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 RINTk is
then simply a command.
We may now give semantics to this language in our framework. For a concrete model,
we select the category 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 9 by Theorem 4.4. By our developments previously
in this section, to give a full semantics to RINTk in PInj, it suffices to provide an object
(i.e., a set) of stores Σ, 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) Σ → Σ, and denotations of our class of elementary predicates
(here, testing whether a variable is zero or not) as decisions Σ → Σ ⊕ Σ. These are all shown
in Figure 4. It is uncomplicated to show that all of these are partial injective functions, and
that the denotation of each predicate Jxi K is a decision, so that this is, in fact, a model of
RINTk in PInj.
We can now reap the benefits in the form of a reversibility theorem for free:
Theorem 8.2 (Reversibility). Every RINTk program p is semantically reversible in the sense
that JpK is a partial isomorphism.

30

GLÜCK AND KAARSGAARD

Σ = Zk

∐1 (a1 , . . . , ak )
if ai = 0
Jxi K (a1 , . . . , ak ) =
∐2 (a1 , . . . , ak )
otherwise
q
y
xi += xj (a1 , . . . , ak ) = (a1 , . . . , ai−1 , ai + aj , . . . , ak )

Jxi += nK (a1 , . . . , ak ) = (a1 , . . . , ai−1 , ai + n, . . . , ak )
y
q
xi −= xj (a1 , . . . , ak ) = (a1 , . . . , ai−1 , ai − aj , . . . , ak )

Figure 4: The object of stores and semantics of elementary operations and predicates of
RINTk in PInj.
y
y†
q
q
= xi −= xj and
Further, since we can straightforwardly show that xi += xj
Jxi += nK† = Jxi += −n K, we can use the technique from Sec. 8.1 to obtain a sound and
complete program inverter.
Theorem 8.3 (Program inversion). RINTk has a (sound and complete) program inverter.
In particular, for every RINTk program p there exists a program I[p] such that JI[p]K = JpK† .
8.3. Decisions as a programming technique. Decisions offer a solution to the awkwardness in representing predicates reversibly. On the programming side, the reversible duplication/equality operator [15] (see also [31]) can be seen as a distant ancestor to predicatesas-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
data PBool α = True α | False α
storing not only the result, but also what was tested to begin with. With this definition,
negation on these polymorphic Booleans (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 (peven)
is also shown in Figure 5, with fmap given in the straightforward way on polymorphic
Booleans. For comparison, the corresponding irreversible predicate is typically defined as
follows, with not the usual negation of Booleans
even
:: Nat → Bool
even 0
= True
even (n + 1) = not (even n) .
As such, the reversible implementation as a decision is nearly identical, the only difference
being the use of fmap in the definition of peven to recover the input value once the branch
has been decided.

CATEGORICAL FOUNDATIONS FOR REVERSIBLE FLOWCHART LANGUAGES

pnot
:: PBool α ↔ PBool α
pnot (True x ) = False x
pnot (False x ) = True x

31

peven
:: Nat ↔ PBool Nat
peven 0
= True 0
peven (n + 1) = fmap (+1) (pnot (peven n))

Figure 5: The definition of the 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 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 sound and adequate with respect to the operational semantics, and given a sufficient
condition for 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 partially inspired by the instruments
associated with predicates in Effectus theory [19]. Given that side effect free instruments ι
satisfy a similar rule, ∇ι = 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 [32].
References
[1] Abramov, S. M. and R. Glück, The universal resolving algorithm: inverse computation in a functional
language, in: R. Backhouse and J. N. Oliveira, editors, Mathematics of Program Construction. Proceedings, LNCS 1837 (2000), pp. 187–212.
[2] Axelsen, H. B. and R. Glü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.
[3] Axelsen, H. B., R. Glü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.
[4] Axelsen, H. B. and R. Kaarsgaard, Join inverse categories as models of reversible recursion, in: B. Jacobs
and C. Löding, editors, FOSSACS 2016, Proceedings, number 9634 in LNCS (2016), pp. 73–90.
[5] 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.
[6] 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.
[7] Cockett, J. R. B., Itegories & PCAs (2007), slides from talk at FMCS 2007.

32

GLÜCK AND KAARSGAARD

[8] Cockett, J. R. B. and S. Lack, Restriction categories I: Categories of partial maps, Theoretical Computer
Science 270 (2002), pp. 223–259.
[9] Cockett, J. R. B. and S. Lack, Restriction categories II: Partial map classification, Theoretical Computer
Science 294 (2003), pp. 61–102.
[10] Cockett, R. and S. Lack, Restriction categories III: Colimits, partial limits and extensivity, Mathematical
Structures in Computer Science 17 (2007), pp. 775–817.
[11] Fiore, M. P., “Axiomatic Domain Theory in Categories of Partial Maps,” Ph.D. thesis, University of
Edinburgh (1994).
[12] Frank, M. P., “Reversibility for efficient computing,” Ph.D. thesis, EECS Dept., Massachusetts Institute
of Technology (1999).
[13] Giles, B. G., “An Investigation of some Theoretical Aspects of Reversible Computing,” Ph.D. thesis,
University of Calgary (2014).
[14] Glück, R. and R. Kaarsgaard, A categorical foundation for structured reversible flowchart languages,
in: Proceedings of the 33rd Conference on the Mathematical Foundations of Programming Semantics
(MFPS XXXIII), 2017, to appear.
[15] Glü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.
[16] Glück, R. and T. Yokoyama, A linear-time self-interpreter of a reversible imperative language, Computer
Software 33 (2016), pp. 108–128.
[17] Glück, R. and T. Yokoyama, A minimalist’s reversible while language, IEICE Transactions on Information and Systems E100-D (2017), pp. 1026–1034.
[18] Guo, X., “Products, Joins, Meets, and Ranges in Restriction Categories,” Ph.D. thesis, University of
Calgary (2012).
[19] Jacobs, B., New directions in categorical logic, for classical, probabilistic and quantum logic, Logical
Methods in Computer Science 11 (2015), pp. 1–76.
[20] Joyal, A., R. Street and D. Verity, Traced monoidal categories, Mathematical Proceedings of the Cambridge Philosophical Society 119 (1996), pp. 447–468.
[21] Kaarsgaard, R., H. B. Axelsen and R. Glück, Join inverse categories and reversible recursion, Journal
of Logical and Algebraic Methods in Programming 87 (2017), pp. 33–50.
[22] 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.
[23] Mogensen, T. Æ., Partial evaluation of the reversible language Janus, in: Partial Evaluation and Program Manipulation. Proceedings (2011), pp. 23–32.
[24] Plotkin, G., Full abstraction, totality and PCF, Mathematical Structures in Computer Science 9 (1999),
pp. 1–20.
[25] Selinger, P., Dagger compact closed categories and completely positive maps, Electronic Notes in Theoretical Computer Science 170 (2007), pp. 139–163.
[26] Selinger, P., A survey of graphical languages for monoidal categories, in: B. Coecke, editor, New Structures for Physics, number 813 in Lecture Notes in Physics (2011), pp. 289–355.
[27] Thomsen, M. K., H. B. Axelsen and R. Glü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.
[28] Thomsen, M. K., R. Glück and H. B. Axelsen, Reversible arithmetic logic unit for quantum arithmetic,
Journal of Physics A: Mathematical and Theoretical 43 (2010), p. 382002.
[29] Yokoyama, T., H. B. Axelsen and R. Glück, Reversible flowchart languages and the structured reversible
program theorem, in: L. Aceto, I. Damgård, L. A. Goldberg, M. M. Halldórsson, A. Ingólfsdóttir and
I. Walukiewicz, editors, International Colloquium on Automata, Languages and Programming. Proceedings, Lecture Notes in Computer Science 5126 (2008), pp. 258–270.
[30] Yokoyama, T., H. B. Axelsen and R. Glück, Optimizing clean reversible simulation of injective functions,
Journal of Multiple-Valued Logic and Soft Computing 18 (2012), pp. 5–24.
[31] Yokoyama, T., H. B. Axelsen and R. Glück, Towards a reversible functional language, in: A. De Vos
and R. Wille, editors, RC 2011, LNCS 7165 (2012), pp. 14–29.
[32] Yokoyama, T. and R. Glück, A reversible programming language and its invertible self-interpreter, in:
Partial Evaluation and Semantics-Based Program Manipulation. Proceedings (2007), pp. 144–153.

