Department of Computer Science and Engineering, University of Bologna, Italyis
partially supported by the MIUR FARE project CAFFEINE, “Compositional and
Effectful Program Distances”, R20LW7EJ7L.Université Paris-Saclay, CNRS, ENS
Paris-Saclay, Inria, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette,
France0000-0003-1761-3244 Université Paris-Saclay, CNRS, CentraleSupélec, ENS
Paris-Saclay, Inria, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette,
France Kostia Chardonnet, Louis Lemonnier and Benoît Valiron [500]Theory of
computation Program semantics This work has been partially funded by the
French National Research Agency (ANR) within the framework of “Plan France
2030”, under the research project ANR-22-PETQ-0007.John Q. Open and Joan R.
Access 2 42nd Conference on Very Important Topics (CVIT 2016) CVIT 2016 CVIT
2016 December 24–27, 2016 Little Whinging, United Kingdom 42 23

# Semantics for a Turing-complete Reversible Programming Language with
Inductive Types

Kostia Chardonnet  Louis Lemonnier111Corresponding author. Benoît Valiron

###### Abstract

This paper is concerned with the expressivity and denotational semantics of a
functional higher-order reversible programming language based on Theseus. In
this language, pattern-matching is used to ensure the reversibility of
functions. We show how one can encode any Reversible Turing Machine in said
language. We then build a sound and adequate categorical semantics based on
join inverse categories, with additional structures to capture pattern-
matching. We then derive a full completeness result, stating that any
computable, partial injective function is the image of a term in the language.

###### keywords:

Reversible programming, functional programming, Computability, Denotational
Semantics

###### category:

##  1 Introduction

Originally, reversible computation has emerged as an energy-preserving model
of computation in which no data is ever erased. This comes from Laundauer’s
principle which states that the erasure of information is linked to the
dissipation of energy as heat [30, 6]. In reversible computation, given some
process $f$, there always exists an inverse process $f^{-1}$ such that their
composition is equal to the identity: it is always possible to “ _go back in
time_ ” and recover the input of your computation. Although this can be seen
as very restrictive, as shown for instance in [5] non-reversible computation
can be emulated in a reversible setting, by keeping track of intermediate
results.

Reversible computation has since been shown to be a versatile model. In the
realm of quantum computation, reversible computing is at the root of the
construction of _oracles_ , subroutines describing problem instances in
quantum algorithms [34]. Most of the research in reversible circuit design can
then been repurposed to design efficient quantum circuits. On the theoretical
side, reversible computing serves the main ingredient in several operational
models of linear logics, whether through token-based Geometry of Interaction
[32] of through the Curry-Howard correspondence for $\mu$MALL [9, 7].

Reversible programming has been approached in two different ways. The first
one, based on Janus and later R-CORE and R-WHILE [31, 40, 15, 39], considers
imperative and flow-chart languages. The other one follows a functional
approach [38, 37, 20, 19, 36, 9]: a function $A\to B$ in the language
represents a function —a bijection— between values of type $A$ and values of
type $B$. In this approach, types are typically structured, and functional
reversible languages usually feature pattern-matching to discriminate on
values.

One of the issue reversible programming has to deal with is _non-termination_
: in general, a reversible program computes a _partial injective map_. This
intuition can be formalized with the concept of _inverse categories_ [27, 10,
11, 12]: categories in which every morphism comes with a partial inverse, for
which the category $\mathbf{PInj}$ of sets and partial injective maps is the
emblematic concrete instance. This categorical setting has been successfully
used in the study of reversible programming semantics, whether based on flow-
charts [14, 22], with recursion [3, 24, 23, 26], with side-effects [18, 17],
etc.

Although much work has been dedicated to the categorical analysis of
reversible computation, the _adequacy_ of the developed categorical constructs
with reversible functional programming languages has only recently been under
scrutiny, either in _concrete_ categories of partial isomorphisms [26, 25], or
for simple, _non Turing-complete_ languages [8]. A formal, categorical
analysis of a Turing-complete, reversible language is still missing.

Contributions. In this paper, we aim at closing this gap: we proposed a
Turing-complete, reversible language, together with a categorical semantics.
In particular, the contributions of this paper are as follows.

  * •

Turing-complete, higher-order reversible language with inductive types.
Building on the Theseus-based family of languages studied in [36, 8, 9, these-
kostia], we consider an extension with _inductive types_ , general _recursion_
and _higher-order_ functions.

  * •

Sound and adequate categorical semantics. We show how the language can be
interpreted in rig join inverse categories. The result relies on the
$\mathbf{DCPO}$-enrichments of rig join inverse categories.

  * •

Full completeness result for _computable_ functions. We finally discuss how
the interpretation of the language in the category $\mathbf{PInj}$ is fully
complete in the sense that any computable, partial injective set-function on
the images of types is realizable within the language.

##  2 Language

In this section, we present a reversible language, unifying and extending the
Theseus-based variants presented in the literature [36, 8, 9]. In particular,
the language we propose features higher-order (unlike [8]), pairing,
injection, inductive types (unlike [36]) and general recursion (unlike [9]).
Functions in the language are based on pattern-matching, following a strict
syntactic discipline: term variables in patterns should be used linearly, and
clauses should be non-overlapping on the left _and_ on the right (therefore
enforcing non-ambiguity and injectivity). In [36, 8, 9] one also requires
exhaustivity for totality. In this paper, we drop this condition in order to
allow non-terminating behavior.

(Base types) $\displaystyle A,B$ $\displaystyle::=\leavevmode\nobreak\ $
$\displaystyle\mathds{1}\leavevmode\nobreak\ \mid\leavevmode\nobreak\
X\leavevmode\nobreak\ \mid\leavevmode\nobreak\ A\oplus B\leavevmode\nobreak\
\mid\leavevmode\nobreak\ A\otimes B\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \mu X.A\leavevmode\nobreak\ \mid\leavevmode\nobreak\
X$ (Isos) $\displaystyle\alpha$ $\displaystyle::=$ $\displaystyle
A\leftrightarrow B\mid(A\leftrightarrow B)\to\alpha$ (Values) $\displaystyle
v$ $\displaystyle::=$ $\displaystyle()\leavevmode\nobreak\
\mid\leavevmode\nobreak\ x\leavevmode\nobreak\ \mid\leavevmode\nobreak\
\mathtt{inj}_{\ell}{\;v}\leavevmode\nobreak\ \mid\leavevmode\nobreak\
\mathtt{inj}_{r}{\;v}\leavevmode\nobreak\ \mid\leavevmode\nobreak\ \langle
v_{1},v_{2}\rangle\leavevmode\nobreak\ \mid\leavevmode\nobreak\
\mathtt{fold}{\;v}$ (Pattern) $\displaystyle p$ $\displaystyle::=$
$\displaystyle x\leavevmode\nobreak\ \mid\leavevmode\nobreak\ \langle
p_{1},p_{2}\rangle$ (Expressions) $\displaystyle e$ $\displaystyle::=$
$\displaystyle v\leavevmode\nobreak\ \mid\leavevmode\nobreak\
{\mathtt{let}}\,{p_{1}}={\omega\leavevmode\nobreak\ p_{2}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {e}$ (Isos) $\displaystyle\omega$
$\displaystyle::=$ $\displaystyle\\{v_{1}\leftrightarrow e_{1}\mid\dots\mid
v_{n}\leftrightarrow e_{n}\\}\leavevmode\nobreak\ \mid\leavevmode\nobreak\
\mathbf{fix}\leavevmode\nobreak\ \phi.\omega\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \lambda\psi.\omega\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \phi\leavevmode\nobreak\ \mid\leavevmode\nobreak\
\omega_{1}\leavevmode\nobreak\ \omega_{2}$ (Terms) $\displaystyle t$
$\displaystyle::=$ $\displaystyle()\leavevmode\nobreak\
\mid\leavevmode\nobreak\ x\leavevmode\nobreak\ \mid\leavevmode\nobreak\
\mathtt{inj}_{\ell}{\;t}\leavevmode\nobreak\ \mid\leavevmode\nobreak\
\mathtt{inj}_{r}{\;t}\leavevmode\nobreak\ \mid\leavevmode\nobreak\ \langle
t_{1},t_{2}\rangle\leavevmode\nobreak\ \mid\leavevmode\nobreak\ $
$\displaystyle\mathtt{fold}{\;t}\leavevmode\nobreak\ \mid\leavevmode\nobreak\
\omega\leavevmode\nobreak\ t\leavevmode\nobreak\ \mid\leavevmode\nobreak\
{\mathtt{let}}\,{p}={t_{1}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {t_{2}}$ Table 1: Terms and types.

The language is presented in Table 1. It consists in two layers.

  * •

Base types: The base types consist of the unit type $\mathds{1}$ along with
its sole constructor $()$, coproduct $A\oplus B$ and tensor product $A\otimes
B$ with their respective constructors,
$\mathtt{inj}_{\ell}{\;(t)},\mathtt{inj}_{r}{\;(t)}$ and $\langle
t_{1},t_{2}\rangle$. Finally, the language features inductive types of the
form $\mu X.A$ where $X$ is a type variable occurring in $A$ and $\mu$ is its
binder. Its associated constructor is $\mathtt{fold}{\;(t)}$. The inductive
type $\mu X.A$ can then be unfolded into $A[X\leftarrow\mu X.A]$, i.e.,
substituting each occurrence of $X$ by $\mu X.A$ in $A$. Typical example of
inductive types that can be encoded this way are the natural number, as
$\mathtt{nat}=\mu X.(\mathds{1}\oplus X)$ or the lists of types $A$, noted
$[A]=\mu X.\mathds{1}\oplus(A\otimes X)$. Note that we only work with closed
types. We shall denote term-variables with $x,y,z$.

  * •

Isos types: The language features isos, noted $\omega$, higher order
reversible functions whose types $\alpha$ consist either of a pair of base
type, noted $A\leftrightarrow B$ or function types between isos,
$\alpha\to\alpha$. A first-order iso of type $A\leftrightarrow B$ consists in
a finite set of _clauses_ , written $v\leftrightarrow e$ where $v$ is a value
of type $A$ and $e$ an expression of type $B$. An expression consists in a
succession of applications of isos to some argument, described by
$\mathtt{let}$ constructions:
${\mathtt{let}}\,{(x_{1},\dots,x_{n})}={\omega\leavevmode\nobreak\
(y_{1},\dots,y_{n})}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{e}$. Isos can take other, first-order isos as arguments through the
$\lambda\psi.\omega$ construction. Those lambda-abstraction are restricted to
first-order isos, meaning that $\psi$ is of type $A\leftrightarrow B$.
Finally, isos can also represent _recursive computation_ through the
$\mathbf{fix}\leavevmode\nobreak\ \phi.\omega$ construction, where $\phi$ is
an _iso-recursive-variable_. In general, we shall denote iso-variable with
$\phi_{1},\phi_{2},\dots$ and we use the shorthands
$\mathbf{fix}\leavevmode\nobreak\ \overrightarrow{\phi}$ or
$\mathbf{fix}\leavevmode\nobreak\ .\phi_{1},\dots,\phi_{n}$ and
$\lambda\overrightarrow{\phi}$ or $\lambda\phi_{1},\dots,\phi_{n}$ for
$\mathbf{fix}\leavevmode\nobreak\ \phi_{1}.\mathbf{fix}\leavevmode\nobreak\
\phi_{2}.\dots\mathbf{fix}\leavevmode\nobreak\ \phi_{n}.$ and
$\lambda\phi.\lambda\phi_{2}.\dots\lambda\phi_{n}$.

Convention. We write $(t_{1},\dots,t_{n})$ for $\langle
t_{1},\langle\dots,t_{n}\rangle\rangle$ and $\bigoplus^{n}A$ (resp.
$\bigotimes^{n}A$) for $A\oplus\dots\oplus A$ (resp. $A\otimes\dots\otimes A$)
$n$ times and $\omega_{1}\dots\omega_{n}t$ for a succession of $\mathtt{let}$
constructions applying $\omega_{n}$ to $\omega_{1}$. We also consider
constructors to be right-associative, meaning that
$\mathtt{fold}{\;\mathtt{inj}_{r}{\;\langle x,y\rangle}}$ should be read as
$\mathtt{fold}{\;(\mathtt{inj}_{r}{\;(\langle x,y\rangle)})}$. In order to
avoid conflicts between variables we will always work up to
$\alpha$-conversion and use Barendregt’s convention [4, p.26] which consists
in keeping all to $\alpha$-conversion and use Barendregt’s bound and free
variable names distinct, even when this remains implicit.

$\begin{array}[]{c}\Psi;\emptyset\vdash_{e}():\mathds{1}\quad\Psi;x:A\vdash_{e}x:A\quad\Psi;\Delta\vdash_{e}\mathtt{inj}_{\ell}{\;t}:A\oplus
B\Psi;\Delta\vdash_{e}t:A\quad\Psi;\Delta\vdash_{e}\mathtt{inj}_{r}{\;t}:A\oplus
B\Psi;\Delta\vdash_{e}t:B\\\\[4.30554pt]
\Psi;\Delta_{1},\Delta_{2};\vdash_{e}\langle t_{1},t_{2}\rangle:A\otimes
B\Psi;\Delta_{1}\vdash_{e}t_{1}:A\hfil\lx@intercol&\Psi;\Delta_{2}\vdash_{e}t_{2}:B\quad\Delta;\Psi\vdash_{e}\mathtt{fold}{\;t}:\mu
X.A\Delta;\Psi\vdash_{e}t:A[X\leftarrow\mu X.A]\\\\[4.30554pt]
\Psi;\Delta\vdash_{e}\omega\leavevmode\nobreak\
t:B\Psi\vdash_{\omega}\omega:A\leftrightarrow
B\hfil\lx@intercol&\Psi;\Delta\vdash_{e}t:A\\\\[4.30554pt]
\Psi;\Delta_{1},\Delta_{2}\vdash_{e}{\mathtt{let}}\,{(x_{1},\dots,x_{n})}={t_{1}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\
{t_{2}}:B\Psi;\Delta_{1}\vdash_{e}t_{1}:A_{1}\otimes\dots\otimes
A_{n}\qquad\Psi;\Delta_{2},x_{1}:A_{1},\dots,x_{n}:A_{n}\vdash_{e}t_{2}:B\end{array}$
Table 2: Typing of terms and expressions.
$\begin{array}[]{c}\Psi\vdash_{\omega}\\{v_{1}\leftrightarrow
e_{1}\mid\dots\mid v_{n}\leftrightarrow e_{n}\\}:A\leftrightarrow
B.\begin{array}[]{l@{\quad}l@{\quad}l@{\qquad}l}\Delta_{1}\vdash_{e}v_{1}:A&\ldots&\Delta_{n}\vdash_{e}v_{n}:A&\forall
i\not=j,v_{i}\bot v_{j}\\\
\Psi;\Delta_{1}\vdash_{e}e_{1}:B&\ldots&\Psi;\Delta_{n}\vdash_{e}e_{n}:B&\forall
i\not=j,Val(e_{i})\bot Val(e_{j})\end{array}\\\\[4.30554pt]
\Psi\vdash_{\omega}\mathbf{fix}\leavevmode\nobreak\
\phi.\omega:(A_{1}\leftrightarrow B_{1})\to\dots\to(A_{n}\leftrightarrow
B_{n})\to(A\leftrightarrow B)\phi:A\leftrightarrow
B,\Psi\vdash_{\omega}\omega:(A_{1}\leftrightarrow
B_{1})\to\dots\to(A_{n}\leftrightarrow B_{n})\to(A\leftrightarrow B)\qquad
f:\alpha,\Psi\vdash_{\omega}\phi:\alpha\\\\[4.30554pt]
\Psi\vdash_{\omega}\lambda\phi.\omega:(A\leftrightarrow
B)\to\alpha\phi:A\leftrightarrow
B,\Psi\vdash_{\omega}\omega:\alpha\qquad\Psi\vdash_{\omega}\omega_{1}\leavevmode\nobreak\
\omega_{2}:\alpha\Psi\vdash_{\omega}\omega_{1}:(A\leftrightarrow
B)\to\alpha\qquad\Psi\vdash_{\omega}\omega_{2}:A\leftrightarrow B\\\
\end{array}$ Table 3: Typing of isos.

Typing judgements. Both base terms and isos feature their own typing
judgements, given in Table 2 and Table 3. Term typing judgements are of the
form $\Psi;\Delta\vdash_{e}t:A$ where $\Delta$ is a context of term-variables
of type $A$ and $\Psi$ is a context of iso-variables of type $\alpha$ and
therefore isos typing judgement are of the form
$\Psi\vdash_{\omega}\omega:\alpha$. While $\Delta$ is a _linear_ context,
$\Psi$ is not, as an iso represent a close computation, and can be duplicated
or erased at will.

While [9] and [36] require isos to be exhaustive (i.e. to cover all the
possible values of its input types) and non-overlapping (i.e. two clauses
cannot match a same value), we relax the exhaustivity requirement in this
paper, in the spirit of what was done in [8]. Non-overlapping is formalised by
the notion of _orthogonality_ between values, noted $v_{1}\bot v_{2}$ and is
defined inductively by:
$\mathtt{inj}_{\ell}{\;(v)}\bot\mathtt{inj}_{r}{\;(v^{\prime})}$,
$\mathtt{inj}_{r}{\;(v)}\bot\mathtt{inj}_{\ell}{\;(v^{\prime})}$, and whenever
$v_{1}\bot v_{2}$, we set
$\mathtt{inj}_{\ell}{\;(v_{1})}\bot\mathtt{inj}_{\ell}{\;(v_{2})}$,
$\mathtt{inj}_{r}{\;(v_{1})}\bot\mathtt{inj}_{r}{\;(v_{2})}$,
$\mathtt{fold}{\;(v_{1})}\bot\mathtt{fold}{\;(v_{2})}$, $\langle
v,v_{1}\rangle\bot\langle v^{\prime},v_{2}\rangle$ and $\langle
v_{1},v\rangle\bot\langle v_{2},v^{\prime}\rangle$. In the typing rule for
isos, $\operatorname{Val}(e)$ is defined as:
$\operatorname{Val}({\mathtt{let}}\,{t_{1}}={t_{2}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {t_{3}})=\operatorname{Val}(t_{3})$ and
$\operatorname{Val}(v)=v$.

$\begin{array}[]{c}C[t_{1}]\to C[t_{2}]t_{1}\to
t_{2}\qquad{\mathtt{let}}\,{p}={v}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {t}\to\sigma(t)\sigma(p)=v\\\\[6.45831pt]
(\mathbf{fix}\leavevmode\nobreak\
\phi.\omega)\to\lambda\phi_{1}\dots\phi_{n}.(\omega[\phi\leftarrow((\mathbf{fix}\leavevmode\nobreak\
\phi.\omega)\phi_{1}\dots\phi_{n})])\phi_{1}\dots\phi_{n}\phi:A\leftrightarrow
B,\Psi\vdash_{\omega}\omega:(A_{1}\leftrightarrow
B_{1})\to\dots\to(A_{n}\leftrightarrow B_{n})\to(A\leftrightarrow
B)\\\\[6.45831pt] \\{v_{1}\leftrightarrow e_{1}\mid\dots\mid
v_{n}\leftrightarrow e_{n}\\}\leavevmode\nobreak\
v^{\prime}\to\sigma(e_{i})\sigma(v_{i})=v^{\prime}\qquad(\lambda\phi.\omega_{1})\leavevmode\nobreak\
\omega_{2}\to\omega_{1}[\phi\leftarrow\omega_{2}]\end{array}$ Table 4:
Evaluation relation $\to$.

Operational semantics. The language comes equipped with a rewriting system
$\to$ on terms, defined in Table 4. As usual we note $\to^{*}$ for the
reflexive transitive closure of $\to$. The evaluations contexts $C$ are
defined as by the grammar $[\leavevmode\nobreak\ ]\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \mathtt{inj}_{\ell}{\;C}\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \mathtt{inj}_{r}{\;C}\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \omega\leavevmode\nobreak\ C\leavevmode\nobreak\
\mid\leavevmode\nobreak\ {\mathtt{let}}\,{p}={C}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {t}\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \langle C,v\rangle\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \langle v,C\rangle\leavevmode\nobreak\
\mid\leavevmode\nobreak\ C\leavevmode\nobreak\ t\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \mathtt{fold}{\;C}$. In particular, the rewriting
system follow a _call-by-value_ strategy, requiring that the argument of an
iso is fully evaluated to a value before firing the substitution. Note that
unlike [9, 36], we do not require any form of termination and isos are not
required to be exhaustive: the rewriting system can diverge or be stuck. The
evaluation of an iso applied to a value is dealt with pattern-matching: the
input value will try to match one of the value from the clauses and
potentially create a substitution if the two values match, giving the
corresponding expression as an output under that substitution. A substitution
$\sigma$ is a mapping from a set of variables to terms. The substitution of
$\sigma$ on an expression $t$, written $\sigma(t)$, defined in the usual way
by $\sigma(())=()$; $\sigma(x)=v$ if $\\{x\mapsto v\\}\subseteq\sigma$;
$\sigma(\mathtt{inj}_{r}{\;(t)})=\mathtt{inj}_{r}{\;(\sigma(t))}$;
$\sigma(\mathtt{inj}_{\ell}{\;(t)})=\mathtt{inj}_{\ell}{\;(\sigma(t))}$;
$\sigma(\mathtt{fold}{\;(t)})=\mathtt{fold}{\;(\sigma(t))}$ $\sigma(\langle
t,t^{\prime}\rangle)=\langle\sigma(t),\sigma(t^{\prime})\rangle$;
$\sigma(\omega\leavevmode\nobreak\ t)=\omega\leavevmode\nobreak\ \sigma(t)$
and $\sigma({\mathtt{let}}\,{p}={t_{1}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\
{t_{2}})=({\mathtt{let}}\,{p}={\sigma(t_{1})}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {\sigma(t_{2})})$. The support of a
substitution, written $\text{supp}(\sigma)$ is defined as $\\{x\mid(x\mapsto
v)\in\sigma\\}$.

######  Lemma 2.1 (Subject Reduction).

If $\Psi;\Delta\vdash_{e}t:A$ and $t\rightarrow t^{\prime}$ then
$\Psi;\Delta\vdash_{e}t^{\prime}:A$.∎

The proof is similar to what has been done in [9]. As the rewriting system is
deterministic, confluence is direct; meanwhile progress is not guaranteed: a
term can be stuck, for example, $\\{\mathtt{inj}_{\ell}{\;(x)}\leftrightarrow
e\\}\leavevmode\nobreak\ \mathtt{inj}_{r}{\;(v)}$ does not reduce.

Inversion. Finally, any iso $\omega:\alpha$ can be inverted into an iso
$\omega^{-1}:\alpha^{-1}$, such that their composition makes up the identity.
Intuitively, if $\omega$ is of type $A\leftrightarrow B$, then $\omega^{-1}$
will be of type $B\leftrightarrow A$. Inversion is defined as follows. Given a
iso-type $\alpha$, we define its inverse $\alpha^{-1}$ as: $(A\leftrightarrow
B)^{-1}=B\leftrightarrow A$ and $((A\leftrightarrow
B)\to\alpha)^{-1}=(B\leftrightarrow A)\to\alpha^{-1}$. Given an iso $\omega$,
we define its dual $\omega^{-1}$ as: $\phi^{-1}=\phi$;
$(\mathbf{fix}\leavevmode\nobreak\
\phi.\omega)^{-1}=\mathbf{fix}\leavevmode\nobreak\ \phi.\omega^{-1}$;
$(\omega_{1}\leavevmode\nobreak\
\omega_{2})^{-1}=(\omega_{1})^{-1}(\omega_{2})^{-1}$;
$(\lambda\phi.\omega)^{-1}=\lambda\phi.(\omega)^{-1}$ and
$\\{(v_{i}\leftrightarrow e_{i})_{i\in I}\\}^{-1}=\\{((v_{i}\leftrightarrow
e_{i})^{-1})_{i\in I}\\}$ and

$\left(\begin{array}[]{l@{~}c@{~}l}v_{1}\hfil\leavevmode\nobreak\
&{\leftrightarrow}\hfil\leavevmode\nobreak\
&{\mathtt{let}}\,{p_{1}}={\omega_{1}\leavevmode\nobreak\
p_{1}^{\prime}}\leavevmode\nobreak\ {\mathtt{in}{}\nobreak\leavevmode}\\\
\hfil\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\ &\cdots\\\
\hfil\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\
&{\mathtt{let}}\,{p_{n}}={\omega_{n}\leavevmode\nobreak\
p^{\prime}_{n}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{v^{\prime}_{1}}\end{array}\right)^{-1}:=\left(\begin{array}[]{lcl@{}l@{}l}v^{\prime}_{1}&{\leftrightarrow}&{\mathtt{let}}\,{p^{\prime}_{n}}={\omega_{n}^{-1}\leavevmode\nobreak\
p_{n}}\leavevmode\nobreak\ {\mathtt{in}{}\nobreak\leavevmode}\\\ &&\cdots\\\
&&{\mathtt{let}}\,{p^{\prime}_{1}}={\omega_{1}^{-1}\leavevmode\nobreak\
p_{1}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{v_{1}}\end{array}\right).$

######  Lemma 2.2 (Inversion is well-typed).

If $\phi_{1}:A_{1}\leftrightarrow B_{1}\ldots\phi_{1}:A_{n}\leftrightarrow
B_{n}\vdash_{\omega}\omega:\alpha$, then $\phi_{1}:B_{1}\leftrightarrow
A_{1}\ldots\phi_{1}:B_{n}\leftrightarrow
A_{n}\vdash_{\omega}\omega^{-1}:\alpha^{-1}$. ∎

######  Lemma 2.3 (Inversion is preserved by evaluation).

If $\omega\to\omega^{\prime}$ then $\omega^{-1}\to\omega^{\prime-1}$.∎

######  Theorem 2.4 (Isos are isomorphisms [9]).

For all well-typed isos $\vdash_{\omega}\omega:A\leftrightarrow B$, and for
all well-typed values $\vdash_{e}v:A$, if $(\omega\leavevmode\nobreak\
(\omega^{-1}\leavevmode\nobreak\ v))\rightarrow^{*}v^{\prime}$ then
$v=v^{\prime}$.∎

######  Example 2.5.

Remember that $[A]=\mu X.\mathds{1}\oplus(A\otimes X)$. One can define the
_map_ operator on list with an iso of type $(A\leftrightarrow
B)\to[A]\leftrightarrow[B]$, defined as

$\lambda\psi.\mathbf{fix}\leavevmode\nobreak\
\phi.\left\\{\begin{array}[]{l@{~}c@{~}l}[\leavevmode\nobreak\
]\hfil\leavevmode\nobreak\ &{\leftrightarrow}\hfil\leavevmode\nobreak\
&[\leavevmode\nobreak\ ]\\\ h::t\hfil\leavevmode\nobreak\
&{\leftrightarrow}\hfil\leavevmode\nobreak\
&{\mathtt{let}}\,{h^{\prime}}={\psi\leavevmode\nobreak\ h}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\
{}{\mathtt{let}}\,{t^{\prime}}={\phi\leavevmode\nobreak\
t}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}h^{\prime}::t^{\prime}\end{array}\right\\},$

with the terms $[\leavevmode\nobreak\
]=\mathtt{fold}{\;\mathtt{inj}_{\ell}{\;(())}}$, representing the empty list,
and $h::t=\mathtt{fold}{\;(\mathtt{inj}_{r}{\;\langle h,t\rangle})}$,
representing the head and tail of the list. Its inverse
$\operatorname{map}^{-1}$ is

$\lambda\psi.\mathbf{fix}\leavevmode\nobreak\
\phi.\left\\{\begin{array}[]{l@{~}c@{~}l}[\leavevmode\nobreak\
]\hfil\leavevmode\nobreak\ &{\leftrightarrow}\hfil\leavevmode\nobreak\
&[\leavevmode\nobreak\ ]\\\ h^{\prime}::t^{\prime}\hfil\leavevmode\nobreak\
&{\leftrightarrow}\hfil\leavevmode\nobreak\
&{\mathtt{let}}\,{t}={\phi\leavevmode\nobreak\ t^{\prime}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {}{\mathtt{let}}\,{h}={\psi
h^{\prime}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}h::t\end{array}\right\\}.$

Note that in the latter, the variable $\psi$ has type $B\leftrightarrow A$. If
we consider the inverse of the term $(\operatorname{map}\leavevmode\nobreak\
\omega)$ we would obtain the term
$(\operatorname{map}^{-1}\leavevmode\nobreak\ \omega^{-1})$ where
$\omega^{-1}$ would be of type $B\leftrightarrow A$.

######  Example 2.6 (Cantor Pairing).

One can encode the Cantor Pairing between
$\mathbb{N}\otimes\mathbb{N}\leftrightarrow\mathbb{N}$. First recall that the
type of natural number $\mathtt{nat}$ is given by $\mu X.\mathds{1}\oplus X$,
then define $\overline{n}$ as the encoding of natural numbers into a closed
value of type $\mathtt{nat}$ as
$\overline{0}=\mathtt{fold}{\;(\mathtt{inj}_{\ell}{\;()})}$ and given a
variable $x$ of type $\mathtt{nat}$, its successor is
$\overline{S(x)}=\mathtt{fold}{\;(\mathtt{inj}_{r}{\;(x)})}$. Omitting the
$\overline{\ \cdot\ }$ operator for readability, the pairing is then defined
as:

$\begin{array}[]{ll}\omega_{1}:\mathtt{nat}\otimes\mathtt{nat}\leftrightarrow(\mathtt{nat}\otimes\mathtt{nat})\oplus\mathds{1}\\\
=\left\\{\begin{array}[]{lcl}\langle
S(i),j\rangle&{\leftrightarrow}&\mathtt{inj}_{\ell}{\;(\langle
i,S(j)\rangle)}\\\ \langle
0,S(S(j))\rangle&{\leftrightarrow}&\mathtt{inj}_{\ell}{\;(\langle
S(j),0\rangle)}\\\ \langle
0,S(0)\rangle&{\leftrightarrow}&\mathtt{inj}_{\ell}{\;(\langle 0,0\rangle)}\\\
\langle
0,0\rangle&{\leftrightarrow}&\mathtt{inj}_{r}{\;(())}\end{array}\right\\},\end{array}\hfill\begin{array}[]{ll}\omega_{2}:(\mathtt{nat}\otimes\mathtt{nat})\oplus\mathds{1}\leftrightarrow\mathtt{nat}\\\
=\left\\{\begin{array}[]{lcl}\mathtt{inj}_{\ell}{\;(x)}&{\leftrightarrow}&{\mathtt{let}}\,{y}={g\leavevmode\nobreak\
x}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\ {S(y)}\\\
\mathtt{inj}_{r}{\;(())}&{\leftrightarrow}&0\end{array}\right\\},\\\
\operatorname{CantorPairing}:\mathtt{nat}\otimes\mathtt{nat}\leftrightarrow\mathtt{nat}\\\
=\mathbf{fix}\leavevmode\nobreak\
\phi.\left\\{\begin{array}[]{lcl}x&{\leftrightarrow}&{\mathtt{let}}\,{y}={\omega_{1}\leavevmode\nobreak\
x}\leavevmode\nobreak\ {\mathtt{in}{}\nobreak\leavevmode}\\\
&&{\mathtt{let}}\,{z}={\omega_{2}\leavevmode\nobreak\ y}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {z}\end{array}\right\\},\end{array}$

where $\omega_{2}$ can be seen as an iterator of the recursive iso $\phi$
until it reaches the base case.

##  3 Expressivity

We now show how one can encode any Reversible Turing Machine [2] as a well-
typed iso. We first recall the main definition and results of RTM.

######  Definition 3.1 (Reversible Turing Machine [2]).

Given a Turing Machine $M=(Q,\Sigma,\delta,b,q_{s},q_{f})$, where $Q$ is a set
of state, $\Sigma$ is a finite set of tape symbols,
$\delta\subseteq\Delta=(Q\times[(\Sigma\times\Sigma)\cup\\{\uparrow,\downarrow,\rightarrow\\}]\times
Q)$ is a partial relation defining the transition relation, $b$ a blank symbol
and $q_{s}$ and $q_{f}$ the initial and final states. We say that $M$ is a
_Reversible Turing Machine_ (RTM) if it is:

  * •

Forward deterministic: for any two distinct pair of triple
$(q_{1},a_{1},q_{1}^{\prime})$ and $(q_{2},a_{2},q_{2}^{\prime})$ in $\delta$,
if $q_{1}=q_{2}$ then $a_{1}=(s_{1},s_{1}^{\prime})$ and
$a_{2}=(s_{2},s_{2}^{\prime})$ and $s_{1}\not=s_{2}$.

  * •

Backward deterministic: for any two distinct pair of triple
$(q_{1},a_{1},q_{1}^{\prime})$ and $(q_{2},a_{2},q_{2}^{\prime})$ in $\delta$,
if $q_{1}^{\prime}=q_{2}^{\prime}$ then $a_{1}=(s_{1},s_{1}^{\prime})$ and
$a_{2}=(s_{2},s_{2}^{\prime})$ and $s_{1}^{\prime}\not=s_{2}^{\prime}$.

######  Definition 3.2 (Configuration).

A configuration of a RTM is a tuple $(q,(l,s,r))\in
Q\times(\Sigma^{*}\times\Sigma\times\Sigma^{*})$ where $q$ is the internal
state, $l,r$ are the left and right parts of the tape (as string) and
$s\in\Sigma$ is the current symbol being scanned.

######  Definition 3.3 (RTM Transition).

A RTM $M$ in configuration $C=(q,(l,s,r))$ goes to a configuration
$C^{\prime}=(q^{\prime},(l^{\prime},s^{\prime},r^{\prime}))$, written $T\vdash
C\rightsquigarrow C^{\prime}$ in a single step if there exists a transition
$(q,a,q^{\prime})\in\delta$ where $a$ is either $(s,s^{\prime})$, and then
$l=l^{\prime}$ and $r=r^{\prime}$ or
$a\in\\{\leftarrow,\downarrow,\rightarrow\\}$, and we have for the case
$a=\leftarrow$: $l^{\prime}=l\cdot s$ and for $r=x\cdot r_{2}$ we have
$s^{\prime}=x$ and $r^{\prime}=r_{2}$, similarly for the case $a=\rightarrow$
and for the case $a=\downarrow$ we have $l^{\prime}=l$ and $r^{\prime}=r$.

The semantics of a RTM is given on standard configurations of the form
$(q,(\epsilon,b,s))$ where $q$ is a state, $\epsilon$ is an infinite tape of
blank symbol and $s$ is the blank-free input of the RTM.

######  Definition 3.4 (String Semantics [2]).

The semantics of a RTM $M$, written $\operatorname{Sem}(M)$ is given by
$\operatorname{Sem}(M)=\\{(s,s^{\prime})\in((\Sigma\backslash\\{b\\})^{*}\times(\Sigma\backslash\\{b\\})^{*})\mid
M\vdash(q_{s},(\epsilon,b,s))\rightsquigarrow^{*}(q_{f},(\epsilon,b,s^{\prime}))\\}$.

######  Theorem 3.5 (Properties of RTM [2]).

For all RTM $M$, $\operatorname{Sem}(M)$ is an injective function, and
conversely all injective computable function (on a tape) are realizable by a
RTM. Finally, any Turing Machine can be simulated by a Reversible Turing
Machine.∎

###  3.1 Encoding

We are now ready to encode any RTM as a well-typed iso of the language. We
first need to choose an encoding for the set of states and the set of tape
symbols:

######  Definition 3.6 (Encoding of States and Tape Symbols).

Given a non-empty finite set of states $Q=\\{q_{1},\dots,q_{n}\\}$ and finite
set of tape symbols $\Sigma=\\{s_{1},\dots,s_{m}\\}$ with $b\in\Sigma$ and
$q_{s},q_{f}\in Q$, we define the types $Q^{T}$ and $\Sigma^{T}$ as
respectively $\bigoplus^{n}\mathds{1}$ and $\bigoplus^{m}\mathds{1}$.

We then directly get a one-to-one correspondence between elements of $Q$ and
$\Sigma$ with closed values of $Q^{T}$ and $\Sigma^{T}$.

######  Property 3.7.

Given two different states (resp. two letter) $a_{1},a_{2}$ we get
$a_{1}^{T}\bot a_{2}^{T}$.∎

Since the String Semantics defined on Definition 3.4 is only defined on a
terminating run that uses a finite amount of tape, we can represent the tapes
as a Zipper on $\Sigma^{T}$: a pair of lists of type $\Sigma^{T}$. Hence the
given data of a zipper and a state as a configuration.

######  Definition 3.8 (Encoding of Standard Configurations).

We define the type of zippers as
$\operatorname{Zipper}=[\Sigma^{T}]\otimes[\Sigma^{T}]$ and of configurations
as $C^{T}=(Q^{T}\otimes\operatorname{Zipper})$. Given a finite tape
$s=a_{1}a_{2}\dots a_{n}$ without blank symbols, we translate it as a list of
the encoding of each of its symbol, written $s^{T}$ and defined as
$[a_{1}^{T},a_{2}^{T},\dots,a_{n}^{T}]$. The standard configuration
$C=(q,(\epsilon,b,s))$ is then represented as
$\operatorname{isos}(C)=(q^{T},([],b^{T}::s^{T}))$.

We can finally encode the transition relation $\delta$ where each element of
$\delta$ is encoded as a clause between values. Then the encoding of the whole
transition relation is simply the iso that have for clauses the encoding of
each element of $\delta$.

######  Definition 3.9 (Encoding of $\delta$).

Given a RTM $M=(Q,\Sigma,\delta,b,q_{s},q_{f})$ a relation
$(q,r,q^{\prime})\in\delta$, is encoded as a clause between values
$v_{1}\leftrightarrow v_{2}$ of type $C^{T}\leftrightarrow C^{T}$ defined by
case analysis on $r$, where $x_{1},x_{2},y$ are variables:

  * •

Transition $(q,\rightarrow,q^{\prime})$ is encoded as the clause
$(q^{T},(x_{1},y::x_{2}))\leftrightarrow(q^{\prime T},(y::x_{1},x_{2}))$.

  * •

Transition $(q,\leftarrow,q^{\prime})$ is encoded as the clause
$(q^{T},(x_{1},y::x_{2}))\leftrightarrow(q^{\prime T},(y::x_{1},x_{2}))$.

  * •

Transition $(q,\downarrow,q^{\prime})$ is encoded as the clause
$(q^{T},(x_{1},x_{2}))\leftrightarrow(q^{\prime T},(x_{1},x_{2}))$.

  * •

Transition $(q,(s,s^{\prime}),q^{\prime})$ is encoded as the clause
$(q^{T},(x_{1},s^{T}::x_{2}))\leftrightarrow(q^{\prime T},(x_{1},s^{\prime
T}::x_{2}))$

Then, we define $\operatorname{isos}(M)$ as the iso whose clauses are the
encoding of each rule of $\delta$.

Along with 3.7 and the backward determinism of the RTM, we get that clauses in
the resulting iso are orthogonal to one another, and that
$\operatorname{isos}(M)$ is well-typed.

######  Corollary 3.10 ($\operatorname{isos}(M)$ is well-typed).

Given a RTM $M$, then
$\vdash_{\omega}\operatorname{isos}(M):C^{T}\leftrightarrow C^{T}$.∎

We now show that the encoding of $\delta$ simulate a step of the RTM.

######  Lemma 3.11.

Given a RTM $M$, if $M\vdash C\rightsquigarrow C^{\prime}$ then
$\operatorname{isos}(M)\operatorname{isos}(C)\rightarrow\operatorname{isos}(C^{\prime})$.∎

So far, $\operatorname{isos}(M)$ simulates exactly one evaluation step of the
Turing Machine. In order to simulate a full run, we need to define an iterator
iso. It takes as argument an iso of type $A\leftrightarrow
A\otimes(\mathds{1}\oplus\mathds{1})$, which acts on data of type $A$ until
the additional boolean is set to $\mathtt{f}\\!\mathtt{f}$.

######  Definition 3.12 (Iterator Iso).

Let $\omega_{\operatorname{aux}}:(A\leftrightarrow A\otimes\mathtt{nat})\to
A\otimes(\mathds{1}\oplus\mathds{1})\leftrightarrow A\otimes\mathtt{nat}$ be

$\omega_{\operatorname{aux}}=\lambda\psi^{\prime}.\left\\{\begin{array}[]{l@{~}c@{~}l}(y,\mathtt{t}\\!\mathtt{t})\hfil\leavevmode\nobreak\
&\leftrightarrow\hfil\leavevmode\nobreak\
&{\mathtt{let}}\,{(z,n)}={\psi^{\prime}\leavevmode\nobreak\
y}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{(z,S\leavevmode\nobreak\ n)}\\\
(y,\mathtt{f}\\!\mathtt{f})\hfil\leavevmode\nobreak\
&\leftrightarrow\hfil\leavevmode\nobreak\ &(y,0)\end{array}\right\\}$

Defined $\operatorname{It}:(A\leftrightarrow
A\otimes(\mathds{1}\oplus\mathds{1}))\to(A\leftrightarrow
A\otimes\mathtt{nat})$, counting the number of times its iso argument has been
iterated:

$\operatorname{It}=\lambda\psi.\mathbf{fix}\leavevmode\nobreak\
\phi.\left\\{\begin{array}[]{l@{~}c@{~}l}x\hfil\leavevmode\nobreak\
&\leftrightarrow\hfil\leavevmode\nobreak\
&{\mathtt{let}}\,{y}={\psi\leavevmode\nobreak\ x}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\
{}{\mathtt{let}}\,{z}={(\omega_{\operatorname{aux}}\leavevmode\nobreak\
\phi)\leavevmode\nobreak\ y}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {}z\end{array}\right\\}$

######  Lemma 3.13 (Semantics of $\operatorname{It}(\omega)$).

Given $\omega:A\leftrightarrow A\otimes(1\oplus 1)$ and some value
$\vdash_{e}v:A$ if $(\operatorname{It}\leavevmode\nobreak\
\omega)\leavevmode\nobreak\ v\rightarrow^{*}(v^{\prime},\overline{n})$ then
$\underbrace{\omega\leavevmode\nobreak\ \dots\leavevmode\nobreak\
\omega}_{n+1\text{ times}}\leavevmode\nobreak\
v\to^{*}(v^{\prime},\mathtt{f}\\!\mathtt{f})$, where $\overline{n}$ is the
encoding of the natural number $n$ into an element of type $\mathtt{nat}$, as
given in Example 2.6.∎

With this, we just need to adapt the encoding $\delta$ to the type
$C^{T}\leftrightarrow C^{T}\otimes(\mathds{1}\oplus\mathds{1})$:

######  Definition 3.14 (Encoding of $\delta$).

We modify the encoding of $\delta$ to be of type $C^{T}\leftrightarrow
C^{T}\otimes(1\oplus 1)$ to be the same but if the translation leads into the
final state, the second argument is sent to $\mathtt{f}\\!\mathtt{f}$
otherwise it is sent to $\mathtt{t}\\!\mathtt{t}$. By abuse of notation, we
also call this encoding $\operatorname{isos}(M)$.

The new encoding does not change the orthogonality and hence the new iso is
well-typed:

######  Lemma 3.15.

For any RTM $M$ we have
$\vdash_{\omega}\operatorname{isos}(M):C^{T}\otimes(\mathds{1}\oplus\mathds{1})\leftrightarrow
C^{T}\otimes(\mathds{1}\oplus\mathds{1})$.∎

Finally, we get from Lemma 3.11 and Lemma 3.13 that if, from an initial
configuration $C$, a RTM goes into the final configuration $C^{\prime}$ in
$n+1$ steps, then the Iterator iso on $\operatorname{isos}(M)$ with input the
encoding of $C$ reduces to the pair of the encodings of $C^{\prime}$ and $n$.

######  Theorem 3.16 (Simulation of String Semantics).

Let $M$ be a RTM. If
$M\vdash(q_{s},(\epsilon,b,s))\rightsquigarrow^{n+1}(q_{f},(\epsilon,b,s^{\prime}))$,
then $It(\operatorname{isos}(M))\leavevmode\nobreak\
\operatorname{isos}(q_{s},([],b,s))\rightarrow^{*}(\operatorname{isos}(q_{f},(\epsilon,b,s^{\prime})),\overline{n})$.∎

##  4 Categorical Background

We aim at providing a denotational semantics for the programming language
introduced above, meaning a mathematical interpretation abstract to the
syntax. Our approach is categorical, in the spirit of many others before us.
Programs are compositional by design, making it very natural to be interpreted
in a framework ruled by compositionality. Types are usually interpreted as
objects in a category $\mathcal{C}$, and terms as morphisms in this category.
We have seen that the main feature of our programming language is
reversibility and its terms can be seen as partial isomorphisms, or partial
injections. We want this property to be carried on the interpretation, and we
present in this section the right categories to do so. The category of sets
and partial injective functions, written $\mathbf{PInj}$, will be the
recurring example throughout this section to help the intuition.

###  4.1 Rig join inverse category

The axiomatisation of rig join inverse categories gives the conditions for the
morphisms of a category to be _partial injections_. First, the notion of
restriction allows to capture the _actual_ domain of a morphism through a
partial identity function. Historically, _inverse_ categories [27] were
introduced before _restriction_ categories, but the latter are more convenient
to introduce the subject.

######  Definition 4.1 (Restriction [10]).

A restriction structure is an operator that maps each morphism $f:A\rightarrow
B$ to a morphism $\overline{f}:A\rightarrow A$ such that
$f\circ\overline{f}=f$,
$\overline{f}\circ\overline{g}=\overline{g}\circ\overline{f}$,
$\overline{f\circ\overline{g}}=\overline{f}\circ\overline{g}$ and
$\overline{h}\circ f=f\circ\overline{h\circ f}$. A morphism $f$ is said to be
_total_ if $\overline{f}=1_{A}$. A category with a restriction structure is
called a _restriction category_. A functor
$F:\mathcal{C}\rightarrow\mathcal{D}$ is a _restriction functor_ if
$\overline{F(f)}=F\left(\overline{f}\right)$ for all morphism $f$ of
$\mathcal{C}$. The definition is canonically extended to bifunctors. When
unambiguous, we write $gf$ for the composition $g\circ f$.

######  Example 4.2.

Given sets $A,B$ and a function $f:A\to B$ defined on $A^{\prime}\subseteq A$
and undefined on $A\setminus A^{\prime}$, the restriction of $f$ is
$\overline{f}:A\to A$, the identity on $A^{\prime}\subseteq A$ and undefined
on $A\setminus A^{\prime}$. This example shows that $\mathbf{PInj}$ is a
restriction category.

To interpret reversibility, we need to introduce a notion of reversed process,
a process that exactly reverses another process. This is given by a
generalised notion of inverse.

######  Definition 4.3 (Inverse category [24]).

An _inverse category_ is a restriction category where all morphisms are
partial isomorphisms; meaning that for $f:A\rightarrow B$, there exists a
unique $f^{\circ}:B\rightarrow A$ such that $f^{\circ}\circ f=\overline{f}$
and $f\circ f^{\circ}=\overline{f^{\circ}}$.

######  Example 4.4.

In $\mathbf{PInj}$, let us consider the partial function
$f\colon\\{0,1\\}\to\\{0,1\\}$ as $f(0)=1$ and undefined on $1$. Its
restriction $\overline{f}$ is undefined on $1$ also but $\overline{f}(0)=0$.
its _inverse_ $f^{\circ}$ is undefined on $0$ and such that $f^{\circ}(1)=0$.

The example above generalises and $\mathbf{PInj}$ is an actual inverse
category. Even more, it is _the_ inverse category: [27] proves that every
locally small inverse category is isomorphic to a subcategory of
$\mathbf{PInj}$.

######  Definition 4.5 (Restriction compatible [24]).

Two morphisms $f,g:A\to B$ in a restriction category $\mathcal{C}$ are
restriction compatible if $f\overline{g}=g\overline{f}$. The relation is
written $f\smile g$. If $\mathcal{C}$ is an inverse category, they are inverse
compatible if $f\smile g$ and $f^{\circ}\smile g^{\circ}$, noted $f\asymp g$.
A set $S$ of morphisms of the same type $A\to B$ is restriction compatible
(resp. inverse compatible) if all elements of $S$ are pairwise restriction
compatible (resp. inverse compatible).

######  Definition 4.6 (Partial order [10]).

Let $f,g:A\to B$ be two morphisms in a restriction category. We then define
$f\leq g$ as $g\overline{f}=f$.

######  Definition 4.7 (Joins [16]).

A restriction category $\mathcal{C}$ is equipped with joins if for all
restriction compatible sets $S$ of morphisms $A\to B$, there exists
$\bigvee_{s\in S}s:A\to B$ morphism of $\mathcal{C}$ such that, whenever
$t:A\to B$ and whenever for all $s\in S$, $s\leq t$, $s\leq\bigvee_{s\in S}s$,
$\bigvee_{s\in S}s\leq t$, $\overline{\bigvee_{s\in S}s}=\bigvee_{s\in
S}\overline{s}$, $f\circ\left(\bigvee_{s\in S}s\right)=\bigvee_{s\in S}fs$,
$\left(\bigvee_{s\in S}s\right)\circ g=\bigvee_{s\in S}sg$. Such a category is
called a _join restriction category_. An inverse category with joins is called
a _join inverse category_.

Building up from Definition 4.1, a _join restriction functor_ is a restriction
functor that preserves all thus constructed joins.

######  Definition 4.8 (Zero [24]).

Since $\emptyset\subseteq\text{Hom}_{\mathcal{C}}(A,B)$, and since all of its
elements are restriction compatible, there exists a morphism
$0_{A,B}\doteq\bigvee_{s\in\emptyset}s$, called _zero_.

######  Lemma 4.9 ([24]).

Whenever well-typed, the zero satisfies the following equations: $f0=0$,
$0g=0$, $0_{A,B}^{\circ}=0_{B,A}$, $\overline{0_{A,B}}=0_{A,A}$.∎

######  Definition 4.10 (Disjointness tensor [24]).

An inverse category $\mathcal{C}$ is said to have a disjointness tensor if it
is equipped with a restriction bifunctor
$.\oplus.:\mathcal{C}\times\mathcal{C}\rightarrow\mathcal{C}$, with a unit
object $0$ and morphisms $\iota_{l}:A\rightarrow A\oplus B$ and
$\iota_{r}:B\rightarrow A\oplus B$ that are total and such that
$\overline{\iota_{l}^{\circ}}\leavevmode\nobreak\
\overline{\iota_{r}^{\circ}}=0_{A\oplus B}$.

######  Definition 4.11 ([25]).

Let us consider a join inverse category equipped with a symmetric monoidal
tensor product $(\otimes,1)$ and a disjointness tensor $(\oplus,0)$ that are
join preserving, and such that there is an isomorphism
$\delta_{A,B,C}:A\otimes(B\oplus C)\rightarrow(A\otimes B)\oplus(A\otimes C)$.
This is called a _join inverse rig category_.

###  4.2 $\mathbf{DCPO}$-category

We use the vocabulary of enriched category theory to shorten the discussion in
this section. The notions of enrichment required to understand the semantics
later is basic and should not frighten the reader. Categories in computer
science are usually _locally small_ , meaning that given two objects $A$ and
$B$, there is a _set_ of morphisms $A\to B$. Enrichment is the study of the
structure of those sets of morphisms, which could be vector spaces or
topological spaces for example, more details can be found in [28, 29, 33]. It
turns out that homsets in join inverse rig categories are dcpos – directed-
complete partial order, i.e. a partial-ordered set with all directed joins.
This allows us to consider fixpoints in homsets. $\mathbf{DCPO}$ is the
category of directed complete partial orders and Scott-continuous functions –
monotone functions preserving joins. Dcpos are often used for the denotational
interpretation of different sorts of $\lambda$-calculi, and more generally to
interpret recursive functions or indefinite loops.

######  Definition 4.12 ([13]).

A $\mathbf{DCPO}$-category is a locally small category whose hom-sets are
directly partial ordered and where composition is a continuous operation (i.e.
a morphism in $\mathbf{DCPO}$). It is also said that the given category is
enriched in $\mathbf{DCPO}$.

######  Remark 4.13.

We can more generally define $\mathcal{V}$-categories with a monoidal category
$\mathcal{V}$, where hom-sets are objects of $\mathcal{V}$ and the composition
is in $\mathcal{V}$ as morphism.

######  Theorem 4.14 ([24]).

A join inverse category is enriched in $\mathbf{DCPO}$.∎

######  Remark 4.15.

Theorem 4.14 allows then to consider fixpoints of continuous functions.
Indeed, A continuous
$f:\text{Hom}_{\mathcal{C}}(A,B)\to\text{Hom}_{\mathcal{C}}(A,B)$ in a rig
join inverse category admits $\mathbf{fix}\leavevmode\nobreak\ f:A\to B$, that
can be defined as $\sup_{n}f^{n}(0_{A,B})$.

######  Definition 4.16 ([13]).

A $\mathbf{DCPO}$-functor $F:\mathcal{K}\to\mathcal{L}$ between
$\mathbf{DCPO}$-categories is such that for every pair of objects $A,B$ in
$\mathcal{K}$, the associated morphism scheme
$F_{A,B}:\text{Hom}_{\mathcal{K}}(A,B)\to\text{Hom}_{\mathcal{L}}(FA,FB)$ is a
morphism in $\mathbf{DCPO}$.

In particular, join restriction functors in a join inverse category are
$\mathbf{DCPO}$-functors.

######  Lemma 4.17.

Let $\mathcal{C}$ be a rig join inverse category. The functors:
$-\otimes-:\mathcal{C}\times\mathcal{C}\to\mathcal{C}$,
$-\oplus-:\mathcal{C}\times\mathcal{C}\to\mathcal{C}$,
$-^{\circ}:\mathcal{C}^{op}\to\mathcal{C}$ are $\mathbf{DCPO}$-functors.∎

###  4.3 Compactness

Inductive data types are written in the syntax as some lowest fixed point of a
type judgement. As said earlier, types are represented as objects in the
category, and thus a type judgement is an object mapping, or rather an
endofunctor. We show here how to consider fixed points of endofunctors in our
categorical setting.

######  Definition 4.18 (Initial Algebra).

Given an endofunctor $F:\mathcal{C}\to\mathcal{C}$, an $F$-algebra is a pair
of an object $A$ and a morphism $f:FA\to A$. $F$-algebras form a category with
$F$-algebras homomorphisms. An initial $F$-algebra is an initial object in the
category of $F$-algebras.

######  Theorem 4.19 (Lambek’s theorem).

Given an endofunctor $F:\mathcal{C}\to\mathcal{C}$ and an $F$-initial algebra
$(X,\alpha\colon FX\to X)$, $\alpha$ is an isomorphism.∎

With Lambek’s theorem, we know that an initial algebra provides an object $X$
such that $X\cong FX$; $X$ is a fixed point of the endofunctor $F$, as
requested. The existence of such fixed points is given by the next theorem.

######  Theorem 4.20 ([13]).

A $\mathbf{DCPO}$-category with ep-zero and colimits of $\omega$-chains of
embeddings is parametrised $\mathbf{DCPO}$-algebraically $\omega$-compact;
meaning that for every $\mathbf{DCPO}$-functor
$F\colon\mathcal{C}\times\mathcal{D}\to\mathcal{D}$, there is a pair
consisting of a $\mathbf{DCPO}$-functor $F^{\text{\char
5\relax}}\\!\colon\mathcal{C}\to\mathcal{D}$ and an indexed family
$\alpha^{F}=\\{\alpha^{F}_{A}:F(A,F^{\text{\char 5\relax}}\\!A)\to
F^{\text{\char 5\relax}}\\!A\\}$ of initial $F(A,-)$-algebras. This pair is
called a _parametrised_ initial algebra. ∎

The hypothesis of the theorem above are verified by the categories we want to
work with, without loss of generality.

######  Proposition 4.21 ([24]).

Any rig join inverse category can be faithfully embedded in a rig join inverse
category with colimits of $\omega$-chains of embeddings. ∎

##  5 Denotational semantics

We now show how to build a denotational semantics for the language we
presented thus far. The semantics is akin to the one presented in [8] but with
extra structure to handle inductive types and recursive functions. While the
semantics is sound and adequate w.r.t. a notion of operational equivalence
between terms, the main interest of the semantics rest in showing that, given
some RTM $M$ whose semantics is a function $f$, we show that the semantics of
$\operatorname{isos}(M)$ is the same as $f$. This would provide us with a
formal proof that any computable reversible function can be captured by an
iso.

Types. Let us consider $\mathcal{C}$ a rig join inverse category (Definition
4.11). We can assume without loss of generality that $\mathcal{C}$ verifies
the hypothesis of Theorem 4.20. In order to deal with open types, we make use
an auxiliary judgement for types, of the form $X_{1},\ldots,X_{n}\vDash A$,
where $\\{X_{i}\\}_{i}$ is a subset of the free type variables appearing in
$A$. We interpret this kind of judgement as a $\mathbf{DCPO}$-functor
$\mathcal{C}^{\left|\Theta\right|}\to\mathcal{C}$ written
$\left\llbracket\Theta\vDash A\right\rrbracket$. This can be formally defined
as a (simple) inductive relation222See Table 6 in the Appendix., and the
semantics is defined similarly to what is done in [13, 21].
$\left\llbracket\Theta\vDash\mathds{1}\right\rrbracket$ is the constant
functor that maps to the tensor product unit. $\left\llbracket\Theta,X\vDash
X\right\rrbracket$ is a projection. The other judgements are obtained by
induction: if $\left\llbracket\Theta\vDash A\right\rrbracket=f$ and
$\left\llbracket\Theta\vDash B\right\rrbracket=g$, then
$\left\llbracket\Theta\vDash A\oplus B\right\rrbracket=\oplus\circ\langle
f,g\rangle$ and $\left\llbracket\Theta\vDash A\otimes
B\right\rrbracket=\otimes\circ\langle f,g\rangle$. Finally,
$\left\llbracket\Theta\vDash\mu
X.A\right\rrbracket=\left(\left\llbracket\Theta,X\vDash
A\right\rrbracket\right)^{\text{\char 5\relax}}\\!$. Lemma 4.17 and Theorem
4.20 ensure that this is well-defined. For closed types, we have
$\left\llbracket\mathds{1}\right\rrbracket=1$, $\left\llbracket A\oplus
B\right\rrbracket=\left\llbracket A\right\rrbracket\oplus\left\llbracket
B\right\rrbracket$, $\left\llbracket A\otimes
B\right\rrbracket=\left\llbracket A\right\rrbracket\otimes\left\llbracket
B\right\rrbracket$ and $\left\llbracket\mu
X.A\right\rrbracket\cong\left\llbracket A[X\leftarrow\mu
X.A]\right\rrbracket$. Isos are represented by dcpos of morphisms in
$\mathcal{C}$, written $\left\llbracket A\leftrightarrow
B\right\rrbracket=\text{Hom}_{\mathcal{C}}(\left\llbracket
A\right\rrbracket,\left\llbracket B\right\rrbracket)$. The terms used to build
isos are dependent in two contexts: variables in $\Delta$ and isos in $\Psi$.
In general, if $\Delta=x_{1}:A_{1},\dots,x_{m}:A_{m}$ and
$\Psi=\phi_{1}:B_{1}\leftrightarrow C_{1},\dots,\phi_{n}:B_{n}\leftrightarrow
C_{n}$, then we set $\left\llbracket\Delta\right\rrbracket=\left\llbracket
A_{1}\right\rrbracket\otimes\dots\otimes\left\llbracket A_{m}\right\rrbracket$
and $\left\llbracket\Psi\right\rrbracket=\text{Hom}(\left\llbracket
B_{1}\right\rrbracket,\left\llbracket
C_{1}\right\rrbracket)\times\dots\times\text{Hom}(\left\llbracket
B_{n}\right\rrbracket,\left\llbracket C_{n}\right\rrbracket)$, with $\otimes$
being the monoidal product in $\mathcal{C}$ and $\times$ the cartesian product
in $\mathbf{DCPO}$.

Values. Values have type judgements of the form $\Delta\vdash_{v}v:A$, and
they are interpreted with morphisms in $\mathcal{C}$, written
$\left\llbracket\Delta\vdash_{v}v:A\right\rrbracket:\left\llbracket\Delta\right\rrbracket\to\left\llbracket
A\right\rrbracket$. The interpretation is defined inductively on the typing
rules of values. The initial ones are
$\left\llbracket\vdash_{v}():\mathds{1}\right\rrbracket=Id_{1}$ and
$\left\llbracket x:A\vdash_{v}x:A\right\rrbracket=Id_{\left\llbracket
A\right\rrbracket}$. Given
$f_{1}=\left\llbracket\Delta_{1}\vdash_{v}v_{1}:A_{1}\right\rrbracket$ and
$f_{2}=\left\llbracket\Delta_{2}\vdash_{v}v_{2}:A_{2}\right\rrbracket$, we
define
$\left\llbracket\Delta_{1}\vdash_{v}\mathtt{inj}_{\ell}{\;v}_{1}:A_{1}\oplus
B\right\rrbracket=\iota_{l}\circ f_{1}$,
$\left\llbracket\Delta_{1}\vdash_{v}\mathtt{inj}_{r}{\;v}_{1}:B\oplus
A_{1}\right\rrbracket=\iota_{r}\circ f_{1}$, amd
$\left\llbracket\Delta_{1},\Delta_{2}\vdash_{v}\langle
v_{1},v_{2}\rangle:A_{1}\otimes A_{2}\right\rrbracket=f_{1}\otimes f_{2}$.
Finally, given $f=\left\llbracket\Delta\vdash_{v}v:A[X\leftarrow\mu
X.A]\right\rrbracket$, we defined
$\left\llbracket\Delta\vdash_{v}\mathtt{fold}{\;v}:\mu
X.A\right\rrbracket=\alpha^{\left\llbracket X\vdash
A\right\rrbracket}_{\left\llbracket\mu X.A\right\rrbracket}\circ f$.

Extended values. The most general terms that we have to manipulate have a type
judgement which is written “$\Psi;\Delta\vdash_{e}e:A$”. $\Psi$ and $\Delta$
live in two different levels, and we choose to denote the judgement as if it
was written “$\Psi\Vdash\Delta\vdash_{e}e:A$” in order to make difference
between the two layers even clearer, with variables of iso types first and
then ground variables. Extended values are then interpreted as morphisms in
$\mathbf{DCPO}$,
$\left\llbracket\Psi\Vdash\Delta\vdash_{e}e:A\right\rrbracket:\left\llbracket\Psi\right\rrbracket\to\text{Hom}(\left\llbracket\Delta\right\rrbracket,\left\llbracket
A\right\rrbracket)$. This map is obviously a morphism in $\mathbf{Set}$ and we
will have to prove, with our construction, that it is a morphism in
$\mathbf{DCPO}$ in order to have a fixpoint that can interpretation recursion.
We will name those morphisms _morphism schemes_ , to differentiate with
morphisms in $\mathcal{C}$. To say that a function between two dcpos is a
morphism in $\mathbf{DCPO}$, we sometimes only mention that it is Scott-
continuous, or continuous; we allow ourselves these variations because the
context is not ambiguous.

The typing rules when $\Psi$ is not altered are the same as the typing rules
for values; considering those rules on terms, only the output of the morphism
scheme will be modified, as written above. The only different rule is the one
introducing $\mathbf{let}$. Given the morphisms
$\zeta_{1}=\left\llbracket\Psi,\phi:A\leftrightarrow
B\Vdash\Delta_{1}\vdash_{e}e_{1}:A\right\rrbracket$ and
$\zeta_{2}=\left\llbracket\Psi,\phi:A\leftrightarrow
B\Vdash\Delta_{2},p:B\vdash_{e}e_{2}:C\right\rrbracket$, we define
$\left\llbracket\Psi,\phi:A\leftrightarrow
B\Vdash\Delta_{1},\Delta_{2}\vdash_{v}{\mathtt{let}}\,{p}={\phi
e_{1}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{e_{2}}:C\right\rrbracket$ of type
$\left\llbracket\Psi\right\rrbracket\times\text{Hom}_{\mathcal{C}}(\left\llbracket
A\right\rrbracket,\left\llbracket
B\right\rrbracket)\to\text{Hom}_{\mathcal{C}}(\left\llbracket\Delta_{2},\Delta_{1}\right\rrbracket,\left\llbracket
C\right\rrbracket)$ by
$(\gamma,f)\mapsto\zeta_{2}(\gamma)\circ(Id_{\left\llbracket\Delta_{2}\right\rrbracket}\otimes(f\circ\zeta_{1}(\gamma)))$
This interpretation is a function in $\mathbf{Set}$. The
$\mathbf{DCPO}$-enrichment of $\mathcal{C}$ and Lemma 4.17 are sufficient to
show that it is a continuous function.

######  Lemma 5.1.

Given $\Psi\Vdash\Delta\vdash_{e}e:A$,
$\left\llbracket\Psi\Vdash\Delta\vdash_{e}e:A\right\rrbracket$ is a morphism
in $\mathbf{DCPO}$.

Isos. Isos do only depend on function variables, but they are innately
morphisms, so their denotation will be similar to terms – a morphism scheme:
$\left\llbracket\Psi\vdash_{\omega}\omega:A\leftrightarrow
B\right\rrbracket:\left\llbracket\Psi\right\rrbracket\to\text{Hom}_{\mathcal{C}}(\left\llbracket
A\right\rrbracket,\left\llbracket B\right\rrbracket)$. We define the
denotation of an iso by induction on the typing rules. The first one is
direct:

$\begin{split}\left\llbracket\Psi,\phi:A\leftrightarrow
B\vdash_{\omega}\phi:A\leftrightarrow
B\right\rrbracket=\left\\{\begin{array}[]{cl}\left\llbracket\Psi\right\rrbracket\times\text{Hom}_{\mathcal{C}}(\left\llbracket
A\right\rrbracket,\left\llbracket
B\right\rrbracket)&\to\text{Hom}_{\mathcal{C}}(\left\llbracket
A\right\rrbracket,\left\llbracket B\right\rrbracket)\\\ (\gamma,f)&\mapsto
f.\end{array}\right.\end{split}$

This is the usual interpretation for a variable in a simply-typed
$\lambda$-calculus. The two remaining ones need more details. Let us consider
the rule that builds an iso. We write $[n]=\\{1,\dots,n\\}$. Let
$n\in\mathbb{N}$ and for any $i\in[n]$ ,
$f_{i}=\left\llbracket\Delta_{i}\vdash_{v}v_{i}:A\right\rrbracket$ and
$\zeta_{i}=\left\llbracket\Psi\Vdash\Delta_{i}\vdash_{e}e_{i}:B\right\rrbracket$.

$\begin{split}\left\llbracket\Psi\vdash_{\omega}\left\\{\leavevmode\nobreak\
\mid\leavevmode\nobreak\ v_{1}\leftrightarrow
e_{1}\mid\dots\mid\leavevmode\nobreak\ v_{n}\leftrightarrow
e_{n}\leavevmode\nobreak\ \right\\}:A\leftrightarrow
B\right\rrbracket=\left\\{\begin{array}[]{cl}\left\llbracket\Psi\right\rrbracket&\to\text{Hom}_{\mathcal{C}}(\left\llbracket
A\right\rrbracket,\left\llbracket B\right\rrbracket)\\\
\gamma&\mapsto\bigvee_{i\in[n]}\left(\zeta_{i}(\gamma)\circ
f_{i}^{\circ}\right).\end{array}\right.\end{split}$

This scheme is not well-defined unless the joined morphisms are compatible
(Definition 4.5). Compatibility falls from a certain number of lemmas [8]
which conclude with:

######  Lemma 5.2.

If the families of values $(v_{i})_{i}$ and of expressions $(e_{i})_{i}$
respect the conditions of the iso creation rule, then for any different $i,j$
and any $\gamma\in\left\llbracket\Psi\right\rrbracket$:

$\left\llbracket\Psi\Vdash\Delta_{i}\vdash_{e}e_{i}:B\right\rrbracket(\gamma)\circ\left\llbracket\Delta_{i}\vdash_{v}v_{i}:A\right\rrbracket^{\circ}\asymp\left\llbracket\Psi\Vdash\Delta_{j}\vdash_{e}e_{j}:B\right\rrbracket(\gamma)\circ\left\llbracket\Delta_{j}\vdash_{v}v_{j}:A\right\rrbracket^{\circ}.$

This lemma ensures that
$\left\llbracket\Psi\vdash_{\omega}\left\\{\leavevmode\nobreak\
\mid\leavevmode\nobreak\ v_{1}\leftrightarrow
e_{1}\mid\dots\mid\leavevmode\nobreak\ v_{n}\leftrightarrow
e_{n}\leavevmode\nobreak\ \right\\}:A\leftrightarrow B\right\rrbracket$ is
well-defined.

We now take a look at how recursive functions are dealt with. We show that all
the morphism schemes that we manipulate are actually morphisms in
$\mathbf{DCPO}$ – or say, continuous.

######  Lemma 5.3.

Let us consider
$\xi_{1},\xi_{2}:\left\llbracket\Psi\right\rrbracket\to\text{Hom}_{\mathcal{C}}(A,B)$
continuous, such that for all
$\gamma\in\left\llbracket\Psi\right\rrbracket,\xi_{1}(\gamma)\asymp\xi_{2}(\gamma)$.
Thus $\gamma\mapsto\xi_{1}(\gamma)\vee\xi_{2}(\gamma)$ is continuous.

######  Proof 5.4.

The join (or meet) $\vee$ is directly the one in the dcpo
$\mathbf{DCPO}\left(\left\llbracket\Psi\right\rrbracket,\text{Hom}_{\mathcal{C}}(A,B)\right)$,
this operator is then continuous.

All the other denotations are defined with functors considered in Lemma 4.17
and by composition; which ensures the next lemma.

######  Lemma 5.5.

For all $\Psi$ context of isos, $a,b$ types and $\omega:A\leftrightarrow B$;
if $\Psi\vdash_{\omega}\omega:A\leftrightarrow B$ is derivable, then
$\left\llbracket\Psi\vdash_{\omega}\\{v_{1}\leftrightarrow e_{1}\mid\dots\mid
v_{n}\leftrightarrow e_{n}\\}:A\leftrightarrow B\right\rrbracket$ is a
morphism in $\mathbf{DCPO}$.

If we have $\xi=\left\llbracket\Psi,\phi:A\leftrightarrow
B\vdash_{\omega}\omega:A\leftrightarrow B\right\rrbracket$, we should be able
to express the semantics of the judgement
$\Psi\vdash_{\omega}\mathbf{fix}\leavevmode\nobreak\ \phi.\omega\colon
A\leftrightarrow B$. Indeed, for all
$\gamma\in\left\llbracket\Psi\right\rrbracket$, $\xi_{\gamma}=\xi(\gamma,-)$
is still a continuous function – since the tensor functor and the covariant
functor form an adjunction, currying being a very usually notion in the
semantics of simply-typed $\lambda$-calculus – and thus we can consider its
least fixpoint: $\sup_{n}\xi^{n}_{\gamma}\left(0_{\left\llbracket
A\right\rrbracket,\left\llbracket B\right\rrbracket}\right)$. In this case,
the following morphism scheme is well-defined:

$\left\llbracket\Psi\vdash_{\omega}\mathbf{fix}\leavevmode\nobreak\
\phi.\omega:A\leftrightarrow
B\right\rrbracket=\left\\{\begin{array}[]{cl}\left\llbracket\Psi\right\rrbracket&\to\text{Hom}_{\mathcal{C}}(\left\llbracket
A\right\rrbracket,\left\llbracket B\right\rrbracket)\\\
\gamma&\mapsto\text{lfp}\leavevmode\nobreak\ \xi_{\gamma},\end{array}\right.$

and it is continuous ([1, Proposition 5.2.7]). This continuity allows some
notion of commutativity between functions and fixpoints, which also ensures
that:

$\left\llbracket\Psi\vdash_{\omega}\mathbf{fix}\leavevmode\nobreak\
\phi.\mathbf{fix}\leavevmode\nobreak\ \chi.\omega:A\leftrightarrow
B\right\rrbracket=\left\llbracket\Psi\vdash_{\omega}\mathbf{fix}\leavevmode\nobreak\
\chi.\mathbf{fix}\leavevmode\nobreak\ \phi.\omega:A\leftrightarrow
B\right\rrbracket.$

This is sound with the commutativity of the product in $\mathbf{DCPO}$ and
thus in $\left\llbracket\Psi\right\rrbracket$.

Isos are well interpreted as Scott-continuous functions, and thus can form a
simply-typed $\lambda$-calculus, with the usual interpretation.

######  Lemma 5.6 (Continuity).

For all $\Psi$ context of isos, $A,B$ types and $\omega:A\leftrightarrow B$;
if $\Psi\vdash_{\omega}\omega:A\leftrightarrow B$ is derivable, then
$\left\llbracket\Psi\vdash_{\omega}\omega\colon A\leftrightarrow
B\right\rrbracket$ is a morphism in $\mathbf{DCPO}$.

Terms. We can apply an iso to a term with the correct type. If
$\zeta=\left\llbracket\Psi\Vdash\Delta\vdash t:A\right\rrbracket$ and
$\xi=\left\llbracket\Psi\vdash_{\omega}\omega:A\leftrightarrow
B\right\rrbracket$ then we can define the morphism
$\left\llbracket\Psi\Vdash\Delta\vdash\omega
t:B\right\rrbracket:\left\llbracket\Psi\right\rrbracket\to\text{Hom}_{\mathcal{C}}(\left\llbracket
A\right\rrbracket,\left\llbracket B\right\rrbracket)$ by
$\gamma\mapsto\xi(\gamma)\circ\zeta(\gamma)$.

######  Lemma 5.7 (Soundness).

Let us fix an interpretation $\left\llbracket-\right\rrbracket$ into a rig
join inverse category $\mathcal{C}$, in which $0\neq 1$. If
$t_{1}\to^{*}t_{2}$, then $\left\llbracket
t_{1}\right\rrbracket=\left\llbracket t_{2}\right\rrbracket$.

Our adequacy statement links the denotational semantics to the notion of
termination in the operational semantics. Given $\vdash t\colon A$, $t$ is
said _terminating_ if there exists a value $v$ such that $t\rightarrow^{*}v$.
We write $t\downarrow$. The next theorem is proven with the use of formal
approximation relations, introduced by Plotkin [35].

######  Theorem 5.8 (Adequacy).

Under the same hypotheses as Lemma 5.7, given $\vdash t\colon A$,
$t\downarrow$ iff $\left\llbracket t\right\rrbracket\neq 0_{\left\llbracket
A\right\rrbracket}$.

##  6 Semantics preservation

In this section, we fix the interpretation $\left\llbracket-\right\rrbracket$
of the language in $\mathbf{PInj}$, the category of sets and partial
injections. This choice comes without any loss of generality, and allows us to
consider _computable_ functions. So far we have shown how (i) to encode any
iso into a Reversible Turing Machine and (ii) given a sound and adequate
denotational semantics to our language. One question remain is, given any
computable function $f:\left\llbracket A\right\rrbracket\to\left\llbracket
B\right\rrbracket$, whether there exists an iso $\omega:A\leftrightarrow B$
such that $\left\llbracket\omega\right\rrbracket=f$. In order to do that, we
fix a canonical represent of our types into a suitable encoding.

###  6.1 A Canonical Representation

We define a canonical representation of closed values of some type $A$ into a
new type
$\operatorname{Enc}=\mathbb{B}\oplus\mathds{1}\oplus\mathds{1}\oplus\mathds{1}\oplus\mathds{1}\oplus\mathtt{nat}$
(recall that $\mathbb{B}=\mathds{1}\oplus\mathds{1}$ and $\mathtt{nat}=\mu
X.\mathds{1}\oplus X$). For simplicity let us name each the following terms of
type $\operatorname{Enc}$ :

$\begin{array}[]{c}\mathbf{tt}=\mathtt{inj}_{\ell}{\;(\mathtt{inj}_{\ell}{\;()})},\quad\mathbf{ff}=\mathtt{inj}_{\ell}{\;(\mathtt{inj}_{r}{\;()})},\\\
S=\mathtt{inj}_{r}{\;(\mathtt{inj}_{\ell}{\;()})},\quad
D^{\oplus}=\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\mathtt{inj}_{\ell}{\;()})})},\\\
D^{\otimes}=\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\mathtt{inj}_{\ell}{\;()})})})},\quad
D^{\mu}=\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\mathtt{inj}_{\ell}{\;()})})})})},\end{array}$

and for every natural number $n$, we write $\tilde{n}$ for
$\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\mathtt{inj}_{r}{\;(\overline{n})})})})})})}$.
Now, given some closed type $A$, we can define
$\lfloor-\rfloor_{A}:A\leftrightarrow[\operatorname{Enc}]$ the iso that
transform any close value of type $A$ into a list of $\operatorname{Enc}$. The
iso is defined inductively over $A$.

######  Definition 6.1 (Canonical Encoding).

$\lfloor-\rfloor_{A}$ is defined inductively on $A$ by
$\lfloor-\rfloor_{\mathds{1}}=\\{()\leftrightarrow[S]\\}$,

$\lfloor-\rfloor_{A\oplus
B}=\left\\{\begin{array}[]{lcl}\mathtt{inj}_{\ell}{\;(x)}&\leftrightarrow&{\mathtt{let}}\,{y}={\lfloor
x\rfloor_{A}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{D^{\oplus}::\mathbf{ff}::y}\\\
\mathtt{inj}_{r}{\;(x)}&\leftrightarrow&{\mathtt{let}}\,{y}={\lfloor
x\rfloor_{B}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{D^{\oplus}::\mathbf{tt}::y}\end{array}\right\\},$ $\lfloor-\rfloor_{A\otimes
B}=\left\\{\begin{array}[]{lcl}\langle
x,y\rangle&\leftrightarrow&{\mathtt{let}}\,{x^{\prime}}={\lfloor
x\rfloor_{A}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}{\mathtt{let}}\,{y^{\prime}}={\lfloor y\rfloor_{B}}\leavevmode\nobreak\
{\mathtt{in}{}\nobreak\leavevmode}\\\ &&{\mathtt{let}}\,{\langle
z,n\rangle}={++\leavevmode\nobreak\ \langle
x^{\prime},y^{\prime}\rangle}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\
{}D^{\otimes}::\tilde{n}::z\end{array}\right\\},$ $\lfloor-\rfloor_{\mu
X.A}=\left\\{\begin{array}[]{lcl}\mathtt{fold}{\;x}&\leftrightarrow&{\mathtt{let}}\,{y}={\lfloor
x\rfloor_{A[X\leftarrow\mu X.A]}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {}D^{\mu}::y\end{array}\right\\},$

where the iso $++:[A]\otimes[A]\leftrightarrow[A]\otimes\mathtt{nat}$ is
defined as:

$\mathbf{fix}\leavevmode\nobreak\
f.\left\\{\begin{array}[]{lcl}\langle[],x\rangle&\leftrightarrow&\langle
x,0\rangle\\\ \langle h::t,x\rangle&\leftrightarrow&{\mathtt{let}}\,{\langle
y,n\rangle}={f\leavevmode\nobreak\ \langle t,x\rangle}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {}\langle
h::y,S(n)\rangle\end{array}\right\\}.$

###  6.2 Getting rid of the garbage

As we mentioned, often in order to realise some operation in a reversible way,
one need to add some additional garbage. Nevertheless, there exists a way to
remove this garbage, albeit at the cost of a heavier computation time. First
described in [5], given two Turing machines $f_{1}$ and $f_{2}$ and some input
$\operatorname{in}$ such that if
$f_{1}(\operatorname{in})=\operatorname{out}\otimes\operatorname{garbage}$ and
$f_{2}(\operatorname{out})=\operatorname{in}\otimes\operatorname{garbage^{\prime}}$,
then the process consist of taking additional tapes in the Turing Machine in
order to reversibly duplicate (represented by the $\oplus$) or reversibly
erase some data (represented by the $\chi$) in order to recover only the
output of $f_{1}$, without any garbage. The process is shown in Figure 1.

$f_{1}$$f_{1}^{-1}$$f_{2}$$f_{2}^{-1}$$\chi$in$\emptyset$$\emptyset$outgarbageoutin$\emptyset$ingarbage’out$\emptyset$in$\emptyset$out$\emptyset$
Figure 1: Reversibly removing additional garbage from some process.

In order to recreate this process, one therefore need a reversible duplication
process and a reversible erasure process. The two process are obviously the
inverse from one another and so we only focus on the duplication one. Note
that every closed value of a closed type can be reversibly duplicated.

######  Definition 6.2 (Duplication).

We define $\operatorname{Dup}_{A}^{S}$ the iso of type $A\leftrightarrow
A\otimes A$ which can duplicate any close value of type $A$ by induction on
$A$, where $S$ is a set of pairs of a type-variable $X$ and an iso-variable
$\phi$, such that for every free-variable $X\subseteq A$, there exists a pair
$(X,\phi)\in S$ for some $\phi$. The iso is defined by induction on $A$:
$\operatorname{Dup}_{\mathds{1}}^{S}=\\{()\leftrightarrow\langle(),()\rangle\\}$,
and

  * •

$\operatorname{Dup}_{A\otimes B}^{S}=\left\\{\begin{array}[]{lcl}\langle
x,y\rangle&\leftrightarrow&{\mathtt{let}}\,{\langle
x_{1},x_{2}\rangle}={\operatorname{Dup}_{A}^{S}\leavevmode\nobreak\
x}\leavevmode\nobreak\ {\mathtt{in}{}\nobreak\leavevmode}\\\\[5.0pt]
&&{\mathtt{let}}\,{\langle
y_{1},y_{2}\rangle}={\operatorname{Dup}_{B}^{S}\leavevmode\nobreak\
y}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\ {}\langle\langle
x_{1},y_{1}\rangle,\langle x_{2},y_{2}\rangle\rangle\end{array}\right\\}$;

  * •

$\operatorname{Dup}_{A\oplus
B}^{S}=\left\\{\begin{array}[]{lcl}\mathtt{inj}_{\ell}{\;(x)}&\leftrightarrow&{\mathtt{let}}\,{\langle
x_{1},x_{2}\rangle}={\operatorname{Dup}_{A}^{S}\leavevmode\nobreak\
x}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}\langle\mathtt{inj}_{\ell}{\;(x_{1})},\mathtt{inj}_{\ell}{\;(x_{2})}\rangle\\\\[5.0pt]
\mathtt{inj}_{r}{\;(y)}&\leftrightarrow&{\mathtt{let}}\,{\langle
y_{1},y_{2}\rangle}={\operatorname{Dup}_{B}^{S}\leavevmode\nobreak\
y}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}\langle\mathtt{inj}_{r}{\;(y_{1})},\mathtt{inj}_{r}{\;(y_{2})}\rangle\end{array}\right\\}$;

  * •

$\operatorname{Dup}_{\mu X.A}^{S}=\mathbf{fix}\leavevmode\nobreak\
\phi.\\{\mathtt{fold}{\;(x)}\leftrightarrow{\mathtt{let}}\,{\langle
x_{1},x_{2}\rangle}={Dup_{A[X\leftarrow\mu
X.A]}^{S^{\prime}}\leavevmode\nobreak\ x}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\
{\langle\mathtt{fold}{\;(x_{1})},\mathtt{fold}{\;(x_{2})}\rangle}\\}$

if $(X,\\_)\not\in S$ and where $S^{\prime}=S\cup\\{(X,\phi)\\}$;

  * •

$\operatorname{Dup}_{\mu X.A}^{S}=\\{x\leftrightarrow{\mathtt{let}}\,{\langle
x_{1},x_{2}\rangle}={\phi\leavevmode\nobreak\ x}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {\langle x_{1},x_{2}\rangle}\\}$ where
$(X,\phi)\in S$.

######  Lemma 6.3 (Properties of Duplication).

Given a closed type $A$, then $\operatorname{Dup}_{A}^{\emptyset}$ is well-
defined, and the iso $\operatorname{Dup}_{A}^{\emptyset}$ is well typed of
type $A\leftrightarrow A\otimes A$.∎

######  Lemma 6.4 (Semantics of Duplication).

Given a closed type $A$ and a closed value $v$ of type $A$, then
$\operatorname{Dup}_{A}^{\emptyset}\leavevmode\nobreak\ v\to^{*}\langle
v_{1},v_{2}\rangle$ and $v=v_{1}=v_{2}$; and
$\left\llbracket\vdash_{\omega}\operatorname{Dup}_{A}^{\emptyset}\colon
A\leftrightarrow A\otimes A\right\rrbracket=x\mapsto(x,x)$.∎

Now, given an iso $\omega:A\leftrightarrow B\otimes C$ and
$\omega^{\prime}:B\leftrightarrow A\otimes C^{\prime}$ where $C,C^{\prime}$
represent garbage, we can build an iso from $A\leftrightarrow B$ as follows
where the variables $x,y,z$ (and their indices) respectively correspond to the
first, second, and third wire of Figure 1:

######  Definition 6.5 (Garbage Removal Iso).

We defined $\operatorname{GarbRem}(\omega,\omega^{\prime})$ by
$\\{x_{1}\leavevmode\nobreak\ \leftrightarrow\leavevmode\nobreak\
{\mathtt{let}}\,{\langle x_{2},y\rangle}={\omega\leavevmode\nobreak\
x_{1}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}{\mathtt{let}}\,{\langle
x_{3},z\rangle}={\operatorname{Dup}_{B}^{\emptyset}\leavevmode\nobreak\
x_{2}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}{\mathtt{let}}\,{x_{4}}={\omega^{-1}\leavevmode\nobreak\ \langle
x_{3},y\rangle}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}{\mathtt{let}}\,{\langle
z_{2},y_{2}\rangle}={\omega^{\prime}\leavevmode\nobreak\
z}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}{\mathtt{let}}\,{z_{3}}={(\operatorname{Dup}_{B}^{\emptyset})^{-1}\leavevmode\nobreak\
\langle z_{2},x_{4}\rangle}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\
{}{\mathtt{let}}\,{z_{4}}={\omega^{\prime-1}\leavevmode\nobreak\ \langle
z_{3},y_{2}\rangle}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}z_{4}\\}$.

######  Lemma 6.6 (Garbage Removal is well-typed).

Given $\omega:A\leftrightarrow B\otimes C$ and
$\omega^{\prime}:B\leftrightarrow A\otimes C^{\prime}$ then
$\operatorname{GarbRem}(\omega,\omega^{\prime})$ is a well-typed iso of type
$A\leftrightarrow B$.∎

######  Lemma 6.7 (Garbage Removal Semantics).

Given $\omega:A\leftrightarrow B\otimes C$ and
$\omega^{\prime}:B\leftrightarrow A\otimes C^{\prime}$ and any well-typed
value $v$ of type $A$, such that if $\omega\leavevmode\nobreak\
v\to^{*}\langle v_{1},v_{2}\rangle$ and $\omega^{\prime}\leavevmode\nobreak\
v_{1}\to^{*}\langle v_{3},v_{4}\rangle$ then $v_{3}=v_{1}$, then if
$\operatorname{GarbRem}(\omega,\omega^{\prime})\leavevmode\nobreak\
v\to^{*}v_{5}$ then $v_{1}=v_{5}$. The denotational semantics
$\left\llbracket\omega,\omega^{\prime}\vdash_{\omega}\operatorname{GarbRem}(\omega,\omega^{\prime})\right\rrbracket(x)$
is $\left\llbracket\omega\right\rrbracket(x)$ if
$(\left\llbracket\omega^{\prime}\right\rrbracket((\left\llbracket\omega\right\rrbracket(x))_{1}))_{1}=x$
and $\bot$ otherwise.∎

###  6.3 Capturing every computable function

With this encoding, every iso $\omega:A\leftrightarrow B$ can be turned into
another iso
$\lfloor\omega\rfloor:[\operatorname{Enc}]\leftrightarrow[\operatorname{Enc}]$
by composing $\lfloor-\rfloor_{A}$, followed by $\omega$, followed by
$\lfloor-\rfloor_{B}^{-1}$. This is in particular the case for isos that are
the images of a Turing Machine. We are now ready to see how every computable
function $f$ from $\left\llbracket A\right\rrbracket\to\left\llbracket
B\right\rrbracket$ can be turned into an iso whose semantics is $f$. Given a
computable function $f:\left\llbracket A\right\rrbracket\to\left\llbracket
B\right\rrbracket$, call $M_{f}$ the RTM computing $f$. Since $f$ is in
$\mathbf{PInj}$, its output uniquely determines its input. Following [5],
there exists another Turing Machine $M_{f}^{\prime}$ which, given the output
of $M_{f}$ recovers the initial input. In our encoding of a RTM, the iso will
have another additional garbage which consist of a natural number, i.e. the
number of steps of the RTM $M_{f}$. Using
$\operatorname{GarbRem}(\operatorname{isos}(M_{f}),\operatorname{isos}(M_{f}^{\prime}))$
we can obtain a single iso, from the encoding of $A$ to the encoding of $B$,
without any garbage left. This also ensures that
$\left\llbracket\operatorname{GarbRem}(\operatorname{isos}(M_{f}),\operatorname{isos}(M_{f}^{\prime}))\right\rrbracket(x)=(\left\llbracket\operatorname{isos}(M_{f})\right\rrbracket(x))_{1}$,
for any input $x$.

######  Theorem 6.8 (Computable function as Iso).

Given a computable function $f\colon\left\llbracket
A\right\rrbracket\to\left\llbracket B\right\rrbracket$, let
$g\colon\left\llbracket[\operatorname{Enc}]\otimes[\operatorname{Enc}]\right\rrbracket\to\left\llbracket[\operatorname{Enc}]\otimes[\operatorname{Enc}]\right\rrbracket$
be defined as $g=\left\llbracket\lfloor-\rfloor_{B}\right\rrbracket\circ
f\circ\left\llbracket\lfloor-\rfloor_{A}^{-1}\right\rrbracket$, and let
$\omega\colon A\leftrightarrow B$ be defined as $\\{x\leavevmode\nobreak\
\leftrightarrow\leavevmode\nobreak\ {\mathtt{let}}\,{y}={\lfloor
x\rfloor_{A}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}{\mathtt{let}}\,{y^{\prime}}={\operatorname{GarbRem}(\operatorname{isos}(M_{g}),\operatorname{isos}(M_{g}^{\prime}))\leavevmode\nobreak\
y}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{}{\mathtt{let}}\,{z}={\lfloor y^{\prime}\rfloor_{B}^{-1}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {z}\\}$. Then
$\left\llbracket\omega\right\rrbracket=f$.∎

##  7 Conclusion

In this paper, we built upon the language presented in [8, 9, 36] in order to
represent any partial injective function which can manipulate inductive types.
We showed how one can encode any Reversible Turing Machine, hence the Turing
Completeness and we gave a denotational semantics based on join inverse rig
categories, together with a soundness and adequacy theorem. Most notably, we
showed that for any computable function $f$ from $\mathbf{PInj}$, there exists
an iso whose semantics is $f$, thus our language fully characterize all the
computable functions of $\mathbf{PInj}$.

## Acknowledgements

The authors thank Vladimir Zamdzhiev for his expert insight on specific parts
of the denotational semantics.

## References

  * [1] Samson Abramsky and Achim Jung.  Domain Theory, page 1–168.  Oxford University Press, Inc., USA, 1995.
  * [2] Holger Bock Axelsen and Robert Glück.  A simple and efficient universal reversible turing machine.  In Adrian-Horia Dediu, Shunsuke Inenaga, and Carlos Martín-Vide, editors, Language and Automata Theory and Applications, pages 117–128, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.  doi:10.1007/978-3-642-21254-3\\_8.
  * [3] Holger Bock Axelsen and Robin Kaarsgaard.  Join inverse categories as models of reversible recursion.  In Bart Jacobs and Christof Löding, editors, Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’16), volume 9634 of Lecture Notes in Computer Science, pages 73–90, Eindhoven, The Netherlands, 2016. Springer.  doi:10.1007/978-3-662-49630-5\\_5.
  * [4] Henk Barendregt.  ’the lambda calculus: its syntax and semantics’.  Studies in logic and the foundations of Mathematics, 1984.
  * [5] Charles H Bennett.  Logical reversibility of computation.  IBM Journal of Research and Development, 17(6):525–532, 1973.  doi:10.1147/rd.176.0525.
  * [6] Antoine Bérut, Artak Arakelyan, Artyom Petrosyan, Sergio Ciliberto, Raoul Dillenschneider, and Eric Lutz.  Experimental verification of landauer’s principle linking information and thermodynamics.  Nature, 483(7388):187–189, 2012.
  * [7] Kostia Chardonnet.  Towards a Curry-Howard Correspondence for Quantum Computation.  Theses, Université Paris-Saclay, January 2023.  URL: https://theses.hal.science/tel-03959403.
  * [8] Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron.  Categorical semantics of reversible pattern-matching.  Electronic Proceedings in Theoretical Computer Science, 351:18–33, Dec 2021.  URL: http://dx.doi.org/10.4204/EPTCS.351.2, doi:10.4204/eptcs.351.2.
  * [9] Kostia Chardonnet, Alexis Saurin, and Benoît Valiron.  A Curry-Howard correspondence for linear, reversible computation.  In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1–13:18, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  URL: https://drops.dagstuhl.de/opus/volltexte/2023/17474, doi:10.4230/LIPIcs.CSL.2023.13.
  * [10] J. Robin B. Cockett and Stephen Lack.  Restriction categories I: Categories of partial maps.  Theoretical Computer Science, 270(1):223–259, 2002.  doi:10.1016/S0304-3975(00)00382-0.
  * [11] J. Robin B. Cockett and Stephen Lack.  Restriction categories ii: partial map classification.  Theoretical Computer Science, 294(1):61–102, 2003.  doi:10.1016/S0304-3975(01)00245-6.
  * [12] Robin Cockett and Stephen Lack.  Restriction categories III: Colimits, partial limits and extensivity.  Mathematical Structures in Computer Science, 17(4):775–817, 2007\.  doi:10.1017/S0960129507006056.
  * [13] M.P. Fiore.  Axiomatic Domain Theory in Categories of Partial Maps.  Distinguished Dissertations in Computer Science. Cambridge University Press, 2004.  URL: https://books.google.co.uk/books?id=rsIAmbc2cIoC.
  * [14] Robert Glück and Robin Kaarsgaard.  A categorical foundation for structured reversible flowchart languages: Soundness and adequacy.  Log. Methods Comput. Sci., 14(3), 2018.  doi:10.23638/LMCS-14(3:16)2018.
  * [15] Robert Glück, Robin Kaarsgaard, and Tetsuo Yokoyama.  Reversible programs have reversible semantics.  In Emil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, and David Delmas, editors, Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II, volume 12233 of Lecture Notes in Computer Science, pages 413–427. Springer, 2019.  doi:10.1007/978-3-030-54997-8\\_26.
  * [16] Xiuzhan Guo.  Products, Joins, Meets, and Ranges in Restriction Categories.  PhD thesis, University of Calgary, 2012.  doi:10.11575/PRISM/4745.
  * [17] Chris Heunen, Robin Kaarsgaard, and Martti Karvonen.  Reversible effects as inverse arrows.  In Sam Staton, editor, Proceedings of the 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV), volume 341 of Electronic Notes in Theoretical Computer Science, pages 179–199, Dalhousie University, Halifax, Canada, 2018. Elsevier.  doi:10.1016/j.entcs.2018.11.009.
  * [18] Chris Heunen and Martti Karvonen.  Reversible monadic computing.  In Dan Ghica, editor, Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI), volume 319 of Electronic Notes in Theoretical Computer Science, pages 217–237, Nijmegen, The Netherlands, 2015.  doi:10.1016/j.entcs.2015.12.014.
  * [19] Petur Andrias Højgaard Jacobsen, Robin Kaarsgaard, and Michael Kirkedal Thomsen.  CoreFun : A typed functional reversible core language.  In Jarkko Kari and Irek Ulidowski, editors, Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14, 2018, Proceedings, volume 11106 of Lecture Notes in Computer Science, pages 304–321. Springer, 2018.  doi:10.1007/978-3-319-99498-7\\_21.
  * [20] Rosham P. James and Amr Sabry.  Theseus: A high-level language for reversible computing.  Draft, available at https://legacy.cs.indiana.edu/~sabry/papers/theseus.pdf, 2014.
  * [21] Xiaodong Jia, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev.  Commutative monads for probabilistic programming languages.  In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, jun 2021.  URL: https://doi.org/10.1109%2Flics52264.2021.9470611, doi:10.1109/lics52264.2021.9470611.
  * [22] Robin Kaarsgaard.  Condition/decision duality and the internal logic of extensive restriction categories.  In Barbara König, editor, Proceedings of the 35th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXV), volume 347 of Electronic Notes in Theoretical Computer Science, pages 179–202, London, UK, 2019.  doi:10.1016/j.entcs.2019.09.010.
  * [23] Robin Kaarsgaard.  Inversion, iteration, and the art of dual wielding.  In Michael Kirkedal Thomsen and Mathias Soeken, editors, Proceedings of the 11th International Conference on Reversible Computation (RC 2019), volume 11497 of Lecture Notes in Computer Science, pages 34–50, Lausanne, Switzerland, 2019. Springer.  doi:10.1007/978-3-030-21500-2\\_3.
  * [24] Robin Kaarsgaard, Holger Bock Axelsen, and Robert Glück.  Join inverse categories and reversible recursion.  Journal of Logical and Algebraic Methods in Programming, 87:33–50, 2017.  doi:10.1016/j.jlamp.2016.08.003.
  * [25] Robin Kaarsgaard and Mathys Rennela.  Join inverse rig categories for reversible functional programming, and beyond.  In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of Electronic Proceedings in Theoretical Computer Science, pages 152–167. Open Publishing Association, 2021.  doi:10.4204/EPTCS.351.10.
  * [26] Robin Kaarsgaard and Niccolò Veltri.  En garde! unguarded iteration for reversible computation in the delay monad.  In Graham Hutton, editor, Proceedings of the 13th International Conference on Mathematics of Program Construction (MPC 2019), volume 11825 of Lecture Notes in Computer Science, pages 366–384, Porto, Portugal, October 2019. Springer Verlag.  doi:10.1007/978-3-030-33636-3\\_13.
  * [27] J. Kastl.  Inverse categories.  In Algebraische Modelle, Kategorien und Gruppoide, Studien zur Algebra und ihre Anwendungen, Band 7, pages 51–60. Berlin, Akademie-Verlag, 1979.
  * [28] G.M Kelly.  Tensor products in categories.  Journal of Algebra, 2(1):15–37, 1965.  URL: https://www.sciencedirect.com/science/article/pii/0021869365900220, doi:https://doi.org/10.1016/0021-8693(65)90022-0.
  * [29] Max Kelly.  Basic concepts of enriched category theory, volume 64.  CUP Archive, 1982.
  * [30] Rolf Landauer.  Irreversibility and heat generation in the computing process.  IBM Journal of Research and Development., 5(3):183–191, 1961\.  doi:10.1147/rd.53.0183.
  * [31] Christopher Lutz.  Janus: a time-reversible language.  Letter to Rolf Landauer, posted online by Tetsuo Yokoyama on http://www.tetsuo.jp/ref/janus.html, 1986.
  * [32] Ian Mackie.  The geometry of interaction machine.  In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’95, pages 198–208. ACM Press, 1995\.  doi:10.1145/199448.199483.
  * [33] J.-M. Maranda.  Formal categories.  Canadian Journal of Mathematics, 17:758–801, 1965.  doi:10.4153/CJM-1965-076-0.
  * [34] Michael A. Nielsen and Isaac L. Chuang.  Quantum Computation and Quantum Information.  Cambridge University Press, 2002.
  * [35] Gordon D. Plotkin.  Lectures on predomains and partial functions.  Stanford University, 1985.
  * [36] Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto.  From symmetric pattern-matching to quantum control.  In Christel Baier and Ugo Dal Lago, editors, Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FOSSACS’18), volume 10803 of Lecture Notes in Computer Science, pages 348–364, Thessaloniki, Greece, 2018. Springer.  doi:10.1007/978-3-319-89366-2\\_19.
  * [37] Michael Kirkedal Thomsen and Holger Bock Axelsen.  Interpretation and programming of the reversible functional language RFUN.  In Ralf Lämmel, editor, Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, IFL 2015, Koblenz, Germany, September 14-16, 2015, pages 8:1–8:13. ACM, 2015\.  doi:10.1145/2897336.2897345.
  * [38] Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Glück.  Towards a reversible functional language.  In Alexis De Vos and Robert Wille, editors, Revised Papers of the Third International Workshop on Reversible Computation (RC’11), volume 7165 of Lecture Notes in Computer Science, pages 14–29, Gent, Belgium, 2012\. Springer.  doi:10.1007/978-3-642-29517-1\\_2.
  * [39] Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Glück.  Fundamentals of reversible flowchart languages.  Theoretical Computer Science, 611:87–115, 2016.  doi:10.1016/j.tcs.2015.07.046.
  * [40] Tetsuo Yokoyama and Robert Glück.  A reversible programming language and its invertible self-interpreter.  In G. Ramalingam and Eelco Visser, editors, Proceedings of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2007, Nice, France, January 15-16, 2007, pages 144–153, 2007.  doi:10.1145/1244381.1244404.

##  Appendix A Proof of Section 2

The matching predicate, written $\sigma[v]=v^{\prime}$ is defined in Table 5,
and one can see that $\sigma[v]=v^{\prime}$ if and only if
$\sigma(v)=v^{\prime}$.

$\sigma[x]=e\sigma=\\{x\mapsto
e\\}\quad\sigma[\mathtt{inj}_{\ell}{\;(e)}]=\mathtt{inj}_{\ell}{\;(e^{\prime})}\sigma[e]=e^{\prime}\quad\sigma[\mathtt{inj}_{r}{\;(e)}]=\mathtt{inj}_{r}{\;(e^{\prime})}\sigma[e]=e^{\prime}\quad\sigma[\mathtt{fold}{\;(e)}]=\mathtt{fold}{\;(e^{\prime})}\sigma[e]=e^{\prime}$

$\sigma[\langle e_{1},e_{2}\rangle]=\langle
e^{\prime}_{1},e^{\prime}_{2}\rangle\sigma_{1}[e_{1}]=e^{\prime}_{1}&\sigma_{2}[e_{2}]=e^{\prime}_{2}\text{supp}(\sigma_{1})\cap\text{supp}(\sigma_{2})=\emptyset\sigma=\sigma_{1}\cup\sigma_{2}\quad\sigma[()]=()$

Table 5: Pattern-matching.

We can first show that two different orthogonal values cannot match a same
value:

######  Lemma A.1.

Given $S$, a finite set of values of type $A$ such that for all
$v_{1},v_{2}\in S,v_{1}\bot v_{2}$, and a value $v$ of type $A$, if there
exists $v_{1},v_{2}\in S$ and $\sigma_{1},\sigma_{2}$ such that
$\sigma_{1}(v_{1})=v$ and $\sigma_{2}(v_{2})=v$ then $v_{1}=v_{2}$.∎

######  Proof A.2 (Proof of Lemma A.1).

By induction on $\sigma_{1}[v_{1}]=v$

  * •

Case $\sigma_{1}[x]=v$: There is no value $v_{2}$ such that $v_{2}\bot x$,
hence $S=\\{x\\}$ so $v_{2}=x$.

  * •

Case $\sigma_{1}[()]=()$: Similarly.

  * •

Case
$\sigma_{1}[\mathtt{inj}_{\ell}{\;v_{1}^{\prime}}]=\mathtt{inj}_{\ell}{\;v^{\prime}}$:
By definition of the pattern-matching we have
$\sigma_{1}[v_{1}^{\prime}]=v^{\prime}$. The only possible value for $v_{2}$
is then $\mathtt{inj}_{\ell}{\;v_{2}^{\prime}}$. By IH we get
$v_{1}^{\prime}=v_{2}^{\prime}$ hence $v_{1}=v_{2}$.

  * •

The case for $\mathtt{inj}_{r}{\;v_{1}}$ and $\mathtt{fold}{\;v_{1}}$ are
similar.

  * •

Case for $\sigma[\langle v_{1}^{1},v_{1}^{2}\rangle]=\langle
v^{1},v^{2}\rangle$: By definition of the pattern-matching we have
$\sigma_{1}[v_{1}^{1}]=v^{1}$ and $\sigma_{2}[v_{1}^{2}]=v^{2}$. By
orthogonality, we have that $v_{2}=\langle v_{2}^{1},v_{2}^{2}\rangle$ and
therefore by IH $v_{1}^{1}=v_{2}^{1}$ and $v_{1}^{2}=v_{2}^{2}$ so
$v_{1}=v_{2}$.

######  Proof A.3 (Proof of Lemma 2.2).

By induction on $\omega$.

  * •

$\omega=\phi:\alpha$. Therefore $\Psi=\phi:\alpha\cup\Psi^{\prime}$ for some
$\Psi^{\prime}$. Then $\Psi^{-1}=\phi:\alpha^{-1}\cup\Psi^{\prime-1}$ and
$\omega^{-1}=\phi:\alpha^{-1}$.

  * •

If $\omega=\omega_{1}\leavevmode\nobreak\ \omega_{2}$, in this case we get
$\omega_{1}$ is of type $(A\leftrightarrow B)\to\alpha$ while $\omega_{2}$ is
of type $A\leftrightarrow B$. Since $(\omega_{1}\leavevmode\nobreak\
\omega_{2})^{-1}=\omega_{1}^{-1}\leavevmode\nobreak\ \omega_{2}^{-1}$ we get
that $\omega_{1}^{-1}:(B\leftrightarrow A)\to\alpha^{-1}$ and
$\omega_{2}:B\leftrightarrow A$ which can be proved by induction hypothesis as
the context $\Psi$ is duplicated on both premises.

  * •

If $\omega=\mathbf{fix}\leavevmode\nobreak\
\phi.\omega^{\prime}:(A_{i}\leftrightarrow B_{i})_{i\in I}\to(A\leftrightarrow
B)$, then we obtain

$\Psi\vdash_{\omega}\mathbf{fix}\leavevmode\nobreak\
\phi.\omega^{\prime}:(A_{i}\leftrightarrow B_{i})_{i\in I}\to(A\leftrightarrow
B)\Psi,\phi:A\leftrightarrow
B\vdash_{\omega}\omega^{\prime}:(A_{i}\leftrightarrow B_{i})_{i\in I}$.

By definition we get

$\Psi^{-1}\vdash_{\omega}\mathbf{fix}\leavevmode\nobreak\
\phi.\omega^{\prime-1}:(B_{i}\leftrightarrow A_{i})_{i\in
I}\to(B\leftrightarrow A)\Psi^{-1},\phi:B\leftrightarrow
A\vdash_{\omega}\omega^{\prime-1}:(B_{i}\leftrightarrow A_{i})_{i\in
I}\to(B\leftrightarrow A)$ which can then be proved by induction hypothesis.

  * •

If $\omega=\lambda\phi.\omega^{\prime}$, is similar.

  * •

If $\omega=\\{v_{1}\leftrightarrow e_{1}\mid\dots\mid v_{n}\leftrightarrow
e_{n}\\}$, is direct as the typing contexts stays the same for the values and
expressions and $OD$ is trivially preserved and by induction hypothesis on all
isos subterms of $\omega$

######  Proof A.4 (Proof of Lemma 2.3).

By a direct induction on $\to$, there is only two possible rewriting rule for
an iso: either it is $(\lambda\psi.\omega_{1})\omega_{2}$ which rewrites to
$\omega_{1}[\psi\leftarrow\omega_{2}]$ and whose inverse
$(\lambda\psi.\omega_{1}^{-1})\omega_{2}^{-1}$ rewrites to
$\omega_{1}^{-1}[\psi\leftarrow\omega_{2}^{-1}]$. The case where the iso is of
the shape $\mathbf{fix}\leavevmode\nobreak\ \phi.\omega$ is also direct. All
the congruence case are handled by induction hypothesis.

######  Lemma A.5 (Commutativity of substitution [9]).

Let $\sigma_{1},\sigma_{2}$ and $v$, such that $\sigma_{1}\cup\sigma_{2}$
closes $v$ and
$\mathtt{supp}(\sigma_{1})\cap\mathtt{supp}(\sigma_{2})=\emptyset$ then
$\sigma_{1}(\sigma_{2}(v))=\sigma_{2}(\sigma_{1}(v))$

######  Proof A.6.

Direct by induction on $v$ as $\sigma_{1}$ and $\sigma_{2}$ have disjoint
support: In the case where $v=x$ then either $\\{x\mapsto
v^{\prime}\\}\in\sigma_{1}$ or $\\{x\mapsto v^{\prime}\\}\in\sigma_{2}$ and
hence $\sigma_{1}(\sigma_{2}(x))=v^{\prime}=\sigma_{2}(\sigma_{1}(x))$. All
the other case are by direct induction hypothesis as the substitutions enter
the subterms.

######  Proof A.7 (Proof of Theorem 2.4).

Without lost of generality we only consider the case where $\omega$ is a set
of clauses, then by induction hypothesis on the size of $\omega$:

  * •

Case where $\omega=\\{v_{1}\leftrightarrow v_{1}\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \dots\leavevmode\nobreak\ \mid\leavevmode\nobreak\
v_{n}\leftrightarrow v_{n}^{\prime}\\}$ then
$\omega^{-1}(\omega\leavevmode\nobreak\ v_{0})$, by non-overlapping and the
fact that the whole term reduce to a value, there exists a $v_{i}$ such that
$\sigma[v_{i}]=v_{0}$ and hence the term reduces to
$\omega^{-1}\sigma(v_{i}^{\prime})$. It is clear that
$\sigma[v_{i}^{\prime}]=\sigma(v_{i})$ and hence the terms reduces to
$\sigma(v_{i})$, but by the first pattern-matching we know that
$\sigma(v_{i})=v_{0}$, which concludes the case.

  * •

Case where $\omega=\\{v_{1}\leftrightarrow e_{1}\mid\dots\mid
v_{n}\leftrightarrow e_{n}\\}$,

for simplicity of writing we write a single clause:

$\begin{array}[]{c}\left(\begin{array}[]{l@{~}c@{~}l}v_{1}\hfil\leavevmode\nobreak\
&{\leftrightarrow}\hfil\leavevmode\nobreak\
&{\mathtt{let}}\,{p_{1}}={\omega_{1}\leavevmode\nobreak\
p_{1}^{\prime}}\leavevmode\nobreak\ {\mathtt{in}{}\nobreak\leavevmode}\\\
\hfil\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\ &\cdots\\\
\hfil\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\
&{\mathtt{let}}\,{p_{n}}={\omega_{n}\leavevmode\nobreak\
p^{\prime}_{n}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{v^{\prime}_{1}}\end{array}\right)^{-1}:=\left(\begin{array}[]{lcl@{}l@{}l}v^{\prime}_{1}&{\leftrightarrow}&{\mathtt{let}}\,{p^{\prime}_{n}}={\omega_{n}^{-1}\leavevmode\nobreak\
p_{n}}\leavevmode\nobreak\ {\mathtt{in}{}\nobreak\leavevmode}\\\ &&\cdots\\\
&&{\mathtt{let}}\,{p^{\prime}_{1}}={\omega_{1}^{-1}\leavevmode\nobreak\
p_{1}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{v_{1}}\end{array}\right).\end{array}$

Take some closed value $\vdash_{e}v_{0}:A$ such that $\sigma[v_{1}]=v_{0}$.

By linearity, we can decompose $\sigma$ into
$\sigma_{1},\dots,\sigma_{n},\sigma_{n+1}$ such that, after substitution we
obtain

${\mathtt{let}}\,{p_{1}}={\omega_{1}\,\sigma_{1}(p^{\prime}_{1})}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\
{}\dots\mathtt{let}\,{p_{n}}={\omega_{n}\,\sigma_{n}(p^{\prime}_{n})}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {}\sigma_{n+1}(v_{1}^{\prime})$

Given By our hypothesis that the whole term reduces to a value, we know that
each $\mathtt{let}$ construction will reduce, and by the rewriting strategy we
get:

$\begin{array}[]{c}{\mathtt{let}}\,{p_{1}}={\omega_{1}\,\sigma_{1}(p^{\prime}_{1})}\leavevmode\nobreak\
{\mathtt{in}{}\nobreak\leavevmode}\\\ \dots\\\
{\mathtt{let}}\,{p_{n}}={\omega_{n}\,\sigma_{n}(p^{\prime}_{n})}\leavevmode\nobreak\
{\mathtt{in}{}\nobreak\leavevmode}\\\
\sigma_{n+1}(v_{1}^{\prime})\end{array}\to\begin{array}[]{c}{\mathtt{let}}\,{p_{1}}={\overline{v_{1}}}\leavevmode\nobreak\
{\mathtt{in}{}\nobreak\leavevmode}\\\ \dots\\\
{\mathtt{let}}\,{p_{n}}={\omega_{n}\,\sigma_{n}(p^{\prime}_{n})}\leavevmode\nobreak\
{\mathtt{in}{}\nobreak\leavevmode}\\\
\sigma_{n+1}(v_{1}^{\prime})\end{array}\to\begin{array}[]{c}{\mathtt{let}}\,{p_{2}}={\omega_{2}\,\gamma_{1}^{2}(\sigma_{1}(p^{\prime}_{1}))}\leavevmode\nobreak\
{\mathtt{in}{}\nobreak\leavevmode}\\\ \dots\\\
{\mathtt{let}}\,{p_{n}}={\omega_{n}\,\gamma_{1}^{n}(\sigma_{n}(p^{\prime}_{n}))}\leavevmode\nobreak\
{\mathtt{in}{}\nobreak\leavevmode}\\\ \sigma_{n+1}(v_{1}^{\prime})\end{array}$

The final term reduces to
$\gamma_{n}^{n}(\dots(\gamma_{1}^{n}(\sigma_{n+1}(v_{1}^{\prime})))\dots)$ and
creates a new substitution $\gamma_{i}$, the term will hence reduce to
$\gamma_{n}(\dots(\gamma_{1}(\sigma_{n+1}(v_{1}^{\prime})))\dots)$. Let
$\delta=\cup_{i}\gamma_{i}\cup\sigma_{n+1}$

We are left to evaluate

$\left(\begin{array}[]{lcl@{}l@{}l}v_{1}^{\prime}&{\leftrightarrow}&{\mathtt{let}}\,{p^{\prime}_{n}}={\omega_{n}^{-1}\leavevmode\nobreak\
p_{n}}\leavevmode\nobreak\ {\mathtt{in}{}\nobreak\leavevmode}\\\ &&\cdots\\\
&&{\mathtt{let}}\,{p^{\prime}_{1}}={\omega_{1}^{-1}\leavevmode\nobreak\
p_{1}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{v_{1}}\end{array}\right)\leavevmode\nobreak\ \delta(v_{1}^{\prime})$

We get $\delta[v_{1}^{\prime}]=\delta(v_{1}^{\prime})$.

We know that each $\gamma_{i}$ closes only $p_{i}$, we can therefore
substitute the term as:

${\mathtt{let}}\,{p_{n}^{\prime}}={\omega_{n}\leavevmode\nobreak\
\gamma_{n}(p_{n})}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{\dots}{\mathtt{let}}\,{p_{1}^{\prime}}={\omega_{1}\gamma_{1}(p_{1})}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {\sigma_{n+1}(v_{1}^{\prime})}$

By induction hypothesis, Each $\mathtt{let}$ clause will re-create the
substitution $\sigma_{i}$, we know this as the fact that the initial
$\mathtt{let}$ construction,
${\mathtt{let}}\,{p_{i}}={\omega_{i}\leavevmode\nobreak\
\sigma_{i}(p_{i}^{\prime})}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {\dots}$ reduces to
${\mathtt{let}}\,{p_{i}}={v_{i}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {\dots}$ While the new one,
${\mathtt{let}}\,{p_{i}^{\prime}}={\omega^{-1}\gamma_{i}(p_{i})}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {\dots}$, is, by definition of the
substitution the same as
${\mathtt{let}}\,{p_{i}^{\prime}}={\omega^{-1}v_{i}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {\dots}$

Then, since we know that $v_{i}$ is the result of $\omega\leavevmode\nobreak\
\sigma_{i}(p_{i}^{\prime})$, we get by induction hypothesis
$\sigma(p_{i}^{\prime})$ as the result of the evaluation.

Therefore, after rewriting we obtain:
$\sigma_{n}(\dots(\sigma_{1}(\sigma_{n+1}(v_{1}^{\prime})))\dots)$. By Lemma
A.5 we get $\sigma_{1}(\dots(\sigma_{n}(\sigma_{n+1}(v_{1}^{\prime})))\dots)$
which is equal to $v$.

######  Lemma A.8 (Substitution Lemma of variables).

  * •

For all values $v_{1},\dots,v_{n}$, types $A_{1},\dots,A_{n}$ and context
$\Delta_{1},\dots,\Delta_{n}$ such that for
$i\in\\{1,\dots,n\\},\Delta_{i}\vdash_{e}v_{i}:A_{i}$.

  * •

For all term $t$, type $B$ and context $\Gamma$ and variables
$x_{1},\dots,x_{n}\in{\mathtt{FV}}(t)$ such that
$\Gamma,x_{1}:A_{1},\dots,x_{n}:A_{n}\vdash_{e}t:B$

Let $\sigma=\\{x_{1}\mapsto v_{1},\dots,x_{n}\mapsto v_{n}\\}$ then
$\Gamma,\Delta_{1},\dots,\Delta_{n}\vdash_{e}\sigma(t):B$

######  Proof A.9 (Proof of Lemma A.8).

By induction on $t$.

  * •

Case $x$, then $\Gamma=\emptyset$ and we have $\sigma=\\{x\mapsto v\\}$ for
some $v$ of type $B$ under some context $\Delta$, then we get
$\Delta\vdash_{e}\sigma(x):B$ which leads to $\Delta\vdash_{e}v:B$ which is
typable by our hypothesis.

  * •

Case $()$, nothing to do.

  * •

Case $\mathtt{inj}_{\ell}{\;t^{\prime}}$, by substitution we have
$\sigma(\mathtt{inj}_{\ell}{\;t^{\prime}})=\mathtt{inj}_{\ell}{\;\sigma(t^{\prime})}$
and by typing we get

$\Gamma,\Delta_{1},\dots,\Delta_{n}\vdash\mathtt{inj}_{\ell}{\;\sigma(t^{\prime})}\Gamma,\Delta_{1},\dots,\Delta_{n}\vdash\sigma(t^{\prime})$
which is typable by induction hypothesis on $t^{\prime}$.

  * •

Case
$\mathtt{inj}_{r}{\;t^{\prime}},\mathtt{fold}{\;t^{\prime}},\omega\leavevmode\nobreak\
t^{\prime}$ are similar.

  * •

Case $\langle t_{1},t_{2}\rangle$, by typing we get that we can split $\Gamma$
into $\Gamma_{1},\Gamma_{2}$ and the variables $x_{1},\dots,x_{n}$ are split
into two parts for typing both $t_{1}$ or $t_{2}$ depending on whenever or not
a variable occurs freely in $t_{1}$ or $t_{2}$, w.l.o.g. say that
$x_{1},\dots,x_{l}$ are free in $t_{1}$ and $x_{l+1},\dots,x_{n}$ are free in
$t_{2}$ then we get:

$\Gamma_{1},\Gamma_{2},x_{1}:A_{1},\dots,x_{l}:A_{l},x_{l+1}:A_{l+1},\dots,x_{n}:A_{n}\vdash_{e}\langle
t_{1},t_{2}\rangle:B_{1}\otimes
B_{2}\Gamma_{1},x_{1}:A_{1},\dots,x_{l}:A_{l}\vdash_{e}t_{1}:B_{1}\qquad\Gamma_{2},x_{l+1}:A_{l+1},\dots,x_{n}:A_{n}\vdash_{e}t_{2}:B_{2}$

By substitution we get that $\sigma(\langle
t_{1},t_{2}\rangle)=\langle\sigma(t_{1}),\sigma(t_{2})\rangle$ so we get the
following typing derivation which is completed by induction hypothesis on the
subterms:

$\Gamma_{1},\Gamma_{2},\Delta_{1},\dots,\Delta_{l},\Delta_{l+1},\dots,\Delta_{n}\vdash_{e}\langle
t_{1},t_{2}\rangle:B_{1}\otimes
B_{2}\Gamma_{1},\Delta_{1},\dots,\Delta_{l}\vdash_{e}t_{1}:B_{1}\qquad\Gamma_{2},\Delta_{l+1},\dots,\Delta_{n}\vdash_{e}t_{2}:B_{2}$

  * •

Case ${\mathtt{let}}\,{p}={t_{1}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {t_{2}}$ Similar to the case of the tensor.

######  Lemma A.10 (Substitution Lemma Of Isos).

If :

  * •

$\Psi,\phi:\alpha\Vdash\Delta\vdash_{e}t:A$

  * •

$\Psi^{\prime}\vdash_{\omega}\omega:\alpha$

Then $\Psi,\Psi^{\prime}\Vdash\Delta\vdash_{e}t[\phi\leftarrow\omega]:A$.

If :

  * •

$\Psi,\phi:\alpha\vdash_{\omega}\omega_{1}:\beta$

  * •

$\Psi^{\prime}\vdash_{\omega}\omega_{2}:\alpha$

Then
$\Psi,\Psi^{\prime}\vdash_{\omega}\omega_{1}[\phi\leftarrow\omega_{2}]:\beta$.

######  Proof A.11 (Proof of Lemma A.10).

We prove those two propositions by mutual induction on $t$ and $\omega_{1}$.

Terms, by induction on $t$.

  * •

If $t=x$ or $t=()$ then there is nothing to do.

  * •

If $t=\mathtt{inj}_{\ell}{\;t^{\prime}}$ or $\mathtt{inj}_{r}{\;t^{\prime}}$
or $\mathtt{fold}{\;t^{\prime}}$ or $\langle t_{1},t_{2}\rangle$ or
${\mathtt{let}}\,{p}={t_{1}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {t_{2}}$, then similarly to the proof of
Lemma A.8 the substitution goes to the subterms and we can apply the induction
hypothesis.

  * •

If $t=\omega^{\prime}\leavevmode\nobreak\ t^{\prime}$. In that case, the
substitution goes to both subterms:
$t[f\leftarrow\omega]=(\omega^{\prime}[f\leftarrow\omega])\leavevmode\nobreak\
(t^{\prime}[f\leftarrow\omega])$ and by induction hypothesis on $t^{\prime}$
and by the mutually recursive proof.

Isos, by induction on $\omega_{1}$.

  * •

If $\omega_{1}=\phi$, then we get
$\Psi,\Psi^{\prime}\vdash_{\omega}\phi[\phi\leftarrow\omega_{2}]:\alpha$ which
is typable by hypothesis.

  * •

If $\omega_{1}=\phi^{\prime}\not=\phi$ is impossible by our typing hypothesis.

  * •

If $\omega_{1}=\mathbf{fix}\leavevmode\nobreak\ \phi^{\prime}.\omega$, then by
straightforward induction hypothesis on $\omega$.

  * •

If $\omega_{1}=\lambda\phi^{\prime}.\omega$, then by straightforward induction
hypothesis on $\omega$.

  * •

If $\omega_{1}=\\{v_{1}\leftrightarrow e_{1}\mid\dots\mid v_{n}\leftrightarrow
e_{n}\\}$, then, by definition of the substitution we have that

$\displaystyle\\{v_{1}\leftrightarrow e_{1}\mid\dots\mid v_{n}\leftrightarrow
e_{n}\\}[f\leftarrow\omega_{2}]$ $\displaystyle=\\{v_{1}\leftrightarrow
e_{1}[f\leftarrow\omega_{2}]\leavevmode\nobreak\ \mid\leavevmode\nobreak\
\dots\leavevmode\nobreak\ \mid\leavevmode\nobreak\
v_{n}[f\leftarrow\omega_{2}]\leftrightarrow e_{n}[f\leftarrow\omega_{2}]\\}$

in which case we apply the substitution lemma of isos on terms.

######  Proof A.12 (Proof of Lemma 2.1).

By induction on $t\to t^{\prime}$ and direct by Lemma A.8 and Lemma A.10

##  Appendix B Proof of Section 3

######  Proof B.1 (Proof of Lemma 3.11).

By analysis on $M\vdash C\rightsquigarrow C^{\prime}$: Given the configuration
$(q,(l,s,r))$ where $l,r$ are the tapes and $s$ the letter pointed by the head
of the RTM. We have $\operatorname{isos}(C)=(q^{T},(l^{T},s^{T}::r^{T}))$.

We then consider the two possible kind of rule:

  * •

Considering a rule $(q,(s,s^{\prime}),q^{\prime})$, by definition this
correspond to the clause
$(q^{T}),(x_{1},s^{T}::x_{2})\leftrightarrow(q^{\prime T},(x_{1},s^{\prime
T}::x_{2}))$, where $x_{1},x_{2}$ are variables. By pattern matching we have
that the first element of each pair matches since they are equal, and closed
values. Then, by pattern-matching, $l^{T}$ and $r^{T}$ matches respectively
$x_{1}$ and $x_{2}$ and $s^{T}$ matches with $s^{T}$ as they are equal closed
values. Thus, the term reduces to $\sigma((q^{\prime T},(x_{1},s^{\prime
T}::x_{2})))$ with $\sigma=\\{x_{1}\mapsto l^{T},x_{2}\mapsto r^{T}\\}$ which
is equal to $(q^{\prime T},(l^{T},s^{\prime
T}::s^{T}))=\operatorname{isos}(C^{\prime})$

  * •

Considering a rule $(q,d,q^{\prime})$ for
$d\in\\{\leftarrow,\downarrow,\rightarrow\\}$, suppose $d=\leftarrow$ (the
other case being similar), we get the corresponding clause
$(q^{T},(x_{1},y::x_{2}))\leftrightarrow(q^{\prime T},(y::x_{1},x_{2}))$,
which, as previously will match with $\sigma=\\{x_{1}\mapsto
l^{T},x_{2}\mapsto r^{T},y\mapsto s^{T}\\}$ and reduce to $\sigma((q^{\prime
T},(y::x_{1},x_{2})))=(q^{T},(s^{T}::l^{T},r^{T}))=\operatorname{isos}(C^{\prime})$.

######  Proof B.2 (Proof of Lemma 3.13).

By induction on $n$.

  * •

$0$, Our hypothesis state that:

$\displaystyle(\operatorname{It}\leavevmode\nobreak\
\omega)\leavevmode\nobreak\ v$
$\displaystyle\to{\mathtt{let}}\,{y}={\omega\leavevmode\nobreak\
v}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{{\mathtt{let}}\,{z}={\omega_{\operatorname{aux}}\leavevmode\nobreak\
y}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\ {z}}$
$\displaystyle\to{\mathtt{let}}\,{z}={\omega_{\operatorname{aux}}\leavevmode\nobreak\
(v^{\prime},\mathtt{f}\\!\mathtt{f})}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {z}$ $\displaystyle\to(v^{\prime},0)$

Therefore: $\omega\leavevmode\nobreak\
v\to(v^{\prime},\mathtt{f}\\!\mathtt{f})$.

  * •

$n+1$: Our hypothesis state that:

$\displaystyle(\operatorname{It}\leavevmode\nobreak\
\omega)\leavevmode\nobreak\ v$
$\displaystyle\to{\mathtt{let}}\,{y}={\omega\leavevmode\nobreak\
v}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{({\mathtt{let}}\,{z}={\omega_{\operatorname{aux}}\leavevmode\nobreak\
y}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\ {z})}$
$\displaystyle\to{\mathtt{let}}\,{z}={\omega_{\operatorname{aux}}\leavevmode\nobreak\
(v_{1},\mathtt{t}\\!\mathtt{t})}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {z}$
$\displaystyle\equiv{\mathtt{let}}\,{z}={\left\\{\begin{array}[]{l@{~}c@{~}l}(y,\mathtt{t}\\!\mathtt{t})\hfil\leavevmode\nobreak\
&\leftrightarrow\hfil\leavevmode\nobreak\
&{\mathtt{let}}\,{(z,n)}={\operatorname{It}(\omega)\leavevmode\nobreak\
y}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{(z,S\leavevmode\nobreak\ n)}\\\
(y,\mathtt{f}\\!\mathtt{f})\hfil\leavevmode\nobreak\
&\leftrightarrow\hfil\leavevmode\nobreak\ &(y,S\leavevmode\nobreak\
0)\end{array}\right\\}\leavevmode\nobreak\
(v_{1},\mathtt{t}\\!\mathtt{t})}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {z}$
$\displaystyle\to{\mathtt{let}}\,{y}={({\mathtt{let}}\,{(z,n)}={\operatorname{It}\leavevmode\nobreak\
v_{1}}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{(z,S\leavevmode\nobreak\ n)})}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {y}$

Then we know that $\operatorname{It}\leavevmode\nobreak\ v_{1}$ will reduce to
some $v^{\prime},n$ and so by IH we get that
$\underbrace{\omega\leavevmode\nobreak\ \dots\leavevmode\nobreak\
\omega}_{n+1\text{ times}}\leavevmode\nobreak\
v_{1}\to^{*}(v^{\prime},\mathtt{f}\\!\mathtt{f})$, so we get
$\underbrace{\omega\leavevmode\nobreak\ \dots\leavevmode\nobreak\
\omega}_{n+2\text{ times}}\leavevmode\nobreak\
v\to^{*}(v^{\prime},\mathtt{f}\\!\mathtt{f})$.

##  Appendix C Proof of Theorem 5.8

$\begin{array}[]{c}\Theta\vDash\mathds{1}\qquad\Theta,X\vDash
X\qquad\Theta\vDash\mu X.A\Theta,X\vDash A\qquad\Theta\vDash A\star
B\Theta\vDash A\hfil\lx@intercol&\Theta\vDash B\end{array}$ Table 6: Formation
rules for types.

######  Lemma C.1.

Given $\sigma[p]=v$ and the judgement $\Psi\Vdash\Delta,p:A\vdash t:B$ is
valid, then $\left\llbracket\sigma(t)\right\rrbracket(\gamma)=\left\llbracket
t\right\rrbracket(\gamma)\circ(Id\otimes\left\llbracket v\right\rrbracket)$.
In other words, $\left\llbracket{\mathtt{let}}\,{p}={v}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\
{t}\right\rrbracket=\left\llbracket\sigma(t)\right\rrbracket$ when
$\sigma[p]=v$.

######  Proof C.2 (Proof of Lemma 5.7).

This is proven by induction on the number of reductions and then on all the
possible reductions.

  * •

The cases for injections, pairs and compositions are straightforward.

  * •

${\mathtt{let}}\,{p}={t_{1}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\
{t^{\prime}}\to{\mathtt{let}}\,{p}={t_{2}}\leavevmode\nobreak\
{\mathtt{in}}\leavevmode\nobreak\ {t^{\prime}}$ simply corresponds to
precomposition in the denotational semantics, the result is then
straightforward.

  * •

${\mathtt{let}}\,{p}={v}\leavevmode\nobreak\ {\mathtt{in}}\leavevmode\nobreak\
{t}\to\sigma(t)$ is handled by the previous lemma.

  * •

$\\{v_{1}\leftrightarrow e_{1}\mid\dots\mid v_{n}\leftrightarrow
e_{n}\\}v^{\prime}\to\sigma(e_{i})$.

$\left\llbracket\\{v_{1}\leftrightarrow e_{1}\mid\dots\mid
v_{n}\leftrightarrow
e_{n}\\}v^{\prime}\right\rrbracket=\left(\bigvee_{j}\left\llbracket
e_{j}\right\rrbracket\left\llbracket
v_{j}\right\rrbracket\right)\left\llbracket v^{\prime}\right\rrbracket$

where $v^{\prime}$ is orthogonal to all $v_{j}$ except $v_{j}$, thus

$\left\llbracket\\{v_{1}\leftrightarrow e_{1}\mid\dots\mid
v_{n}\leftrightarrow e_{n}\\}v^{\prime}\right\rrbracket=\left\llbracket
e_{i}\right\rrbracket\left\llbracket v_{i}\right\rrbracket\left\llbracket
v^{\prime}\right\rrbracket,$

and this is equal to $\left\llbracket\sigma(e_{i})\right\rrbracket$ by
induction on $v^{\prime}$.

This proves soundness.

######  Corollary C.3.

If $t\downarrow$, then $\left\llbracket t\right\rrbracket\neq 0$.

######  Proof C.4.

It is required here that values are not interpreted as a $0$ morphism.
Hopefully, this has been assumed thanks to $0\neq 1$.

Adequacy is obtained with the introduction of formal approximation relations.
First we define a new notation: given morphisms $f_{1}:1\to
A_{1},\ldots,f_{n}:1\to A_{n}$, we write
$\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\ldots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}$
for the morphism

$\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\ldots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}:=\left(1\xrightarrow{\cong}1\otimes\cdots\otimes
1\xrightarrow{f_{1}\otimes\cdots\otimes f_{n}}A_{1}\otimes\cdots\otimes
A_{n}\right).$

For example,
${\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},f_{2}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}=(f_{1}\otimes
f_{2})\circ\lambda_{1}^{-1}}$.

######  Definition C.5.

We introduce two relations, given a closed type $A$:

$\displaystyle\trianglelefteq_{A}$
$\displaystyle\subseteq\left(\mathcal{C}(1,\left\llbracket
A\right\rrbracket)\setminus\\{\bot\\}\right)\times\text{ExtVal}(A)$
$\displaystyle\sqsubseteq_{A}$
$\displaystyle\subseteq\mathcal{C}(1,\left\llbracket
A\right\rrbracket)\times\text{Terms}(A)$

They are defined as follows:

  * •

$f\trianglelefteq_{A\oplus B}\mathtt{inj}_{\ell}{\;v}$ iff there exists
$f^{\prime}$ st. $f=\iota_{A}\circ f^{\prime}$ and
$f^{\prime}\trianglelefteq_{A}v$;

  * •

$f\trianglelefteq_{A\oplus B}\mathtt{inj}_{r}{\;v}$ iff there exists
$f^{\prime}$ st. $f=\iota_{B}\circ f^{\prime}$ and
$f^{\prime}\trianglelefteq_{B}v$;

  * •

$f\trianglelefteq_{A\otimes B}\langle v,v^{\prime}\rangle$ iff there exists
$f^{\prime},f^{\prime\prime}$ st.
$f=\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f^{\prime},f^{\prime\prime}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}$
and $f^{\prime}\trianglelefteq_{A}v$,
$f^{\prime\prime}\trianglelefteq_{B}v^{\prime}$;

  * •

$f\trianglelefteq_{\mu X.A}\mathtt{fold}{\;v}$ iff $\alpha^{-1}\circ
f\trianglelefteq_{A[x\rightarrow\mu X.A]}v$;

  * •

$f\sqsubseteq_{A}t$ iff, when $f\neq\bot$, there exists $v\in\text{Val}(A)$
st. $t\to^{*}v$ and $f\trianglelefteq_{A}v$.

The existence of the relation is ensured by induction on the values.

######  Lemma C.6.

Given $\Delta\vdash t\colon A$, with $\Delta=x_{1}\colon
A_{1},\dots,x_{n}\colon A_{n}$, given for all $n$,
$f_{i}\trianglelefteq_{A_{i}}v_{i}$ and given $\\{x_{i}\mapsto
v_{i}\\}\subseteq\sigma$, we have:

$\left\llbracket
t\right\rrbracket\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\dots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}\sqsubseteq_{A}\sigma(t)$

######  Proof C.7.

The proof is done by induction on $t$. There are few non trivial cases:

  * •

$t=\mathtt{fold}{\;t}^{\prime}$. We suppose that there exists a value $v$ st.
$\sigma(t^{\prime})\to^{*}v$ and $\left\llbracket
t^{\prime}\right\rrbracket\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\dots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}\trianglelefteq_{A[x\rightarrow\mu
X.A]}v$. We directly get that
$\mathtt{fold}{\;\sigma}(t^{\prime})\to^{*}\mathtt{fold}{\;v}$ which is a
value; moreover $\left\llbracket
t^{\prime}\right\rrbracket\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\dots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}=\alpha^{-1}\circ\alpha\circ\left\llbracket
t^{\prime}\right\rrbracket\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\dots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}$
then by definition, $\alpha\circ\left\llbracket
t^{\prime}\right\rrbracket\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\dots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}\trianglelefteq_{\mu
X.A}\mathtt{fold}{\;v}$.

  * •

$t=\\{v_{1}\leftrightarrow e_{1}\mid\dots\mid v_{n}\leftrightarrow
e_{n}\\}\leavevmode\nobreak\ t^{\prime}$. We suppose that there exists a value
$v$ st. $\sigma(t^{\prime})\to^{*}v$ and $\left\llbracket
t^{\prime}\right\rrbracket\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\dots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}\trianglelefteq_{A}v$,
and that for all $i$ and all $g_{1},\dots,g_{k}$, there exists
$v^{\prime}_{i}$ st. $\sigma^{\prime}(e_{i})\to^{*}v^{\prime}_{i}$ and
$\left\llbracket
e_{i}\right\rrbracket\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}g_{1},\dots,g_{k}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}\trianglelefteq_{B}v^{\prime}_{i}$,
without loss of generality. $\omega\sigma(t^{\prime})\to^{*}\omega v$ which is
not a value, but there exists $j$ st. $\omega v\to\sigma^{\prime}(e_{j})$,
because the interpretation is not $\bot$. Thanks to the induction assumptions,
$\omega\sigma(t^{\prime})\to^{*}\sigma^{\prime}(e_{j})\to^{*}v^{\prime}_{j}$.
On the categorical side,

$\displaystyle\left\llbracket
t\right\rrbracket\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\dots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}$
$\displaystyle=\left(\bigvee_{i}\left\llbracket
e_{i}\right\rrbracket\circ\left\llbracket
v_{i}\right\rrbracket^{\circ}\right)\circ\left\llbracket
t^{\prime}\right\rrbracket\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\dots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}$
$\displaystyle=\left(\bigvee_{i}\left\llbracket
e_{i}\right\rrbracket\circ\left\llbracket
v_{i}\right\rrbracket^{\circ}\circ\left\llbracket
t^{\prime}\right\rrbracket\right)\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\dots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}$
$\displaystyle=\left\llbracket e_{j}\right\rrbracket\circ\left\llbracket
v_{j}\right\rrbracket^{\circ}\circ\left\llbracket
t^{\prime}\right\rrbracket\circ\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}f_{1},\dots,f_{n}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}$
$\displaystyle=\left\llbracket e_{j}\right\rrbracket\circ\left\llbracket
v_{j}\right\rrbracket^{\circ}\circ\left\llbracket\sigma(t^{\prime})\right\rrbracket\trianglelefteq_{B}v^{\prime}_{j}.$

The last lign holds because $\left\llbracket
v_{j}\right\rrbracket^{\circ}\circ\left\llbracket\sigma(t^{\prime})\right\rrbracket\colon
1\to A\to\Delta$ is some
$\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\langle}$}}g_{1},\dots,g_{k}\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\leavevmode\hbox{\set@color${\rangle}$}}$.

Theorem 5.8 is a corollary of the previous lemma with $\cdot\vdash t\colon A$.

##  Appendix D Proof of Section 6

######  Proof D.1 (Proof of Lemma 6.3).

The first case if done by a straightforward case analysis on $A$. The second
case is done by induction on $A$. the case of the type $\mathds{1},A\otimes B$
and $A\oplus B$ are straightforward. For an inductive type $\mu X.A$, due to
Lemma 6.3 we can reason on whether or not $X$ is in the set $S$. If it is, it
means that a previous instance of the type $\mu X.A$ has been encountered, in
which case the associated iso variable $\phi$ is of type $\mu
X.A\leftrightarrow(\mu X.A)\otimes(\mu X.A)$ and so the iso is well-typed. If
$X$ is not in $S$ then by induction hypothesis.

######  Proof D.2 (Proof of Lemma 6.4).

The reduction is proven by a straightforward induction on $v$. The
denotational semantics is given by definition.

######  Proof D.3 (Proof of Lemma 6.6).

Direct as each variable is used indeed only once, and by well-typing
hypothesis on $\omega,\omega^{\prime}$, Lemma 2.2 and Lemma 6.3.

######  Proof D.4 (Proof of Lemma 6.7).

Direct by Lemma 6.4.

######  Proof D.5 (Proof of Theorem 6.8).

  * •

In $\omega$, call the right-hand-side $e$.

  * •

Notice that $\left\llbracket
e\right\rrbracket=\left\llbracket\lfloor-\rfloor_{B}^{-1}\right\rrbracket\circ\left\llbracket\operatorname{GarbRem}(\operatorname{isos}(M_{g}),\operatorname{isos}(M_{g}^{\prime}))\right\rrbracket\circ\left\llbracket\lfloor-\rfloor_{A}\right\rrbracket$

  * •

By Theorem 3.16 and Lemma 5.7, we know that
$\left\llbracket\operatorname{GarbRem}(\operatorname{isos}(M_{g}),\operatorname{isos}(M_{g}^{\prime}))\right\rrbracket=g$.

  * •

Therefore, since $g=\left\llbracket\lfloor-\rfloor_{B}\right\rrbracket\circ
f\circ\left\llbracket\lfloor-\rfloor_{A}^{-1}\right\rrbracket$ by definition,
we get

$\displaystyle\left\llbracket e\right\rrbracket$
$\displaystyle=\left\llbracket\lfloor-\rfloor_{B}^{-1}\right\rrbracket\circ\left\llbracket\operatorname{GarbRem}(\operatorname{isos}(M_{g}),\operatorname{isos}(M_{g}^{\prime}))\right\rrbracket\circ\left\llbracket\lfloor-\rfloor_{A}\right\rrbracket$
$\displaystyle=\left\llbracket\lfloor-\rfloor_{B}^{-1}\right\rrbracket\circ
g\circ\left\llbracket\lfloor-\rfloor_{A}\right\rrbracket$
$\displaystyle=\left\llbracket\lfloor-\rfloor_{B}^{-1}\right\rrbracket\circ\left\llbracket\lfloor-\rfloor_{B}\right\rrbracket\circ
f\circ\left\llbracket\lfloor-\rfloor_{A}^{-1}\right\rrbracket\circ\left\llbracket\lfloor-\rfloor_{A}\right\rrbracket$

  * •

By Lemma 5.7 we get that
$\left\llbracket\lfloor-\rfloor_{B}^{-1}\right\rrbracket\circ\left\llbracket\lfloor-\rfloor_{B}\right\rrbracket=Id_{B}$
and
$\left\llbracket\lfloor-\rfloor_{A}^{-1}\right\rrbracket\circ\left\llbracket\lfloor-\rfloor_{A}\right\rrbracket=Id_{A}$.

  * •

Therefore $\left\llbracket e\right\rrbracket=f$.

  * •

Since the left-hand-side of $\omega$ is just a variable we get
$\left\llbracket\omega\right\rrbracket=\left\llbracket e\right\rrbracket\circ
Id^{\circ}=\left\llbracket e\right\rrbracket=f$.