A Curry-Howard Correspondence for Linear, Reversible Computation]A
Curry-Howard Correspondence for  Linear, Reversible
This is a extended version
of the proceeding paper published in LIPICS <cit.>. It contains all the missing proofs, together with
additional discussions.

K. Chardonnet]Kostia Chardonnet[a]
A. Saurin]Alexis Saurin[b]
B. Valiron]Benoît Valiron0000-0002-1008-5605[c]

Department of Computer Science and Engineering, University of Bologna, Italy

Université Paris Cité, CNRS, IRIF, 75013, Paris, France. Équipe
$\pi r^2$, Inria

Université Paris-Saclay, CNRS,
CentraleSupélec, ENS Paris-Saclay, LMF, 91190, Gif-sur-Yvette, France

Équipe Quacs, Inria, Palaiseau, France

In this paper, we present a linear and reversible programming language with
inductive types and recursion. The semantics of the language is based on
pattern-matching; we show how ensuring syntactical exhaustivity and
non-overlapping of clauses is enough to ensure reversibility. The language
allows to represent any Primitive Recursive Function. We then provide a
Curry-Howard correspondence with the logic : linear logic extended
with least fixed points allowing inductive statements. The critical part of
our work is to show how primitive recursion yields circular proofs that
satisfy  validity criterion and how the language simulates the
cut-elimination procedure of .

§ INTRODUCTION

Computation and logic are two faces of the same coin.  For instance,
consider a proof $s$

\infer*{A\rightarrow B}{s}
\infer*{A}{t}
Modus Ponens

of $A\rightarrow B$ and a proof $t$ of $A$. With
the logical rule Modus Ponens one can construct a proof of
$B$: <ref> features a graphical presentation of the corresponding
proof. Horizontal lines stand for deduction steps —they separate conclusions
(below) and hypotheses (above). These deduction steps can be stacked vertically
up to axioms in order to describe complete proofs. In <ref> the
proofs of $A$ and $A\to B$ are symbolized with vertical ellipses. The ellipsis
annotated with $s$ indicates that $s$ is a complete proof of $A\to B$ while $t$
stands for a complete proof of $A$.

This connection is known as the Curry-Howard
correspondence <cit.>.
In this general framework, types correspond to formulas and programs to
proofs, while program evaluation is mirrored with proof
simplification (the so-called cut-elimination).

The Curry-Howard correspondence formalizes the fact that the proof $s$
of $A\to B$ can be regarded as a function —parametrized by an
argument of type $A$— that produces a proof of $B$ whenever it is
fed with a proof of $A$. Therefore, the computational interpretation
of Modus Ponens corresponds to the application of an argument
(i.e. $t$) of type $A$ to a function (i.e. $s$) of type $A\to
B$. When computing the corresponding program, one substitutes the parameter
of the function with $t$ and get a result of type $B$. On the logical
side, this corresponds to substituting every axiom introducing $A$ in
the proof $s$ with the full proof $t$ of $A$. This yields a direct
proof of $B$ without any invocation of the “lemma” $A\to B$.

Paving the way toward the verification of critical software, the
Curry-Howard correspondence provides a versatile framework. It has
been used to mirror first and second-order logics with dependent-type
systems <cit.>, separation logics with
memory-aware type
systems <cit.>,
resource-sensitive logics with differential
privacy <cit.>, logics with monads
with reasoning on
side-effects <cit.>, etc.

The idea of reversible computation comes from Landauer and
Bennett <cit.> with the analysis of its
expressivity, and the relationship between irreversible computing and
dissipation of energy. Indeed, Laundauer's principle states that the erasure of
information is linked to the dissipation of energy as heat <cit.>. This principle was enough to motivate the study of
reversible processes. In order to avoid erasure of information, reversible
computation often makes use of garbage or auxiliary wires:
additional information kept in order to ensure both reversibility and the
non-erasure of information. In reversible computation, given some process $f$,
there always exists an inverse process $f^{-1}$ such that their composition is
equal to the identity: $f \circ f^{-1} = \operatorname{Id} = f^{-1} \circ f$. In
programming languages, this is done by ensuring both forward and
backward determinism. Forward determinism is almost always ensured in
programming language: it is about making sure that, given some state of your
system, there is a unique next state that it can go to. Backward determinism on
the other hand checks that given a state, there is only one state that it comes
from. Standard programming languages does not ensure backward determinism.

From a computational perspective, the Toffoli gate <cit.>, is enough to
realize universal classical computation: any boolean function can be implemented
by Toffoli gates. The Toffoli gate is a reversible 3-input 3-output gate which
flips the 3rd input if and only if the first two are at $1$. This also means
that when implementing a classical, reversible computation with only Toffoli
gates, additional information is necessarily kept. Nevertheless, there exists a
way to turn a non-reversible process into a reversible one, without additional
information at the end, albeit with an increase in computational
time <cit.>.

Many aspects of reversible computation have been considered, such as the
development of reversible Turing Machines <cit.>, reversible programming
languages, both imperative and
functional <cit.> and their
semantics <cit.>.

Closely related to the notion of reversible computation is the
notion of type isomorphisms. As opposed to reversible computation, which
focuses on the functions, the study of type isomorphisms focus on
types. Therefore, one looks at when two types are “the same” according
to the structure of some logic. For instance, in intuitionistic logic, there
exists a isomorphism between the formulas $A\times B$ and $B\times A$, meaning
that there is a pair of proof $A\times B \vdash B\times A$ and $B\times A \vdash
A \times B$ which, when cut together, reduces to the axiom rule on either
$A$ or $B$, depending on the way the proofs where cut together. The same notion
is also present in category theory where instead of proofs one speak of
morphisms. For instance, any cartesian category features the isomorphism
$A\times B \approxeq B\times A$, allowing one to freely pass from one object to
the other. Types isomorphisms have been studied to find suitable equations in
some logical system (like the $\lambda$-calculus) in order to characterize all
isomorphisms between two types <cit.>, in higher-order type system using game
semantics <cit.>, with application in code reuse by searching
through libraries <cit.>. Type isomorphisms have also been
studied in the context of linear logic, for the multiplicative
fragment <cit.> and more recently for the multiplicative
additive fragment <cit.>. However, the formal
relationship between a logical system and a reversible computational model have
not been developed yet.

This paper aims at proposing a type system featuring
inductive types for a purely linear and reversible language.

We base our study on the approach presented
in <cit.>. In this model, reversible computation is
restricted to two main types: the tensor, written $A\tensor B$ and the
co-product, written $A\oplus B$. The former corresponds to the type of
all pairs of elements of type $A$ and elements of type $B$, while
the latter represents the disjoint union of all elements of type $A$
and elements of type $B$. For instance, a bit can be typed with
$\one\oplus\one$, where $\one$ is a type with only one element. The
language in <cit.> offers the possibility to code
isos —reversible maps— with pattern matching. An iso is for
instance the swap operation, typed with $A\otimes B\iso B\otimes A$.
However, if <cit.> hints at an extension towards
pure quantum computation, the type system is not formally connected to
any logical system.

The problem of reversibility between finite type of same cardinality
simply requires to check that the function is injective. That is no
longer the case when we work with types of infinite cardinality such
as natural numbers.

The main contribution of this work is a Curry-Howard correspondence for a purely
reversible typed language in the style of <cit.>, with added
generalised inductive types and terminating recursion, enforced by the fact that
recursive functions must be structurally recursive: each recursive call must be
applied to a decreasing argument. We show how ensuring exhaustivity and
non-overlapping of the clauses of the pattern-matching are enough to ensure
reversibility and that the obtained language can encode any Primitive Recursive
function <cit.>. For the Curry-Howard part, we capitalize on
the logic  <cit.>: an extension of the additive and multiplicative fragment of
linear logic with least and greatest fixed points allowing inductive and
coinductive statements. This logic contains both a tensor and a co-product, and
its strict linearity makes it a good fit for a reversible type system. In the
literature, multiple proofs systems have been considered for , some
finitary proof system with explicit induction inferences à la
Park <cit.> as well as non-well-founded proof
systems which allow to build infinite
derivation <cit.>. The present paper focuses on
the latter. In general, an infinite derivation is called a pre-proof and
is not necessarily consistent. To solve this problem  comes equipped
with a validity criterion, telling us when an infinite derivation can be
considered as a logical proof. We show how the syntactical constraints of being
structurally recursive imply the validity of pre-proofs.

Organisation of the paper

The paper is organised as follows: in <ref> we
introduce the technical background needed for this work, split into two
part:<ref> focus on introducing the Recursive Primitive
Permutations (RPP) <cit.> language, while <ref>
introduce the logic .
In <ref> introduce the language, its syntax, typing rules
and semantics and show that any function that can be encoded in our language
represents an isomorphism. We finally show in <ref> the
expressiveness of the language by encoding any Recursive Primitive
Permutation <cit.> into our language. Then in <ref>, we develop
on the Curry-Howard Correspondence part: we show, given a well-typed term from
our language, how to translate it into a circular derivation of the logic
and show that the given derivation respects the validity condition and
how our evaluation strategy simulates the cut-elimination procedure of the

§ TECHNICAL BACKGROUND

We introduce the technical background necessary for this work. The first part,
in <ref>, focus on the language of Recursive Primitive
Permutations (RPP), which we use as a model of reversible computing to show the
expressiveness of our language. The second part, in <ref>
focus on the logic . We do not give all the details on  but
just the necessary definitions and intuitions. More details for RPP can be found
in <cit.> while <cit.>, contains more details on the logic

§.§ Background on RPP

RPP is a set of integer-valued functions of variable arity; we define
it by arity as follows: we note $\RPP{k}$ for the set of functions in
RPP from $\intT^k$ to $\intT^k$, it is built inductively on $k \in
\natT$ by first what we call the primitives that are part of $\RPP{1}$
and $\RPP{2}$ for the last construction:

* the successor ($S$);

* the predecessor ($P$);

* the identity $(\operatorname{Id})$;

* the sign-change $(\opn{Sign})$;

* the binary permutation $\mathcal{X}$ which sends the pair $(x, y)$ to
$(y, x)$.

And then for any function $f, g, h \in \RPP{k}$ and $j\in\RPP{l}$, the composite

* the sequential composition $f;g \in
\RPP{k}$;

* the parallel composition $f\mid\mid j\in\RPP{k+l}$;

* the iterator $\mathbf{It}[f]\in\RPP{k+1}$;

* the selection $\mathbf{If}[f,g,h]\in\RPP{k+1}$.

Finally, the set of all functions that form $\RPP{}$ is taken as the
union for all $k$ of the $\RPP{k}$:

\[\operatorname{RPP} = \cup_{k\in\mathbb{N}} \operatorname{RPP}^k\]

We present the semantics of each constructor of $\operatorname{RPP}$
under a graphical form, as in <cit.>, where the left-hand-side
variables of the diagram represent the input of the function and the
right-hand-side is the output of the function. The semantics of all
those operators are given in <ref>.

\[
\begin{bNiceMatrix}[first-col, last-col=2, nullify-dots]
x & S & x + 1
\end{bNiceMatrix}
\qquad
\begin{bNiceMatrix}[first-col, last-col=2, nullify-dots]
x & P & x - 1
\end{bNiceMatrix}
\qquad
\begin{bNiceMatrix}[first-col, last-col=2, nullify-dots]
x & \operatorname{Sign} & -x
\end{bNiceMatrix}
\qquad
\begin{bNiceMatrix}[first-col, last-col=2, nullify-dots]
x & \operatorname{Id} & x
\end{bNiceMatrix}
\qquad
\begin{bNiceMatrix}[first-col, last-col=2, nullify-dots]
x & \phantom{\mathcal{X}} \begin{tikzpicture}[remember picture, overlay] \node at (-0.14, -.15) {$\mathcal{X}$}; \end{tikzpicture} & y \\ %  (-.12, -.15)
y & \phantom{\mathcal{X}} & x
\end{bNiceMatrix}
\]

\[
\begin{bNiceMatrix}[first-col, last-col=2, nullify-dots]
x_1 & ~~ & y_1 \\
\vdots & f;g & \vdots \\
x_n & ~~ & y_n \\
\end{bNiceMatrix} =
\begin{bNiceMatrix}[first-col, nullify-dots]
x_1 & ~~  \\
\vdots & f \\
x_n & ~~ \\
\end{bNiceMatrix}\begin{bNiceMatrix}[last-col=2, nullify-dots]
~~ & y_1 \\
g & \vdots \\
~~ & y_n \\
\end{bNiceMatrix}
\qquad
\begin{bNiceMatrix}[first-col, last-col=2, nullify-dots]
x_1 & ~~ & y_1 \\
\vdots & ~~ & \vdots \\
x_k & f \mid\mid g  & y_k \\
x'_1 & ~~ & y'_1 \\
\vdots & ~~ & \vdots \\
x'_l & ~~ & y'_l \\
\end{bNiceMatrix} =
\begin{array}{c}
\begin{bNiceMatrix}[first-col, last-col=2]
x_1 & ~~ & y_1 \\
\vdots & f & \vdots \\
x_k & ~~ & y_n \\
\end{bNiceMatrix} \\
\begin{bNiceMatrix}[first-col, last-col=2]
x'_1 & ~~ & y'_1 \\
\vdots & g & \vdots \\
x_l & ~~ & y'_l \\
\end{bNiceMatrix}
\end{array}
\]

\[
\begin{bNiceMatrix}[first-col, last-col=2, nullify-dots]
x_1 & ~~ & y_1 \\
\vdots & \mathbf{If}[f,g,h] & \vdots \\
x_n & ~~ & y_n \\
x &  & x \\
\end{bNiceMatrix}
\hspace{-0em}\setlength{\arraycolsep}{0pt}
\begin{array}{ c }
\left.\kern-\nulldelimiterspace
\vphantom{\begin{array}{ c }
b_N  \\
\vdots \\
\end{array}}
\right\}= \left\{ \begin{array}{cc}
f~(x_1, \dots, x_n) & \text{ if } x > 0 \\
g~(x_1, \dots, x_n) & \text{ if } x = 0 \\
h~(x_1, \dots, x_n) & \text{ if } x < 0 \\
\end{array} \right. \\
\vphantom{a_N}
\end{array}
\qquad
\begin{bNiceMatrix}[first-col, last-col=2, nullify-dots]
x_1 & ~~ & y_1 \\
\vdots & \mathbf{It}[f] & \vdots \\
x_n & ~~ & y_n \\
x &  & x \\
\end{bNiceMatrix}
\hspace{-0em}\setlength{\arraycolsep}{0pt}
\begin{array}{ c }
\left.\kern-\nulldelimiterspace
\vphantom{\begin{array}{ c }
b_N  \\
\vdots \\
\end{array}}
\right\}= \underbrace{(f;\dots ; f)}_{\alt x \alt} (x_1, \dots, x_n) \\
\vphantom{a_N}
\end{array}
\]

Generators of RPP

In their paper <cit.>, the authors make use of two other
constructors: generalised rewiring permutations over $\intT^k$ and
weakenings of functions, meaning that given $f \in \RPP{k}$ there exists
an infinite set of functions $w^n(f)$ for all $n\leq 1$ such that
$w^n(f)\in\RPP{k + n}$ and whose semantics is $w^n(f) = f \parallel \opn{Id}^n$,
where $\opn{Id}^n$ is $n$ parallel composition of the identity. Both
constructions can be inferred from the basic generators
of <ref> <cit.>.

Then, if $f\in \RPP{k}$ we can define an inverse $f^{-1}$:

The inversion is defined as follows:

$\operatorname{Id}^{-1} = \operatorname{Id}$
$\operatorname{S}^{-1} = \operatorname{P}$
$\operatorname{P}^{-1} = \operatorname{S}$

$\operatorname{Sign}^{-1} = \operatorname{Sign}$
$\mathcal{X}^{-1} = \mathcal{X}$     $(g; f)^{-1} =
f^{-1} ; g^{-1}$

$(f \mid\mid g)^{-1} = f^{-1} \mid\mid g^{-1}$
$(\mathbf{It}[f])^{-1} = \mathbf{It}[f^{-1}]$     $(\mathbf{If}[f,
g, h])^{-1} = \mathbf{If}[f^{-1}, g^{-1}, h^{-1}]$

Given $f\in\RPP{k}$ then $f;f^{-1} = \operatorname{Id} = f^{-1}; f$

RPP is PRF-Complete and PRF-Sound: it can represent any Primitive
Recursive Function and every function in RPP can be represented in

While RPP is expressive enough to encode any Primitive Recursive Function, it
does so at the cost of auxiliary inputs and output. For instance, the Cantor
Pairing can be encoded inside RPP with the help auxiliaries <cit.>.

§.§ Background on

Given an infinite set of variables $\mathcal{V} = \{X, Y, \dots\}$, we
call formulas of  the objects generated by $A, B ::= X
\mid \one \mid \zero \mid \top \mid \bot \mid A \otimes B \mid A\parr
B\mid A\oplus B \mid A\with B\mid \mu X. A\mid \nu X. A$ where $\mu$
and $\nu$ bind the variable $X$ in $A$. The negation on formula is
defined in the usual way: $X^\bot = X, \zero^\bot = \top, \one^\bot =
\bot, (A\parr B)^\bot = A^\bot \otimes B^\bot, (A\oplus B)^\bot =
A^\bot \with B^\bot, (\nu X. A)^\bot = \mu X. A^\bot$ having $X^\bot =
X$ is harmless since we only deal with closed formulas.

We call an occurrence, a word of the form $\alpha \cdot w$
where $\alpha \in \goth{A}_{\text{fresh}}$ an infinite set of
atomic addresses and its dual $\goth{A}_{\text{fresh}}^\bot =
\set{\alpha^\bot \mid \alpha\in\goth{A}_{\text{fresh}}}$ and $w$ a
word over $\{l, r, i\}^*$ (for left, right and
inside) and formulas occurrences $F, G, H, \dots$ as a
pair of a formula and an occurrence, written $A_\alpha$.
Finally, we write $\Sigma, \Phi$ for formula contexts: sets of
formulas occurrences. We write $A_\alpha \equiv B_\beta$ when $A = B$.
Negation is lifted to formulas with $(A_\alpha)^\bot =
A^\bot_{\alpha^\bot}$ where $(\alpha \cdot w)^\bot = \alpha^\bot \cdot
w$ and $(\alpha^\bot \cdot w)^\bot = \alpha\cdot w$. In general, we
write $\alpha, \beta$ for occurrences.

The connectives need then to be lifted to occurrences as well:

* Given $\# \in \{\otimes,\oplus,\parr,\with\}$, if $F =
A_{\alpha l}$ and $G = B_{\alpha r}$ then $(F \# G) = (A\# B)_{\alpha}$

* Given $\# \in \{\mu, \nu\}$ if $F = A_{\alpha i}$ then
$\# X. F = (\# X. A)_{\alpha}$

Occurrences allow us to follow a subformula uniquely inside a
derivation. Since in  we only work with formula occurrences,
we simply use the term formula.

The (possibly infinite) derivation trees of , called
pre-proofs are coinductively generated by the rules given in
<ref>. We say that a formula is principal when
it is the formula that the rule is being applied to.

Taking the natural number $\natT = \mu X. \one\oplus X$, one can
define the proof of $0$ and of $n$ as:

\[\pi_0 = \begin{array}{c}\infer[\mu]{\vdash \mu X. \one\oplus
X}{\infer[\oplus^1]{\vdash \one\oplus \natT}{\infer[\one]{\vdash
\one}{}}}\end{array} \qquad\qquad \pi_n =
\begin{array}{c}\infer[\mu]{\vdash \mu X. \one\oplus
X}{\infer[\oplus^2]{\vdash \one\oplus \natT}{\infer{\vdash
\natT}{\pi_{n-1}}}}\end{array}\]

Among the infinite derivations that  offer we can look at the
circular ones: an infinite derivation is circular if it has
finitely many different subtrees. The circular derivation can
therefore be represented in a more compact way with the help of
back-edges: arrows in the derivation that represent a
repetition of the derivation. Derivations with back-edge are
represented with the addition of sequents marked by a back-edge label,
noted $\vdash^f$, and an additional rule, $\infer[be(f)]{\vdash
\Sigma}{}$, which represent a back-edge pointing to the sequent
$\vdash^f$. We take the convention that from the root of the
derivation from to rule $be(f)$ there must be exactly one sequent
annotated by $f$.

[𝕀]⊢F^, GF≡G     []⊢Σ, Φ⊢Σ, F   ⊢Φ, F^

[]⊢FG, Σ⊢F, G, Σ     []⊢FG, Σ, Φ⊢F, Σ  ⊢G, Φ
[]⊢Σ, ⊢Σ

[]⊢FG, Σ⊢F, Σ  ⊢G,Σ     [⊕^i, i∈{1, 2}]⊢F_1⊕F_2, Σ⊢F_i, Σ

[μ]⊢μX. F, Σ⊢F[X←μX. F], Σ     [ν]⊢νX. F, Σ⊢F[X←νX. F], Σ

Rules for .

An infinite derivation and
two different circular representations with back-edges.

\[\begin{prooftree}

\hypo{}
\ellipsis{\tikzmark{ex_top3}}{}
\infer1[$\mu$]{\vdash \mu X. X}
\infer1[$\mu$]{\vdash \tikzmark{ex_bot3}\mu X. X}
\end{prooftree}\qquad
\begin{prooftree}
\infer0[$be(f)$]{\vdash \mu X. X}
\infer1[$\mu$]{\vdash^f \mu X. X}
\end{prooftree}
\qquad
\begin{prooftree}
\infer0[$be(f)$]{\vdash \mu X. X}
\infer1[$\mu$]{\vdash \mu X. X}
\infer1[$\mu$]{\vdash^f \mu X. X}
\end{prooftree}
\begin{tikzpicture}[remember picture, overlay]
\draw[->, >=latex,rounded corners, smooth=2] ([xshift=-0.3cm,
yshift=0cm]pic cs:ex_top3) .. controls +(170:2.5cm) and +(250:1cm)
.. ([yshift=-0.1cm]pic cs:ex_bot3);
\end{tikzpicture}
\]

While a circular proof has multiple finite representations (depending
on where the back-edge is placed), they can all be mapped back to the
same infinite derivation via an infinite unfolding of the back-edge
and forgetting the back-edge labels:

We define the unfolding of a circular derivation $P$ with a
valuation $v$ from back-edge labels to derivations by:

* $\unfold\left(P :\begin{array}{c}
\infer[r]{\vdash\Sigma}{P_1, \dots, P_n}\end{array}, v\right) =
\begin{array}{c}\infer[r]{\vdash\Sigma}{\unfold(P_1, v), \dots, \unfold(P_n, v)}\end{array}$

* $\unfold(be(f), v) = v(f)$

* $\unfold\left(P : \begin{array}{c}\infer[r]{\vdash^f
\Sigma}{P_1, \dots, P_n}\end{array}, v\right) =
\left(\pi = \begin{array}{c}\infer[r]{\vdash\Sigma}{\unfold(P_1,
v'), \dots, \unfold(P_n, v')}\end{array}\right)$ with $v'(g) =
\pi$ if $g = f$ else $v(g)$.

comes with a validity criterion on pre-proofs that determines when a
pre-proof can be considered as a proof: mainly, whether or not each infinite
branch can be justified by a form of coinductive reasoning. The criterion also
ensures that the cut-elimination procedure holds. For that, we can define a
notion of thread <cit.>: an infinite
sequence of tuples of formulas, sequents and directions (either up or down).
Intuitively, these threads follow some formula starting from the root of the
derivation and start by going up. If the thread encounters an axiom rule, it
will bounce back and start going down in the dual formula of the axiom rule. It
may bounce back again, when going down on a cut rule, if it follows the
cut-formula. A thread can be decomposed into two parts, its visible part
and its hidden part. A thread will be called valid when it is
non-stationary (does not follow a formula that is never a principal formula of a
rule), and when in the set of formulas appearing infinitely often on its visible
part, the minimum formula (according to the subformula ordering) is a $\nu$
formula. For the multiplicative fragment, we say that a pre-proof is valid if
for all infinite branches, there exists a valid thread, while for the additive
part, we require a notion of additive slices and persistent slices
which we do not detail here. <ref> features an example of a
valid proof together with its thread. More details on the notion of pre-threads,
threads, their associated weight and of slices can be found in <cit.> as well as
in <cit.>.

Consider the  proof $\pi_S$ of $A\otimes B\vdash B\otimes A$ defined as

\[\pi_S = \begin{array}{c}\infer[\parr]{(A\otimes B)_\gamma \vdash
(B\otimes A)_{\gamma'}}{\infer[\otimes]{A_{\gamma l}, B_{\gamma r}\vdash (B\otimes A)_{\gamma'}}{\infer[\id]{A_{\gamma l}\vdash
A_{\gamma' r}}{}\qquad \infer[\id]{B_{\gamma r}\vdash B_{\gamma' l}}{}}}\end{array}\]

We can use this proof to define the infinite, circular proof $\phi(\pi_S)$,
where $\aob = (A\otimes B)_{\alpha irl}$ and $\boa = (B\otimes
A)_{\beta irl}$, then $[\aob]$ and $[\boa]$ are respectively of address
$\alpha$ and $\beta$:

\[\scalebox{0.8}{
\begin{prooftree}

\infer0[$\one$]{\vdash \one}
\infer1[$\oplus^1$]{\vdash \one \oplus (\boa \otimes [\boa])}
\infer1[$\mu$]{\vdash [\boa]}
\infer1[$\bot$]{\one \vdash [\boa]}

\infer0[\id]{\aob\vdash \aob}
\hypo{\pi_S}
\infer1{\aob\vdash \boa}
\infer2[\cut]{\aob\vdash \boa}
\hypo{\tikzmark{r77}\qquad\tikzmark{r88}}
\infer1[\id]{\colorbox{cyan!30}{$[\tikzmark{r7}\aob]$}\vdash \colorbox{cyan!30}{$[\tikzmark{r8}\aob]$}}
\hypo{\tikzmark{r10}\phi(\pi_S)}
\infer1{\colorbox{cyan!30}{$[\tikzmark{r9}\aob]$}\vdash [\boa]}
\infer2[\cut]{\colorbox{cyan!30}{$[\tikzmark{r6}\aob]$}\vdash [\boa]}

\infer0[\id]{\boa\vdash \boa}
\infer0[\id]{[\boa]\vdash [\boa]}
\infer2[$\otimes$]{\boa, [\boa]\vdash (\boa) \otimes [\boa]}
\infer1[$\oplus^2$]{\boa, [\boa]\vdash \one \oplus (\boa \otimes [\boa])}
\infer1[$\mu$]{\boa, [\boa]\vdash [\boa]}
% \hypo{\tau}
\infer1[]{\boa, [\boa]\vdash [\boa]}
\infer2[\cut]{\boa, \colorbox{cyan!30}{$[\tikzmark{r5}\aob]$}\vdash [\boa]}
\infer2[\cut]{\aob, \colorbox{cyan!30}{$[\tikzmark{r4}\aob]$}\vdash [\boa]}
\infer1[$\parr$]{\aob \otimes \colorbox{cyan!30}{$[\tikzmark{r3}\aob]$} \vdash [\boa]}

\infer2[$\with$]{\one \oplus \colorbox{cyan!30}{$(\aob \tikzmark{r2}\otimes [\aob])$} \vdash [\boa]}
\infer1[$\nu$]{ \colorbox{cyan!30}{[\tikzmark{r1}\aob]}\vdash [\boa]}

\end{prooftree}

\begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic
cs:r1)+(-.1cm,.1cm)$) to ($(pic cs:r2)+(.1cm,-.2cm)$)to ($(pic
cs:r2)+(-.1,.2cm)$) to($(pic cs:r3)+(0,.2cm)$) to($(pic
cs:r4)+(0,.2cm)$) to($(pic cs:r5)+(0,.1cm)$) to($(pic
cs:r6)+(.1cm,.1cm)$) to($(pic cs:r7)+(0,.2cm)$) to($(pic
cs:r77)+(0,.2cm)$) to($(pic cs:r88)+(0,.2cm)$) to($(pic
cs:r8)+(0,.2cm)$) to($(pic cs:r9)+(0,.2cm)$) to($(pic
\end{tikzpicture}

\]

We painted in blue the pre-thread that will validate the
proof. The pre-thread starts at the root on the formula $[F]$ and follows a
sub-formula when some rules (here $\nu, \with, \parr$) are applied to it. The
pre-thread is then inactive during the multiple cut rules until it
reaches the id rule, where the pre-thread bounces and starts going
down before bouncing back up again in the cut rule, into the infinite
branch, where the behaviour of the pre-thread will repeat itself. One can then
show that this pre-thread is indeed a thread, according to <cit.> and
that it is valid: among the formulas it visits infinitely often on its visible
part, the minimal formula is $[F]$, which is a $\nu$ formula.

§ FIRST-ORDER ISOS

Our language is based on the one introduced by Sabry et
al <cit.> which defines isomorphisms between various
types, included the type of lists. We build on the reversible part of
the paper by extending the language to support both a more general
rewriting system and more general inductive types: while they only
allow the inductive type of lists, we consider arbitrary inductive

The language is defined by layers. Terms and types are presented
in <ref>, while typing derivations, inspired from ,
can be found in <ref> and <ref>. The language
consists of the following pieces.

Basic type.  They allow us to construct first-order terms. The
constructors $\inl{}$ and $\inr{}$ represent the choice between either the left
or right-hand side of a type of the form $A\oplus B$; the constructor $\pv{}{}$
builds pairs of elements (with the corresponding type constructor $\otimes$);
$\fold{}$ represents inductive structure of the types $\mu X.
A$, where $\mu$ is a binder, binding the type-variable $X$ in
$A$. A value can serve both as a result and as a pattern in the defining clause
of an iso. We write $(x_1, \dots, x_n)$ for $\pv{x_1}{\pv{\dots}{x_n}}$ or
$\overrightarrow{x}$ when $n$ is non-ambiguous and $A_1\otimes \dots\otimes A_n$
for $A_1\otimes (\dots \otimes A_n)$ and $A^n$ for $\underbrace{A\otimes \dots
\otimes A}_{n \text{ times}}$. We assume that every type is

First-order isos.  An iso of type $A\iso B$ acts on terms of base types.
An iso is a function of type $A\iso B$, defined as a set of clauses of the form
. In the clauses, the tokens $v_i$ are open values and $e_i$ are
expressions. In order to apply an iso to a term, the iso must be of type $A\iso
B$ and the term of type $A$. In the typing rules of isos, the
$\PE_A(\set{v_1,\dots,v_n})$ predicate syntactically enforces the exhaustivity
and non-overlapping conditions on a set of well-typed values $v_1, \dots, v_n$
of type $A$. The typing conditions make sure that both the left-hand-side and
right-hand-side of clauses satisfy this condition. Its formal definition can be
found in <ref> where $Val(e)$ is defined as
$Val(\letv{p}{\omega~p'}{e}) = Val(e)$, and $Val(v) = v$ otherwise. These checks
are crucial to make sure that our isos are indeed reversible. In the last rule
on <ref>, we define $\pi_1(S)$ and $\pi_2(S)$ as respectively $\set{v
\mid \pv{v}{w} \in S}$ and $\set{w\mid\pv{v}{w}\in S}$ and $S_v^1$ and $S_v^2$
respectively as $\set{w \mid \pv{v}{w}\in S}$ and $\set{w \mid \pv{w}{v} \in

Exhaustivity for an iso $\isobasique$ of type $A \leftrightarrow B$
means that the expressions on the left (resp. on the right) of the
clauses describe all possible values for the type $A$ (resp. the type
$B$). Non-overlapping means that two expressions cannot match the same
value. For instance, the left and right injections $\inl{v}$ and
$\inr{v'}$ are non-overlapping while a variable $x$ is always
exhaustive. The construction $\fix g . \omega$ represents the creation
of a recursive function, rewritten as $\omega[g := \fix g. \omega]$ by
the operational semantics. Each recursive function needs to satisfy a
structural recursion criterion: making sure that one of the input
arguments strictly decreases on each recursive call. Indeed, since
isos can be non-terminating (due to recursion), we need a criterion
that implies termination to ensure that we work with total functions.
If $\omega$ is of type $A\iso B$, we can build its inverse
$\omega^\bot : B\iso A$ and show that their composition is the
identity. In order to avoid conflicts between variables we will always
work up to $\alpha$-conversion and use Barendregt's
convention <cit.> which consists in keeping all
bound and free variable names distinct, even when this remains

The type system is split in two parts: one for terms and expressions (noted
$\Delta; \Psi\vdash_e t : A$) and one for isos (noted $\Psi\vdash_\omega \omega
: A\iso B$). In the typing rules, the contexts $\Delta$ are sets of pairs that
consist of a term-variable and a base type, where each variable can only occur
once and $\Psi$ is a singleton set of a pair of an iso-variable and an iso-type

We assume that the type constructors are right-associative, hence
$\fold{\inl{x}}$ is $\fold{(\inl{(x)})}$.

[Terms and Types]

(Base types)       A, B          ::=         A ⊕B
A ⊗B μX. A X

(Isos, first-order)     α         ::=      AB

(Values)     v          ::=       () x v v
v_1v_2 v

(Pattern)     p          ::=       x p_1p_2

(Expressions)     e          ::=       v p_1ω p_2e

(Isos)              ::=       f.f

(Terms)     t          ::=       () x t t

t  t pt_1t_2

In <cit.> the type of lists of type $A$ is defined as $[A] =
\one \oplus (A\otimes [A])$, while in our language we make use of the inductive
type constructor $\mu X.$ to define the type of lists as $[A] = \mu X. \one
\oplus (A\otimes X)$.

This generalisation allows us to write any kind of inductive types, which is not
possible in <cit.>. One exception to that is the type of
natural numbers. which in <cit.> can be encoded as a list of
unit type, i.e. $[\one]$. One can note that the type $[\one]$ is isomorphic to
the type $\mu X. \one\oplus X$, which is the way natural numbers are represented
in our language.

[Typing of Terms and Expressions]

\[
\begin{array}{c}
\infer{\emptyset;\Psi\entaile () : \one}{}
\quad
\infer{x:A;\Psi \entaile x :A}{}
\quad
\infer{\Delta;\Psi\entaile \inl{t}:A \oplus B}{\Delta;\Psi\entaile
\quad
\infer{\Delta;\Psi\entaile\inr{t}:A \oplus B}{\Delta;\Psi\entaile t:B}
\mynl
\infer{
\Delta_1,\Delta_2;\Psi\entaile \pv{t_1}{t_2} : A \otimes B
\Delta_1;\Psi\entaile t_1 : A
\Delta_2;\Psi\entaile t_2 : B
\qquad
\infer{\Delta; \Psi \entaile \fold{t} : \mu X. A }{\Delta; \Psi \entaile t : A[X\leftarrow \mu X. A]}
\mynl
\infer{
\Delta;\Psi\entaile f~t : B
\Psi\entailiso f : A \iso B
\Delta; \Psi\entaile t : A
\qquad
\infer{
\Delta;\Psi\entaile \isoterm~t : B
\entailiso \isoterm : A \iso B
\Delta;\Psi\entaile t : A
\mynl
\infer{\Delta_1,\Delta_2;\Psi \entaile \letv{(x_1, \dots, x_n)}{t_1}{t_2} :
B}{\Delta_1;\Psi\entaile t_1 : A_1 \otimes \dots \otimes A_n\qquad\Delta_2, x_1 : A_1, \dots, x_n : A_n; \Psi\entaile t_2 : B}
\mynl
\end{array}
\]

[Typing of isos]

\[
\begin{array}{c}
\infer{
\Psi \entailiso
\isobasique : A \iso B.
\begin{array}{l@{\quad}l@{\quad}l@{\qquad}l}
\Delta_1 \entaile v_1 : A
\ldots
\Delta_n\entaile v_n : A
\PE_A(\{v_1, \dots, v_n\})   \\
\Delta_1;\Psi\entaile e_1 : B
\ldots
\Delta_n;\Psi\entaile e_n : B
& \PE_B(\{Val(e_1),\ldots,Val(e_n)\})
\end{array}
\mynl
\infer{f : \alpha \entailiso f : \alpha}{}
\qquad
\inferrule{
f:\alpha\entailiso \omega : \alpha \qquad \fix f. \omega\text{ is structurally recursive}
\Psi\entailiso \fix f.\omega : \alpha
\\
\end{array}
\]

[Structurally Recursive]
Given an iso $\fix f. \isobasique : A_1\otimes \dots \otimes A_m
\iso C$, it is structurally recursive if there is $1 \leq
j \leq m$ such that $A_j = \mu X. B$ and for all
$i\in\{1,\dots,n\}$ we have that $v_i$ is of the form $(v_i^1,
\dots, v_i^m)$ such that $v_i^j$ is either:

* A closed value, in which case $e_i$ does not contain the
subterm $f~p$

* Open, in which case for all subterm of the form $f~p$
in $e_i$ we have $p = (x_1, \dots, x_m)$ and $x_j : \mu
X. B$ is a strict subterm of $v_i^j$.

Given a clause $v \iso e$, we call the value $v_i^j$ (resp. the
variable $x_j$) the decreasing argument (resp. the
focus) of the structurally recursive criterion.

As we are focused on a very basic notion of structurally recursive
function, the typing rules of isos allow to have at most one
iso-variable in the context, meaning that we cannot have intertwined
recursive calls.

[Exhaustivity and Non-Overlapping]

\[
\begin{array}{c}
\infer{\PE_A{(\set{x})}}{} \qquad \infer{\PE_\one{(\set{()})}}{} \qquad
\infer{\PE_{A\oplus B}(\{\inl{v} \alt v \in S \} \cup \{\inr{v} \alt v\in T \})}{\PE_A(S)\qquad \PE_B(T)} \qquad
\mynl
\infer{\PE_{\mu X. A}{(\set{\fold{v} \alt v \in S})}}{\PE_{A[X \leftarrow \mu X. A]}(S)} \qquad
\infer{\PE_{A\otimes B}(S = \{\pv{v_1}{v_1'}, \dots, \pv{v_n}{v'_n}\})}{\begin{array}{l}
\PE_{A}(\pi_1(S)), \forall v\in \pi_1(S), \PE_B(S^1_v) \\
\text{ or } \PE_{B}(\pi_2(S)), \forall v\in \pi_2(S), \PE_A(S^2_v)
\end{array}}
\end{array}
\]

We can define the iso of type : $A\oplus (B\oplus C)\iso C\oplus
(A\oplus B)$, where $a, b$ and $c$ are variables as:

\[
\scalebox{0.8}{$\left\{
\begin{array}{l@{~}c@{~}l}
\inl{(a)} & {\iso} & \inr{(\inl{(a)})} \\
\inr{(\inl{(b)})} & {\iso} & \inr{(\inr{(b)})} \\
\inr{(\inr{(c)})} & {\iso} & \inl{(c)} \\
\end{array}
\right\}$}
\]

While we will show in <ref> that the definition of the $\PE_A$
predicate is sound, we can notice that it is non-complete: there exists some set
of clauses that are exhaustive and non-overlapping but that do not match the
$\PE_A$ predicate. For instance, the following set of clauses of type $((A\oplus
B) \oplus C) \otimes (D\oplus E)$:

\pv{\inr{(x)}}{\inl{(y)}}  & \iso & \dots \\
\pv{\inr{(x)}}{\inr{(y)}}  & \iso & \dots \\
\pv{\inl{(x)}}{\inr{(y)}}  & \iso & \dots \\
\pv{\inl{(\inl{(x)})}}{\inl{(y)}}  & \iso & \dots \\
\pv{\inl{(\inr{(x)})}}{\inl{(y)}}  & \iso & \dots \\
\end{array}\right\}$.

While the set of clauses is indeed exhaustive and non-overlapping and would be
accepted in a typical functional programming language such as OCaml or Haskell,
it does not check the $\PE$ predicate. One immediate fix would be to ask that
there is no unifier between two patterns, but extending the predicate is left
for future works. Also notice that the order between patterns does not matter.

The definition of $\PE_A(S)$ is inspired from <cit.>, but
is less restrictive, as their definition makes it impossible to type the
Toffoli gate.

Finally, our language is equipped with a rewriting system
$\to$ on terms, defined in <ref>, that
follows a deterministic call-by-value strategy: each argument of a
function is fully evaluated before applying the substitution. This is
done through the use of an evaluation context $C[]$, which consists of
a term with a hole (where $C[t]$ is $C$ where the hole has been filled
with $t$). Due to the deterministic nature of the strategy we directly
obtain the unicity of the normal form. The evaluation of an iso
applied to a value relies on pattern-matching: the argument is
matched against the left-hand-side of each clause until one of them
matches (written $\sigma[v] = v'$), in which case the
pattern-matching, as defined in <ref>,
returns a substitution $\sigma$ that sends variables to values.
Because we ensure exhaustivity and non-overlapping
(<ref>), the pattern-matching can always occur on
well-typed terms. The support of a substitution $\sigma$ is
defined as $\operatorname{supp}(\sigma) = \{x \mid (x \mapsto v) \in \sigma \}$.

\[
\infer{\sigma[\inl{e}] = \inl{e'}}{\sigma[e] = e'}
\quad
\infer{\sigma[\inr{e}] = \inr{e'}}{\sigma[e] = e'}
\quad
\infer{\sigma[x] = e}{\sigma = \{ x \mapsto e\}}
\quad
\infer{\sigma[\fold{e}] = \fold{e'}}{\sigma[e] = e'}
\]

\[
\infer{
\sigma[\pv{e_1}{e_2}] = \pv{e'_1}{e'_2}
\sigma_1[e_1] = e'_1
\sigma_2[e_2] = e'_2
\operatorname{supp}(\sigma_1) \cap \operatorname{supp}(\sigma_2) = \emptyset
\sigma = \sigma_1\cup\sigma_2
} \quad \infer{\sigma[()] = ()}{}
\]

Applying substitution $\sigma$ to an expression $t$, written $\sigma(t)$, is
defined as: $\sigma(()) = (), \sigma(x) = v$ if $\{x\mapsto v\}\subseteq
\sigma, \sigma(\inr{(t)}) = \inr{(\sigma(t))}, \sigma(\inl{(t)}) =
\inl{(\sigma(t))}, \sigma(\fold{(t)}) = \fold{(\sigma(t))}, \sigma(\pv{t}{t'})
= \pv{\sigma(t)}{\sigma(t')}, \sigma(\omega~t) = \omega~\sigma(t)$ and
$\sigma(\letv{p}{t_1}{t_2}) = (\letv{p}{\sigma(t_1)}{\sigma(t_2)})$ where the
variables from $p$ do not occur in the domain of $\sigma$ (this assumption can
always be fulfilled thanks to $\alpha$-renaming).

Notice the difference between $\sigma[v] = t$ and $\sigma(t)$. The first one
define the fact that $v$ and $t$ matches under the substitution $\sigma$, while
the second one define the actual substitution. In fact if $\sigma[v] = t$ then
$\sigma(v) = t$.

[Evaluation Contexts]
The evaluation contexts $C$ are defined as:

$$C ::= [~] \alt \inl{C} \alt \inr{C} \alt \omega~C \alt
\letv{p}{C}{t} \alt \pv{C}{v} \alt \pv{v}{C} \alt \fold{C} \alt C~t$$

[Evaluation relation  $\to$]

We define $\to$ the rewriting system of our language as follows:

\[
\begin{array}{c}
\infer[\mathrm{Cong}]{C[t_1] \to C[t_2]}{t_1 \to t_2}
\qquad
\infer[\mathrm{LetE}]{\letv{p}{v}{t} \to \sigma(t)}{\sigma[p] = v}
\quad
\infer[\mathrm{IsoRec}]{
(\fix f.\isoterm) \to \omega[f := (\fix f. \omega)]
\infer[\mathrm{IsoApp}]{ \isobasique~v' \to \sigma(e_i)}{
\sigma[v_i] = v'}
\end{array}
\]

As usual, we note $\to^*$ for the reflexive transitive closure of

Given a set $S$ of well-typed values of type $A$ such that $\PE_A(S)$ holds,
then for all closed value $v$ of type $A$, there exists a unique $v'\in S$
and a unique $\sigma$ such that $\sigma[v'] = v$.

By induction on a derivation of $\PE_A(S)$:

* $\PE_A(\{x\})$ and $\PE_\one(\set{()})$ are direct.

* $\PE_{A\oplus B}(\{\inl{v}\alt v\in S_A\} \cup
\{\inr{v}\alt v\in S_B\})$ let $v = \inl{(\widetilde{v})}$ then
by induction hypothesis on $\PE_A(S_A)$ there exists $v_1\in S_A$
such that $\sigma_1[v_1] = \widetilde{v}$, hence
$\sigma_1[\inl{(v_1)}] = \inl{(\widetilde{v})}$. Now assume there
also exists $v_2 \in S_A$ such that $\sigma_2[v_2] =
\widetilde{v}$, by induction hypothesis we have that $v_1 =
v_2$ hence $\inl{(v_1)} = \inl{(v_2)}$. Similar case for the $\inr{}$.

* $\PE_{\mu X. A}(\set{\fold{(v)} \alt v\in S_{A[X\leftarrow \mu X.
A]}})$. Let $v = \fold{(\tilde{v})}$, by induction hypothesis on
$\PE_{A[X\leftarrow \mu X. A]}(S_{A[X\leftarrow \mu X. A]})$ there exists
some $v_1 \in S_{A[X\leftarrow \mu X. A]}$ and some $\sigma$, such that
$\sigma[v_1] = \tilde{v}$; hence $\sigma[\fold{(v_1)}] =
\fold{(\tilde{v})}$. And if we have another $v_2 \in S_{A[X\leftarrow \mu
X. A]}$ we know by induction hypothesis that $v_1 = v_2$, hence
$\fold{(v_1)} = \fold{(v_2)}$.

* Assuming we are in the first case of the disjunction in the
premise of $\PE_{A\otimes B}$, the other case being similar:

Take some value $\pv{\widetilde{v}}{\widetilde{v'}}$, by
induction hypothesis we know that there exists some
$v_i\in\set{v_1,\dots, v_n}$ such that $\sigma_i[v_i] =
\widetilde{v}$ and therefore that there also exists some
$v_i'\in S_{v_i}^1$ such that $\sigma_i'[v_i'] = v'$.

Now assuming that there exists another pair $\pv{v_1}{v_2}\in
S$ such that $\sigma[\pv{v_1}{v_2}] =
\pv{\widetilde{v}}{\widetilde{v'}}$, by induction hypothesis
we know that $v_1 = v_i$ and that therefore $v_2\in S_{v_i}^1
= S_{v_1}^1$ so $v_2 = v_i'$.

As mentioned above, from any iso $\omega : A\iso B$ we can build its
inverse $\omega^\bot : B \iso A$, the inverse operation is defined
inductively on $\omega$ and is given in <ref>.

Given an iso $\omega$, we define its dual $\omega^\bot$ as: $f^\bot
= f, (\fix f. \omega)^\bot = \fix f. \omega^\bot, \{(v_i\iso
e_i)_{i\in I}\}^\bot = \{((v_i\iso e_i)^\bot)_{i\in I}\}$ and the inverse of a clause as:

\[\begin{array}{c} \left(
\begin{array}{l@{~}c@{~}l} v_1&{\iso}&{\tt
let}\,p_1=\isoterm_1\,p'_1\,{\tt in} \\
&& \cdots \\
&& {\tt let}\,p_n=\isoterm_n\,p'_n\,{\tt in}~v'_1
\end{array}
\right)^\bot := \left(
\begin{array}{lcl@{}l@{}l} v'_1&{\iso}&{\tt
let}\,p'_n&=\isoterm_n^{\bot}&\,p_n\,{\tt in} \\
&& \cdots \\
&& {\tt let}\,p'_1&=\isoterm_1^{\bot}&\,p_1\,{\tt in}~v_1
\end{array}
\right).
\end{array}
\]

We can show that the inverse is well-typed and behaves as expected:

Given $\Psi \vdash_\omega \omega : A\iso B$, then
$\Psi\vdash_\omega\omega^\bot : B\iso A$.

w.l.o.g. consider $\omega = \isobasique$, we look at one clause in
particular and its dual:

\[\begin{array}{c} \left(
\begin{array}{l@{~}c@{~}l} v_1&{\iso}&\letv{p_1}{\omega_1~p_1'}{} \\
&& \cdots \\
&& \letv{p_n}{\isoterm_n~p'_n}{v'_1}
\end{array}
\right)^\bot := \left(
\begin{array}{lcl@{}l@{}l} v'_1&{\iso}&\letv{p'_n}{\isoterm_n^{\bot}~p_n}{} \\
&& \cdots \\
&& \letv{p'_1}{\isoterm_1^{\bot}~p_1}{v_1}
\end{array}
\right).
\end{array}
\]

By typing we know that $\Delta \vdash_e v_1 : A$ and
$\Delta;\Psi\vdash_e \letv{p_1}{\omega_1~p_1'}{\dots v_1'} : B$

$\Delta$ can be split into $\Delta_1, \dots, \Delta_n, \Delta_{n+1}$
and for all $1 \leq i \leq n$ we get that the typing judgment of the
expression $\letv{p_i}{\omega_i~p_i'}{\dots}$ generates the new typing
judgment $\Gamma_i^{i+1}, \dots, \Gamma_i^{n+1}$. For all $i$ we get
that $\Delta_i \bigcup_{j=1}^{i-1} \Gamma_j^i \vdash_e \omega~p_i'$,
finally $v_1'$ is typed by $\Delta_{n+1}\bigcup_{i=1}^n \Gamma_i^{n+1}$.

When typing the dual clause, we start with contexts
$\Delta_{n+1}\bigcup_{i=1}^n \Gamma_i^{n+1}$. We have by hypothesis

* Each $\omega_i^\bot p_i$ is typed by $\bigcup_{j=i+1}^{n}
\Gamma_j^n$, which is possible by our typing hypothesis.

* Each $p_i'$ generates the contexts $\Delta_i, \bigcup_{j=1}^{i}
\Gamma_j^i$.

Eventually we end up with $\Delta_1,\dots,\Delta_n,\Delta_{n+1}\vdash_e v_1$
which is typable by our hypothesis.

We give the encoding of the isomorphism map$(\omega)$ and its
inverse: for any given iso $\vdash \omega : A\iso B$ in our language, we can
define $\textit{map}(\omega) : [A]\iso [B]$ where $[A] = \mu X. \one\oplus
(A\otimes X)$ is the type of lists of type $A$ and $[\,]$ is the empty list
($\fold{(\inl{()})}$) and $h :: t$ is the list construction
($\fold{(\inr{\pv{h}{t}})}$). We also give its dual
$\textit{map}(\omega)^\bot$ below, as given by <ref>.

\[\begin{array}{ll}
\textit{map}(\omega):[A]\iso[B] \\
= \fix f.\left\{
\begin{array}{l@{~}c@{~}l}
[~] & {\iso} & [~] \\
h :: t & {\iso} & \letv{h'}{\omega~h}{} \\
& &  \letv{t'}{f~t}{}\\
& & h' :: t' \\
\end{array}
\right\}
\end{array}
\hfill
\begin{array}{ll}
\textit{map}(\omega)^\bot:[B]\iso[A] \\
= \fix f.\left\{
\begin{array}{l@{~}c@{~}l}
[~] & {\iso} & [~] \\
h' :: t' & {\iso} & \letv{t}{f~t'}{} \\
&  &  \letv{h}{\omega^\bot h'}{}\\
& & h :: t \\
\end{array}
\right\}
\end{array}\]

In our two examples, the left and right-hand side of the $\iso$
on each function respect both the criteria of exhaustivity —every-value of
each type is being covered by at least one expression— and non-overlapping
—no two expressions cover the same value. Both isos are therefore
bijections. Also notice that while the iso $\fix f. \set{x\iso
\letv{y}{f~x}{y}}$ is not structurally recursive while the one
from <ref> is.

The language enjoys the standard properties of typed languages, namely progress
and subject reduction, but requires a substitution lemma on both terms and isos:

* 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\set{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 \FV(t)$ such that $\Gamma, x_1 :
A_1, \dots, x_n : A_n \vdash_e t : B$

If $\sigma = \{x_1 \mapsto v_1, \dots, x_n \mapsto v_n\}$ then
$\Gamma, \Delta_1, \dots, \Delta_n \vdash_e \sigma(t) : B$

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 $\inl{t'}$, by substitution we have $\sigma(\inl{t'}) =
\inl{\sigma(t')}$ and by typing we get

$\infer{\Gamma,\Delta_1,\dots, \Delta_n \vdash
\inl{\sigma(t')}}{\Gamma,\Delta_1,\dots, \Delta_n \vdash
\sigma(t')}$ which is typable by induction hypothesis on $t'$.

* Case $\inr{t'}, \fold{t'}, \omega~t'$ are similar.

* Case $\pv{t_1}{t_2}$, 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:

$\infer{\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 \pv{t_1}{t_2} : 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(\pv{t_1}{t_2}) =
\pv{\sigma(t_1)}{\sigma(t_2)}$, so we get the following typing
derivation which is completed by induction hypothesis on the

$\infer{\Gamma_1,\Gamma_2, \Delta_1, \dots, \Delta_l,
\Delta_{l+1}, \dots, \Delta_n\vdash_e \pv{t_1}{t_2} : 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 $\letv{p}{t_1}{t_2}$ Similar to the case of the tensor.

The following substitution properties hold:

* If: $\Delta; f : \alpha \vdash_e t : A$ and $g : \beta \vdash_\omega \omega :
\alpha$
then $\Delta; g : \beta \vdash_e t[f \leftarrow \omega] : A$.

* If: $f : \alpha \vdash_\omega \omega_1 : \beta$
and $h : \gamma \vdash_\omega \omega_2 : \alpha$
then $h : \gamma \vdash_\omega \omega_1[f \leftarrow \omega_2] : \beta$.

We prove those two propositions by mutual induction on $t$ and

Terms, by induction on $t$.

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

* If $t = \inl{t'}$ or $\inr{t'}$ or $\fold{t'}$ or
$\pv{t_1}{t_2}$ or $\letv{p}{t_1}{t_2}$, then similarly to the
proof of <ref> the substitution goes to
the subterms and we can apply the induction hypothesis.

* If $t = \omega'~t'$. In that case, the substitution goes
to both subterms: $t[f \leftarrow \omega] = (\omega'[f
\leftarrow \omega])~(t'[f \leftarrow \omega])$ and by induction
hypothesis on $t'$ and by the induction hypothesis on isos.

Isos, by induction on $\omega_1$.

* If $\omega_1 = f$, then we get $h : \gamma \vdash_\omega f[f
\leftarrow \omega_2] : \beta$ which is typable by hypothesis.

* $If \omega_1 = g \not= f$ is impossible by our typing

* If $\omega_1 = \fix g. \omega$, then by typing $f$ does
not occur in $\omega_1$ so nothing happens.

* If $\omega_1 = \isobasique$, then, by definition of the
substitution we have that
\begin{align*}&\isobasique[f \leftarrow
\omega_2] \\ &= \{v_1 \iso e_1[f \leftarrow \omega_2] \alt \dots \alt
v_n[f \leftarrow \omega_2] \iso e_n[f \leftarrow \omega_2] \}\end{align*}
which case we apply the substitution lemma of isos on terms.

From that we can directly deduce subject reduction and progress:

$\Delta;\Psi\vdash_e t : A$ and $t\rightarrow t'$ then
$\Delta;\Psi\vdash_e t' : A$.

By induction on $t\to t'$ and direct by <ref>
and <ref>

If $~\vdash_e t : A$
then, either $t$ is a value, or $t\to t'$.

Direct by induction on $\vdash_e t : A$. The two possible
reduction cases, $\omega~v$ and $\letv{p}{v}{t}$ always reduce by
typing, pattern-matching and by <ref>.

We are left to show that our isos indeed represent isomorphisms, meaning that
given some iso $\vdash_\omega \omega : A\iso B$ and some value $\vdash_e v : A$,
then $\omega^\bot(\omega~v) \to^* v$. For that we need the following lemma:

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))$

Direct by induction on $v$ as $\sigma_1$ and $\sigma_2$ have disjoint
support: In the case where $v = x$ then either $\set{x\mapsto v'} \in
\sigma_1$ or $\set{x\mapsto v'}\in\sigma_2$ and hence
$\sigma_1(\sigma_2(x)) = v' = \sigma_2(\sigma_1(x))$. All the other
cases are by direct induction hypothesis as the substitutions enter the

For all well-typed isos $\vdash_\omega \omega : A\iso B$, and for
all well-typed values $\vdash_e v : A$, if
$(\omega~(\omega^\bot~v))\rightarrow^* v'$ then $v = v'$.

By induction hypothesis on the size of $\omega$:

* Case where $\omega = \{v_1\iso v_1\alt \dots\alt v_n\iso
v_n'\}$ then $\omega^\bot(\omega~v_0)$, by non-overlapping and
exhaustivity there exists a $v_i$ such that $\sigma[v_i] = v_0$
and hence the term reduces to $\omega^\bot \sigma(v_i')$. It is
clear that $\sigma[v_i'] = \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 = \isobasique$, for clarity we write a single

\[\begin{array}{c} \left(
\begin{array}{l@{~}c@{~}l} v_1&{\iso}&\letv{p_1}{\omega_1~p_1'}{} \\
&& \cdots \\
&& \letv{p_n}{\isoterm_n~p'_n}{v'_1}
\end{array}
\right)^\bot := \left(
\begin{array}{lcl@{}l@{}l} v'_1&{\iso}&\letv{p'_n}{\isoterm_n^{\bot}~p_n}{} \\
&& \cdots \\
&& \letv{p'_1}{\isoterm_1^{\bot}~p_1}{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

\[ \letv{p_1}{\omega_1\,\sigma_1(p'_1)}{} \dots
\letv{p_n}{\omega_n\,\sigma_n(p'_n)}{}
\sigma_{n+1}(v_1').\]

By <ref>, each  construction will reduce,
and by the rewriting strategy we get:

\[\begin{array}{c} \letv{p_1}{\omega_1\,\sigma_1(p'_1)}{}
\\
\dots \\
\letv{p_n}{\omega_n\,\sigma_n(p'_n)}{} \\
\sigma_{n+1}(v_1') \end{array}
\to \begin{array}{c} \letv{p_1}{\overline{v_1}}{}
\\
\dots \\
\letv{p_n}{\omega_n\,\sigma_n(p'_n)}{} \\
\sigma_{n+1}(v_1') \end{array}
\to \begin{array}{c} \letv{p_2}{\omega_2\,\gamma_1^2(\sigma_1(p'_1))}{}
\\
\dots \\
\letv{p_n}{\omega_n\,\gamma_1^n(\sigma_n(p'_n))}{} \\
\sigma_{n+1}(v_1') \end{array} \]
The final term reduces to
and creates a new substitution $\gamma_i$, the term will hence reduce
to $\gamma_n(\dots(\gamma_1(\sigma_{n+1}(v_1')))\dots)$. Let $\delta =
\cup_i \gamma_i \cup \sigma_{n+1}$. We are left to evaluate

\[\left(
\begin{array}{lcl@{}l@{}l} v_1'&{\iso}&
\letv{p'_n}{\isoterm_n^\bot~p_n}{} \\
&& \cdots \\
&& \letv{p'_1}{\isoterm_1^\bot~p_1}{v_1}
\end{array}
\right)~\delta(v_1')\]

We get $\delta[v_1'] = \delta(v_1')$.

We know that each $\gamma_i$ closes only $p_i$, we can
therefore substitute the term as:

\[\letv{p_n'}{\omega_n~\gamma_n(p_n)}{\dots}
\letv{p_1'}{\omega_1\gamma_1(p_1)}{\sigma_{n+1}(v_1')}\]

By induction hypothesis, each  clause will re-create the
substitution $\sigma_i$, we know this from the fact that the initial
construction, $\letv{p_i}{\omega_i~\sigma_i(p_i')}{\dots}$
reduces to $\letv{p_i}{v_i}{\dots}$ While the new one,
$\letv{p_i'}{\omega^\bot\gamma_i(p_i)}{\dots}$, is, by definition
of the substitution, the same as $\letv{p_i'}{\omega^\bot

Then, since we know that $v_i$ is the result of
$\omega~\sigma_i(p_i')$, we get by induction hypothesis $\sigma(p_i')$
as the result of the evaluation.

Therefore, after rewriting we obtain:
By <ref> we get

$\sigma_1(\dots(\sigma_n(\sigma_{n+1}(v_1')))\dots)$ which is
equal to $v$.

§ COMPUTATIONAL CONTENT

In this section, we study the computational content of our language. In the case
of only finite types made up of the tensor, plus and unit, one can represent any
bijection by case analysis. However, with infinite types, the expressivity
becomes less clear. We show that we can encode Recursive Primitive
Permutations <cit.> (RPP), implying that we can encode at least all
Primitive Recursive Functions <cit.>.

§.§ From RPP to Isos

We start by defining the type of strictly positive natural numbers,
$\operatorname{npos}$, as $\operatorname{npos} = \mu X. \one \oplus
X$. We define $\underline{n}$, the encoding of a positive natural
number into a value of type $\operatorname{npos}$ as $\underline{1} =
\fold{\inl{()}}$ and $\underline{n+1} = \fold{\inr{\underline{n}}}$.
Finally, we define the type of integers as $Z = \one \oplus
(\operatorname{npos} \oplus \operatorname{npos})$ along with
$\overline{z}$ the encoding of any $z\in\intT$ into a value of type
$Z$ defined as: $\overline{0} = \inl{()}$, $\overline{z} =
\inr{\inl{\underline{z}}}$ for $z$ positive, and $\overline{z} =
\inr{\inr{\underline{- z}}}$ for $z$ negative. Given some function $f
\in \RPP{k}$, we will build an iso $\operatorname{isos}(f) : Z^k \iso
Z^k$ which simulates $f$. $\operatorname{isos}(f)$ is defined by the
size of the proof that $f$ is in $\RPP{k}$.

[Encoding of the primitives]

* The Sign-change of type $Z\iso Z$ is

\inr{(\inl{x})} &\iso& \inr{(\inr{x})} \\
\inr{(\inr{(x)})} &\iso& \inr{(\inl{x})} \\
\inl{()} &\iso&\inl{()}
\end{array}\right\}$

* The identity is $\{x\iso x\} : Z \iso Z$

* The Swap is $\{(x, y) \iso (y, x)\} : Z^2 \iso

* The Predecessor is the inverse of the Successor

* The Successor is

\[\left\{\begin{array}{ccc}
\inl{()} &\iso& \inr{(\inl{(\fold{(\inl{()})})})} \\
\inr{(\inl{x})}&\iso&\inr{(\inl{(\fold{(\inr{x})})})} \\
\inr{(\inr{(\fold{(\inl{()})})})}&\iso& \inl{()}\\
\inr{(\inr{(\fold{(\inr{x})})})}& \iso & \inr{(\inr{x})}
\end{array}\right\} : Z \iso Z \]

[Encoding of Composition]
Let $f, g\in \RPP{j}$, $\omega_f = \operatorname{isos}(f)$ and
$\omega_g = \operatorname{isos}(g)$ the isos encoding $f$ and $g$, we
build $\operatorname{isos}(f;g)$ of type $Z^{j} \iso Z^{j}$ as:

\[\operatorname{isos}(f;g) = \left\{\begin{array}{ccc} &  & \letv{(y_1, \dots, y_j)}{\omega_f~(x_1, \dots, x_j)}{} \\
(x_1, \dots, x_j) & \iso & \letv{(z_1,
\dots, z_j)}{\omega_g~(y_1, \dots, y_j)}{} \\
& & (z_1, \dots, z_j) \end{array}\right\}\]

[Encoding of Parallel Composition]

Let $f \in \RPP{j}$ and $g \in \RPP{k}$, and $\omega_f =
\operatorname{isos}(f)$ and $\omega_g = \operatorname{isos}(g)$, we
define $\operatorname{isos}(f\mid\mid g)$ of type $ Z^{j+k} \iso
Z^{j+k}$ as:.

\[\operatorname{isos}(f\mid\mid g) = \left\{\begin{array}{ccc} &  & \letv{(x_1', \dots, x_j')}{\omega_f~(x_1, \dots, x_j)}{} \\
(x_1, \dots, x_j, y_1, \dots, y_k) & \iso & \letv{(y_1',
\dots, y_k')}{\omega_g~(y_1, \dots, y_k)}{} \\
& & (x_1', \dots, x_j', y_1', \dots, y_k') \end{array}\right\}\]

[Encoding of Finite Iteration]
Let $f\in \RPP{k}$, and $\omega_f = \operatorname{isos}(f)$, we encode
the finite iteration $\mathbf{It}[f]\in\RPP{k+1}$ with the help of an
auxiliary iso, $\omega_{\operatorname{aux}}$, of type $Z^k
\otimes~\operatorname{npos} \iso Z^k \otimes~\operatorname{npos}$
doing the finite iteration using $\operatorname{npos}$, defined as:

\[\omega_{\operatorname{aux}} = \fix g.
\left\{\begin{array}{ccc}
(\overrightarrow{x}, \fold{(\inl{()})}) & \iso & \letv{\overrightarrow{y}}{\omega_f~\overrightarrow{x}}{}
\\
& & (\overrightarrow{y},\fold{(\inl{()})}) \\[0.5em]
(\overrightarrow{x}, \fold{(\inr{n})})& \iso &  \letv{(\overrightarrow{y})}{\omega_f~(\overrightarrow{x})}{} \\
& & \letv{(\overrightarrow{z}, n')}{g~(\overrightarrow{y}, n)}{} \\
& & (\overrightarrow{z}, \fold{(\inr{n'})}) \\[0.5em]
\end{array}\right\}\]

We can now properly define $\operatorname{isos}(\mathbf{It}[f])$ of
type $Z^{k+1} \iso Z^{k+1}$ as:

\[\operatorname{isos}(\mathbf{It}[f]) = \left\{\begin{array}{ccc}
(\overrightarrow{x}, \inl{()})&\iso&(\overrightarrow{x}, \inl{()}) \\[0.5em]
(\overrightarrow{x}, \inr{(\inl{z})})&\iso& \letv{(\overrightarrow{y}, z')}{\omega_{aux} (\overrightarrow{x}, z)}{} \\
& & (\overrightarrow{y}, \inr{(\inl{z'})}) \\[0.5em]
(\overrightarrow{x}, \inr{(\inr{z})})&\iso& \letv{(\overrightarrow{y}, z')}{\omega_{aux} (\overrightarrow{x}, z)}{} \\
& & (\overrightarrow{y}, \inr{(\inr{z'})}) \\[0.5em]
\end{array}\right\}\]

[Encoding of Selection]

Let $f, g, h\in\RPP{k}$ and their corresponding isos $\omega_f =
\operatorname{isos}(f), \omega_g = \operatorname{isos}(g), \omega_h =
\operatorname{isos}(h)$. We define
$\operatorname{isos}(\mathbf{If}[f,g,h])$ of type $Z^{k+1} \iso
Z^{k+1}$ as:

1$\operatorname{isos}(\mathbf{If}[f,g,h]) = \left\{\begin{array}{ccl}
(\overrightarrow{x}, \inr{(\inl{z})}) &\iso&
\letv{\overrightarrow{x'}}{\omega_f
(\overrightarrow{x})}{(\overrightarrow{x'}, \inr{(\inl{z})})} \\
(\overrightarrow{x}, \inl{()}) &\iso&
\letv{\overrightarrow{x'}}{\omega_g
(\overrightarrow{x})}{(\overrightarrow{x'}, \inl{()})} \\
(\overrightarrow{x}, \inr{(\inr{z})}) &\iso&
\letv{\overrightarrow{x'}}{\omega_h
(\overrightarrow{x})}{(\overrightarrow{x'}, \inr{(\inr{z})})}
\end{array}\right\}$

[Encoding of generalised permutations]
Given a set of distinct variables $\set{x_1, \dots, x_n}$ and a permutation
$\gamma$ on natural numbers, the permutation is encoded as the iso $\{ (x_1, \dots, x_n)
\iso (x_{\gamma(1)}, \dots, x_{\gamma(n)}) \} : \intT^k \iso \intT^k$.

Given a function $f\in\RPP{k}$ and its weakening $w^n(f)$ for $n \geq 1$, the
function $w^n(f)\in\RPP{k+n}$ is encoded as

$\set{(x_1, \dots, x_k, x_{k+1}, \dots, x_n) \iso \letv{(x_1', \dots,
x_k')}{f~(x_1, \dots, x_k)}{(x_1', \dots, x_k', x_{k+1}, \dots, x_n)}} :
\intT^{k+n} \iso \intT^{k+n}$.

Let $f\in \RPP{k}$, then $\vdash_\omega \operatorname{isos}(f) : Z^k \iso Z^k$.

By induction on $f$, for the two compositions, iteration, and
selection the variables $\overrightarrow{x}$ are all of type $Z$,
while for $\omega_{\opn{aux}}$ the last argument is of type
$\opn{npos}$. The predicate $\PE_Z$ is always satisfied as the
left columns of the $n$-fold tensor are always variables and the
right-most argument on each isos always satisfies $\PE_Z$.

Let $f\in \RPP{k}$ and $~n_1, \dots, n_k$ elements of $~\intT$
such that $f(n_1, \dots, n_k) = (m_1, \dots, m_k)$ then $\operatorname{isos}(f)
(\overline{n_1}, \dots, \overline{n_k}) \to^* (\overline{m_1}, \dots,
\overline{m_k})$

By induction on $f$.

* Direct for the identity, swap and sign-change.

* For the Successor:

\[\omega = \left\{\begin{array}{ccc}
\inl{()} &\iso& \inr{\inl{\fold{\inl{()}}}} \\
\inr{\inl{x}}&\iso&\inr{\inl{\fold{\inr{x}}}} \\
\inr{\inr{\fold{\inl{()}}}}&\iso& \inl{()}\\
\inr{\inr{\fold{\inr{x}}}}& \iso & \inr{\inr{x}}
\end{array}\right\}\]
we do it by case analysis on the sole
input $n$.

* $n = 0$ then $\ov{0} = \inl{()}$ and
$\omega~\inl{()} \to \inr{(\inl{(\fold{(\inl{()})})})} = \ov{1}$

* $n = -1$ then $\ov{-1} =
\inr{(\inr{(\fold{(\inl{()})})})}$, so the term reduces to
$\inl{()} = \ov{0}$

* Case $n < -1$, we have $\ov{n} =
\inr{(\inr{(\fold{(\inr{\underline{n'}})})})}$ with
$\underline{n'} = \underline{n+1}$, by pattern-matching we
get $\inr{\inr{x}}$ which is $\ov{n'}$

* Case $n > 1$ is similar.

* The Predecessor is the dual of the Successor.

* Composition & Parallel composition: Direct by
induction hypothesis on $\omega_f$ and $\omega_g$.: for the
composition, $\omega_f$ if first applied on all the input and
then $\omega_g$ on the result of $\omega_f$. For the parallel
composition, $\omega_f$ is applied on the first $j$ arguments
and $\omega_g$ on the argument $j+1$ to $k$ before
concatenating the results from both isos.

* Finite Iteration: $\opn{It}[f]$.

We need the following lemma: $\omega_{\text{aux}} (\bar{x_1},
\dots, \bar{x_n}, \underline{z}) \to^* (\bar{z_1}, \dots,
\bar{z_n}, \underline{z})$ where $z$ is a non-zero integer and
$(z_1, \dots, z_n) = f^{\mid z \mid} (x_1, \dots, x_n)$ which
can be shown by induction on $\mid z\mid$: the case $z = 1$
and $\bar{z} = \fold{\inl{()}}$ is direct by induction
hypothesis on $\omega_f$. Then if $z = n+1$ we get it directly
by induction hypothesis on both $\omega_f$ and our lemma.

Then, for $\opn{isos}{\opn{It}[f]}$ we do it by case analysis
on the last argument: when it is $\bar{0}$ then we simply
return the result, if it is $\bar{z}$ for $z$ (no matter if
strictly positive or strictly negative) then we enter
$\omega_{aux}$, and apply the previous lemma.

* Conditional: $\opn{If}[f, g, h]$. Direct by case
analysis of the last value and by induction hypothesis on
$\omega_f, \omega_g, \omega_h$.

* Generalised Permutation: Direction by the definition of the
generalised permutation.

* Weakening: By induction hypothesis on $f$.

With <ref>, this tells us
that any primitive recursive function can effectively be encoded as a well-typed
iso with the appropriate semantics.

Notice that $\operatorname{isos}(f)^\bot \not=
\operatorname{isos}(f^{-1})$, due to the fact that
$\operatorname{isos}(f)^\bot$ will inverse the order of the
let constructions, which will not be the case for
$\operatorname{isos}(f^{-1})$. They can nonetheless be considered
equivalent up to a permutation of  constructions and
renaming of variable.

§ PROOF THEORICAL CONTENT

We want to relate our language of isos to proofs in a suitable logic.
As mentioned earlier, an iso $\vdash_\omega \omega : A\iso B$
corresponds to both a computation sending a value of type $A$ to a
result of type $B$ and a computation sending a value of type $B$ to a
result of type $A$. Therefore, we want to be able to translate an iso
into a proof isomorphism : two proofs $\pi$ and $\pi^\bot$ of
respectively $A\vdash B$ and $B\vdash A$ such that their composition
reduces through the cut-elimination to the identity either on $A$ or
on $B$ depending on the way we make the cut between those proofs.

Since we are working in a linear system with inductive types we will use an
extension of Linear Logic called : linear logic with least and
greatest fixed points <cit.>, which allows us to
reason about inductive and coinductive statements.  also allows us to
consider infinite derivation trees, which is required as our isos can contain
recursive variables. We need to be careful though: infinite derivations cannot
always be considered as proofs, hence  comes with a validity criterion
on infinite derivations trees (called pre-proofs) that tells us whether
such derivations are indeed proofs. We recall briefly the basic notions of
, while more details can be found in <cit.>.

§.§ Translating isos into

We start by giving the translation from isos to pre-proofs, and then
show that they are actually proofs, therefore obtaining a
static correspondence between programs and proofs. We then
show that our translation entails a dynamic correspondence
between the evaluation procedure of our language and the
cut-elimination procedure of . This will imply that the
proofs we obtain are indeed isomorphisms, meaning that if we cut the
aforementioned proofs $\pi$ and $\pi^\bot$, performing the
cut-elimination procedure would give either the identity on $A$ or the
identity on $B$.

The derivation we obtain are circular, and we therefore
translate the isos directly into finite derivations with back-edge,
written $\circu(\omega)$. We can define another translation into
infinite derivations as the composition of $\circu()$ with the
unfolding: $\bbracket{\omega} = \unfold(\circu(\omega))$.

Because we need to keep track of which formula is associated to which
variable from the typing context, the translation uses a slightly
modified version of  in which contexts are split in two
parts, written $\Upsilon; \Theta$, where $\Upsilon$ is a list of
formulas and $\Theta$ is a set of formulas associated with a
term-variable (written $x : F$). When starting the translation of an
iso of type $A\iso B$, we start in the context $[A_\alpha]; \emptyset$
(for some address $\alpha$) and end in the context $[]; \Theta$. The
additional information of the variable in $\Theta$ is here to make
sure we know how to split the contexts accordingly when needed later
during the translation, with respect to the way they are split in the
typing derivation. We write $\overline{\Theta} = \{ F \mid x : F \in
\Theta \}$ and $\underline{\Theta} = \{ x : A \mid x : A_\alpha \in
\Theta\}$. We also use another rule which allow to send the first
formula from $\Upsilon$ to $\Theta$ and associate it a variable to the
\[\infer[ex(x)]{F :: \Upsilon ; \Theta\vdash G}{\Upsilon ; x
: F, \Theta \vdash G}\]
Given a derivation $\iota$ in this system, we
write $\ffloor{\iota}$ for the function that sends $\iota$ into a
derivation of  where (i) we remove all occurrence of the
exchange rule (ii) the contexts $[]; \Theta$ becomes

Given an iso $\omega : A\iso B$ and initial addresses $\alpha, \beta$,
its translation into a derivation of  of $A_\alpha \vdash
B_\beta$ is described with three separate phases:

Iso Phase. The first phase consists in travelling through the
syntactical definition of an iso, keeping as information the last
encountered iso-variable bounded by a $\fix f. \omega$ and calling the
negative phase when encountering an iso of the form $\isobasique$ and
attaching to the formulas $A$ and $B$ two distinct addresses $\alpha$
and $\beta$ and to the sequent as a label of name of the last
encountered iso-variable. Later on during the translation, this phase
will be recalled when encountering another iso in one of the $e_i$,
and, if said iso correspond to an iso-variable, we will create a
back-edge pointing towards the corresponding sequents.

Negative Phase.  Starting from some context $[A_\alpha],
\Theta$, the negative phase consists into decomposing the formula $A$
according to the way in which the values of type $A$ on the
left-hand-side of $\omega$ are decomposed. The negative phase works as
follows: we consider a set of (list of values, typing judgment),
written $(l, \xi)$ where each element of the set corresponds to one
clause $v \iso e$ of the given iso and $\xi$ is the typing judgment of
$e$. The list of values corresponds to what is left to be decomposed
in the left-hand-side of the clause (for instance if $v$ is a pair
$\pv{v_1}{v_2}$ the list will have two elements to decompose). Each
element of the list $\Upsilon$ will correspond to exactly one value in
the list $l$. If the term that needs to be decomposed is a variable
$x$, then we will apply the $ex(x)$ rule, sending the formula to the
context $\Theta$. The negative phase ends when the list is empty and
hence when $\Upsilon = []$. When it is the case, we can start
decomposing $\xi$ and the positive phase start. The negative
phase is defined inductively on the first element of the list of every
set, which are known by typing to have the same prefix, and is given
in <ref>.

Positive phase. The translation of an expression is pretty
straightforward: each let and iso-application is represented
by two  rules, as usual in Curry-Howard correspondence. Keeping
the variable-formula pair in the derivation is here to help us know
how to split accordingly the context $\Theta$ when needed, while
$\Upsilon$ is always empty and is therefore omitted. While the
positive phase carry over the information of the last-seen
iso-variable, it is not noted explicitly as it is only needed when
calling the Iso Phase. The positive phase is given
in <ref>.

While  is presented in a one-sided way, we write
$\Sigma\vdash\Phi$ for $\vdash \Sigma^\bot, \Phi$ in order to stay
closer to the formalism of the type system of isos.

${\circu(\omega, S, \alpha, \beta)} = \pi$ takes a well-typed iso, a
singleton set $S$ of an iso-variable corresponding to the last
iso-variable seen in the induction definition of $\omega$ and two
fresh addresses $\alpha, \beta$ and produces a circular derivation
of the variant of  described above with back-edges.
$\circu(\omega, S, \alpha, \beta)$ is defined inductively on

* $\circu(\fix f. \omega, S, \alpha, \beta) = \circu(\omega, \set{f}, \alpha, \beta)$

* $\circu(f, \set{f}, \alpha, \beta) = \infer[be(f)]{[A_\alpha] ; \emptyset\vdash B_\beta}{}$

* $ \circu(\{(v_i\iso e_i)_{i\in I}\} : A\iso B, \set{f},
\alpha, \beta) = \stretchleftright{\llfloor}{\begin{array}{c}\infer{[A_\alpha];\emptyset\vdash^f
B_\beta}{\Foc{([v_i], \xi_i)_{i\in I}}}\end{array}}{\rrfloor}$ where $\xi_i$
is the typing derivation of $e_i$.

The translation $\pi = \circu(\omega, \emptyset, \alpha, \beta)$
of the iso $\omega$ from <ref>, with  $F =
A_{\alpha l}, G = B_{\alpha rl}, H = C_{\alpha rr}$ and $F' =
A_{\beta rl}, G' = B_{\beta rr}, H' = C_{\beta l}$ is:

0[𝕀][] ; a : F⊢F'
1[$\oplus^1$][] ; a : F ⊢F'⊕G'
1[$\oplus^2$][] ; a : F⊢H'⊕(F'⊕G')
1[ex(a)][F] ; ∅⊢H'⊕(F'⊕G')

0[𝕀][] ; b : G ⊢G'
1[$\oplus^2$][] ; b : G ⊢F'⊕G'
1[$\oplus^2$][] ; b : G ⊢H'⊕(F'⊕G')
1[ex(b)][G] ; ∅⊢H'⊕(F'⊕G')

0[𝕀][] ; c : H ⊢H'
1[$\oplus^1$][] ; c : H ⊢H'⊕(F'⊕G')
1[ex(c)][H] ; ∅⊢H'⊕(F'⊕G')

2[$\parr$][G⊕H]; ∅⊢H'⊕(F'⊕G')
2[$\parr$][F⊕(G⊕H)] ; ∅⊢H'⊕(F'⊕G')

and its corresponding proof $\ffloor{\pi}$ in :

Considering the iso swap of type $A\otimes B \iso B\otimes A$ defined as
$\opn{swap} = \{\pv {x}{y} \iso \pv{y}{x} \}$, its corresponding proof is the
proof $\pi_S$ given in <ref> whereas the iso
$\opn{map}(\opn{swap})$ as defined by <ref> have for corresponding
proof the proof $\phi(\pi_S)$ from <ref>. Notice that the
blue thread follows the focus of the structurally recursive criterion. The
negative phase consist of the $\nu, \with, \parr$ and $\bot$ rules,
where the pre-thread is going up, while the positive phase consist of
the multiple cut-rules where the pre-thread is not active.

\[ \begin{array}{rl}\infer{F_1\oplus F_2 :: \Upsilon ; \Theta\vdash G}{\Neg( \set{(\inl{v_j} :: l_j, \xi_j)_{j\in J}}
\cup \set{(\inr{v_k} :: l_k, \xi_k)_{k\in K}})} &= \\[2em]
\infer[\with]{F_1 \oplus F_2 :: \Upsilon; \Theta\vdash
G}{\infer{F_1 :: \Upsilon ; \Theta \vdash G}{\Neg(\set{(v_j ::
l_j, \xi_j)_{j\in J}})} \qquad \infer{F_2 :: \Upsilon ; \Theta
\vdash G}{\Neg(\set{(v_k :: l_k, \xi_k)_{k\in K}})}} \end{array}
\qquad\]

\[\scalebox{0.9}{$\begin{array}{c}\infer{[] ; \Theta \vdash
G}{\Neg(\set{([], \xi)})}\end{array} = \begin{array}{c}\infer{[] ; \Theta
\vdash G}{\Pos(\xi)}\end{array}$}
\qquad
\scalebox{0.9}{$\begin{array}{c}\infer{\one :: \Upsilon ; \Theta\vdash
G}{\Neg(\set{(() :: l, \xi)})}\end{array} = \begin{array}{c}\infer[\bot]{\one
:: \Upsilon; \Theta \vdash G}{\infer{\Upsilon ; \Theta \vdash
G}{\Neg(\set{l, \xi})}}\end{array}$}\]

\[ \scalebox{0.9}{$\begin{array}{c}\infer{F_1\otimes F_2 ::
\Upsilon ; \Theta\vdash G}{\Neg(\set{(\pv{v^1_i}{v^2_i} :: l_i,
\xi_i)_{i\in I}})}\end{array} = \hspace{0cm}
\begin{array}{c}\infer[\parr]{F_1\otimes F_2 :: \Upsilon ; \Theta
\vdash G}{\infer{F_1, F_2 :: \Upsilon ; \Theta \vdash
G}{\Neg(\set{(v_i^1 :: v_i^2 :: l_i, \xi_i)_{i\in
I}})}}\end{array}$} \]

\[ \scalebox{0.9}{$\begin{array}{c}\infer{\mu X. F :: \Upsilon ;
\Theta \vdash G}{\Neg(\set{(\fold{v_i} :: l_i, \xi_i)_{i\in
I}})}\end{array} =
\begin{array}{c}\infer[\nu]{\mu X. F :: \Upsilon ; \Theta\vdash
G}{\infer{F[X \leftarrow \mu X. F] :: \Upsilon ; \Theta\vdash
G}{\Neg(\set{(v_i :: l_i, \xi_i)_{i \in I}})}}\end{array}$}\]

\[\scalebox{0.9}{$\begin{array}{c}\infer{F :: \Upsilon ; \Theta
\vdash G}{\Neg(\set{(x :: l , \xi)})}\end{array} =
\begin{array}{c}\infer[ex(x)]{F :: \Upsilon ; \Theta \vdash
G}{\infer{\Upsilon ; \Theta, x : F \vdash G}{\Neg(\set{l,
\xi})}}\end{array}$} \]

Negative Phase

\begin{align*}
\myPos{\infer{\vdash_e () : \one}{}} &=
\begin{array}{c}\infer[\one]{[] ; \emptyset \vdash \one_\alpha}{}\end{array} \\[0.5em]
\myPos{\infer{x : A\vdash_e x : A}{}} &= \begin{array}{c}\infer[\id]{[]
; x : A_\alpha \vdash A_\beta}{}\end{array} \\
\myPos{\infer{\underline{\Theta} \vdash_e \inl{t} :
A_1\oplus A_2}{\infer{\underline{\Theta} \vdash_e t : A_1}{\xi}}} &=
\begin{array}{c}\infer[\oplus^1]{[] ; {\Theta} \vdash (A_1 \oplus A_2)_\alpha}{\infer{{\Theta}
\vdash (A_{1})_{\alpha l}}{\Pos(\xi)}}\end{array} \\
\myPos{\infer{\underline{\Theta} \vdash_e \inr{t} : A_1\oplus
A_2}{\infer{\underline{\Theta} \vdash_e t : A_2}{\xi}}} &=
\begin{array}{c}\infer[\oplus^2]{[] ; {\Theta} \vdash (A_1 \oplus A_2)_\alpha}{\infer{[] ;
{\Theta} \vdash (A_2)_{\alpha r}}{\Pos(\xi)}}\end{array} \\
\myPos{\infer{\underline{\Theta}_1,
\underline{\Theta}_2 \vdash_e \pv{t_1}{t_2} : A_1\otimes
A_2}{\infer{\underline{\Theta}_1 \vdash_e t_1}{\xi_1}\qquad
\infer{\underline{\Theta}_2\vdash_e t_2 : A_2}{\xi_2}}} &=
\begin{array}{c}\infer[\otimes]{[] ; {\Theta}_1,{\Theta}_2\vdash (A_1\otimes
A_2)_\alpha}{\infer{[] ; {\Theta}_1\vdash (A_1)_{\alpha l}}{\Pos(\xi_1)}\qquad\infer{[] ;
{\Theta}_2\vdash (A_2)_{\alpha r}}{\Pos(\xi_2)}}\end{array} \\
\myPos{\infer{\underline{\Theta} \vdash_e \fold{t} :
\mu X. A}{\infer{\underline{\Theta} \vdash_e t : A[X\leftarrow \mu X.
A]}{\xi}} } &= \begin{array}{c}\infer[\mu]{[]; {\Theta} \vdash (\mu X. A)_\alpha}{\infer{[] ;
{\Theta} \vdash (A[X\leftarrow \mu X. A])_{\alpha i}}{\Pos(\xi)}}\end{array} \\
\myPos{\infer{\underline{\Theta};\Psi\vdash_e
\omega~t : B}{\Psi\vdash_\omega \omega : A \iso
B\qquad\infer{\underline{\Theta}\vdash_e t : A}{\xi}}} &=
\begin{array}{c}\infer[\cut]{[] ; {\Theta}\vdash B_\beta}{\infer{[] ; {\Theta}\vdash
A}{\Pos(\xi)}\qquad\infer{[A] ; \emptyset\vdash
B_\beta}{\circu(\omega, \set{f}, \alpha, \beta)}}\end{array}
\end{align*}

\[
\begin{array}{rl}
\myPos{\infer{\underline{\Theta}_1,\underline{\Theta}_2\entaile
\letv{(x_i)_{i\in I}}{t_1}{t_2} :
B}{\infer{\underline{\Theta}_1\entaile t_1 : A_1\otimes\dots\otimes
A_n}{\xi_1}\qquad\infer{\underline{\Theta}_2, x_1 : A_1, \dots, x_n :
A_n\entaile t_2 : B}{\xi_2}}} &= \\[2em]
\infer[\cut]{[] ; {\Theta}_1,{\Theta}_2\vdash B_\alpha}{\infer{[] ;
{\Theta}_1\vdash F_1\otimes\dots\otimes
F_n}{\Pos(\xi_1)}\qquad\infer{[F_1\otimes\dots\otimes F_n] ;
{\Theta}_2\vdash B_\alpha}{\Foc{([(x_i)_{i\in I}], \xi_2)}}} \end{array}\]

Positive Phase

Given $\pi = \circu(\omega)$, for each infinite branch of $\pi$,
only a single iso-variable is visited infinitely often.

Since we have at most one iso-variable, we never end up in the case
that between an annotated sequent $\vdash^f$ and a back-edge pointing
to $f$ we encounter another annotated sequent.

Among the terms that we translate, the translation of a value yields
what we call a Purely Positive Proof: a finite derivation whose
only rules have for active formula the sole formula on the right of
the sequent. Any such derivation is trivially a valid pre-proof.

[Purely Positive Proof]

A Purely Positive Proof is a finite, cut-free proof whose
rules are only $\oplus^i, \otimes, \mu, \one, \textit{id}$ for

Given $x_1 : A^1, \dots, x_n : A^n\vdash v : A$ then $\begin{array}{c}\infer{[]; x_1
: A^1_{\alpha_1}, \dots, x_n : A^n_{\alpha_n}\vdash
A_\alpha}{\bbracket{v}}\end{array}$ is a purely positive proof.

By induction on $\Delta\vdash_e v : A$

* $x : A \vdash_e x : A$ then the derivation is
$\infer[\id]{[] ; F\vdash F}{}$, which is a purely positive proof;

* $\vdash () : \one$ then the derivation is $\infer[\one]{[]
; \emptyset \vdash \one}{}$, which is a purely positive proof;

* $\underline{\Delta_1}, \underline{\Delta_2} \vdash
\pv{v_1}{v_2} : A\otimes B$ then we get
$\begin{array}{c}\infer[\otimes]{[] ;\Delta_1,\Delta_2\vdash A\otimes
B}{\infer{\Delta_1\vdash A}{\pi_1}\qquad \infer{\Delta_2\vdash
B}{\pi_2}}\end{array}$ and then by induction hypothesis on $\pi_1$ and

* $\underline{\Delta}\vdash \inl{v} : A\oplus B$ then the
derivation is $\infer[\oplus^1]{[] ; \Delta\vdash A\oplus
B}{\infer{\Delta\vdash A}{\pi}}$ then by induction hypothesis on

* Similar for $\inr{v}$ and $\fold{v}$.

We can then define the notion of bouncing-cut and their origin:

A Bouncing-cut is a cut of the form:
$\infer[\cut]{\Sigma \vdash F}{\infer{\Sigma \vdash
G}{\pi}\qquad\infer[be(f)]{G \vdash F}{}}$

Due to the syntactical restrictions of the language we get the

Given a well-typed iso, every occurrence of a rule $be(f)$ in
$\ffloor{\circu(\omega)}$ is a premise of a bouncing-cut.

In particular, when following a thread going up into a
bouncing-cut, it will always start from the left-hand-side of
the sequent, before going back down on the right-hand-side of the
sequent. It will also always bounce back up on the bouncing-cut to
reach the back-edge.

[Term Occurrence]
We note by $Occ(v)$ the set of Occurrence in the value $v$
defined inductively on $v$ by:

* $Occ(v) = \{\epsilon\}$ if $v = x$ or $v = ()$

* $Occ(\pv{v_1}{v_2}) = \{\epsilon\} \cup l \cdot Occ(v_1)
\cup r \cdot Occ(v_2)$

* $Occ(\inl{v}) = \{\epsilon\}\cup l \cdot Occ(v)$

* $Occ(\inr{v}) = \{\epsilon\}\cup r \cdot Occ(v)$

* $Occ(\fold{v}) = \{\epsilon\} \cup i \cdot Occ(v)$

Where $x \cdot S = \{x\alpha \mid \alpha\in S\}$ for $x\in\{l,r,i\}$

Given $\alpha \in Occ(v)$ we write $v @ \alpha$ for the subterm
of $v$ at position $\alpha$

We write $\xi(v) = \{\alpha \in Occ(v) \alt v@\alpha = x\}$ for
the set of position of variables in $v$ and $\xi(x, v)$ for the
position of $x$ in $v$.

Given a sequence of sequents $S_0, \dots, S_n$, with $S_0 =
A_\alpha \vdash B_\beta$ and $S_n = \Sigma \vdash B_\beta$ and the
only rules applied are $\top, \with, \parr, \nu$.

There exists a unique value $v$ and context $\Delta$ such that
$\Delta \vdash_e v : A$ and such that for all expressions $e$ such
that $\Delta\vdash_e e : B$, for all isos $\vdash_\omega \omega :
A\iso B$ such that $v \iso e$ is a clause of $\omega$, consider
$\pi = \ffloor{\circu(\omega, \emptyset,\alpha,\beta)}$ then $S_0,
\dots, S_n$ is a branch of $\pi$ and for all formulas $A_\alpha
\in \Sigma$, there exists a unique variable $x$ such that $\xi(x,
v)$ is a suffix of $\alpha$.

By induction on $n$.

* Case $0$, then take $\Delta = x : A$ and $v = x$,
obviously $\Delta \vdash_e x : A$. We also get that $\omega =
\set{x\iso e}$ and $\ffloor{\circu(\omega)} = \infer{A_\alpha \vdash
B_\beta}{\ffloor{\Pos(e)}}$ so the empty sequence is a branch and
$\xi(v, v) = \epsilon$ which is a suffix of $\alpha$.

* Case $n+1$. By induction hypothesis, the sequence $S_0,
\dots, S_n$ with $S_n$ sequent of $\Sigma^n \vdash B_\beta$
gives us $\Delta^n \vdash_e v^n : A$. Define the values
contexts as $\mathcal{V} = [] \mid \pv{\mathcal{V}}{v} \mid
\pv{v}{\mathcal{V}} \mid \inl{\mathcal{V}} \mid
\inr{\mathcal{V}} \mid \fold{\mathcal{V}}$.

Then, by case analysis on the rule of $S_{n+1}$.

* $\parr$: we can write $\Sigma^n$ as $A^1_{\alpha_1},
\dots, (C_1\otimes C_2)^k_{\alpha_k}, \dots,
A^n_{\alpha_n} \vdash B_\beta$, and we know that $\Delta^n
= x_1 : A^1, \dots, x_k : C_1\otimes C_2, \dots, x_n : A^n$
then $v$ can be written as $\mathcal{V}[x_k]$.

Build $v^{n+1} = \mathcal{V}[\pv{y}{z}]$ and $\Delta^{n+1} = \Delta
\backslash \{x_k : C_1\otimes C_2\} \cup \set{y : C_1, z :

We get that $\Delta^{n+1} \vdash_e v^{n+1}$, then for any
iso $\omega$ such that $\mathcal{V}[x_k]\iso e$ is a
clause, we can replace the clause by
$\mathcal{V}[\pv{y}{z}] \iso e[x \leftarrow \pv{y}{z}]$ in
order to build $\omega'$, and if $S_0, \dots, S_n$ was a
branch in $\ffloor{\circu(\omega)}$ then so is $S_0,
\dots, S_n, S_{n+1}$ in $\omega'$.

We know that $\xi(x, v) = \gamma$ is a suffix of
$\alpha_k$, then after applying the $\parr$ rule we have
that $C_1$ has address $\alpha_k l$ and $C_2$ has
address $\alpha_k r$. Therefore, $\xi(y, v^{n+1}) =
\gamma~l$ and $\xi(z, v^{n+1}) = \gamma~r$ which are
respectively suffixes of $\alpha_k l$ and $\alpha_k r$.

* $\with$. Assuming that $S_{n+1}$ goes to the left
branch of the $\with$ rule.

We then have $\Sigma^n = A^1_{\alpha_1}, \dots, (C_1\oplus
C_2)^k_{\alpha_k}, \dots, A^n_{\alpha_n} \vdash B_\beta$
and $\Delta^n = x_1 : A^1, \dots, x_k : C_1\oplus C_2,
\dots, x_n : A^n$ with $v = \mathcal{V}[x_k]$.

Consider $v^{n+1} = \mathcal{V}[\inl{y}]$ and $\Delta^{n+1}$.

For any iso $\omega$ where $v^n \iso e$ was a clause, we
can consider the isos $\omega'$ where the clause $v^n \iso
e$ has been replaced by two clauses $\mathcal{V}[\inl{y}]$
and $\mathcal{V}[\inr{r}]$ with $e[x \leftarrow y]$ and
$e[x\leftarrow z]$. $S_0, \dots, S_n, S_{n+1}$ is
obviously a branch in $\ffloor{\circu(\omega)}$ by
definition of the negative phase.

Also since $\xi(x, v) = \gamma$ is a suffix of $\alpha_k$,
after applying the $\with$ rule, on the left branch we get
$C_1$ with address $\alpha_k l$. And $\xi(y, v^{n+1}) =
\gamma~l$ is a suffix of $\alpha_k l$.

* The other side of the $\with$ is similar.

* The $\nu$ rule is similar.

* $\top$. In which case we have $\Sigma^n =
\one_{\alpha}, A^1_{\alpha_1} \dots, A^n_{\alpha_n}$ with
$\Delta^n = x : \one, x_1 : A^1, \dots, x_n : A^n$ with
$v^n = \mathcal{V}[x]$, build $v^{n+1}$ as
$\mathcal{V}[()]$ and $\Delta^{n+1} = x_1 : A^1, \dots,
x_n : A^n$. Then after the $\top$ rule we get
$\Gamma^{n+1} = A^1_{\alpha_1}, \dots, A^n_{\alpha_n}$ so
the property holds by our induction hypothesis.

We can now show that our translation is well-defined:

Given a closed iso $\vdash_\omega \omega$ then $\circu(\omega,
\emptyset, \alpha, \beta)$ for $\alpha, \beta$ fresh addresses, is

By induction on $\vdash_\omega$. The iso is of the form $\fix f_1.
\dots, \fix f_n. \isobasique$ and as only the last iso-variable is
kept, we end up in the case $\circu(\{(v_i\iso e_i')_{i\in I}\} :
A\iso B, \set{f_n}, \alpha, \beta)$, where the root of the
derivation take place, annotated with $f_n$.

The negative phase $\Neg(([v_i], \xi_i')_{i\in I})$ is
well-defined due to the predicate $\PE_A$: by definition of
$\PE_A$ all left-hand-side values have the same type constructors,
they also have the same type.

The positive phase is well-defined as it consists in recreating the
typing judgment of each expression $e_i$. By <ref>
we know that the typing context of $e_i$ and the one obtained from
the negative phase contain the same variable associated to the
same formula / formula occurrence.

Given an iso $\omega = \fix f. \isobasique$, we want to show that for
any infinite branch there exists a valid thread that inhabits it. As
given by <ref>, an infinite branch is uniquely
defined by a single iso-variable.

Given the value $v_i^j$ that is the decreasing argument for the
structurally recursive criterion, we want to build a pre-thread that
follows the variable $x_j : \mu X. B$ in $v_i^j : \mu X. B$ that is
the focus of the criterion.

Since our sequents are different from the one of  during the negative
phase, we are forced to define properly the way the pre-thread is built. Whereas
for the positive phase, our sequents and the one of  are the same,
aside from the fact that the context also contains variables, so for this part
the thread is created in the same way as in <cit.>.

[Pre-Thread of the negative phase]

Given a well-typed iso
$\omega = \fix f. \isobasique : A\iso B$
and a clause $v_i \iso e_i$ such that $f~p$ is a subterm of $e_i$
and the variable $x^p$ is the focus of the primitive recursive
criterion, and considering $\pi = \circu(\omega)$, we define
$PT_n(x^p, \pi)$ as the pre-thread that follow the formula $\mu X.
A'$ corresponding to $x^p$ up to the positive phase by induction
on $\Foc{\{([v_i], e_i)_{i\in I}\}}$. For simplicity, we simply
omit the first argument of $PT_n$.

* $PT_n(\Foc{\{([], e)\}})$ is impossible as we follow a

* $PT_n(\Foc{\{((()::l, e))\}}) = PT_n(\Foc{\{(l, e)\}})$;

* $PT_n(\Foc{\{((y::l, e))\}}) = \begin{cases}
\epsilon & \text{ if } y = x^p \\
PT_n(\Foc{\{(l, e)\}}) & \text{ otherwise;} \end{cases}$

* $PT_n(\Foc{\{(\inl{v_i} :: l_i, e_i)_{i\in I}\} \cup
\{(\inl{v_j} :: l_j, e_j)_{j\in J}\}})$

$= \left\{\begin{array}{l} (A\oplus
C; A\oplus C, \Delta\vdash B)\cdot (A; A, \Delta\vdash B) \cdot
PT_n(\Foc{\{(v_i :: l_i, e_i)_{i\in I}\}}) \\ \qquad \text{ if } x^p
\subseteq v_i \\
(C\oplus A; C\oplus A, \Delta\vdash B)\cdot (A; A, \Delta\vdash
B) \cdot PT_n(\Foc{\{(v_j :: l_j, e_j)_{j\in J}\}}) \\ \qquad
\text{ if } x^p \subseteq v_j \\
(\mu X. D; A_1\oplus A_2, \Delta\vdash B) \cdot (\mu X. D, A_k,
\Delta \vdash B) \cdot PT_n(\Foc{\{(v_l :: l_l, e_l)_{l \in
L}\}}) \\ \qquad \text{ for } L \in \{I, J\}, k\in\{1,2\} \text{
and if } x^p \subset l_L\\
\end{array}\right.$

* Case $PT_n(\Foc{\{(v_i^1, v_i^2 :: l_i, e_i)_{i\in I}\}})$

$= \left\{\begin{array}{l} (A_1\otimes A_2; A_1\otimes
A_2,\Delta\vdash B)\cdot (A_k; A_1, A_2, \Delta\vdash B) \cdot
PT_n(\Foc{\{(v_i^1, v_i^2 :: l_i, e_i)_{i\in I}\}}) \\ \qquad
\text{ for } k \in \{1,2\} \text{ if } x^p \subset v_k \\
(\mu X. D; A_1\otimes A_2, \Delta\vdash B) \cdot (\mu X. D;
A_1,A_2,\Delta\vdash B) \cdot PT_n(\Foc{\{(v_i^1, v_i^2 :: l_i,
e_i)_{i\in I}\}}) \\ \qquad \text{ if } x^p \subseteq l
\end{array}\right.$

* $PT_n(\Foc{\{(\fold{v_i} :: l_i, e_i)_{i\in I}\}})$

$= \begin{cases} (\mu X. A; \mu X. A, \Delta\vdash B) \cdot
(A[X\leftarrow \mu X. A]; A[X\leftarrow \mu X. A], \Delta\vdash
B) & \text{ if } x^p \subset v_i \\
(\mu X. D; \mu X. A, \Delta\vdash B) \cdot (\mu X. D;
A[X\leftarrow \mu X. A], \Delta\vdash B) & \text { if } x^p
\subset l_i \end{cases}$

Given a well-typed iso $\omega = \fix f. \omega$ with a clause $v \iso e$, then
$w(PT_n(\Neg(\set{([v], e)})))$ is a word over $\{l,r,i,\mathcal{W}\}$.

By case analysis of <ref>:

* If the variable $x^p$ is not a subterm of the first value
from the list $l$ then the thread has the form:$(A;C,\Delta\vdash
B, \uparrow)\cdot (A; C',\Delta\vdash B, \uparrow)$ and the weight is

* If the variable $x^p$ is a subterm of the first value of the
list $l$ then by direct case analysis on the first value: if the
value is of form $\pv{v_1}{v_2}$ then depending on whether $x^p$
is in $v_1$ or $v_2$ the weight will be $l$ or $r$, similarly for
the $\inl{}$ and $\inr{}$, while the $\fold{}$ will create weight

A similar analysis can be done for the positive phase:
[Pre-thread of the positive phase]

Given a well-typed iso

$\omega = \fix f. \isobasique : A\iso B$ and a
clause $v_i \iso e_i$ such that $f~p$ is a subterm of $e_i$ and the
variable $x^p$ is the focus of the primitive recursive criterion, and
considering $\pi = \circu(\omega, S, A_\alpha, B_\beta)$, then we
define $PT_p(x^p, \Pos(e_i))$ as the pre-thread that follow the
formula $\mu X. A'$ corresponding to $x^p$ until the sequent
$A_{\alpha'}\vdash^f B_{\beta'}$ is reached. For simplicity, we also
just write it as $PT_p(x^p)$.

Shape of the pre-thread of the positive phase
Given a well-typed iso $\omega$ such that the variable $x^p$ is
the focus of the primitive recursive criterion, and two successive
elements $a, b$ from the pre-thread $PT(x^p)$ from the translation
of $\omega$, then $a \cdot b$ are of either:

* $(\nu X. F; s; \up) \cdot (\nu X. F; s'; \up)$;

* $((\nu X. A)_\alpha; (\nu X. A)_\alpha\vdash (\nu X.
A)_\beta; \up) \cdot ((\nu X. A)_\beta; (\nu X.
A)_\alpha\vdash (\nu X. A)_\beta; \down)$;

* $(F ; s ; \down) \cdot (F'; s'; \down)$;

* $(F ; s ; \down) \cdot (F ; s' ; \up)$

By a straightforward case analysis on the positive phase:

* If a right-rule is applied while the pre-thread is on
the left side of the sequent, then we are in the first case as
the thread just goes up while following the formula.

* The second case occurs when encountering an axiom rule
on the variable $x^p$ that we follow.

* The third case is when going down on a purely positive
proof. As we follow the sole formula on the right, the formula
necessarily changes and $s, s'$ are of the shape $\Delta
\vdash s, \Delta'\vdash s'$.

* The last one is when encountering a cut, at the root of
the purely positive proof that comes from the translation of a

We can now look at the weight of the positive phase:

Given a well-typed iso such that the variable $x^p$ is the focus of
the primitive recursive criterion, the weight of the pre-thread on the
positive phase $PT_p(x^p)$ is of the shape $\mathcal{W}^*
\mathcal{A}\{\overline{l}, \overline{r}, \mathcal{W}\}^* \mathcal{C}$

By case analysis on $\Pos(e)$. As the thread only goes up by
encountering cut-rules or right-rules, we get $\mathcal{W}^*$, and
the thread goes up all the way to an axiom rule, corresponding to
the formula $x^p : \nu X. F$, which adds the $\mathcal{A}$.
Finally, the thread goes down on the purely positive proof,
generating $\{\overline{l}, \overline{r}, \mathcal{W}\}^*$ until
reaching the cut-rule from the bouncing cut.

We can then consider the infinite pre-thread as the concatenation of
both the pre-thread of the negative phase, and the one of the positive

Given the pre-thread $t$ following $x^p$ we have that $w(t) = p_0
(\Sigma_{i\leq n} p_i \mathcal{W}_i^* \mathcal{A} q_i
\mathcal{C})^\omega$ with

* $p_0$ is any prefix.

* $p_i \in \{l,r,i, \mathcal{W}\}^*$

* $q_i \in \{\overline{l}, \overline{r}, \mathcal{W}\}^*$

With, $\forall i\leq n, \overline{q_i} \sqsubset
\overline{\overline{p_i}}$ and $\mid p_i \mid > \mid q_i \mid$
without counting the $\mathcal{W}$, where $p \sqsubset q$ is $q$
is a prefix of $p$ and with $\overline{xp} =
\overline{x}\overline{p}$ if $x\in\{l,r,i\}$,
$\overline{\overline{x}p} = x\overline{p}$ if $x\in \{l, r, i\}$
and $\overline{\mathcal{W}p} = \overline{p}$

$p_i$ is generated from <ref> while the rest up to the $C$
(included) is generated from <ref>.

First, we show that $\mid p_i \mid > \mid q_i \mid$ modulo the

Since $p_i$ is generated by the negative phase, we have that,
modulo $\mathcal{W}$, $p_i = \{r\}^*l^+ \{l,r,i\}^*$, this is due
by definition of being primitive recursive and because we are
looking for the right variable. By definition of being primitive
recursive the input type of the iso is $A_1 \otimes \dots \otimes
A_n$, hence $\{r\}^*l^+$ correspond to the search for the correct
$A_i$ for the input type $A_1\otimes \dots\otimes A_n$ while
$\set{l,r,i}^*$ is the decomposition of the primitive recursive
value, as described in <ref>.

As $q_i$ corresponds to the Purely Positive Proof, we know that
the Purely Positive Proof is the encoding of a pattern $p =
\pv{x_1}{\pv{\dots}{x_n}}$. Hence, $q_i$ can be decomposed as
$\{\ov{l}^+ \ov{r}^*\}$

By the fact that the iso is primitive recursive we know that the
variable in $p$ is a strict subterm of the primitive recursive
value, hence $\mid p_i \mid > \mid q_i \mid$.

The fact that $\overline{q_i} \sqsubset \overline{\overline{p_i}}$
is direct as the Purely Positive Proof reconstructs the type $A_1
\otimes \dots \otimes A_n$ without modifying the $A_i$ while
$\overline{\overline{p_i}}$ start by searching for the
corresponding type $A_i$, so it is only composed of $\{l, r\}^*$,
which will be the same as $\overline{q_i}$.

We want to find a decomposition of the pre-thread such that it can
uniquely be decomposed into $\bigodot (H_i \odot V_i)$ with

* $w(V_i) \in \{l, r, i, \mathcal{W}\}^\infty$ and non-empty
if $i \not= \lambda$

* $w(H_i) \in \mathcal{H}$

We set $H_0$ as the empty pre-thread. (so $w(H_0) = \epsilon$) We
set $V_0$ as the maximal possible sequence such that $w(V_0) \in
\{l,r,i, \mathcal{W}\}^*$, i.e. the sequence that ends with $(A;
A\vdash A; \up)$. Then, for all $i\geq 1$ we set

* $H_i$ starts at $(A; A\vdash A; \up)$ just before the axiom
rule so that the first element of $w(H_i)$ is $A$. Then $H_i$ is
composed of

* All of the pre-thread going down on the Purely Positive
Proof after the axiom, accumulating a word over
$\{\overline{l},\overline{r}, \overline{i}, \mathcal{W}\}^*$;

* Going back up into the cut-rule of the bouncing cut,
making a $\mathcal{C}$;

* Going up to compensate every $\overline{x}$ seen in the
Purely Positive Proof while going down. This is possible as
shown in <ref>.

* $V_i$ is the maximal possible sequence such that $w(V_i) \in
\{l,r,i, \mathcal{W}\}^*$, i.e. the sequence that ends with $(A;
A\vdash A; \up)$.

$~\vdash_\omega \omega : A\iso B$ and $\pi = \ffloor{\circu(\omega,
\emptyset, \alpha, \beta)}$ then $\pi$ satisfies  validity
criterion from <cit.>.

By <ref> we know that we have a thread of
which we also know by <ref> that the visible
part is not stationary.

Finally, by <ref> and <ref> we know that
the visible part will see infinitely often the subformulas of the formula $\mu
X. B$ that is the focus of the primitive recursive criterion. This is due to
the difference in size in the part of the thread from the negative and from
the positive phase and the fact that the positive phase does not encounter a
$\mu$ formula when going down on a purely positive proof.

Concerning the additives slices <cit.>, one can
notice that every slice of our language is necessarily persistent as the
only possible occurrences of $\with$ rules are during the negative phase,
then by going down a b-path the path will stay on a formula on the
left-hand-side of the sequent, never changing size and never entering a purely
positive proof, where the occurrences of rules $\oplus^i$ are.

Therefore, the smallest formula we will encounter is $\nu$
formula, validating the thread.

§.§ Proof Simulation

In order to show the relationship between the cut-elimination
procedure of  and the rewriting system of our language we
introduce a slightly modified version of the rewriting system, that we
call $\expB$, using explicit substitution.

We fix the following convention: given a substitution $\sigma =
\set{x_1\mapsto v_1, \dots, x_n\mapsto v_n}$ we use the shorthand
$\letsig{\sigma}{t}$ for $\letv{x_1}{v_1}{\dots \letv{x_n}{v_n}{t}}$.

[Explicit Substitution Rewriting System]
$\expB$ is defined by the following rules:

\begin{align*}
\letv{x}{v}{x} &\expLet v \\
\letv{\pv{x_1}{p}}{\pv{t_1}{t_2}}{t} &\expLet \letv{x_1}{t_1}{\letv{p}{t_2}{t}}\\
\letv{x}{v}{\pv{t_1}{t_2}} &\expLet \pv{\letv{x}{v}{t_1}}{t_2} &&\text{when } x\in FV(t_1) \\
\letv{x}{v}{\pv{t_1}{t_2}} &\expLet \pv{t_1}{\letv{x}{v}{t_2}} &&\text{when } x\in FV(t_2) \\
\letv{x}{v}{\inl{t}} &\expLet \inl{\letv{x}{v}{t}} \\
\letv{x}{v}{\inr{t}} &\expLet \inr{\letv{x}{v}{t}} \\
\letv{x}{v}{\fold{t}} &\expLet \fold{\letv{x}{v}{t}} \\
\letv{x}{v}{\omega~t} & \expLet \omega~\letv{x}{v}{t}
\end{align*}

and the following rules:

\[
\begin{array}{c}
\infer[\beta-\mathrm{Cong}]{C[t]\expB C[t']}{t_{\expB\cup\expLet} t'}
\qquad
\infer[\beta-\mathrm{LetE}]{\letv{p}{v}{t}\expB\letsig{\sigma}{t}}{\sigma[p] = v}
\\[1.5ex]
\infer[\beta-\mathrm{IsoRec}]{
(\fix f.\isoterm) \expB \omega[f \leftarrow (\fix f. \omega)]
\infer[\beta-\mathrm{IsoApp}]{\isobasique~v' \expB \letsig{\sigma}{e_i}}{\sigma[v_i] = v'}
\end{array}
\]

The rule $\beta-\mathrm{LetE}$ is superfluous as it can be inferred
from the decomposition of the rule of the decomposition of a

Each step of this rewriting system will correspond to exactly one step
of cut-elimination, while in the previous system, the rewriting that
uses a substitution $\sigma$ correspond in fact to multiple steps of
cut-elimination. $\expB$ makes this explicit. But first, we need to
make sure that both systems do the same thing:

Let $\sigma$ be a substitution that closes $\Delta \vdash_e
\pv{t_1}{t_2}$, then there exists $\sigma_1, \sigma_2$, such that
$\sigma(\pv{t_1}{t_2}) = \pv{\sigma_1(t_1)}{\sigma_2(t_2)}$ Where
$\sigma = \sigma_1 \cup \sigma_2$.

By the linearity of the typing system we know that $FV(t_1) \cup
FV(t_2) = \emptyset$, so there always exists a decomposition of
$\sigma$ into $\sigma_1, \sigma_2$ defined as $\sigma_i = \{(x_i
\mapsto v_i) \mid x_i \in FV(t_i)\}$ for $i\in\{1,2\}$.

Let $\sigma = \{x_i \mapsto v_i\}$ be a substitution that closes $t$,
then $\letsig{\sigma}{t} \expLet^* \sigma(t)$.

By induction on $t$.

* $x$, then $\sigma(x) = v$ and $\letv{x}{v}{x} \expLet v = \sigma(x)$.

* $()$ then $\sigma$ is empty and no substitution applies.

* $\pv{t_1}{t_2}$, then by <ref>
$\sigma(\pv{t_1}{t_2}) = \pv{\sigma_1(t_1)}{\sigma_2(t_2)}$. By
$\expLet$, each $\lett$ construction will enter either $t_1$ or
$t_2$, then by induction hypothesis.

* $\letv{p}{t_1}{t_2}$ is similar to the product case.

* $\inl{t}, \inr{t}, \fold{t}, \omega~t$. All cases are
treated in the same way: by definition of $\expLet$, each
$\lett$ will enter into the subterm $t$, as with the
substitution $\sigma$, then by induction hypothesis.

If $t\to t'$ then $t\expB^* t'$.

By induction on $\to$, the case of $\mathrm{IsoRec}$ is the same, while for
the other rules, just by applying either $\beta-\mathrm{IsoApp}$ or
$\beta-\mathrm{LetE}$ and then by <ref>, $\letsig{\sigma}{t}
\expLet^* \sigma(t)$ for any substitution $\sigma$ that closes $t$. But
$\sigma(t) = t'$, so $t\expB^* t'$.

It is then possible to show a first step of the simulation procedure:
that $\expB$ corresponds to one step of cut-elimination:

Let $\underline{\Theta} \vdash_e t : G$ be a well-typed closed
term: if $t\expLet t'$ then, given some fresh address $\beta$ we
get: $\begin{array}{c}\infer{\Theta\vdash G_\beta}{\ffloor{\Pos(t)}}\end{array} \cute
\begin{array}{c}\infer{\Theta\vdash G_\beta}{\ffloor{\Pos(t')}}\end{array}$.

By case analysis on , for simplicity of reading we omit the
address $\beta$.

* $\letv{x}{v}{x} \expLet v$.

$\begin{array}{c}\infer[\cut]{\Theta \vdash G}{\infer{\Theta \vdash
G}{\ffloor{\Pos(v)}} \qquad \infer[\id]{G\vdash G}{}}\end{array} \cute
\begin{array}{c}\infer{\Theta \vdash G}{\ffloor{\Pos(v)}}\end{array}$

* $\letv{\pv{x_1}{p}}{\pv{t_1}{t_2}}{t} \expLet
\letv{x_1}{t_1}{\letv{p}{t_2}{t}}$.

Then: $\infer[\cut]{\Theta_1,\Theta_2, \Theta_3\vdash
H}{\infer[\otimes]{\Theta_1,\Theta_2\vdash G\otimes
F}{\ffloor{\Pos(t_2)}}}\qquad \infer[\parr]{\Theta_3, G\otimes F\vdash
F}{\infer{\Theta_3, G, F\vdash H}{\ffloor{\Neg(\set{[p], t})}}}}$

([p], t)
2[]Θ_2,Θ_3, G⊢H

* $\letv{x}{v}{\inl{(t)}} \expLet \inl{(\letv{x}{v}{t})}$.

Then: $\begin{array}{c}\infer[\cut]{\Theta_1, \Theta_2 \vdash H\oplus
G}{\infer{\Theta_1 \vdash
F}{\ffloor{\Pos(v)}}\qquad\infer[\oplus^1]{F, \Theta_2 \vdash
H\oplus G}{\infer{F, \Theta \vdash H}{\ffloor{\Pos(t)}}}}\end{array} \cute
\begin{array}{c}\infer[\oplus^1]{\Theta_1, \Theta_2\vdash H\oplus
G}{\infer[\cut]{\Theta_1,\Theta_2\vdash H}{\infer{\Theta_1 \vdash
F}{\ffloor{\Pos(v)}}\qquad\infer{F, \Theta_2 \vdash H}{\ffloor{\Pos(t)}}}}\end{array}$

* The same goes for $\letv{x}{v}{\inr{(t)}} \expLet
\inr{(\letv{x}{v}{t})}$ and $\letv{x}{v}{\fold{(t)}}\expLet
\fold{(\letv{x}{v}{t})}$

* $\letv{x}{v}{\pv{t_1}{t_2}}\expLet\pv{\letv{x}{v}{t_1}}{t_2}$
when $x\in FV(t_1)$.

$\begin{array}{c}\infer[\cut]{\Theta_1, \Theta_2, \Theta_3 \vdash H\otimes
G}{\infer{\Theta_1 \vdash F}{\ffloor{\Pos(v)}}\qquad
\infer[\otimes]{F, \Theta_2, \Theta_3 \vdash H\otimes
G}{\infer{F, \Theta_2\vdash H}{\ffloor{\Pos(t_1)}}\qquad
\infer{\Theta_3\vdash G}{\ffloor{\Pos(t_2)}}}}\end{array}$

\begin{array}{c}\infer[\otimes]{\Theta_1,\Theta_2,\Theta_3\vdash H\otimes
G}{\infer[\cut]{\Theta_1,\Theta_2\vdash H}{\infer{\Theta_1\vdash
F}{\ffloor{\Pos(v)}} \qquad \infer{F, \Theta_2\vdash
H}{\ffloor{\Pos(t_1)}}} \qquad \infer{\Theta_3\vdash

* Similar for the second rule on the pair.

* $\letv{x}{v}{\omega~t} \expLet \omega~(\letv{x}{v}{t})$.

1F, Θ_2⊢G

2[]F, Θ_2⊢H
2[]Θ_1, Θ_2⊢H

$\cute \begin{array}{c}\infer[\cut]{\Theta_1,\Theta_2\vdash
H}{\infer[\cut]{\Theta_1,\Theta_2\vdash G}{\infer{\Theta_1\vdash
F}{\ffloor{\Pos(v)}}\qquad\infer{F, \Theta_2\vdash

We then show that the pattern-matching is captured by the

Let $\Gamma \vdash_e v : A$ and $\Delta \vdash_e v' : A$ such that
$\sigma[v] = v'$ and $\sigma = \set{\overrightarrow{x_j} \mapsto
\overrightarrow{w_j}}$ then for any list $l = [v_1, \dots, v_n]$
where for all $i\in\set{0, \dots, n}$ there exists $\Gamma_i$ such
that $(\Gamma_i \vdash_e v_i)$ and such that $\PE_{A}(\set{v, v_1,
\dots, v_n})$ and for all $i\in\set{0, \dots, n}$ and $e_1,\dots,
e_n$ such that $(\Gamma_i \vdash_e e_i : B)$ and such that
$\PE_B(\set{Val(e_1), \dots, Val(e_n)})$ and given $\Theta = \{x :
A_\alpha \mid x : A \in \Delta \}$ and $G = B_\beta$ we have:

$\pi = \begin{prooftree}

\hypo{\ffloor{\Pos(v')}}
\infer1{\Theta\vdash H}

\hypo{\ffloor{\Neg(\set{((v :: l)_i, e_i)_{i\in I}})}}
\infer1{H\vdash G}
\infer2[\cut]{\Theta\vdash G}
\end{prooftree} \cute^*
\infer{\Theta\vdash G}{\ffloor{\Neg(\set{l,
\letv{\overrightarrow{x_i}}{\overrightarrow{w_i}}{e}})}} = \pi'$

By induction on $\PE_A(\set{v, v_1, \dots, v_n})$:

* Case $\PE_A(\set{x})$ we get $\sigma[x] = v$ then $\pi =
\pi'$.

* Case $\PE_\one(\set{\one})$ then $\sigma[()] = ()$.

$\pi = \begin{array}{c}       \begin{prooftree}

\infer0[$\one$]{\vdash \one}

\hypo{\ffloor{\Pos(e)}}
\infer1{\vdash G}
\infer1[$\bot$]{\one\vdash G}
\infer2[\cut]{\vdash G}
\end{prooftree}\end{array}$ which reduces to $\begin{array}{c}\infer{\vdash
G}{\ffloor{\Pos(e)}}\end{array} = \pi'$ as $\sigma$ is empty.

* Case $\PE_{\mu X. A}(\set{\fold{v_i}})$ such that
$\sigma[\fold{v_j}] = \fold{v'}$.

Then $\pi = \begin{array}{c}\infer[\cut]{\Theta\vdash G}{\infer{\Theta\vdash
\mu X. H}{\infer[\mu]{\Theta\vdash H[X \leftarrow \mu X.
H]}{\ffloor{\Pos(v')}}} \qquad \infer{\mu X. H \vdash
G}{\infer[\nu]{H[X\leftarrow \mu X. H] \vdash
G}{\ffloor{\Neg(\set{[v_i], e_i})}}}}\end{array}$

will reduce to

$\begin{array}{c}\infer[\cut]{\Theta\vdash G}{\infer{\Theta\vdash H[X \leftarrow \mu
X. H]}{\ffloor{\Pos(v')}} \qquad \infer{H[X\leftarrow \mu X. H]
\vdash G}{\ffloor{\Neg(\set{([v_i], e_i)})}}}\end{array}$

then we can apply our induction hypothesis.

* Case $\PE_{A\oplus
B}(\set{\inl{v_i}}\cup\set{\inr{v_k}})$ with
$\sigma[\inl{v_j}] = \inl{v'}$

Then the proof
$\pi = \begin{prooftree}
\hypo{\ffloor{\Pos(v')}}
\infer1{\Theta\vdash H}
\infer1[$\oplus^1$]{\Theta\vdash H\oplus F}

\hypo{\ffloor{\Neg(\set{[v_i], e_i})}}
\infer1{H\vdash G}

\hypo{\ffloor{\Neg(\set{[v_k], e_k})}}
\infer1{F\vdash G}
\infer2[$\with$]{H\oplus F\vdash G}
\infer2[\cut]{\Theta\vdash G}
\end{prooftree}

reduces to

([v_i], e)

then we can apply our induction hypothesis.

* The case $\sigma[\inr{v_j}] = \inr{v'}$ is similar to the
previous case.

* Case $\PE_{A\otimes B}(\set{\pv{v_i^1}{v_i^2}})$ with
$\sigma[\pv{v_j^1}{v_j^2}] = \pv{v_1'}{v_2'}$.

Then $\pi = \begin{prooftree}

\hypo{\ffloor{\Pos(v_1')}}
\infer1{\Theta_1\vdash H}

\hypo{\ffloor{\Pos(v_2')}}
\infer1{\Theta_2\vdash F}
\infer2[$\otimes$]{\Theta_1,\Theta_2\vdash H\otimes F}

\hypo{\ffloor{\Neg(\set{([\pv{v_1, v_2}_i], e_i)_{i\in I}})}}
\infer1{H, F\vdash G}
\infer1[$\parr$]{H\otimes F\vdash G}
\infer2[\cut]{\Theta_1,\Theta_2\vdash G}
\end{prooftree}$

Which reduces to

(((v_1 :: v_2 :: l)_i,
1H, F⊢G
2[]Θ_2, H⊢G

Because the negative phase on $[v_1, v_2]$ only produces
$\with, \parr, \top, \nu$ rules, we get that $\Neg(\set{(v1 ::
v2 :: l, e)}) = \Neg(\set{(v2 :: v1 :: l, e)})$
by the
commutation of rules of Linear Logic. Therefore, we can get

(((v_2 :: v_1 :: l)_i,
1H, F⊢G
2[]Θ_2, H⊢G

which, by induction hypothesis on $v_2$, reduces to

(((v_1 :: l)_i,

And then we can apply our second induction hypothesis on

We can then conclude with the global simulation theorem as a direct
implication of the two previous lemmas:

Let $\isobasique~v \to \sigma(e_i)$ when $\sigma[v_i] = v$ then
$\ffloor{\Pos(\isobasique~v)} \cute^*
\ffloor{\Pos(\letv{x_j}{v_j}{e_i})} \cute^*
\ffloor{\Pos(\sigma(e_i))}$ when $\sigma =\{x_j\mapsto v_j\}$

By <ref>, we know that the explicit substitution and
the substitution coincide. <ref> tells us that one step
of $\expLet$ is simulated by exactly one step of cut-elimination and
finally <ref> tells us that we
simulate properly the pattern-matching.

Provided an iso $\vdash_\omega \omega : A\iso B$ and values $\vdash_e
v : A$ and $\vdash_e v' : B$, let $\pi = \ffloor{\Pos(\omega~v)}$ and
$\pi' = \ffloor{\Pos(v')}$, if $\omega~v\to^* v'$ then $\pi\cute^*
\pi'$.

Direct application of <ref>.

This leads to the following corollary:

Given a well-typed iso $\vdash_\omega \omega : A\iso B$ and two
well-typed close value $v_1$ of type $A$ and $v_2$ of type $B$ and the
proofs $\pi : F_1\vdash G_1$, $\pi^\bot : G_2\vdash F_1$, $\phi :
F_3$, $\psi : G_2$ corresponding respectively to the translation of
$\omega, \omega^\bot, v_1, v_2$ then:

\[ \scalebox{0.8}{$\infer{\vdash F_3}{\phi}~
\rotatebox[origin=c]{180}{$\rightsquigarrow$}
\infer[\cut]{\vdash F_2}{\infer[\cut]{\vdash G_1}{\infer{\vdash
G_1}{\pi}}\qquad\infer{G_2\vdash F_2}{\pi^\bot}} \qquad
\infer[\cut]{\vdash G_1}{\infer[\cut]{\vdash F_2}{\infer{\vdash
G_2}{\pi^\bot}}\qquad\infer{F_1\vdash G_1}{\pi} }
\rightsquigarrow \infer{\vdash G_3}{\psi}$} \]

As a direct implication of <ref>
and <ref>.

§ CONCLUSION

Summary of the contribution.

We presented a linear, reversible language with inductive types. We showed how
ensuring non-overlapping and exhaustivity is enough to ensure the reversibility
of the isos. The language comes with both an expressivity result that shows that
any Primitive Recursive Functions can be encoded in this language as well as an
interpretation of programs into  proofs. The latter result rests on the
fact that our isos are structurally recursive.

Future works.

We showed a one-way encoding from isos to proofs of , it is clear that
there exist proof-isomorphisms of  that do not correspond to an iso of
our language. Therefore, a first extension to our work would be to relax the
different constraints to allow for more functions to be encoded. For instance,
the Cantor Pairing $\natT \iso \natT\otimes \natT$ can be encoded as (with $0 =
\fold{(\inl{()})}$ and $S~x = \fold{(\inr{(x)})}$):
[Cantor Pairing]

\[\scalebox{1}{$\omega_1 = \left\{
\begin{array}{l@{~}c@{~}l}
\pv{S~i}{j} & {\iso} & \inl{(\pv{i}{S~j})}\\
\pv{0}{S~S~j} & {\iso} & \inl{(\pv{S~j}{0})} \\
\pv{0}{S~0} & {\iso} &  \inl{(\pv{0}{0})}\\
\pv{0}{0} & {\iso} & \inr{()} \\
\end{array}
\right\} : \natT\otimes\natT \iso (\natT\otimes\natT) \oplus\one$}\]

\[\scalebox{1}{$\omega_2 = \left\{
\begin{array}{l@{~}c@{~}l}
\inl{(x)} & {\iso} & \letv{y}{g~x}{S~y}\\
\inr{(())} & {\iso} & 0 \\
\end{array}
\right\} : (\natT\otimes\natT) \oplus\one \iso \natT$}\]

\[\scalebox{1}{$\opn{Cantor Pairing} = \fix g. \left\{
\begin{array}{l@{~}c@{~}l}
x & {\iso} & \letv{y}{\omega_1~x}{}\\
&  & \letv{z}{\omega_2~y}{z} \\
\end{array}
\right\} : (\natT\otimes\natT) \iso \natT$}\]

Then, consider its associated proofs $\pi, \pi_{\omega_1}, \pi_{\omega_2}$,
given in <ref>, of (respectively) the
Pairing}$, $\omega_1$ and $\omega_2$ isos.
While the iso has the expected operational semantics, it is not well-typed as it
is not structurally recursive. On the other hand, its
derivation is valid. In order to properly type this iso, one would require
accepting lexicographical order (or more generally, any well-founded order) on
recursive isos that act as a termination proof. And then, see how such a
criterion would be captured in terms of pre-proof validity. Along with this,
allowing for coinductive statements and non-polarity-preserving
types and terms would allow to express more functions and capture a bigger
subset of  isomorphisms. This would require relaxing the condition on recursive
isos, as termination would be no longer possible to ensure. This is a focus of
our forthcoming research.

A second direction for future work is to consider quantum computation, by
extending our language with linear combinations of terms. We plan to study
purely quantum recursive types and generalised quantum loops:
in <cit.>, lists are the only recursive type which is
captured and recursion is terminating. The logic  would help in
providing a finer understanding of termination and non-termination. While little
difficulty are present in extending the language to the quantum case, the same
cannot be said for the logic. In order to develop a quantum version of
, one can either add two new rules: one for the scalar, where the
single hypothesis is the same as the conclusion, and one for the product, where
the two identical hypothesis are the same as the conclusion. Then, one would
need to adapt the notion of threads to this new logic and ensure that similar
notions of productivity of the cut-elimination still holds. The problem with
that approach is that one would need to either consider additional algebraic
rules on top of  (for instance, two scalar rules one after another can
be reduced to a single one, corresponding to the product of the scalars) or to
consider interpreting the rules in an external structure.

\[\infer[prod(\alpha)]{\Delta\vdash\Gamma}{\Delta\vdash\Gamma}\qquad\qquad\infer[sum]{\Delta\vdash\Gamma}{\Delta\vdash\Gamma\qquad\Delta\vdash\Gamma}\]

A quantum-oriented version of the language presented in this paper has already
been studied from a denotational semantics point of view <cit.>,
albeit without inductive types and the proof-theorical aspects haven't been
studied yet.

Define the proof $\pi_0$ and $\pi_S$ of the natural number $0$ and the
Successor as:
$\pi_0 = \begin{array}{c} \infer[\mu]{\vdash
\natT}{\infer[\oplus^1]{\vdash \one\oplus\natT}{\infer[\one]{\vdash\one}{}}}
\end{array}$ and $\pi_S = \begin{array}{c}
\infer[\mu]{\natT\vdash\natT}{\infer[\oplus^2]{\natT\vdash\one\oplus\natT}{\infer[\id]{\natT\vdash\natT}{}}}
\end{array}$.

Then the proof of $\omega_1, \omega_2$ and $\opn{CantorPairing}$ are:

1[$\bot$], ⊢

2[$\with$]⊕, ⊢
1[$\nu$], ⊢

0[$be({\color{red} g} )$]⊢

Cantor Pairing in