\section{Introduction}\label{section:intro}

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

\begin{wrapfigure}{R}{0.3\textwidth}
  \centering
  $\infer{
      B
    }{
      \infer*{A\rightarrow B}{s}
      &
      \infer*{A}{t}
    }
  $
  \caption{Modus Ponens}
  \label{fig:modus}
\end{wrapfigure}
\noindent
of $A\rightarrow B$ and a proof $t$ of $A$. With
the logical rule \textit{Modus Ponens} one can construct a
proof of $B$: Figure~\ref{fig:modus} 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
Figure~\ref{fig:modus} 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 \emph{Curry-Howard
  correspondence}~\cite{curry1934functionality,howard1980formulae}.
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 \emph{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 \emph{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 softwares, the
Curry-Howard correspondence provides a versatile framework. It has
been used to mirror first and second-order logics with dependent-type
systems~\cite{coqart,leroy2009compcert}, separation logics with
mem\-o\-ry-aware type
systems~\cite{reynolds02separation,jung2018rustbelt},
resource-sensitive logics with differential
privacy~\cite{gaboardu2013differential-privacy}, logics with monads
with reasoning on
side-effects~\cite{swamy2016dependent,maillard2020relational}, etc.

\emph{Reversible computation} is a paradigm of computation which
emerged as an energy-preserving model of computation in which data is
never erased~\cite{fredkin1982conservative} that makes sure that, given
some process $f$, there always exists an inverse process $f^{-1}$ such
that $f \circ f^{-1} = \operatorname{Id} = f^{-1} \circ f$. Many
aspects of reversible computation have been considered, such as the
development of reversible Turing Machines~\cite{rtm1}, reversible
programming languages~\cite{james2014theseus} and their
semantics~\cite{Chardonnet_2021, Kaarsgaard_2021}. However, the formal
relationship between a logical system and a 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~\cite{sabry2018symmetric}. In this model, reversible computation is
restricted to two main types: the tensor, written $A\otimes B$ and the
co-product, written $A\oplus B$. The former corresponds to the type of
all pairs of el\-e\-ments 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
$\ensuremath{\mathds{1}}\oplus\ensuremath{\mathds{1}}$, where $\ensuremath{\mathds{1}}$ is a type with only one element. The
language in~\cite{sabry2018symmetric} offers the possibility to code
isos ---reversible maps--- with pattern matching. An iso is for
instance the swap operation, typed with $A\otimes B\leftrightarrow B\otimes A$.
However, if~\cite{sabry2018symmetric} 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~\cite{sabry2018symmetric}, 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~\cite{rogers1987theory}. For the
Curry-Howard part, we capitalize on the logic
\ensuremath{\mu\textsf{MALL}}~\cite{baelde2007least,baelde2016infinitary}: 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
{\ensuremath{\mu\textsf{MALL}}}, some finitary proof system with explicit induction
inferences à la Park~\cite{baelde2007least} as well as
non-well-founded proof systems which allow to build infinite
derivation~\cite{baelde2016infinitary,bouncing}. The present paper
focuses on the latter. In general, an infinite derivation is called a
\emph{pre-proof} and is not necessarily consistent. To solve this
problem {\ensuremath{\mu\textsf{MALL}}} comes equipped with a \emph{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.

\subparagraph*{Organisation of the paper}
The paper is organised as follows: in Section~\ref{section:language}
we present the language, its syntax, typing rules and semantics and
show that any function that can be encoded in our language represents
an isomorphism. In Section~\ref{sec:rpp} we show that our language can
encode any Primitive Recursive Function~\cite{rogers1987theory}, this
is shown by encoding the set of Recursive Primitive
Permutations~\cite{rpp} functions. Then in Section~\ref{sec:ch}, 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 {\ensuremath{\mu\textsf{MALL}}} and show that the given derivation
respects the validity condition and how our evaluation strategy
simulates the cut-elimination procedure of the logic.

\section{First-order Isos}\label{section:language}

Our language is based on the one introduced by Sabry et
al~\cite{sabry2018symmetric} which define 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
types.
The language is defined by layers. Terms and types are presented in
Table~\ref{tab:termtypes}, while typing derivations, inspired from
{\ensuremath{\mu\textsf{MALL}}}, can be found in Tables~\ref{tab:typterm}
and~\ref{tab:typisos}. The language consists of the following pieces.

\smallskip
\noindent
\emph{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$.  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}}$.

\smallskip
\noindent
\emph{First-order isos.}~ An iso of type $A\leftrightarrow B$ acts on terms of
base types. An iso is a function of type $A\leftrightarrow B$, defined as a set
of clauses of the form \ensuremath{\{v_1~\iso~e_1 \alt \dots \alt v_n~\iso~e_n\}}. 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\leftrightarrow B$ and the term of type $A$. In
the typing rules of isos, the $\ensuremath{\mathtt{OD}}_A(\set{v_1,\dots,v_n})$ predicate
(corrected from~\cite{sabry2018symmetric}, as their definition makes
it impossible to type Toffoli) 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 Table \ref{tab:OD} 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~\Cref{tab:OD}, 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 S}$
Exhaustivity for an iso $\ensuremath{\{v_1~\iso~e_1 \alt \dots \alt v_n~\iso~e_n\}}$ 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 $\ensuremath{\mathbf{fix}~} g . \omega$ represents the creation
of a recursive function, rewritten as $\omega[g := \ensuremath{\mathbf{fix}~} g. \omega]$ by
the operational semantics. Each recursive function needs to satisfy a
structural recursion criteria: 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\leftrightarrow B$, we can build its inverse
$\omega^\bot : B\leftrightarrow 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~\cite[p.26]{henk1984lambda} which consists in keeping all
bound and free variables names distinct, even when this remains
implicit.

The type system is split in two parts: one for terms (noted $\Delta;
\Psi\vdash_e t : A$) and one for isos (noted $\Psi\vdash_\omega \omega
: A\leftrightarrow 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 association.

\begin{definition}[Structurally Recursive]
  Given an iso $\ensuremath{\mathbf{fix}~} f. \ensuremath{\{v_1~\iso~e_1 \alt \dots \alt v_n~\iso~e_n\}} : A_1\otimes \dots \otimes A_m
  \leftrightarrow C$, it is \textit{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:
  \begin{itemize}
    \item A closed value, in which case $e_i$ does not contain the
    subterm $f~p$
    \item 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$.
  \end{itemize}
Given a clause $v \leftrightarrow e$, we call the value $v_i^j$ (resp. the
variable $x_j$) the \emph{decreasing argument} (resp. the
\emph{focus}) of the structurally recursive criterion.
\end{definition}
\begin{table}[t]
  \begin{alignat*}{100}
    &\text{(Base types)} \quad& A, B &&&::=~ && \ensuremath{\mathds{1}} ~\mid~ A \oplus B
    ~\mid~ A \otimes B ~\mid~ \mu X. A \\
    &\text{(Isos, first-order)} & \alpha &&&::=&&A\leftrightarrow B \\[1.5ex]
    &\text{(Values)} & v &&&::=&& () ~\mid~ x ~\mid~ \inl{v} ~\mid~ \inr{v}
    ~\mid~
    \pv{v_1}{v_2} ~\mid~ \fold{v} \\
    &\text{(Pattern)} & p &&&::=&& x ~\mid~ \pv{p_1}{p_2} \\
    &\text{(Expressions)} & e &&&::=&& v ~\mid~ \letv{p_1}{\omega~p_2}{e} \\
    &\text{(Isos)} & \omega &&&::=&& \ensuremath{\{v_1~\iso~e_1 \alt \dots \alt v_n~\iso~e_n\}} ~\mid~ \ensuremath{\mathbf{fix}~} f.\omega ~\mid~ f \\
    &\text{(Terms)} & t &&&::=&& () ~\mid~ x ~\mid~ \inl{t} ~\mid~ \inr{t}
    ~\mid~
    \pv{t_1}{t_2} ~\mid~  \\
    & & &&& && \fold{t} ~\mid~ \omega~t ~\mid~
    \letv{p}{t_1}{t_2}
  \end{alignat*}
  \caption{Terms and types}
  \label{tab:termtypes}
\end{table}
\begin{table}[t]
    \[
      \begin{array}{c}
        \infer{\emptyset;\Psi\vdash_e () : \ensuremath{\mathds{1}}}{}
        \quad
        \infer{x:A;\Psi \vdash_e x :A}{}
        \quad
        \infer{\Delta;\Psi\vdash_e \inl{t}:A \oplus B}{\Delta;\Psi\vdash_e
        t:A}
        \quad
        \infer{\Delta;\Psi\vdash_e\inr{t}:A \oplus B}{\Delta;\Psi\vdash_e t:B}
        \\[1ex]
        \infer{
        \Delta_1,\Delta_2;\Psi\vdash_e \pv{t_1}{t_2} : A \otimes B
        }{
        \Delta_1;\Psi\vdash_e t_1 : A
        &
          \Delta_2;\Psi\vdash_e t_2 : B
          }
          \qquad
          \infer{\Delta; \Psi \vdash_e \fold{t} : \mu X. A }{\Delta; \Psi \vdash_e t : A[X\leftarrow \mu X. A]}
        \\[1ex]
        \infer{
        \Delta;\Psi\vdash_e f~t : B
        }{
        \Psi\vdash_{\isoterm} f : A \leftrightarrow B
        &
          \Delta; \Psi\vdash_e t : A
        }
        \qquad
        \infer{
        \Delta;\Psi\vdash_e \omega~t : B
        }{
        \vdash_{\isoterm} \omega : A \leftrightarrow B
        &
          \Delta;\Psi\vdash_e t : A
        }
        \\[1ex]
        \infer{\Delta_1,\Delta_2;\Psi \vdash_e \letv{(x_1, \dots, x_n)}{t_1}{t_2} :
        B}{\Delta_1;\Psi\vdash_e t_1 : A_1 \otimes \dots \otimes A_n\qquad\Delta_2, x_1 : A_1, \dots, x_n : A_n; \Psi\vdash_e t_2 : B}
        \\[1ex]
       
       
      \end{array}
    \]
    \caption{Typing of terms and expressions}
    \label{tab:typterm}
\end{table}
\begin{table}[t]
    \[
      \begin{array}{c}
        \infer{
        \Psi \vdash_{\isoterm}
        \ensuremath{\{v_1~\iso~e_1 \alt \dots \alt v_n~\iso~e_n\}} : A \leftrightarrow B.
        }{
        \begin{array}{l@{\quad}l@{\quad}l@{\qquad}l}
          \Delta_1 \vdash_e v_1 : A
          &
            \ldots
          &
            \Delta_n\vdash_e v_n : A
          &
            \ensuremath{\mathtt{OD}}_A(\{v_1, \dots, v_n\})   \\
          \Delta_1;\Psi\vdash_e e_1 : B
          &
            \ldots
          &
            \Delta_n;\Psi\vdash_e e_n : B
          & \ensuremath{\mathtt{OD}}_B(\{Val(e_1),\ldots,Val(e_n)\})
        \end{array}
            }
        \\[1ex]
        \infer{f : \alpha \vdash_{\isoterm} f : \alpha}{}
        \qquad
        \inferrule{
        f:\alpha\vdash_{\isoterm} \omega : \alpha \qquad \ensuremath{\mathbf{fix}~} f. \omega\text{ is structurally recursive}
        }
        {
        \Psi\vdash_{\isoterm} \ensuremath{\mathbf{fix}~} f.\omega : \alpha
        }
        \\
      \end{array}
    \]
    \caption{Typing of isos}
    \label{tab:typisos}
\end{table}
\begin{table}[t]
    \centering
    \[
    \begin{array}{c}
    \infer{\ensuremath{\mathtt{OD}}_A{(\set{x})}}{} \qquad \infer{\ensuremath{\mathtt{OD}}_\ensuremath{\mathds{1}}{(\set{()})}}{} \qquad
    \infer{\ensuremath{\mathtt{OD}}_{A\oplus B}(\{\inl{v} ~\mid~ v \in S \} \cup \{\inr{v} ~\mid~ v\in T \})}{\ensuremath{\mathtt{OD}}_A(S)\qquad \ensuremath{\mathtt{OD}}_B(T)} \qquad
    \\[1ex]
    \infer{\ensuremath{\mathtt{OD}}_{\mu X. A}{(\set{\fold{v} ~\mid~ v \in S})}}{\ensuremath{\mathtt{OD}}_{A[X \leftarrow \mu X. A]}(S)} \qquad
    \infer{\ensuremath{\mathtt{OD}}_{A\otimes B}(S = \{\pv{v_1}{v_1'}, \dots, \pv{v_n}{v'_n}\})}{\begin{array}{l}
      \ensuremath{\mathtt{OD}}_{A}(\pi_1(S)), \forall v\in \pi_1(S), \ensuremath{\mathtt{OD}}_B(S^1_v) \\
      \text{ or } \ensuremath{\mathtt{OD}}_{B}(\pi_2(S)), \forall v\in \pi_2(S), \ensuremath{\mathtt{OD}}_A(S^2_v)
    \end{array}}
    \end{array}
    \]
    \caption{Exhaustivity and Non-Overlapping}
    \label{tab:OD}
\end{table}
\begin{remark}
  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 call.
\end{remark}

\medskip Finally, our language is equipped with a rewriting system
$\to$ on terms, defined in Definition~\ref{def:rewriting-system}, 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 Table~\ref{tab:pattern_matching},
returns a substitution $\sigma$ that sends variables to values.
Because we ensure exhaustivity and non-overlapping
(Lemma~\ref{lem:od-ok}), the pattern-matching can always occur on
well-typed terms. The \textit{support} of a substitution $\sigma$ is
defined as $\operatorname{supp}(\sigma) = \{x \mid (x \mapsto v) \in \sigma \}$.


\begin{definition}[Substitution]

  Applying substitution $\sigma$ on 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(\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)})$.

\end{definition}

\begin{definition}[Evaluation relation  $\to$]
  \label{def:rewriting-system}
  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}]{
      (\ensuremath{\mathbf{fix}~} f.\omega) \to \omega[f := (\ensuremath{\mathbf{fix}~} f. \omega)]
    }{
    }\\[1.5ex]
    \infer[\mathrm{IsoApp}]{ \ensuremath{\{v_1~\iso~e_1 \alt \dots \alt v_n~\iso~e_n\}}~v' \to \sigma(e_i)}{
      \sigma[v_i] = v'}
    \end{array}
    \]
    with $C ::= [~] ~\mid~ \inl{C} ~\mid~ \inr{C} ~\mid~ \omega~C ~\mid~
    \letv{p}{C}{t} ~\mid~ \pv{C}{v} ~\mid~ \pv{v}{C}$

    As usual we note $\to^*$ for the reflexive transitive closure of
    $\to$.
\end{definition}


\begin{lemma}[$\ensuremath{\mathtt{OD}}_A(A)$ ensures exhaustivity and non-overlapping.]~
  \label{lem:od-ok}
  Let $\ensuremath{\mathtt{OD}}_A(S)$ and $~\vdash_e v : A$, then there exists a unique
  $v'\in S$ such that $v'$ matches $v$ under substitution $\sigma$,
  i.e. $\sigma[v'] = v$.
\end{lemma}

As mentioned above, from any iso $\omega : A\leftrightarrow B$ we can build its
inverse $\omega^\bot : B \leftrightarrow A$, the inverse operation is defined
inductively on $\omega$ and is given in Definition~\ref{def:iso-inv}.
\begin{definition}[Inversion]
  \label{def:iso-inv}
  Given an iso $\omega$, we define its dual $\omega^\bot$ as : $f^\bot
  = f, (\ensuremath{\mathbf{fix}~} f. \omega)^\bot = \ensuremath{\mathbf{fix}~} f. \omega^\bot, \{(v_i\leftrightarrow
  e_i)_{i\in I}\}^\bot = \{((v_i\leftrightarrow e_i)^\bot)_{i\in I}\}$ And the inverse of a clause as : \\
\[\begin{array}{c} \left(
      \begin{array}{l@{~}c@{~}l} v_1&{\leftrightarrow}&{\tt
        let}\,p_1=\omega_1\,p'_1\,{\tt in} \\
           && \cdots \\
           && {\tt let}\,p_n=\omega_n\,p'_n\,{\tt in}~v'_1
      \end{array}
      \right)^\bot := \left(
      \begin{array}{lcl@{}l@{}l} v'_1&{\leftrightarrow}&{\tt
        let}\,p'_n&=\omega_n^{\bot}&\,p_n\,{\tt in} \\
           && \cdots \\
           && {\tt let}\,p'_1&=\omega_1^{\bot}&\,p_1\,{\tt in}~v_1
      \end{array}
      \right).
    \end{array}
  \]

\end{definition}
We can show that the inverse is well-typed and behaves as expected:
\begin{lemma}[Inversion is well-typed]
  \label{lem:inv-type}
  Given $\Psi \vdash_\omega \omega : A\leftrightarrow B$, then
  $\Psi\vdash_\omega\omega^\bot : B\leftrightarrow A$.
\end{lemma}

\begin{theorem}[Isos are isomorphisms]
  \label{thm:isos-iso}
  For all well-typed isos $\vdash_\omega \omega : A\leftrightarrow B$, and for
  all well-typed values $\vdash_e v : A$, if~
  $(\omega~(\omega^\bot~v))\rightarrow^* v'$ then $v = v'$.
\end{theorem}

\begin{table}[t]
    \centering
\[
\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[()] = ()}{}
\]
    \caption{Pattern-matching}
    \label{tab:pattern_matching}
\end{table}

\begin{example}
  \label{ex:iso1}
  We can define the iso of type : $A\oplus (B\oplus C)\leftrightarrow C\oplus
  (A\oplus B)$ as
  \[
    \scalebox{0.8}{$\left\{
      \begin{array}{l@{~}c@{~}l}
        \inl{(a)} & {\leftrightarrow} & \inr{(\inl{(a)})} \\
        \inr{(\inl{(b)})} & {\leftrightarrow} & \inr{(\inr{(b)})} \\
        \inr{(\inr{(c)})} & {\leftrightarrow} & \inl{(c)} \\
      \end{array}
    \right\}$}
  \]
\end{example}

\begin{example}
  \label{ex:map}
  We give the encoding of the isomorphism \textit{map}$(\omega)$ and
  its inverse: for any given iso $\vdash \omega : A\leftrightarrow B$ in our
  language, we can define $\textit{map}(\omega) : [A]\leftrightarrow [B]$ where
  $[A] = \mu X. \ensuremath{\mathds{1}}\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
  Definition~\ref{def:iso-inv}.

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

\begin{remark}\rm In our two examples, the left and right-hand side of
  the $\leftrightarrow$ 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.
\end{remark}

The language enjoys the standard properties of typed languages of
progress and subject reduction:

\begin{lemma}[Subject Reduction]\label{prop:subject_reduction} If
  $\Delta;\Psi\vdash_e t : A$ and $t\rightarrow t'$ then
  $\Delta;\Psi\vdash_e t' : A$.
\end{lemma}

\begin{lemma}[Progress]\label{prop:progress} If $~\vdash_e t : A$
  then, either $t$ is a value, or $t\to t'$.
\end{lemma}


\section{Computational Content}
\label{sec:rpp}

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. Homewer, with
infinite types, the expressivity becomes less clear. We show that we
can encode Recursive Primitive Permutations~\cite{rpp} (RPP), which
shows us that we can encode at least all Primitive Recursive
Functions~\cite{rogers1987theory}.

We give a few reminders on the language RPP and its main results, then
show how to encode it.
\subsection{Reminder 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 $\ensuremath{\mathbb{Z}}^k$ to $\ensuremath{\mathbb{Z}}^k$, it is built inductively on $k \in
\ensuremath{\mathbb{N}}$ by: the successor ($S$), the predecessor ($P$), the identity
$(\operatorname{ID})$ and the sign-change that are part of $\RPP{1}$.
The swap function $(\mathcal{X})$ and the binary permutation
$\mathcal{X}$ which sends the pair $(x, y)$ to $(y, x)$ are part of
$\RPP{2}$ and then, for any function $f, g, h \in \RPP{k}$ and
$j\in\RPP{l}$, we can build (i) the sequential composition $f;g \in
\RPP{k}$, (ii) the parallel composition $f\mid\mid j\in\RPP{k+l}$
(iii) the iterator $\textit{It}[f]\in\RPP{k+1}$ and (iv) the selection
$\textit{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 constructors of $\operatorname{RPP}$
under a graphical form, as in~\cite{rpp}, 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 Figure~\ref{fig:rpp}.


\begin{figure}[t]
\[
    \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 & ~~~\begin{tikzpicture}[remember picture, overlay] \node at (-.12, -.15) {$\mathcal{X}$}; \end{tikzpicture} & y \\
    y & ~~~ & 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 & \textit{If}[f,g,h] & \vdots \\
            x_n & ~~ & y_n \\
            x &  & x \\
        \end{bNiceMatrix}
        \hspace{-1em}\setlength{\arraycolsep}{0pt}
        \begin{array}{ c }
          \left.\kern-\nulldelimiterspace
          \vphantom{\begin{array}{ c }
              b_N  \\
            \vdots \\
              z_N
          \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 & \textit{It}[f] & \vdots \\
    x_n & ~~ & y_n \\
    x &  & x \\
\end{bNiceMatrix}
\hspace{-1em}\setlength{\arraycolsep}{0pt}
\begin{array}{ c }
    \left.\kern-\nulldelimiterspace
    \vphantom{\begin{array}{ c }
        b_N  \\
    \vdots \\
        z_N
    \end{array}}
    \right\}= \underbrace{(f;\dots ; f)}_{~\mid~ x ~\mid~} (x_1, \dots, x_n) \\
    \vphantom{a_N}
\end{array}
\]

\caption{Generators of RPP}
\label{fig:rpp}
\end{figure}

\begin{remark}

    In their paper~\cite{rpp}, the authors make use of two other
    constructors: generalised permutations over $\ensuremath{\mathbb{Z}}^k$ and
    \emph{weakenings} of functions, but those can actually be defined
    from the other constructors so that in the following section we do
    not give their encoding.
\end{remark}

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

\begin{definition}[Inversion]
The inversion is defined as follow :

\begin{tabular}{ccc}
     $\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}]$
\end{tabular}

\end{definition}

\begin{proposition}[Inversion defines an inverse~\cite{rpp}]
Given $f\in\RPP{k}$ then $f;f^{-1} = \operatorname{Id} = f^{-1}; f$
\end{proposition}

\begin{theorem}[Soudness \& Completeness~\cite{rpp}]
    RPP is PRF-Complete and PRF-Sound: it can represent any Primitive
    Recursive Function and every function in RPP can be represented in
    PRF.
\end{theorem}

\subsection{From RPP to Isos}

We start by defining the type of stricly positive natural numbers,
$\operatorname{npos}$, as $\operatorname{npos} = \mu X. \ensuremath{\mathds{1}} \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 = \ensuremath{\mathds{1}} \oplus
(\operatorname{npos} \oplus \operatorname{npos})$ along with
$\overline{z}$ the encoding of any $z\in\ensuremath{\mathbb{Z}}$ 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 \leftrightarrow
Z^k$ which simulates $f$. $\operatorname{isos}(f)$ is defined by the
size of the proof that $f$ is in $\RPP{k}$.


\begin{definition}[Encoding of the primitives]~

\begin{minipage}{0.45\textwidth}
    \begin{itemize}
        \item The Sign-change of type $Z\leftrightarrow Z$ is \\
        \scalebox{0.8}{$\left\{\begin{array}{ccc}
             \inr{(\inl{x})} &\leftrightarrow& \inr{(\inr{x})} \\
             \inr{(\inr{(x)})} &\leftrightarrow& \inr{(\inl{x})} \\
             \inl{()} &\leftrightarrow&\inl{()}
        \end{array}\right\}$} \\[0.5em]
    \end{itemize}
\end{minipage}
\begin{minipage}{0.54\textwidth}
  \begin{itemize}
    \item The identity is $\{x\leftrightarrow x\} : Z \leftrightarrow Z$

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

    \item The Predecessor is the inverse of the Successor
    \end{itemize}
\end{minipage}
\end{definition}
\begin{itemize}
    \item The Successor is
    \[\left\{\begin{array}{ccc}
        \inl{()} &\leftrightarrow& \inr{(\inl{(\fold{(\inl{()})})})} \\
        \inr{(\inl{x})}&\leftrightarrow&\inr{(\inl{(\fold{(\inr{x})})})} \\
        \inr{(\inr{(\fold{(\inl{()})})})}&\leftrightarrow& \inl{()}\\
        \inr{(\inr{(\fold{(\inr{x})})})}& \leftrightarrow & \inr{(\inr{x})}
    \end{array}\right\} : Z \leftrightarrow Z \]
\end{itemize}


\begin{definition}[Encoding of Composition]
\bigskip
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} \leftrightarrow 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) & \leftrightarrow & \letv{(z_1,
   \dots, z_j)}{\omega_g~(y_1, \dots, y_j)}{} \\
   & & (z_1, \dots, z_j) \end{array}\right\}\]

\end{definition}

\begin{definition}[Encoding of Parallel Composition]
\bigskip

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} \leftrightarrow
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) & \leftrightarrow & \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\}\]

\end{definition}

\begin{definition}[Encoding of Finite Iteration]
\bigskip
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} \leftrightarrow Z^k \otimes~\operatorname{npos}$
doing the finite iteration using $\operatorname{npos}$, defined as: \\

\scalebox{1}{\[\omega_{\operatorname{aux}} = \mathbf{fix} g.
    \left\{\begin{array}{ccc}
    (\overrightarrow{x}, \fold{(\inl{()})}) & \leftrightarrow & \letv{\overrightarrow{y}}{\omega_f~\overrightarrow{x}}{}
    \\
    & & (\overrightarrow{y},\fold{(\inl{()})}) \\[0.5em]
    (\overrightarrow{x}, \fold{(\inr{n})})& \leftrightarrow &  \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}(\textit{It}[f])$ of
type $Z^{k+1} \leftrightarrow Z^{k+1}$ as:

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

\end{definition}

\begin{definition}[Encoding of Selection]
\bigskip

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}(\textit{If}[f,g,h])$ of type $Z^{k+1} \leftrightarrow
Z^{k+1}$ as:

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

\end{definition}


\begin{theorem}[The encoding is well-typed]
\label{lem:rpp-typed}
Let $f\in \RPP{k}$, then $\vdash_\omega \operatorname{isos}(f) : Z^k \leftrightarrow Z^k$.
\end{theorem}

\begin{theorem}[Simulation]
\label{thm:rpp-sim}
Let $f\in \RPP{k}$ and $~n_1, \dots, n_k$ elements of~$~\ensuremath{\mathbb{Z}}$
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})$
\end{theorem}

\begin{remark}
    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
    \textit{let} constructions, which will not be the case for
    $\operatorname{isos}(f^{-1})$. They can nonetheless be considered
    equivalent up to a permutation of \textit{let} constructions and
    renaming of variable.
\end{remark}

\section{Proof Theorical Content}\label{sec:ch}

We want to relate our langage of isos to proofs in a suitable logic.
As mentioned earlier, an iso $\vdash_\omega \omega : A\leftrightarrow 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 {\ensuremath{\mu\textsf{MALL}}} : linear logic with
least and greatest fixed points, which allows us to reason about
inductive and coinductive statements. {\ensuremath{\mu\textsf{MALL}}} 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 {\ensuremath{\mu\textsf{MALL}}}
comes with a validity criterion on infinite derivations trees (called
\textit{pre-proofs}) that tells us whether such derivations are indeed
proofs. We recall briefly the basic notions of {\ensuremath{\mu\textsf{MALL}}}, while more
details can be found in~\cite{bouncing}.

\subsection{Background on {\ensuremath{\mu\textsf{MALL}}}}

Given an infinite set of variables $\mathcal{V} = \{X, Y, \dots\}$, we
call \emph{formulas} of {\ensuremath{\mu\textsf{MALL}}} the objects generated by $A, B ::= X
\mid \ensuremath{\mathds{1}} \mid \ensuremath{\mymathbb{0}} \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, \ensuremath{\mymathbb{0}}^\bot = \top, \ensuremath{\mathds{1}}^\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 \emph{occurrence}, a word of the form $\alpha \cdot w$
where $\alpha \in \goth{A}_{\text{fresh}}$ an infinite set of
\emph{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 \emph{left}, \emph{right} and
\emph{inside}) and \emph{formulas occurrences} $F, G, H, \dots$ as a
pair of a \emph{formula} and an \emph{occurrence}, written $A_\alpha$.
Finally we write $\Sigma, \Phi$ for \emph{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:
\begin{itemize}
  \item Given $\# \in \{\otimes,\oplus,\parr,\with\}$, if $F =
  A_{\alpha l}$ and $G = B_{\alpha r}$ then $(F \# G) = (A\# B)_{\alpha}$
  \item Given $\# \in \{\mu, \nu\}$ if $F = A_{\alpha i}$ then
  $\# X. F = (\# X. A)_{\alpha}$
\end{itemize}

Occurrences allow us to follow a subformula uniquely inside a
derivation. Since in {\ensuremath{\mu\textsf{MALL}}} we only work with formula occurrences,
we simply use the term \emph{formula}.

The (possibly infinite) derivation trees of {\ensuremath{\mu\textsf{MALL}}}, called
\emph{pre-proofs} are coinductively generated by the rules given in
\Cref{mumall:rules}. We say that a formula is \textit{principal} when
it is the formula that the rule is being applied to.

\begin{figure}[t]
  \setlength{\tabcolsep}{0.5em}
  \begin{longtable}{ccc}
    \infer[id]{\vdash F^\bot, G}{F\equiv G} & \infer[cut]{\vdash
      \Sigma, \Phi}{\vdash \Sigma, F \quad \vdash \Phi, F^\bot} &
    \infer[\top]{\vdash \top, \Sigma}{} \\[1em]  \infer[\ensuremath{\mathds{1}}]{\vdash \ensuremath{\mathds{1}}}{} &
     \infer[\parr]{\vdash F\parr G, \Sigma}{\vdash F, G, \Sigma} & \infer[\otimes]{\vdash F\otimes
    G, \Sigma, \Phi}{\vdash F, \Sigma\quad \vdash G, \Phi} \\[1em]
    \infer[\with]{\vdash F\with G, \Sigma}{\vdash F, \Sigma \quad \vdash G,\Sigma} & \infer[\oplus  ^i~ i\in\{1, 2\}]{\vdash
    F_1\oplus F_2, \Sigma}{\vdash F_i, \Sigma} & \infer[\bot]{\vdash \Sigma, \bot}{\Sigma} 
  \\[1em] \infer[\mu]{\vdash \mu X. F, \Sigma}{\vdash F[X\leftarrow\mu
      X. F], \Sigma} & \infer[\nu]{\vdash \nu X. F, \Sigma}{\vdash
      F[X\leftarrow \nu X. F], \Sigma} & \\[1em]
  \end{longtable}

  \caption{\label{mumall:rules}Rules for \ensuremath{\mu\textsf{MALL}}.}
\end{figure}

Among the infinite derivations that {\ensuremath{\mu\textsf{MALL}}} offer we can look at the
\emph{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
\emph{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$.

\begin{example}\label{ex:circular-proof} An infinite derivation and
  two different circular representations with back-edges.
  \[\begin{prooftree}

    \hypo{}
    \ellipsis{}{}
    \infer1[$\mu$]{\vdash \mu X. X}
    \infer1[$\mu$]{\vdash \mu X. X}
    \end{prooftree}\qquad
    \begin{prooftree}
    \infer0[$be(f)$]{\tikzmark{ex_top}{\vdash} \mu X. X}
    \infer1[$\mu$]{\vdash^f \mu X. X\tikzmark{ex_bot}}
    \end{prooftree}
    \qquad
    \begin{prooftree}
    \infer0[$be(f)$]{\tikzmark{ex_top2}{\vdash} \mu X. X}
    \infer1[$\mu$]{\vdash\mu X. X}
    \infer1[$\mu$]{\vdash^f \mu X. X\tikzmark{ex_bot2}}
    \end{prooftree}
    \begin{tikzpicture}[remember picture, overlay]

      \draw[->, >=latex,rounded corners, smooth=2] ([xshift=0.5cm,
      yshift=0.5cm]pic cs:ex_top) .. controls +(30:3cm) and +(-30:2cm)
      .. (pic cs:ex_bot);

      \draw[->, >=latex,rounded corners, smooth=2] ([xshift=0.5cm,
      yshift=0.5cm]pic cs:ex_top2) .. controls +(30:3cm) and +(-30:2cm)
      .. (pic cs:ex_bot2);
     
    \end{tikzpicture}
  \]
\end{example}

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:

\begin{definition}[Unfolding]

  We define the unfolding of a circular derivation $P$ with a
  valuation $v$ from back-edge labels to derivations by:
  \begin{itemize}
    \item $\ensuremath{\mathcal{U}}\left(\begin{array}{c}P :
    \infer[r]{\vdash\Sigma}{P_1, \dots, P_n}\end{array}, v\right) =
    \begin{array}{c}\infer[r]{\vdash\Sigma}{\ensuremath{\mathcal{U}}(P_1, v), \dots, \ensuremath{\mathcal{U}}(P_n, v)}\end{array}$
    \item $\ensuremath{\mathcal{U}}(be(f), v) = v(f)$
    \item $\ensuremath{\mathcal{U}}\left(\begin{array}{c}P : \infer[r]{\vdash^f
    \Sigma}{P_1, \dots, P_n}\end{array}, v\right) =
    \left(\pi = \begin{array}{c}\infer[r]{\vdash\Sigma}{\ensuremath{\mathcal{U}}(P_1,
    v'), \dots, \ensuremath{\mathcal{U}}(P_n, v')}\end{array}\right)$ with $v'(g) =
    \pi$ if $g = f$ else $v(g)$.
  \end{itemize}
\end{definition}

{\ensuremath{\mu\textsf{MALL}}} 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
\emph{thread}~\cite{baelde2016infinitary,bouncing}: 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 will
be called \emph{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, 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 \emph{additive slices} and
\emph{persistent slices} which we do not detail here.
\Cref{ex:mumall-thread} features an example of a valid proof together
with its thread. More details can be found in~\cite{bouncing}.


\subsection{Translating isos into {\ensuremath{\mu\textsf{MALL}}}}

We start by giving the translation from isos to pre-proofs, and then
show that they are actually proofs, therefore obtaining a
\textit{static} correspondence between programs and proofs. We then
show that our translation entails a \textit{dynamic} correspondence
between the evaluation procedure of our language and the
cut-elimination procedure of {\ensuremath{\mu\textsf{MALL}}}. 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 \emph{circular}, and we therefore
translate the isos directly into finite derivations with back-edge,
written $\ensuremath{\textit{circ}}(\omega)$. We can define another translation into
infinite derivations as the composition of $\ensuremath{\textit{circ}}()$ with the
unfolding: $\bbracket{\omega} = \ensuremath{\mathcal{U}}(\ensuremath{\textit{circ}}(\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 {\ensuremath{\mu\textsf{MALL}}} 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\leftrightarrow 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
formula: \[\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 {\ensuremath{\mu\textsf{MALL}}} where (i) we remove all occurrence of the
exchange rule (ii) the contexts $[]; \Theta$ becomes
$\overline{\Theta}$.

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

\smallskip
\noindent
\emph{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 $\ensuremath{\mathbf{fix}~} f. \omega$ and calling the
negative phase when encountering an iso of the form $\ensuremath{\{v_1~\iso~e_1 \alt \dots \alt v_n~\iso~e_n\}}$ 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.

\smallskip
\noindent
\emph{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 judgement),
written $(l, \xi)$ where each element of the set corresponds to one
clause $v \leftrightarrow e$ of the given iso and $\xi$ is the typing judgement 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 \emph{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~\Cref{tab:negative_phase}.


\smallskip
\noindent
\emph{Positive phase}.~The translation of an expression is pretty
straightforward: each \textit{let} and iso-application is represented
by two \ensuremath{\mathtt{cut}}~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~\Cref{tab:positive_phase}.


\begin{remark}

While {\ensuremath{\mu\textsf{MALL}}} 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.
\end{remark}

\begin{definition}
  \label{tab:circ_translation}
  ${\ensuremath{\textit{circ}}(\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 {\ensuremath{\mu\textsf{MALL}}} described above with back-edges.
  $\ensuremath{\textit{circ}}(\omega, S, \alpha, \beta)$ is defined inductively on
  $\omega$:
  \begin{itemize}
    \item $\ensuremath{\textit{circ}}(\ensuremath{\mathbf{fix}~} f. \omega, S, \alpha, \beta) = \ensuremath{\textit{circ}}(\omega, \set{f}, \alpha, \beta)$
    \item $\ensuremath{\textit{circ}}(f, \set{f}, \alpha, \beta) = \infer[be(f)]{A_\alpha\vdash B_\beta}{}$
    \item $ \ensuremath{\textit{circ}}(\{(v_i\leftrightarrow e_i)_{i\in I}\} : A\leftrightarrow B, \set{f},
    \alpha, \beta) = \stretchleftright{\llfloor}{\begin{array}{c}\infer{A_\alpha\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$.
  \end{itemize}
\end{definition}

\begin{example} The translation $\ffloor{\ensuremath{\textit{circ}}(\omega, \emptyset,
\alpha, \beta)}$ of the iso $\omega$ from Example~\ref{ex:iso1} is,
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}$:

\scalebox{0.9}{\begin{prooftree}   
  \infer0[id]{[] ; a : F\vdash F'}
  \infer1[$\oplus^1$]{[] ; a : F \vdash F'\oplus G'}
  \infer1[$\oplus^2$]{[] ; a : F\vdash H'\oplus (F'\oplus G')}
  \infer1[ex(a)]{[F] ; \emptyset \vdash H'\oplus (F'\oplus G')}


  \infer0[id]{[] ; b : G \vdash G'}
  \infer1[$\oplus^2$]{[] ; b : G \vdash F'\oplus G'}
  \infer1[$\oplus^2$]{[] ; b : G \vdash H'\oplus (F'\oplus G')}
  \infer1[ex(b)]{[G] ; \emptyset \vdash H'\oplus (F'\oplus G')}

  \infer0[id]{[] ; c : H \vdash H'}
  \infer1[$\oplus^1$]{[] ; c : H \vdash H'\oplus (F'\oplus G')}
  \infer1[ex(c)]{[H] ; \emptyset \vdash H'\oplus (F'\oplus G')}

  \infer2[$\parr$]{[G\oplus H]; \emptyset \vdash H'\oplus (F'\oplus G')}
  \infer2[$\parr$]{[F\oplus (G\oplus H)] ; \emptyset \vdash
  H'\oplus (F'\oplus G')}
\end{prooftree}}
\end{example}

\begin{example}
  \label{ex:mumall-thread}
  \newcommand{\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}}{\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}}
  Considering the iso swap of type $A\otimes B \leftrightarrow B\otimes A$ and
  its $\ensuremath{\mu\textsf{MALL}}$~proof \[\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}\] Following
  Example~\ref{ex:map} we give its corresponding proof
  $\pi_{\textit{map}(S)}$ where $\ensuremath{F}} \newcommand{\boa}{\ensuremath{G} = (A\otimes B)_{\alpha irl}$ and
  $\boa = (B\otimes A)_{\beta irl}$, then $[\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}]$ and $[\boa]$ are
  respectively of address $\alpha$ and $\beta$:

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

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



\infer0[id]{\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}\vdash \ensuremath{F}} \newcommand{\boa}{\ensuremath{G}}
    \hypo{\pi_S}
    \infer1{\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}\vdash \boa}
    \infer2[cut]{\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}\vdash \boa}
  \hypo{\tikzmark{r77}\qquad\tikzmark{r88}}
  \infer1[id]{\colorbox{cyan!30}{$[\tikzmark{r7}\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}]$}\vdash \colorbox{cyan!30}{$[\tikzmark{r8}\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}]$}}
    \hypo{\tikzmark{r10}\pi_{\textit{map}(S)}}
    \infer1{\colorbox{cyan!30}{$[\tikzmark{r9}\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}]$}\vdash [\boa]}
    \infer2[cut]{\colorbox{cyan!30}{$[\tikzmark{r6}\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}]$}\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 \ensuremath{\mathds{1}} \oplus (\boa \otimes [\boa])}
  \infer1[$\mu$]{\boa, [\boa]\vdash [\boa]}
  
    \infer1[]{\boa, [\boa]\vdash [\boa]}
    \infer2[cut]{\boa, \colorbox{cyan!30}{$[\tikzmark{r5}\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}]$}\vdash [\boa]}
    \infer2[cut]{\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}, \colorbox{cyan!30}{$[\tikzmark{r4}\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}]$}\vdash [\boa]}
    \infer1[$\parr$]{\ensuremath{F}} \newcommand{\boa}{\ensuremath{G} \otimes \colorbox{cyan!30}{$[\tikzmark{r3}\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}]$} \vdash [\boa]}

    \infer2[$\with$]{\ensuremath{\mathds{1}} \oplus \colorbox{cyan!30}{$(\ensuremath{F}} \newcommand{\boa}{\ensuremath{G} \tikzmark{r2}\otimes [\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}])$} \vdash [\boa]}
    \infer1[$\nu$]{ \colorbox{cyan!30}{[\tikzmark{r1}{\ensuremath{F}} \newcommand{\boa}{\ensuremath{G}}]}\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
  cs:r10)+(0,.2cm)$);

 
 
 
 
 
 
  \end{tikzpicture}

  }
\]
 
 
 
 
 
We painted in blue the pre-thread that follows the \emph{focus} of the
structurally recursive criterion. During the \emph{negative phase}
which consists of the $\nu, \with, \parr, \bot$ rules the pre-thread
is going up, at each time going into the subformula corresponding to
the \emph{focus}. Then, during the \emph{positive phase} the
pre-thread is not active during the multiple \textit{cut} rules until
it reaches the \textit{id} rule, where the pre-thread bounces and
starts going down before bouncing back up again in the \textit{cut}
rule, into the infinite branch, where the behavior of the pre-thread
will repeat itself. One can then show that this pre-thread is indeed a
thread, according to~\cite{bouncing} and that it is valid: among the
formulas it visits infinitely often, the minimal formula is $[F]$,
which is a $\nu$ formula as since $[F]$ is on the left hand side of
the sequent, we get $[F] = (\mu X. \ensuremath{\mathds{1}} \oplus (F\otimes X))^\bot$.
\end{example}

\begin{figure}[!ht]

 
 
 
 
 

  \[ \begin{array}{rl}\infer{F_1\oplus F_2 :: \Upsilon ; \Theta\vdash G}{\ensuremath{\mathtt{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}{\ensuremath{\mathtt{Neg}}(\set{(v_j ::
  l_j, \xi_j)_{j\in J}})} \qquad \infer{F_2 :: \Upsilon ; \Theta
  \vdash G}{\ensuremath{\mathtt{Neg}}(\set{(v_k :: l_k, \xi_k)_{k\in K}})}} \end{array}
  \qquad\]

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

  \[ \scalebox{0.9}{$\begin{array}{c}\infer{F_1\otimes F_2 ::
  \Upsilon ; \Theta\vdash G}{\ensuremath{\mathtt{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}{\ensuremath{\mathtt{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}{\ensuremath{\mathtt{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}{\ensuremath{\mathtt{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}{\ensuremath{\mathtt{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}{\ensuremath{\mathtt{Neg}}(\set{l,
  \xi})}}\end{array}$} \]

  \caption{Negative Phase}
  \label{tab:negative_phase}
\end{figure}

\begin{figure}[t]
  \centering
  
  \scalebox{1}{\[\myPos{\infer{\vdash_e () : \ensuremath{\mathds{1}}}{}} =
  \begin{array}{c}\infer[\ensuremath{\mathds{1}}]{[] ; \emptyset \vdash \ensuremath{\mathds{1}}_\alpha}{}\end{array}\]} \\[0.5em]
  
  \scalebox{1}{\[\myPos{\infer{x : A\vdash_e x : A}{}} = \begin{array}{c}\infer[id]{[]
  ; x : A_\alpha \vdash A_\beta}{}\end{array}\]}
  
  \scalebox{1}{\[\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}}{\ensuremath{\mathtt{Pos}}(\xi)}}\end{array}\]} \scalebox{1}{\[
  \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}}{\ensuremath{\mathtt{Pos}}(\xi)}}\end{array}\]}
  
  \scalebox{1}{\[\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}}{\ensuremath{\mathtt{Pos}}(\xi_1)}\qquad\infer{[] ;
  {\Theta}_2\vdash (A_2)_{\alpha r}}{\ensuremath{\mathtt{Pos}}(\xi_2)}}\end{array}\]}
  
  \scalebox{1}{\[ \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}}{\ensuremath{\mathtt{Pos}}(\xi)}}\end{array}\]}
  
  \scalebox{1}{\[
  \begin{array}{rl}
      \myPos{\infer{\underline{\Theta}_1,\underline{\Theta}_2\vdash_e
  \letv{(x_i)_{i\in I}}{t_1}{t_2} :
  B}{\infer{\underline{\Theta}_1\vdash_e 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\vdash_e t_2 : B}{\xi_2}}} &= \\[2em]
  \infer[\ensuremath{\mathtt{cut}}]{[] ; {\Theta}_1,{\Theta}_2\vdash B_\alpha}{\infer{[] ;
  {\Theta}_1\vdash F_1\otimes\dots\otimes
  F_n}{\ensuremath{\mathtt{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}\]} \\[0.5em]
  
  \scalebox{1}{\[ \myPos{\infer{\underline{\Theta};\Psi\vdash_e
  \omega~t : B}{\Psi\vdash_\omega \omega : A \leftrightarrow
  B\qquad\infer{\underline{\Theta}\vdash_e t : A}{\xi}}} =
  \begin{array}{c}\infer[\ensuremath{\mathtt{cut}}]{[] ; {\Theta}\vdash B_\beta}{\infer{[] ; {\Theta}\vdash
  A}{\ensuremath{\mathtt{Pos}}(\xi)}\qquad\infer{[A] ; \emptyset\vdash
  B_\beta}{\ensuremath{\textit{circ}}(\omega, \set{f}, \alpha, \beta)}}\end{array} \]}
  
  \caption{Positive Phase}
  \label{tab:positive_phase}
  \end{figure}

\begin{lemma}
  \label{lem:inf-branch-form}
  Given $\pi = \ensuremath{\textit{circ}}(\omega)$, for each infinite branch of $\pi$,
  only a single iso-variable is visited infinitely often.
\end{lemma}
\begin{proof}
  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.
\end{proof}

Among the terms that we translate, the translation of a value yields
what we call a \emph{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.

\begin{definition}[Purely Positive Proof]

  A \textit{Purely Positive Proof} is a finite, cut-free proof whose
  rules are only $\oplus^i, \otimes, \mu, \ensuremath{\mathds{1}}, \textit{id}$ for
  $i\in\{1,2\}$.
\end{definition}
\begin{lemma}[Values are Purely Positive Proofs]
  \label{lem:valppp}
  Given $x_1 : A^1, \dots, x_n : A^n\vdash v : A$ then $\infer{[]; x_1
  : A^1_{\alpha_1}, \dots, x_n : A^n_{\alpha_n}\vdash
  A_\alpha}{\bbracket{v}}$ is a purely positive proof.
\end{lemma}

We can then define the notion of \emph{bouncing-cut} and their origin:

\begin{definition}[Bouncing-Cut]

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}{}}$
\end{definition}
Due to the syntactical restrictions of the language we get the
following:
\begin{property}[Origin of Bouncing-Cut]
  Given a well-typed iso, every occurrence of a rule $be(f)$ in
  $\ffloor{\ensuremath{\textit{circ}}(\omega)}$ is a premise of a bouncing-cut.
\end{property}

In particular, when following a thread going up into a
\emph{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.



\begin{theorem}[\emph{Validity of proofs}]\label{thm:validity} If
  $~\vdash_\omega \omega : A\leftrightarrow B$ and $\pi = \ffloor{\ensuremath{\textit{circ}}(\omega,
  \emptyset, \alpha, \beta)}$ then $\pi$ satisfies {\ensuremath{\mu\textsf{MALL}}} validity
  criterion from~\cite{bouncing}.
\end{theorem}
\begin{proof}[Proof Sketch]

  In order to show the validity of our derivation we need, for each
  infinite branch, to build a valid thread. From the previous lemmas
  and the syntactical constraints of the language, we get that any
  infinite branch is completely defined by a single iso-variable,
  which allows us to reason entirely about a single recursive iso
  $\ensuremath{\mathbf{fix}~} f. \ensuremath{\{v_1~\iso~e_1 \alt \dots \alt v_n~\iso~e_n\}}$. For each infinite branch, we will build a
  pre-thread that follows the focus of the primitive recursive
  criterion. We know that the focus is a \emph{strict subvariable} of
  the argument that is called recursively, as a consequence we can
  split the constructed thread into two parts, $p_0$ and $p_1$,
  corresponding respectively to the \emph{negative phase} and the
  \emph{positive phase}. We also know that, each argument of a
  recursive call gives us a \emph{purely positive proof} which is made
  only of tensors. We can show that the size of $p_0$ is bigger than
  $p_1$ and also that $p_1$ is a prefix of $p_0$. This allows us to
  make sure that our pre-thread is a thread where the \emph{visible
  part} always encounters a $\nu$ formula. Finally, the inductive type
  is decomposed in the negative phase and not in the positive phase
  (as the right-hand side of a recursive call is purely made of
  tensors), we can show that (i) the thread is never stationary and
  (ii) the thread has for minimal recurring formula that is visited
  infinitely often a $\nu$ formula, hence satisfying validity.
\end{proof}


We can also show that the rewriting rules of the language simulate the
cut-elimination procedure, as it is described in~\cite{bouncing}:

\begin{theorem}[Simulation]
  Provided an iso $\vdash_\omega \omega : A\leftrightarrow B$ and values
  $\vdash_e v : A$ and $\vdash_e v' : B$, let $\pi = \ensuremath{\mathtt{Pos}}(\omega~v)$
  and $\pi' = \ensuremath{\mathtt{Pos}}(v)$, if $\omega~v\to^* v'$ then $\pi\to_{\textit{cut-elim}}^* \pi'$.
\end{theorem}

\begin{proof}[Proof sketch]

  The proof relies on the definition of a novel explicit substitution
  rewriting system for the language, called $\ensuremath{\to_{e\beta}}$. Explicit
  substitution are represented as a series of \textit{let} constructs
  where the substitution of a variable by a value only occurs when we
  reach the term $\letv{x}{v}{x}$. Each rewriting step of this system
  represents exactly one step of the cut-elimination procedure of
  {\ensuremath{\mu\textsf{MALL}}}. Then we only need to show that the explicit substitution
  rewriting system matches, meaning that if $\sigma =
  \{\overrightarrow{x} \mapsto \overrightarrow{v}\}$ then
  $\letv{\overrightarrow{x}}{\overrightarrow{v}}{e} \ensuremath{\to_{e\beta}}^*
  \sigma(e)$.
\end{proof}

This leads to the following corollary:

\begin{corollary}[Isomorphism of proofs.]
  Given a well-typed iso $\vdash_\omega \omega : A\leftrightarrow 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[\ensuremath{\mathtt{cut}}]{\vdash F_2}{\infer[cut]{\vdash G_1}{\infer{\vdash
              F_3}{\phi}\qquad\infer{F_1\vdash
              G_1}{\pi}}\qquad\infer{G_2\vdash F_2}{\pi^\bot}} \qquad
 
      \infer[\ensuremath{\mathtt{cut}}]{\vdash G_1}{\infer[cut]{\vdash F_2}{\infer{\vdash
              G_3}{\psi}\qquad\infer{F_2\vdash
              G_2}{\pi^\bot}}\qquad\infer{F_1\vdash G_1}{\pi} }
              \rightsquigarrow \infer{\vdash G_3}{\psi}$} \]
  \end{corollary}

\section{Conclusion}\label{section:conclusion}

\subparagraph*{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 {\ensuremath{\mu\textsf{MALL}}} proofs. The latter result rests on the fact
that our isos are \emph{structurally recursive}.

\subparagraph*{Future works.}
We showned a one-way encoding from isos to proofs of {\ensuremath{\mu\textsf{MALL}}}, it is
clear that there exists proof-isomorphisms of {\ensuremath{\mu\textsf{MALL}}} that does not
correspond to an iso of our language, for instance taking the
reversible map function on streams. Therefore, a first extension to
our work would be to consider a two-way encoding and adding
coinductive types in the language. 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~\cite{sabry2018symmetric}, lists are the only recursive type which
is captured and recursion is terminating. The logic {\ensuremath{\mu\textsf{MALL}}} would
help in providing a finer understanding of termination and
non-termination

