\section{Introduction}
What is the inherent parallelism of higher-order functional programs?
Is it possible to turn $\lambda$-terms into low-level programs, at the
same time exploiting this parallelism? Despite great advances in very
close domains, these questions have not received a definite answer,
yet. The main difficulties one faces when dealing with parallelism
and functional programs are due to the higher-order nature of those
programs, which turns them into objects having a non-trivial
interactive behaviour.

The most promising approaches to the problems above are based on Game
Semantics~\cite{HylandO00,AbramskyJM00} and the Geometry of
Interaction~\cite{Girard89} (GoI), themselves tools which were
introduced with purely semantic motivations, but which have later been
shown to have links to low-level formalisms such as asynchronous
circuits~\cite{GhicaSS11}. This is especially obvious when Geometry of
Interaction is presented in its most operational form, namely as a
token machine~\cite{DanosRegnier}.

Most operational accounts on the Geometry of Interaction are in
\emph{particle-style}, i.e., a \emph{single} token travels around the
net; this is largely due to the fact that parallel computation without
any form of synchronization nor any data sharing is not particularly
useful, so having multiple tokens would not add anything to the
system. While some form of synchronization was implicit in earlier
presentations of GoI, the latter has been given a proper status only
recently, with the introduction of \textsf{SMLL}${}^0$~\cite{lics2014}, where
\emph{multiple} tokens circulate simultaneously, and also
\emph{synchronize} at a new kind of node, called a \emph{sync
  node}. All this has been realized in a minimalistic logic, namely
multiplicative linear logic, a logical system which lacks any copying
(or erasing) capability and, thus, is not an adequate model of realistic
programming languages (except purely linear ones, whose role is
relevant in quantum computation~\cite{SelingerValiron05}).

Multitoken GoI machines are relatively straightforward to define in a
linear setting: all \emph{potential} sources of parallelism give rise
to \emph{actual} parallelism, since erasing and copying are simply
forbidden. As a consequence, managing parallelism, and in particular
the spawning of new tokens, is easy: the mere syntactical occurrence
of a source of parallelism triggers the creation of a new
token. Concretely, these sources of parallelism are \emph{unit nodes}
(when thought logically), or \emph{constants} (when read through the lenses of
functional programming). The reader will find an example in
Section~\ref{sect:multexpo}, Fig.~\ref{fig:potential}.

But can all this scale to more expressive proof theories and
programming formalisms? If programs or proofs are allowed to copy or
erase portions of themselves, the correspondence between potential and
actual parallelism vanishes: any occurrence of a unit node can
possibly be erased, thus giving rise to \emph{no} token, or copied,
thus creating \emph{more than one} token. The underlying interactive
machinery, then, necessarily becomes more complex. But \emph{how}? The
solution we propose here relies on linear logic itself: it is the way
copying and erasing are handled by the exponential connectives of
linear logic which gives us a way out.  We find the resulting theory
simple and elegant.

In this paper we generalize the ideas behind \textsf{SMLL}${}^0${} in giving a
proper status to synchronization and parallelism in GoI. We show that
multiple tokens and synchronization can work well together in a
\emph{very expressive } logical system, namely multiplicative linear
logic with \emph{exponentials}, \emph{fixpoints}, and
\emph{units}. The resulting system, called \textsf{SMEYLL}, is then
general enough to simulate universal models of functional programming:
we prove that \ensuremath{\mathsf{PCF}}{} can be embedded into \textsf{SMEYLL}, both when
call-by-name and call-by-value evaluation are considered.  The latter
is not the case for single-token machines, as we illustrate in
Section~\ref{sect:multexpo}.

This is a   version extended with proofs and more details  of an eponymous paper \cite{lics2015} which appeared in the
proceedings of the Thirteenth Annual Symposium on Logic in Computer Science .

\subsection*{Contributions}
This paper's main contributions can be summarized as follows:
\begin{varitemize}
\item
  \emph{An Expressive Logical System.} We introduce \textsf{SMEYLL}{} nets,
  whose expressiveness is increased over $\textsf{MELL}$ nets by several
  constructs: we have \emph{fixpoints} (captured by the $Y$-box), an
  operator for \emph{synchronization} (the sync node), and a
  \emph{primitive conditional} (captured by the $\bot$-box).  The
  presence of fixpoints forces us to consider a restricted notion of
  reduction, namely closed \emph{surface reduction} (\emph{i.e.}, reduction
  never takes place inside a box).  Cuts can \emph{not} be eliminated
  (in general) from \textsf{SMEYLL}{} proofs, as one expects in a system with
  fixpoints.  Reduction, however, is proved to be
  \emph{deadlock-free}, \emph{i.e.}, normal forms cannot contain surface cuts.
\item
  \emph{A Multitoken Interactive Machine.} \textsf{SMEYLL}{} nets are seen as
  interactive objects through their synchronous interactive abstract
  machine (\textsf{SIAM}{} in the following). Multiple tokens circulate around
  the net simultaneously, and synchronize at sync nodes.  We prove
  that the \textsf{SIAM}{} is an \emph{adequate computational model}, in the
  sense that it precisely reflects normalization through machine
  execution.  The other central result about the \textsf{SIAM}{} is
  \emph{deadlock-freeness}, \emph{i.e.}, if the machine terminates it does so
  in a final state. In other words, the execution does not get stuck,
  which in principle could happen as we have several tokens running in
  parallel and to which we apply guarded operators (\emph{e.g.},
  synchronization). Our proof comes from the interplay of nets and
  machines: we transfer \emph{termination} from machines to
  nets, and then transfer \emph{back deadlock-freeness} from nets to
  machines.
\item
  \emph{A Fresh Look at CBV and CBN.}
  A slight variation on {\textsf{SMEYLL}} nets, and the corresponding notion
  of interactive machine, is shown to be an adequate model of
  reduction for Plotkin's \ensuremath{\mathsf{PCF}}~\cite{Plotkin}. This works both for call-by-name and
  call-by-value evaluation and, noticeably, the \emph{same}
  interactive machine is shown to work in \emph{both} cases: what
  drives the adoption of each of the two mechanisms is, simply, the
  translation of terms into proofs. What is surprising here is that
  CBV can be handled by a stateless interactive machine, even without
  the need to go through a CPS translation. This is essentially due to
  the presence of multiple tokens.
\item
  \emph{New Proof Techniques.} {Deadlock-freeness} is a key issue when
  working with multitoken machines.  A direct scheme to prove it (the
  one used in \cite{lics2014}) would be: (i) prove cut elimination for
  the nets, (ii) prove soundness for the machine, and (iii) deduce
  deadlock-freeness from (i) and (ii).  However, in a setting with
  fixpoints, cut elimination is not available because termination
  simply does not hold\footnote{Even without fixpoints, there is to
    the authors' knowledge no direct combinatorial proof of
    termination for surface reduction.}.  Instead, we develop a new
  technique, which heavily exploit the interplay between net rewriting
  and the multitoken machine.  Namely, we \emph{transfer} termination
  of the machine (including termination as a deadlock) into
  termination of the nets. This combinatorial technique is novel and
  uses multiple tokens in an essential way. It appears to be of
  technical interest in its own.
\end{varitemize}
\subsection*{Related Work}
Almost thirty years after its introduction, the literature on GoI is
vast. Without any aim of being exhaustive, we only mention the works
which are closest in spirit to what we are doing here.

The fact that  GoI can be turned into an implementation scheme for
purely functional (but expressive) $\lambda$-calculi, has been
observed since the beginning of the nineties~\cite{DanosRegnier,Mackie95}. Among
the different ways GoI can be formulated, both (directed) virtual
reduction and bideterministic automata have been shown to be amenable
to such a treatment. In the first case, parallel
implementations~\cite{PediciniQ07,Pinto01} have also been introduced. We
claim that the kind of parallel execution we obtain in this work is
different, being based on the underlying automaton and not on virtual
reduction.

The fact that GoI can simulate call-by-name evaluation is well-known,
and indeed most of earlier results relied on this notion of reduction.
As in games~\cite{AbramskyM97}, call-by-value requires a more
sophisticated machinery to be handled by GoI. This machinery, almost
invariably, relies on effects~\cite{HoshinoMH14,Schopp14}, even when
the underlying language is purely functional. This paper suggests an
alternative route, which consists in making the underlying machine
parallel, nodes staying stateless.

Another line of work is definitely worth mentioning here, namely Ghica
and coauthors' Geometry of Synthesis~\cite{Ghica07,GhicaS10}, in which
GoI suggests a way to compile programs into circuits. The obtained circuit,
however, is bound to be sequential, since the interaction
machinery on which everything is based is particle-style.

On the side of nets, Y-boxes allow us to handle \emph{recursion}. A
similar box was originally introduced by
Montelatici~\cite{Montelatici03}, even though in a polarized
setting. Our Y-box differs from it both in the typing and in the
dynamics; these differences are what make it possible to build a GoI
model.

\section{On Multiple Tokens and the Exponentials}\label{sect:multexpo}
In this section, we will explain through a series of examples
\emph{how} one can build a multitoken machine for a non-linear typed
$\lambda$-calculus, and \emph{why} this is not trivial.

Let us first consider a term computing a simple arithmetical
expression, namely $M=(\lambda x.\lambda y.x+y)(4-2)(1+2)$. This term
evaluates to $5$ and is purely linear, i.e. the variables $x$ and $y$
appear exactly once in the body of the abstraction.  How could one
evaluate this term trying to exploit the inherent parallelism in it?
Since we \emph{a priori} know that the term is linear, we know that
the subexpressions $S=(4-2)$ and $T=(1+2)$ are indeed needed to
compute the result, and thus can be evaluated in parallel. The
subexpression $x+y$ could be treated itself this way, but its
arguments are missing, and should be waited for. What we have just
described is precisely the way the multitoken machine for \textsf{SMLL}${}^0${}
works~\cite{lics2014}, as in Fig.~\ref{fig:potential} (left): each
constant in the underlying proof gives rise to a separate token, which
flows towards the result. Arithmetical operations act as
synchronization points.
\begin{figure}[h]
\begin{center}
\fbox{
\begin{minipage}{.47\textwidth}
\begin{center}\includegraphics[width=8cm]{potential}\end{center}
\end{minipage}}
\end{center}
\caption{Actual vs. Potential Parallelism.}\label{fig:potential}
\end{figure}
Now, consider a slight variation on the term $M$ above, namely
$N=(\lambda x.\lambda y.x+x)(4-2)(1+2)$. The term has a different
normal form, namely $4$, and is \emph{not} linear, for two different
reasons: on the one hand, the variable $x$ is used twice, and on the
other, the variable $y$ is not used at all. How should one proceed,
then, if one wants to evaluate the term in parallel? One possibility
consists in evaluating subexpressions \emph{only if} they are really
needed. Since the subexpression $x+x$ is of course needed (it is,
after all, the result!), one can start evaluating it. The value of the
variable $x$, as a consequence, is needed, and the subexpression it
will be substituted for, namely $4-2$, must itself be evaluated.  On
the other hand, $1+2$ should not be evaluated, simply because its value
does not contribute to the final result. This is precisely what
call-by-name evaluation actually do.  The interactive machine
which we define in this paper captures this process.  It has to be
noticed, in particular, that discovering that one of the
subexpressions is needed, while the other is not, requires some
work. The way we handle all this is strongly related to the structure
of the exponentials in linear logic. We give the CBN translation
of $N$ in Fig.~\ref{fig:potential} (right). The two rightmost
subterms are translated into exponential boxes (where $\mathsf{S}$ is
the net for $4-2$ and $\mathsf{T}$ for $1+2$), which serve as
\emph{boundaries} for parallelism: whatever potential parallelism a
box includes, must be triggered before giving rise to an actual
parallelism. Each of the occurrences of the variable $x$ triggers a
new kind of token, which starts from the dereliction nodes ($?d$) at the
surface  and whose purpose is precisely to look for the box the
variable will be substituted for. We call these \emph{dereliction
  tokens}.

What happens if we rather want to be consistent with
call-by-\emph{value} evaluation?  In this case, both subterms $(4-2)$
and $(1+2)$ in the term $N$ above should be evaluated. Let us however
consider a more extreme example, in which call-by-name and
call-by-value have different \emph{observable} behaviors, for example
the term $L=(\lambda x.1)\Omega$, where $\Omega=(\lambda x.xx)(\lambda
x.xx)$. The call-by-value evaluation of $L$ gives rise to divergence,
while in call-by-name $L$ evaluates to $1$.  Something extremely
interesting happens here.  We give the call-by-value translation of
$L$ in Fig.~\ref{fig:cbvomega}.
\begin{figure}[h]
\begin{center}
\fbox{
\begin{minipage}{.47\textwidth}
\begin{center}\includegraphics[width=8cm]{cvbDiverge2}\end{center}
\end{minipage}}
\end{center}
\caption{The CBV-translation of $(\lambda x.1)\Omega$.}\label{fig:cbvomega}
\end{figure}
First of all, we observe that a standard \emph{single-token} machine
would start from the conclusion, find the node $\mathsf{one}$, and exit
again: such a machine would simply converge on the term $L$. When
running on the term $\Omega$ alone, the machine would diverge, but as
subterm of $L$, $\Omega$ is never reached, so the machine's behaviour
on $L$ is not the one which we would expect in call-by-value.  Our
multitoken machine, instead, simultaneously launches tokens from all
dereliction nodes at surface: the dereliction token coming out of
$\Omega$ (represented on the right in Fig.~\ref{fig:cbvomega}) reaches
the Y-box, and makes the machine diverge.

We end this section by stressing that the interactive machine we use
is the same, and that this machine correctly models CBN and CBV, solely
depending on the chosen translation of terms into nets.  The
call-by-name translation of $L$ puts the subterm $\Omega$ in a box
which is simply unreachable from the rest of the net (as in the case
of $\mathsf{T}$ in Fig.~\ref{fig:potential}), and our machine
converges as expected. The call-by-value translation of $L$, on the
other hand, does \emph{not} put $\Omega$ inside a box. As a
consequence, there is no barrier to the computation to which $\Omega$
gives rise---the same as if $\Omega$ would be alone---and our machine
correctly diverges. This is the key difficulty in any interactive
treatment of CBV, and we claim that the way we have solved it is
novel.

\section{Nets and a Multitoken Interactive Machine }\label{sec:SMELLY}
We start with an overview of this section, which is divided into four
parts.
\paragraph*{Nets and Their Dynamics}
\textsf{SMEYLL}\ nets come with \emph{rewriting} rules, which provide an operational
semantics for them, and with a \emph{correctness} criterion, which
ultimately guarantees that nets rewriting is deadlock-free.
\paragraph*{Multitoken Machines}
On any net we define a \emph{multitoken} machine, called \textsf{SIAM}, which
provides an effective computational model in the style of GoI. A
fundamental property we need to check for the machine is
\emph{deadlock-freeness}, \emph{i.e.}, if the machine terminates it does so in
a final state. From the beginnings of linear logic, the correctness
criterion of nets has been interpreted as deadlock-freeness in
distributed systems \cite{Asperti}; this is also the case for
\textsf{MELLS}. Here, however, we work with surface reduction, and we have
fixpoints. For these reasons, a rather refined approach is needed.
\paragraph*{The Interplay Between Nets and Machines}
Nets rewriting and the \textsf{SIAM}{} are tightly related. We establish the
following results. Let $R$ denote a net, $\mathcal{M}_R$ its machine, and
$\red$ the net rewriting relation. First of all, we know that (i)
if $R$ is cut-and-sync-free, the machine $\mathcal{M}_R$ terminates in a final
state. On the net hand, we establish that (ii) \emph{net rewriting is
  deadlock-free}: if no reduction is possible from $R$, then $R$ is
cut-and-sync-free.  On the machine side, we establish that (iii) if
$R\red S$ then $\mathcal{M}_R$ converges/deadlocks iff the same holds for
$\mathcal{M}_{S}$. We then use the multitoken paradigm to provide a decreasing
parameter for net rewriting, and establish that (iv) if $\mathcal{M}_R$
terminates, then $R$ has no infinite sequence of reductions.
Putting all this together, it follows that \emph{multitoken
  machines are deadlock-free}.
\paragraph*{Computational Semantics}
Finally, by using the machine representation, we associate a
denotational semantics to nets, which we prove to be sound with
respect to net reduction.
\subsection{Nets and Their Dynamics.}
In this section we introduce \textsf{SMEYLL}\ nets, which are a generalization
of \textsf{MELL}\ proof nets. For a detailed account on proof nets,
we refer the reader to Laurent's notes \cite{LaurentTorino}: our
approach to correctness, as well as the way to deal with weakening, is
very close to the one described there.
\subsubsection{Formulas}
The language of \textsf{SMEYLL}{} \emph{formulas} is identical to the one for
\textsf{MELL}.
The language of formulas is therefore:
$$
A ::= \mathsf{1}\; \; \mbox{\Large{$\mid$}}\;\;
\bot\; \; \mbox{\Large{$\mid$}}\;\; X\; \; \mbox{\Large{$\mid$}}\;\; X\b\middA\otimesA\middA\parrA\; \; \mbox{\Large{$\mid$}}\;\;!A\; \; \mbox{\Large{$\mid$}}\;\; ?A,
$$
where $X$ ranges over a denumerable set of {propositional variables}.
The constants $1,\bot$ are the \emph{units}. \emph{Atomic formulas} are
those formulas which are either propositional variables or units.
Linear negation $(\cdot)\b$ is extended into an involution on all
formulas as usual: $A\b\b\equiv A$, $1\b\equiv \bot $,
$(A\otimesB)\b\equiv A\b\parr B\b $,
$(!A)\b \equiv{} ?A\b$.  Linear implication is a defined
connective: $A\linB\equivA\b\parrB$.

Atoms and connectives of linear logic are usually divided in two
classes: positive and negative. Here however, we define
\emph{positive} (denoted by $P$) and \emph{negative} (denoted by $N$)
those formulas which are built from units in the following way: $P ::=
\mathsf{1} \; \; \mbox{\Large{$\mid$}}\;\;P\otimesP$, and $N::= \bot
\; \; \mbox{\Large{$\mid$}}\;\;N\parrN$. So in particular, there are formulas
which are neither positive nor negative, e.g.\ $\bot\parr\mathsf{1}$.
\subsubsection{Structures}
A \textsf{SMEYLL}{} \emph{structure} is a finite labeled \emph{directed} graph
built over the alphabet of nodes which is represented in
Fig.~\ref{SMELLYnets} (where the \emph{orientation} is the top-bottom
one). All edges have a source, but some edges may have no target; such
dangling edges are called the \emph{conclusions of the structure}. The
edges are labeled with \textsf{SMEYLL}{} formulas; the label of an edge is
called its \emph{type}.  We call those edges which are represented
below (resp. above) a node \emph{conclusions} (resp. \emph{premisses})
of the node.  We will often say that a node ``has a conclusion
(premiss) $A$'' as shortcut for ``has a conclusion (premiss) of
type $A$''.  When we need more precision, we distinguish
between an edge and its type, and we use variables such as $e,f$ for
the edges.

The nodes $! $, $Y$ and $\bot$ are called \emph{boxes}. One among
their conclusions (the leftmost ones in Fig.~\ref{SMELLYnets}, which
have type $!A$, $!A$ and $\bot$, respectively) is said to be
\emph{principal}, the other ones being \emph{auxiliary}.
$!$-boxes and Y-boxes are \emph{exponential}. An exponential box is
\emph{closed} if it has no auxiliary conclusions. To each box is associated, in an
 inductive way,  a structure which is called the
\emph{content} of the box. To the $!$-box we associate a structure
with conclusions $A,?\Gamma$. To the Y-box corresponds a structure of
conclusions $A, ?A\b, ?\Gamma$. To the {$\bot$-box} is associated a
structure of non-empty conclusions $\Gamma$, together with a new node
$\mathsf{bot}$ of conclusion $\bot$. We represent a box $b$ and its content
$S$ as in Fig.~\ref{SMELLYboxes}.  With a slight abuse of terminology,
the nodes and edges of $S$ are said to be \emph{inside} $b$.
Similarly, a crossing of any box's border is said to be a \emph{door},
and we often speak of premiss and conclusion \emph{of a} (principal or
auxiliary) \emph{door}. Note that the principal door of the Y-box
(marked by Y) has premisses $A,?A\b$ and conclusion $!A$.

A node \emph{occurs at depth 0} or \emph{at surface} in the structure
$R$ if it is a node of $R$, while it \emph{occurs at depth $n+1$} in
$R$ if it occurs at depth $n$ in a structure associated to a box of
$R$. Please observe that nets being defined inductively, the depth of
nodes is always finite.
 \begin{figure}[htbp]
   \begin{center}
     \fbox{
       \begin{minipage}{.47\textwidth}
         \begin{center}\includegraphics[width=8cm]{SMELLYnets}\end{center}
     \end{minipage}}
   \end{center}
   \caption{\textsf{SMEYLL}\ Nodes.}\label{SMELLYnets}
 \end{figure}
 \begin{figure}[htbp]
   \begin{center}
     \fbox{
       \begin{minipage}{.47\textwidth}
         \begin{center}\includegraphics[width=8cm]{SMELLYboxes}\end{center}
     \end{minipage}}
   \end{center}
   \caption{\textsf{SMEYLL}\ Boxes.}\label{SMELLYboxes}
 \end{figure}
The sort of each node induces constraints on the number and the labels
of its premisses and conclusions, which are shown in
Fig.~\ref{SMELLYnets}. We observe that the $\bot$-box is \emph{the
  same} as in \cite{Girard87} and corresponds to the sequent calculus
rule $\infer[]{ \vdash \bot, \Gamma }{\vdash \Gamma}$. All nodes are
standard except sync nodes and Y-boxes, which need some further
explanation:
\begin{varitemize}
\item
  Y-boxes model \emph{recursion} (more on this when we introduce the
  reduction rules). Proof-theoretically, the Y-box corresponds to
  adding the following fix-point sequent calculus rule to \textsf{MELL}: $$
  \infer[Y]{ \vdash !A,?\Gamma }{\vdash A, ?A\b,?\Gamma} $$
\item
  Sync nodes model {\em synchronization points}. A sync node has $n$
  premisses and $n$ conclusions; for each $i$ ($1\leq i\leq n$) the
  $i$-th premiss and the \emph{corresponding} $i$-th conclusion are
  typed by the \emph{same} formula, which needs to be \emph{positive}.
\end{varitemize}

\vskip 4pt

\noindent\emph{Simple and positive structures.}
Two relevant classes of structures are  simple and positive structures. A formula is \emph{simple} it is is built out of $\{X,X\b, 1, \otimes, \parr\}$. A structure
$R$ is \emph{simple (resp. positive)} if all its conclusions are simple (resp. positive)
formulas. This \emph{does not} mean that all formulas occurring in $R$
are  simple (resp. positive). $R$ can be very complex; the
constraint only deals with $R$'s conclusions.

\subsubsection{Correctness}
A \emph{net} is a structure which fulfills a \emph{correctness
  criterion} defined by means of {switching paths} (see
\cite{LaurentTorino}).  A \emph{switching path} on the structure $R$
is an undirected path\footnote{By path, in this paper we always mean a
  \emph{simple path} (no repetition of either nodes or edges).}  such that
(i) for each $\parr$-or-$?c$-node, the path uses at most one of the
two \emph{premisses}, and (ii) for each sync node, the path uses at
most one of the \emph{conclusions}.  The former condition is standard,
the latter condition rules out paths which bounce on sync nodes ``from
below'': a path crossing a sync node may traverse one premiss and one
conclusion, or traverse two distinct premisses. A structure is
\emph{correct} if:
\begin{varenumerate}
\item
  none of its switching paths are cyclic, and
\item
  the content of each of its boxes is itself correct.
\end{varenumerate}
The reader familiar with linear logic correctness criteria did
probably notice that the only condition we require is acyclicity, and
that connectedness is simply not enforced (as, e.g., in Danos and
Regnier's criterion~\cite{DanosRegnierMult}).  Actually, the only role of
connectedness consists in ruling out the so-called Mix rule from the
sequent calculus. This is not relevant in our development, so we will
ignore it. An advantage of accepting the Mix rule is that we do not
need extra conditions for dealing with weakening. A similar approach
is adopted by Laurent~\cite{LaurentTorino}.  In the following, when we
talk of \textsf{MELL}{} (resp. \ensuremath{\textsf{MLL}}{}), we actually always mean \textsf{MELL}{} + Mix
(resp. \ensuremath{\textsf{MLL}}{} + Mix).
\subsubsection{Net Reduction}
Reduction rules for nets are sketched in Fig.~\ref{SMELLYred}.
Reduction rules can be applied only at surface (\emph{i.e.}, when the redex
occurs at depth $0$), and not in an arbitrary context.  Moreover,
observe that reduction rules involving an \emph{exponential} box can
only be applied when the box is \emph{closed}, \emph{i.e.}, when it has no
auxiliary doors.  We write $\rightsquigarrow$ for the rewriting relation induced
by these rules. Some reduction rules deserve some further
explanations:
\begin{varitemize}
\item
  The $y$-rule unfolds a Y-box, this way modeling recursion.  The
  intuition should be clear when looking at the translation of the
  \ensuremath{\mathsf{PCF}}\ term $L=\PCFletrec{f}{x}{M}{N}$, which reduces to the explicit
  substitution of $f$ by $\lambda x.\PCFletrec{f}{x}{M}{M}$ in $N$,
  call it $P$. Indeed, the encoding of $L$ reduces to the encoding of
  $P$:
  \begin{center}
    \includegraphics[width=6cm]{Yexample}\label{fig:Yexample}

  \end{center}
  (where $M^\dagger$ and $N^\dagger$ stand for the encodings of $M$
  and $N$, respectively). When (and only if!) $N$
  recursively calls $f$, the corresponding $d$ node
  ``opens'' the $!$-box for the first iteration of $f$; if
  $f$ further uses a recursive call of itself, the $Y$-box again
  turns into yet another $!$-box and is opened, and so on.
\item
  The $s.el$-rule erases a sync link whose premisses are \emph{all}
  conclusions of $\mathsf{one}$ nodes.
\item
  The $w$-rule, corresponding to a cut with weakening, \emph{deletes}
  the redex (because the box has no auxiliary conclusions).
\item
  The $bot.el$-rule opens a $\bot$-box.
\end{varitemize}
\begin{figure}[htbp]
  \begin{center}
    \fbox{
      \begin{minipage}{.47\textwidth}
        \begin{center}
          \includegraphics[width=8cm]{SMELLYred_refined}
        \end{center}
    \end{minipage}}
  \end{center}
  \caption{\textsf{SMEYLL}\ Net Rewriting Rules.}\label{SMELLYred}
\end{figure}
It is immediate to check that correctness is preserved by all reduction rules.
\begin{lemma}
  If $R$ is a net and $R\rightsquigarrow S$, then $S$ is itself a net.
\end{lemma}
Since the constraints exclude most of the commutations
which are present in \textsf{MELL}, rewriting enjoys a strong form of
confluence:
\begin{prop}[Confluence and Uniqueness of Normal Forms]\label{net_conf}
  The rewriting relation $\rightsquigarrow$ has the following properties:
  \begin{varenumerate}
  \item
    it is confluent and normal forms are unique;
  \item
    any net weakly normalizes iff it strongly normalizes.
\end{varenumerate}
\end{prop}
\begin{proof}
The only critical pairs are the trivial ones of \ensuremath{\textsf{MLL}}, leading to the
same net. Therefore, reduction enjoys a  diamond property (uniform
confluence): if $R \rightsquigarrow S$ and $R\rightsquigarrow T$, then either $S=T$ or
there exists $U$ such that $S\rightsquigarrow U$ and $T\rightsquigarrow U$.
(1) and (2) are direct consequences.
\end{proof}
The strict constraints on rewriting, however, render cut elimination
non-trivial: it is not obvious that a reduction step is available
whenever a cut is present. We need to prove that in presence of a cut,
there is always a valid redex (\emph{i.e.}, it is surface, and any exponential
box acted upon is closed). The main difficulty comes from $\bot$-boxes, as
they can hide large parts of the net, and in particular dereliction
nodes which may be necessary to fire a reduction. However, the
following establishes that as long as there are cuts or syncs, it is
always possible to perform a valid reduction.
\begin{thm}[Deadlock-Freeness for Nets]\label{main_lem}
  Let $R$ be a simple \textsf{SMEYLL}{} net. If $R$ contains cuts or sync nodes,
  then  a reduction applies, \emph{i.e.}\ there exists $S$ such that $R\rightsquigarrow S$.
\end{thm}
The rather long proof is given in Appendix~\ref{app:SMELLY}. The key element is the
definition of an order on the boxes which occur  at depth $0$ in $R$;
the existence of such an order relies on the correctness criterion. The order
captures the dependency among boxes, \emph{i.e.}, exposes the order in which
cuts are eliminated.

\begin{cor}[Cut Elimination] \label{cutel}
  Let $R$ be a simple \textsf{SMEYLL}\ net. If $R\rightsquigarrow^* S$ and $S$ cannot be
  further reduced, then $S$ is a cut free \ensuremath{\textsf{MLL}}{} net\footnote{Precisely, \ensuremath{\textsf{MLL}}{} + Mix, as we have already pointed
      out.}, \emph{i.e.}, it  only containing $\mathsf{ax}$,
  $\mathsf{one}$, $\otimes$, $\parr$ nodes.
\end{cor}
\paragraph*{Discussion on simple structures}
The hypothesis which we make in Theorem \ref{main_lem}  that a structure is simple
is an assumption which in this section we use
\emph{to simplify auxiliary lemmas}; it will not appear in our main
result, namely Theorem~\ref{SIAM deadlock free}.
\subsection{\textsf{SIAM}}\label{SIAM}
All along this section, $R$ indicates a \textsf{SMEYLL}\ structure
(with no other  hypothesis, unless otherwise stated).
\subsubsection{Preliminary Notions}
Some auxiliary definitions are needed before we can introduce our
interactive machines.  \emph{Exponential signatures} are defined by
the following grammar
$$
  \sigma ::= {*} \; \; \mbox{\Large{$\mid$}}\;\; l(\sigma) \; \; \mbox{\Large{$\mid$}}\;\; r(\sigma)
  \; \; \mbox{\Large{$\mid$}}\;\; \encode{\sigma}{\sigma} \; \; \mbox{\Large{$\mid$}}\;\; y(\sigma,\sigma),
$$
while \emph{stacks} are defined as follows
$$
  \mathord{s} ::= \epsilon \; \; \mbox{\Large{$\mid$}}\;\; l.\mathord{s} \; \; \mbox{\Large{$\mid$}}\;\; r.\mathord{s} \; \; \mbox{\Large{$\mid$}}\;\; \sigma.\mathord{s} \; \; \mbox{\Large{$\mid$}}\;\; \delta,
$$
where $\epsilon$ is the empty stack and $.$ denotes concatenation
(and, thus, $s.\epsilon=s$). Given a formula $A$, a stack $\mathord{s}$
\emph{indicates an occurrence $\alpha$ of an atom} (resp. \emph{an
  occurrence $ \mu$ of a modality}) in $A$ if $\mathord{s}[A]=
\alpha$ (resp. $\mathord{s}[A]= \mu$), where $\mathord{s}[A]$ is defined as
follows:
\begin{varitemize}
\item
  $\epsilon [\alpha] = \alpha$,
\item
  $\sigma.\delta[\mu B] = {\mu}$,
\item
  $\sigma.t[\mu B] = t[B] $ whenever $t\neq\delta$,
\item
  $l.t[B \Box C]= t[B] $ and $r.t[B
  \Box C]=t[C]$, where $\Box$ is either $\otimes$
  or $\parr$.
\end{varitemize}
We observe that a stack can indicate a modality only if its head is
$\delta$.
\begin{example}\label{ex:indic}
  Given the formula $A =\bang(\bot\otimes{!\mathsf{1}})$, the stack $*.\delta$
  indicates the first occurrence of $\bang$, $ *.r.*.\delta[A]$ gives the
  second occurrence of $!$, and $*.\delta, *.l[A]=\bot$.
\end{example}
The set of $R$'s \emph{positions} $\POSALL_R$ contains all the triples
in the form $(\mathord{e}, \mathord{s}, \mathord{t})$, where:
\begin{varenumerate}
\item
  $\mathord{e}$ is an edge of $R$,
\item
  the \emph{formula stack} $\mathord{s}$ is either $\delta$ or a stack which
  indicates an occurrence of atom or modality in the type $A$ of
  $\mathord{e}$,
\item
  the \emph{box stack} $\mathord{t}$ is a stack of $n$ exponential
  signatures, where $n$ is the number of exponential boxes inside
  which $\mathord{e}$ appears.
\end{varenumerate}
We use the metavariables $\ss$ and $\mathbf{p}$ to indicate positions. For
each position $\mathbf{p}=(\mathord{e},\mathord{s},\mathord{t})$, we define its \emph{direction}
$\mathtt{dir} (\mathbf{p})$ as \emph{ upwards} ($\uparrow$) if $\mathord{s}$ indicates an
occurrence of $!$ or of negative atom, as \emph{downwards} ($\downarrow$)
if $\mathord{s}$ indicates an occurrence of $?$ or of positive atom, as
\emph{stable} ($\leftrightarrow$) if $\mathord{s}= \delta$ or if the edge $\mathord{e}$ is
the conclusion of a $\mathsf{bot}$ node. A position $\mathbf{p}=(\mathord{e}, \mathord{s}, \epsilon)$
is \emph{initial} (resp. \emph{final}) if $e$ is a conclusion of
$R$, and $dir(\mathbf{p})$ is $\uparrow$ (resp. $\downarrow$). For simplicity, on
initial (final) positions, we require all exponential signatures in
$\mathord{s}$ to be $*$. So for example, if $!(\bot\otimes{!\mathsf{1}})$ is a
conclusion of $R$, there is one final position ($s=*.r.*$), and three
initial positions (the three stacks given in Example~\ref{ex:indic}). The
following subsets of $\POSALL_R$ play a crucial role in the definition
of the machine:
\begin{varitemize}
\item
  the set $\mathtt{INIT}_R$ of all \emph{initial positions};
\item
  the set $\mathtt{FIN}_R$ of all \emph{final positions};
\item
  the set $\mathtt{ONES}_{R}$ of positions $(\mathord{e}, \epsilon, \mathord{t})$ where
  $\mathord{e}$ is the conclusion of a $\mathsf{one}$ node;
\item
  the set $\mathtt{DER}_{R}$ of positions $(\mathord{e}, *.\delta, \mathord{t})$
  where $\mathord{e}$ is the conclusion of a $\mathsf{?d}$ node;
\item
  the starting positions $\mathtt{START}_{R}= \mathtt{INIT}_R \cup
  \mathtt{ONES}_{R}\cup \mathtt{DER}_{R} $;
\item
  the set $\mathtt{PRIVATE}_R$ of the positions $\mathbf{p}$ for which
  $\mathtt{dir}(\mathbf{p})=\leftrightarrow$.
\end{varitemize}
The multitoken machine $\machine{R}$ for $R$
consists of a set of \emph{states} and a \emph{transition} relation
between them. These are the topics of the following two subsections.
\subsubsection{States}
A state of $\machine{R}$ is a snapshot description of the tokens
circulating in $R$. We also need to keep track of the positions
where the tokens started, so that the machine only uses each starting
position once. Formally, a \emph{state} $\mathbf{T} = ( Cod(\mathbf{T}), Dom(\mathbf{T}))$ is a
set of positions $Cod(\mathbf{T}) \subseteq \POSALL_R$ together with a set of
positions $Dom(\mathbf{T}) \subseteq \mathtt{START}_R$.  Intuitively, $Cod(\mathbf{T}) $ describes
the current position of the tokens, and $Dom(\mathbf{T})$ keeps track of which
starting positions have been used\footnote{In Section~\ref{tracing} we
  show that $Dom(\mathbf{T})$ is actually redundant; we have however decided to
  give it explicitly, because it makes the definition of the machine
  simpler.}. A state is \emph{initial} if $ Cod(\mathbf{T})=Dom(\mathbf{T})=\mathtt{INIT}_R$. We
indicate the (unique) initial state of $\mathcal{M}_R$ by $\mathbf{I}_R$. A state
$\mathbf{T}$ is \emph{final} if all positions in $Cod(\mathbf{T})$ belong to either
$\mathtt{FIN}_R$ or $\mathtt{PRIVATE}_R$. The set of all states will be denoted by
$\mathcal{S}_{R}$. Given a state $\mathbf{T}$ of $\mathcal{M}_R$, we say that
\emph{there is a token in $\mathbf{p}$} if $\mathbf{p}\in Cod(\mathbf{T})$.  We use
expressions such as ``a token moves'', ``crosses a node'', in the
intuitive way.
\subsubsection{Transitions}
The transition rules of $\machine{R}$ are given by the
transitions described in Fig.~\ref{fig:trRules} (where $\Box$ stands
for either $\otimes$ or $\parr$). The rules marked by (i)--(iii)
make the machine concurrent, but the constraints they need to satisfy are rather
technical and for this reason we prefer to postpone the related
discussion.
\paragraph*{Transition Rules, Graphically}
The position $\mathbf{p} = (\mathord{e}, \mathord{s}, \mathord{t})$ is represented graphically by
marking the edge $e$ with a bullet $\bullet$, and writing the stacks
$(\mathord{s}, \mathord{t})$.  A transition $\mathbf{T} \rightarrow \mathbf{U}$ is given by
depicting only the positions in which $\mathbf{T}$ and $\mathbf{U}$ differ.  It
is of course intended that all positions of $\mathbf{T}$ which do not
explicitly appear in the picture also belong to $\mathbf{U}$.  \condinc{}{
  \todo{ To represent a transition $\mathbf{T} \rightarrow \mathbf{U}$, we depict
    $\mathtt{pos}(\ss)$ in the left-hand-side, and $\mathtt{pos_{\sttwo}}(\ss)$ on the
    right-hand-side of the arrow, for each $\ss\inDom(\mathbf{T})$ such that
    $\mathtt{pos_{\sttwo}}(\ss)\not=\mathtt{pos}(\ss)$.  It is of course intended that
    $\mathtt{pos_{\sttwo}}(\ss)=\mathtt{pos}(\ss)$ for all $\ss$ whose value is not
    explicitly appearing in the picture.  }}  To save space, in
Fig.~\ref{fig:trRules} we annotate the transition arrows with a
\emph{direction}; we mean that the rule applies (only) to positions
which have that direction.  We sometimes explicitly indicate the
direction of a position by directly annotating it with
${}^{\downarrow},{}^{\uparrow}$ or ${}^{\leftrightarrow}$. Notice that no transition is
defined for stable positions.  We observe that tokens \emph{changes
  direction} only in one of two cases: either when they move from an
edge of type $A$ to an edge of type $A\b$ (\emph{i.e.}, when crossing a
$\mathsf{ax}$ or a $\mathsf{cut}$ node), or when they cross a $Y$-node, in the
case where the transitions are marked by (*): moving down from the
edge $A$ and then up to $?A\b$, or vice versa.  Whenever a token is on
the conclusion of a box, it can move into that box (graphically, the
token ``crosses'' the border of the box) and it is modified as if it
were crossing a node. For exponential boxes, in Fig.~\ref{fig:trRules}
we depict only the border of the box. The transitions for the
multiplicative nodes $\mathsf{ax}$, $\mathsf{cut}$, $\otimes$, $\parr$ are the
standard ones.  The rules for \emph{exponential nodes} are mostly
standard. There are however two novelties: the introduction of
``dereliction tokens", \emph{i.e.}, tokens which start their path on the
conclusion of a $?d$ node, and the $Y$ box. We discuss both below.
\paragraph*{Some Further Comments}
Certain peculiarities of our interactive machines need to be further
discussed:
\begin{varitemize}
\item
  \emph{Y-boxes}.  The recursive behaviour of Y-boxes is captured by
  the exponential signature in the form $y(\cdot,\cdot)$, which
  intuitively keeps track of how many times the token has entered a
  Y-box so far. Let us examine the transitions via the $Y$ door.  Each
  transition from $!A$ (conclusion of $Y$) or from $?A\b$ (premiss of
  $Y$) to the edge $A$ (premiss of $Y$) corresponds to a recursive
  call. The transition from $A$ to $?A\b$ captures the return from a
  recursive call; when all calls are unfolded, the token exits the
  box.  The auxiliary doors of a $Y$-box have the same behaviour as
  those of $!$-boxes.
\item
  \emph{Dereliction Tokens}.  As we have explained in
  section~\ref{sect:multexpo}, this is a key feature of our machine.
  A dereliction token is generated (according to conditions (i) below)
  on the conclusion of a $\mathsf{?d}$ node, as depicted in
  Fig.~\ref{fig:trRules}. Intuitively, each dereliction token
  corresponds to a copy of a box.
\item
  \emph{Box Copies and stable tokens.} A token in a stable position is said to be
  \emph{stable}.
   Each such token is the remains of a token which
  started its journey from $\mathtt{DER}$ or $\mathtt{ONES}$, and flowed in the graph
  ``looking for a box''.
   This stable token that was once roaming the net
  therefore witnesses the fact that \emph{an instance} of dereliction
  or of $\mathsf{one}$ ``has found its box''.  Stable tokens play an
  essential role, as they keep track of box copies. We are going to
  formalize this immediately below.

  It is immediate to check that a stable token
    can only be located inside a box, more precisely on the premiss of
    its principal door.
  In  Fig.~\ref{SIAM_stable} we indicate   explicitly  all the exponential  transitions which lead to a stable  position; the other transition leading to a stable position is the one on $\bot$-box.
      \begin{figure}[htbp]
        \centering
        \fbox{
        \includegraphics[width=7cm]{SIAM_stable}}
        \caption{Exponential transitions to a stable position }\label{SIAM_stable}
      \end{figure}

\end{varitemize}
\begin{figure}[htbp]
  \begin{center}
    \fbox{
    \begin{minipage}{.47\textwidth}
      \begin{center}
        \includegraphics[width=8cm]{SIAM_transitions}
      \end{center}
    \end{minipage}}
  \end{center}
  \caption{\textsf{SIAM}{} Transition Rules.} \label{fig:trRules}
\end{figure}

\paragraph*{Multitoken Rules}
The rules (i)--(iii) from Fig.~\ref{fig:trRules} are where the  multitoken
nature of the \textsf{SIAM}{} really comes into play.  Those rules are subject to certain conditions,
which are intimately related to box copies. Given a state $\mathbf{T}$ of
$\mathcal{M}_R$, we define $\mathtt{Instances}_{\mathbf{T}}(S)$ to be $\{\epsilon\}$ if $R=S$ (we are at depth 0).
Otherwise, if $S$ is the structure associated to a box node $b$ of $R$, we
define $\mathtt{Instances}_{\mathbf{T}}(S)$ as the set of all $t$ such that $t$ is the box stack
of a stable token at the principal door of $b$.  Intuitively, as we
discussed above, the box stack of each such a token \emph{identifies a
  copy of the box} which contains $S$.
Rules marked as (i)--(iii) only apply if certain conditions are
satisfied:
\begin{varitemize}
\item[(i)]
  The position $(\mathord{e},\epsilon,\mathord{t})$ (resp. $(\mathord{e},\delta,\mathord{t})$) does
  not already belong to $Dom(\mathbf{T})$, and $\mathord{t}\in \mathtt{Instances}_{\mathbf{T}}(S)$, where $S$ is
  the structure to which $e$ belongs.  If both conditions are
  satisfied, $Cod(\mathbf{T})$ and $Dom(\mathbf{T})$ are extended with the position $\mathbf{p}$.
  This is the only transition changing $Dom(\mathbf{T})$. Intuitively, each
  $\mathord{t}$ corresponds to a copy of the (box containing the) $\mathsf{one}$ (resp. $?d$) node.
\item[(ii)]
  The token moves inside the $\bot$-box\ only if its box stack $\mathord{t}$
  belongs to $\mathtt{Instances}_{\mathbf{T}}(S)$, where $S$ is the content of the $\bot$-box.
  (Notice that if the $\bot$-box\ is inside
  an exponential box, there could be several stable tokens at its
  principal door, one for each copy of the box.)
\item[(iii)]
  Tokens cross a sync node $l$ only if for a certain $\mathord{t}$, there is
  a token on each position $(e,\mathord{s},\mathord{t})$ where $e$ is a premiss of
  $l$, and $\mathord{s}$ indicates an occurrence of atom in the type of
  $e$. In this case, all tokens cross the link simultaneously.
  Intuitively, insisting on having the same stack $\mathord{t}$ means that
  the tokens all belong to the same box copy. The simultaneous
  transition of the tokens has to be related to the $s.el$-rule, which
  takes place only when \emph{all} premisses are conclusions of $\mathsf{one}$
  nodes. Note that the tokens traverse a sync link only downwards,
  because all edges are positive.
\end{varitemize}

A \emph{run} of the \textsf{SIAM}{} machine of $R$ is a \emph{maximal}
sequence of transitions $\mathbf{I}_R \rightarrow  \cdots \rightarrow
\mathbf{T}_n \rightarrow \cdots $ from an initial state $\mathbf{I}_R$.\\

\subsubsection{Basic Properties}
In this and next section, we study some properties of the \textsf{SIAM}.  We
write $\mathbf{T} \nrightarrow$ if no reduction applies from $\mathbf{T}$. A non final
state $\mathbf{T} \nrightarrow$ is called a \emph{deadlock} state.  If $\mathbf{I}_R
\rightarrow \mathbf{T}_1 \rightarrow ...\rightarrow \mathbf{T}_n \nrightarrow $ is a run of
$\mathcal{M}_R$ we say that the run \emph{terminates} (in the state $\mathbf{T}_n$).
A run of $\mathcal{M}_R$ \emph{diverges} if it is infinite, \emph{converges}
(resp. \emph{deadlocks}) if it terminates in a final (resp. non final)
state.

\noindent
  \begin{prop}[Confluence and Uniqueness of Normal Forms]\label{lem:diamProp}\label{machine_conf}
    The relation $\rightarrow$ enjoys the following properties:
    \begin{varitemize}
    \item
      it is confluent and normal forms are unique;
    \item
      if a run of the machine $\mathcal{M}_R$ terminates, then all runs of $\mathcal{M}_R$ terminate.
    \end{varitemize}
  \end{prop}
  \begin{proof}
    By checking each pair of transition rules we observe that
    $\rightarrow$ has the diamond property, because the transitions
    do not interfere with each other.
  \end{proof}

\condinc{}{\todo By Lemma \ref{lem:diamProp}, all runs of $\mathcal{M}_R$ have the same behaviour. We can therefore say that
  $\mathcal{M}_R$ \emph{diverges} if    $\mathcal{M}_R$ has an infinite run,  \emph{converges} if its runs converge,   \emph{deadlocks} if its runs do.
By using Lemma \ref{trsf_prop} we can prove that

  \begin{prop}[\todo{What is a good name for this??}]\label{basic_soundness}
    Assume  $R \rightsquigarrow S$. $\mathcal{M}_R$ diverges, converges or deadlocks if and only if  $\mathcal{M}_{S}$   diverges, converges or deadlocks.\\

  \end{prop}
}

\subsubsection{Tracing Back}\label{tracing}
For each position $\mathbf{p}$ in $R$, we observe (by examining the cases in
Fig.~\ref{fig:trRules}) that there is at most one position from which
$\mathbf{p}$ can come via a transition. When disregarding the conditions we
impose on rules labelled as (i)--(iii), the transitions also apply to
a single token, in isolation. By reading the transitions
``backwards'', we can therefore define a partial function $\mathrm{orig} :
\POSALL_R \rightharpoonup \mathtt{START}_R$, where $\mathrm{orig}(\mathbf{p}) := \ss$ if $\mathbf{p}$ traces
back to $\ss$. But there is more:
\begin{lemma}\label{lemma:traceback}
  For any state $\mathbf{T}$ such that $\mathbf{I}_R \rightarrow^* \mathbf{T}$, the
  restriction of $\mathrm{orig} $ to $Cod(\mathbf{T})$ is a total, injective function.
\end{lemma}

Therefore, for every position $\mathbf{p}$  which appears in a run of $\mathcal{M}_R$,
$\mathrm{orig}(\mathbf{p})$ is defined.

With this in mind, $\mathtt{START}_R$ can be seen as an index set identifying
each token. For most of this section (until Theorem~\ref{soundness})
we are only interested in the ``wave'' of tokens, and do not need to
distinguish them individually. In Section~\ref{sec:beyond},
however, we heavily rely on $\mathrm{orig}$ to associate values and
operations to tokens.

\begin{rem}
Tracing back from $Cod(\mathbf{T})$ allows us to reconstruct $Dom(\mathbf{T})$ from the set of current positions. We have preferred to carry along $Dom(\mathbf{T})$ in the definition of state to make it more immediate,
since the definition of $\mathrm{orig}$ is rather technical. Similarly,
 in order not to trace back all the way each time we need the starting position, one can also make the choice to  carry the function  along with the state.  We made a similar choice  in our
 previous work \cite{lics2014}, where a state was defined as a function $ Dom(\mathbf{T}) \to \POSALL_R$
The two definitions  are of course equivalent for all states which can be reached from the initial state, thanks to Lemma~\ref{lemma:traceback}.
\end{rem}

\subsubsection{State Transformation}\label{def:Transformation}
Our central tool to relate net rewriting and the \textsf{SIAM}{} is a mapping
of states to states. More precisely, if $R \rightsquigarrow S$, we
define a \emph{transformation} as a partial function $\mathrm{trsf}_{R
  \rightsquigarrow S}: \POSALL_{R} \rightharpoonup \POSALL_{S}$, which
extends to a transformation on states $\mathrm{trsf}_{R \rightsquigarrow S}:
\mathcal{S}_{R} \rightharpoonup \mathcal{S}_{S}$ in the obvious way,
point-wise. We will omit the subscript $R \rightsquigarrow S$ of
$\mathrm{trsf}_{R \rightsquigarrow S}$ whenever it is obvious.

Assume $R \rightsquigarrow_{a} S$ (axiom step), and $\mathbf{p}=(d, s,
\epsilon) \in \POSALL_{R}$. If $d\in \{e, f, g\}$ as shown in
Fig.~\ref{fig:trsf}(a), then $\mathrm{trsf}_{R \rightsquigarrow S}(\mathbf{p}):=(h,
s, \epsilon) \in \POSALL_{S} $.  For the other edges, $
\mathrm{trsf}_{R \rightsquigarrow S}(\mathbf{p}):= \mathbf{p}$.  This definition can
rigorously be described as in Fig.~\ref{fig:trsf}(b), where the
mapping is shown by the dashed arrows. We give some other cases of
reductions in Fig.~\ref{fig:trsfOthers}. $\mathrm{trsf}$ acts as the identity
on all positions $\mathbf{p}$ relative to those edges which are not modified
by the reduction rule, \emph{i.e.}, $\mathrm{trsf} (\mathbf{p}) = \mathbf{p}$. The cross symbols
$\pmb{\times}$ serves to indicate that the source position has no
corresponding target in $S$ (remember that the mapping is
partial).  Intuitively, the token on that position is \emph{deleted}
by the mapping.  It is important to observe that in the case of steps
$bot.el$ and $d$ (the only rules which open a box), a stable token is
always deleted.

\begin{fact}\label{fact:trsf}
If $R\rightsquigarrow R'$ via a  $bot.el$ or $d$ step, the action of $\mathrm{trsf}$ always delete a stable token.
\end{fact}

\begin{figure}[htbp]
\begin{center}
  \fbox{
    \begin{minipage}{.47\textwidth}
      \begin{center}
      \includegraphics[scale=.6]{trsfAxEdges}
      \qquad\qquad
      \includegraphics[scale=.6]{trsfAx}\\
      \end{center}
  \end{minipage}}
\end{center}
  \caption{$\mathrm{trsf}_{R\rightsquigarrow S}$, Formally and as a Drawing.}\label{fig:trsf}
\end{figure}
The cases of $d$ and $y$ deserve some further discussion:
\begin{varitemize}
\item
  In the $d$ rule, the token generated on the $?d$ node is deleted,
  and disappears in $S$. For the other tokens, those outside the !-box
  are modified by removing the signature $*$
  (which was acquired while crossing that $?d$ node) from the formula stack.
  The tokens $(e,\mathord{s},\mathord{t})$ inside the !-box are modified by removing the
  signature $*$ from the \emph{bottom} of the box stack $\mathord{t}$, which
  is coherent with the invariant on the size of $\mathord{t}$ (its size is
  its exponential depth). Why from the bottom of the stack? Because
  the box $b$ which disappears is at depth 0 in $R$, therefore for
  each position $(e,\mathord{s},\mathord{t})$ inside the box, the signature
  corresponding to $b$ is at the bottom of $\mathord{t}$.
\item
  In the $y$ rule, things are slightly more complicated. What happens
  to the tokens lying inside a Y-box depends on the bottom element of
  their box stack, which is the signature corresponding to the Y-box.
  If the signature at the bottom of the stack is not of the form
  $y(\cdot,\cdot)$, the token has entered the Y-box only once (\emph{i.e.}, it
  belongs to the first recursive call) and hence the token is mapped
  onto a token in the copy of $S$ outside the Y-box.  Otherwise, the
  token is mapped onto a token in the Y-box; it loses one $y(\cdot,\cdot)$
  symbol (\emph{i.e.}, it does one iteration less), but the box stack becomes
  longer (which is coherent with the increase in depth).  We show an
  example in Fig.~\ref{fig:Ytrsf_example}.  The (stable) token with a
  stack $(\delta, *)$ on the premise of $Y$-node is mapped onto a token
  on the premise of the $\bang$ node, with the same stack.  In
  contrast, the token with a stack $(\delta, y(*,y(*,*)))$ is mapped
  onto a token on a premise of the $Y$ node on the right-hand side,
  now with a stack $(\delta, y(*,*).*)$ --- it loses a $y$ symbol.
\end{varitemize}

\begin{figure*}[htbp]
  \begin{center}
    \fbox{
      \begin{minipage}{.97\textwidth}
        \begin{center}
        \includegraphics[width=15cm]{transform_refined}
        \end{center}
    \end{minipage}}
  \end{center}
  \caption{The Function $\mathrm{trsf}_{R\rightsquigarrow S}$.}\label{fig:trsfOthers}
\end{figure*}
\begin{figure}[htbp]
  \begin{center}
    \fbox{
      \begin{minipage}{.47\textwidth}
      \begin{center}
        \includegraphics[width=8cm]{Ytrsf_example}
      \end{center}
      \end{minipage}}
\end{center}
  \caption{$\mathrm{trsf}_{R\rightsquigarrow S}$ on $y$-reduction.}\label{fig:Ytrsf_example}
\end{figure}

Each statement below can be proved by case analysis. The proof is given in Appendix \ref{app:SIAM}.
\begin{lemma}[Properties of $\mathrm{trsf}$]\label{trsf_prop}
  Assume $R \rightsquigarrow S$.
  \begin{varenumerate}
  \item
    If $\mathbf{T} \rightarrow \mathbf{U}$ in $\machine{R}$ then $\mathrm{trsf}(\mathbf{T})
    \rightarrow^* \mathrm{trsf}(\mathbf{U})$ in $\machine{S}$.
  \item
    If $I_R \to \cdots \to \mathbf{T}_n\cdots $ is a run of $\mathcal{M}_R$, then
    $\mathrm{trsf}(I_R) \to^* \cdots \to^* \mathrm{trsf}(\mathbf{T}_n) \cdots$ is a run of
    the machine $\mathcal{M}_{S}$.
  \item\label{trsf_main}
    $I_R \to \cdots \to \mathbf{T}_n \cdots $ diverges/converges/deadlocks
    iff $\mathrm{trsf}(I_R) \to^* \cdots \to^* \mathrm{trsf}(\mathbf{T}_n) \cdots$ does.
  \end{varenumerate}
\end{lemma}
\newcommand{\der}[1]{\mathtt{weight}(#1)}
We end this section by looking at the number of circulating tokens.
We observe that the number of tokens, and stable tokens in particular,
in any state $\mathbf{T}$ which is reached in a run of $\mathcal{M}_R$ is finite.  We
denote by $\der{\mathbf{T}}$ the number of stable tokens in $\mathbf{T}$ (\emph{i.e.},
$Cod(\mathbf{T}) \cap \mathtt{PRIVATE}_R$). The following is immediate by analyzing
Fig.~\ref{fig:trsfOthers} and checking which tokens are deleted.
\begin{lemma}\label{lem:derTokens}\label{derTokens}
  Assume  $R \rightsquigarrow S$. We have that $\der{\mathbf{T}} \geq \der{\mathrm{trsf}(\mathbf{T})}$.
  Moreover, if $R \rightsquigarrow S $  via the $d$-rule or $bot.el$-rule,
  then $\der{\mathbf{T}} > \der{\mathrm{trsf}(\mathbf{T})}$
\end{lemma}
\subsection{The Interplay of Nets and Machines}\label{interplay}
We already know that if a simple net $R$ reduces to a normal form $S$, then
$S$ is an \ensuremath{\textsf{MLL}}{} net (Corollary~\ref{cutel}), actually a very simple one. It is immediate that  in
this case, every run of the machine $\mathcal{M}_S$ terminates in a final
state:
each token in the initial state flows to a final position (the net has neither sync nor boxes to stop them). Given an
arbitrary net $R$, we of course do not know if it reduces to a normal
form, but we are still able to use the facts above to prove that
$\mathcal{M}_R$ is deadlock-free.
\begin{lemma}[Mutual Termination]\label{net_termination}
Let $R$ be a simple net, as in Theorem~\ref{main_lem}. We have:
\begin{varenumerate}
\item
  if a run of $\mathcal{M}_R$ terminates, then each sequence of reductions
  starting from $R$ terminates;
\item
  if a sequence of reductions starting from $R$ terminates, then each
  run of $\mathcal{M}_R$ terminates in a \emph{final} state.
\end{varenumerate}
\end{lemma}
\newcommand{\ww}[1]{\mathtt{weight}(#1)}
\begin{proof}
Let us first consider Point 1. By hypothesis, there is a run of $\mathcal{M}_R$
which terminates in a state $\mathbf{T}$.  We define $\ww{R}:=\der{\mathbf{T}}$.  By
Lemma~\ref{trsf_prop}, if $R \rightsquigarrow S$, $\mathrm{trsf}$ maps the run of $\mathcal{M}_R$
into a run of $\mathcal{M}_{S}$ which terminates in the state $\mathrm{trsf}(\mathbf{T})$.  By
Lemma \ref{derTokens}, $ \der{\mathrm{trsf}(\mathbf{T})} \leq \der{\mathbf{T}}$, hence
$\ww{S} \leq \ww{R}$.  Using Lemma \ref{derTokens}, we prove that it
is not possible to have an infinite sequence of $\rightsquigarrow$ reductions
starting from $R$, because: (i) each rewriting step which opens a box
($d$, or $bot.el$) strictly decreases $\ww{R}$; (ii) there is only a
finite number of rewriting steps which can be performed without
opening a box. Let us then consider Point 2. By hypothesis, $R$
reduces to a cut free net $S$, which has the form described in Corollary~\ref{cutel}. On such a net, all runs of $\mathcal{M}_S$ terminate in
a final state. If $\mathcal{M}_R$ has a run which is infinite
(resp. deadlocks), by Lemma~\ref{trsf_prop} $\mathrm{trsf}$ would map it into
a run of $\mathcal{M}_S$ which is infinite (resp. deadlocks).
\end{proof}
Lemma~\ref{net_termination} entails deadlock-freeness of the \textsf{SIAM}{} as an immediate
consequence:
\begin{thm}[Deadlock-Freeness of the \textsf{SIAM}]\label{SIAM deadlock free}
  Let $R$ be a \textsf{SMEYLL}{} net such that no $?$ appears in its
  conclusions. If a run of $\mathcal{M}_R$ terminates in the state $\mathbf{T}$, then
  $\mathbf{T}$ is a final state.
\end{thm}
\begin{proof}
If $R$ has no $\bot$ and no $!$ in its conclusions, deadlock freeness is immediate consequence of
Theorem~\ref{net_termination}.
However, the result is true also without this constraint,  because we can always ``close'' the net
$R$ into a net $\overline{R}$ in a way that cannot create any new deadlocks.

$\overline{R}$ is the net obtained from $R$ when we cut each
  conclusion $A$ of $R$ with the conclusion $A\b$ of the net $S_{A\b}$
  which is defined as follows. $S_{A\b}$ has  the direct encoding of the formula  tree of $A\b$ above the
  conclusion $A\b$ (each modality $?$ is introduced by a $?d$ node);
  the atomic leaves are conclusion of an axiom in the case of $X,X\b,
  \bot$, or of a $\mathsf{one}$ node in the case of $\mathsf{1}$. Therefore,  $S_{A\b}$ has only conclusions $X\b,X,1$, \emph{i.e.}\ the other side of the axioms.

  To conclude we
  observe that the \textsf{SIAM}{} deadlocks
    in $\overline{R}$ iff it deadlocks in $R$.
\end{proof}

We stress that in the statement above there is \emph{no
  assumption that the conclusions are simple formulas} (unlike in Lemma~\ref{net_termination}, or
Theorem~\ref{main_lem}).
 The constraint that the conclusions are
required not to contain the $?$ modality is instead a real limit,
which is intrinsic to most presentations of GoI (see, \emph{e.g.},
~\cite{Girard89}).
\subsection{Computational Semantics}\label{semantics}
For the rest of this section, we assume the nets to be simple nets. The reason why  this is not a bothering restriction, is that
the nets to which we are going to give computational
meaning in the Section~\ref{sec:beyond} are nets where all conclusions have type $1$.

 The machine $\machine{R}$ implicitly gives a semantics to $R$.  By
Proposition~\ref{lem:diamProp}, all runs of $\mathcal{M}_R$ have the same
behaviour.  We can therefore say that $\mathcal{M}_R$ either \emph{converges}
(to a unique final state) or \emph{diverges}.  We write
$\mathcal{M}_R\Downarrow$ if all runs of the machine converge. We write
$R\Downarrow$ if all sequences of reductions starting from $R$
terminate in the (unique) normal form. In the previous section we have
established (Lemma~\ref{net_termination}) that
\begin{cor}[Adequacy]\label{thm:termination}
  $\mathcal{M}_R \Downarrow$ if and only if $R \Downarrow$.
\end{cor}
We also already know that:
\begin{cor}[Invariance]\label{basic_soundness}
  Assume $R \rightsquigarrow S$.  $\mathcal{M}_R\Downarrow$ if and only if
  $\mathcal{M}_{S}\Downarrow$.
\end{cor}
We now introduce an equivalence on the machines which is finer than
the one induced by convergence. We associate a partial function $\sem
{R}$ to each net $R$ through the machine $\machine{R}$, and show
that $\sem {R}$ is a sound interpretation. This way we have a finer
computational model for $\textsf{SMEYLL}$, on which we will build in the next
sections. The \emph{interpretation} $\sem {R}$ of a net
$R$ is defined as follows
\begin{varitemize}
  \item
    if $\machine{R}$ diverges, $\sem {R} := \Omega$,
  \item
    if $\machine{R}$ converges, $\sem {R}$ is the partial
    function $\sem {R}: \mathtt{INIT}_{R} \rightharpoonup \mathtt{FIN}_{R}$
    where $\sem {R}(\ss) := \mathbf{p}$ if $\mathbf{p}$ is a final position in
    the final state $\mathbf{T}$ of the machine (\emph{i.e.}, $\mathbf{p} \in Cod(\mathbf{T}) \cap
    \mathtt{FIN}_{R}$) and $\mathrm{orig}(\mathbf{p}) = \ss$.
\end{varitemize}
\begin{theorem}[Soundness]\label{soundness}
  If $R \rightsquigarrow S$, $\sem {R}= \sem {S}$.
\end{theorem}
The proof is given in Appendix~\ref{app:SIAM}.
\section{Beyond Nets: Interpreting Programs}\label{sec:beyond}

\textsf{SMEYLL}{} nets as defined and studied in Section~\ref{sec:SMELLY} are
purely ``logical''. In this section we introduce \emph{program nets},
which are a (slight) variation on \textsf{SMEYLL}{} nets in which external
data can be manipulated.  This allows us to interpret \ensuremath{\mathsf{PCF}}-like
languages. The machine running on these nets will be a very simple
extension of the \textsf{SIAM}, of which it inherits all properties.

The intuition behind program nets is as follows. Assume a language
with a single base type. The base type is mapped to the formula
$\mathsf{1}$; values of the base type are stored in a \emph{memory}.
Elementary operations of the base type are modeled using sync nodes,
recursion is modeled by Y-boxes, conditional tests are captured by a
generalization of the $\bot$-box. Arrow and product types (and all the
usual $\lambda$-calculus constructions) are encoded by means of one of
the well-known mappings of intuitionistic logic into linear
logic~\cite{MaraistOTW95,phdmackie,Girard87}, depending on the chosen
evaluation strategy.

Before introducing program nets and interactive machines for them, let
us fix a language which will also be our main application.
\subsection{\ensuremath{\mathsf{PCF}}}
The language we shall consider in this section is nothing more than
Plotkin's \ensuremath{\mathsf{PCF}}, whose \emph{terms} ($ M,N,P$) and \emph{types} ($A,B$) are defined as
  follows:

{\footnotesize
\[
\begin{array}{lll}
  M
  &{:}{:}{=} &
  %
  x \; \; \mbox{\Large{$\mid$}}\;\;
  \lambda x.M \; \; \mbox{\Large{$\mid$}}\;\;
  MM \; \; \mbox{\Large{$\mid$}}\;\;
  \pi_l(M) \; \; \mbox{\Large{$\mid$}}\;\;
  \pi_r(M) \; \; \mbox{\Large{$\mid$}}\;\;\\ &&
  \PCFpair{M,M} \; \; \mbox{\Large{$\mid$}}\;\;
  \PCFn{n} \; \; \mbox{\Large{$\mid$}}\;\;
  \mathtt{s}(M) \; \; \mbox{\Large{$\mid$}}\;\;
  \mathtt{p}(M) \; \; \mbox{\Large{$\mid$}}\;\;\\ &&
  \PCFifzero{P}{M}{M} \; \; \mbox{\Large{$\mid$}}\;\;
  \PCFletrec{f}{x}{M}{M},
  \\
  A
  &{:}{:}{=} &
  %
  \mathbb{N} \; \; \mbox{\Large{$\mid$}}\;\;
  A \to A \; \; \mbox{\Large{$\mid$}}\;\;
  A \times A,
\end{array}
\]
}\\
Here, $n$ ranges over the set of non-negative natural
numbers.  A \emph{typing context} $\Delta$ is a (finite) set of typed
variables $\{x_1:A_1,\dots,x_n:A_n\}$, and \emph{typing judgements}
are in the form $\Delta\vdash M:A$. We say that a typing judgement
is \emph{valid} if it can be derived from a standard set of typing
rules). Most term constructs are self-explanatory: we
only give a few words on the $\mathtt{letrec}$ construction. In
standard \ensuremath{\mathsf{PCF}}, the fixpoint is represented with a Y-combinator: while
this is fine in call-by-name evaluation, it does not behave well in the
context of call-by-value reduction. As the $\mathtt{letrec}$ makes
sense in both situations, we use it instead. Moreover, we only want to
allow recursive definitions of \emph{functions}. To syntactically
enforce this, we consider a $\mathtt{letrec}$ binding two variables:
one for the function to be defined, and one for its argument.

A typing context $\Delta$ is a (finite) set of typed variables
$\{x_1:A_1,\dots,x_n:A_n\}$, and a typing judgement is written as
\[
\Delta\vdash M:A
\]
A typing judgement is \emph{valid} if it can be derived from the
usual set of typing rules, presented in Table~\ref{tab:typrules}.

On PCF terms, we define a call-by-name and a call-by-value
evaluation, in a standard way.

\begin{table*}
\[
\infer{\Delta,x:A\vdash x:A}{}
\qquad
\infer{\Delta\vdash \lambda x.M:A\to B}{\Delta,x:A\vdash
  M:B}
\qquad
\infer{\Delta\vdash MN:B}{
  \Delta\vdash M:A\to B
  &
  \Delta\vdash N:A
}
\]
\[
\infer{\Delta\vdash \pi_l{(M)}:A}{
  \Delta\vdash M:A\times B
}
\qquad
\infer{\Delta\vdash \pi_r{(M)}:B}{
  \Delta\vdash M:A\times B
}
\qquad
\infer{\Delta\vdash \PCFpair{M,N}:A\times B}{
  \Delta\vdash M:A
  &
  \Delta\vdash N:B
}
\]
\[
\infer{\Delta\vdash\PCFn{n}:\mathbb{N}}{}
\quad
\infer{\Delta\vdash\mathtt{s}{(M)}:\mathbb{N}}{
  \Delta\vdash M:\mathbb{N}
}
\quad
\infer{\Delta\vdash\mathtt{p}{(M)}:\mathbb{N}}{
  \Delta\vdash M:\mathbb{N}
}
\quad
\infer{\Delta\vdash \PCFifzero{P}{M}{N}:A}{
  \Delta\vdash P:\mathbb{N}
  &
  \Delta\vdash M:A
  &
  \Delta\vdash N:A
}
\]
\[
\qquad
\infer{\Delta\vdash \PCFletrec{f}{x}{M}{N}:C}{
  \Delta,f:A\to B,x:A\vdash M:B
  &
  \Delta,f:A\to B\vdash N:C
}
\]
\caption{Typing rules for PCF}
\label{tab:typrules}
\end{table*}

\subsubsection{Call-by-name reduction}

A {\em value} in the call-by-name setting is defined from the
following grammar:

{\footnotesize
\[
\begin{array}{lll}
  U
  &
  {:}{:}{=}
  &
  x \; \; \mbox{\Large{$\mid$}}\;\;
  \lambda x.M \; \; \mbox{\Large{$\mid$}}\;\;
  \PCFpair{M,N} \; \; \mbox{\Large{$\mid$}}\;\;
  \PCFn{n}.
\end{array}
\]}
\\
A {\em call-by-name reduction context $C[-]$} is defined with the
following grammar:

{\footnotesize
\[
\begin{array}{lll}
C[-] &{:}{:}{=}
&
[-]\; \; \mbox{\Large{$\mid$}}\;\;
C[-]N\; \; \mbox{\Large{$\mid$}}\;\; \pi_l{C[-]}\; \; \mbox{\Large{$\mid$}}\;\; \pi_r{C[-]}\; \; \mbox{\Large{$\mid$}}\;\;
\\
&&\mathtt{s}(C[-])\; \; \mbox{\Large{$\mid$}}\;\; \mathtt{p}(C[-])\; \; \mbox{\Large{$\mid$}}\;\; \PCFifzero{C[-]}{M}{N}.
\end{array}
\]}
\\
In call-by-name, $M$ rewrites to $N$, written as $M \to_{\it cbn} N$, is
defined according to the rules presented in Table~\ref{tab:cbnrw}.
\begin{table*}
\begin{center}
\begin{minipage}{.6\textwidth}
(1) {\em Axiom rules.}
\[
\infer{(\lambda x.M)N \to_{\it cbn} M\{x:=N\}}{}
\qquad
\infer{\pi_l{\PCFpair{M,N}} \to_{\it cbn} M}{}
\qquad
\infer{\pi_r{\PCFpair{M,N}} \to_{\it cbn} N}{}
\]
\[
\infer{\mathtt{s}(\PCFn{n}) \to_{\it cbn} \PCFn{n+1}}{}
\qquad
\infer{\mathtt{p}(\PCFn{n+1}) \to_{\it cbn} \PCFn{n}}{}
\qquad
\infer{\mathtt{p}(\PCFn{0}) \to_{\it cbn} \PCFn{0}}{}
\]
\[
\infer{\PCFifzero{\PCFn{0}}{M}{N}\to_{\it cbn} M}{}
\qquad
\infer{\PCFifzero{\PCFn{n+1}}{M}{N}\to_{\it cbn} N}{}
\]
\[
\infer{\PCFletrec{f}{x}{M}{N} \to_{\it cbn} N\{f := \lambda x.\PCFletrec{f}{x}{M}{f\,x}\}}{}
\]
(2) {\em Congruence rules.} Provided that $C[-]$ is a call-by-name context:
\[
\infer{C[M]\to_{\it cbn} C[N]}{M\to_{\it cbn} N}
\]
\end{minipage}
\end{center}
\caption{Call-by-name reduction strategy for PCF.}
\label{tab:cbnrw}
\end{table*}

\subsubsection{Call-by-value reduction}
A value in the call-by-value setting is defined from the following
grammar

{\footnotesize\[
\begin{array}{lll}
  U
  &
  {:}{:}{=}
  &
  x \; \; \mbox{\Large{$\mid$}}\;\;
  \lambda x.M \; \; \mbox{\Large{$\mid$}}\;\;
  \PCFpair{U,U} \; \; \mbox{\Large{$\mid$}}\;\;
  \PCFn{n}.
\end{array}
\]
}\\
A {\em call-by-value
  reduction context $C[-]$} is defined with the following grammar:
{\footnotesize
\[
\begin{array}{lll}
C[-] &{:}{:}{=}
&
[-]\; \; \mbox{\Large{$\mid$}}\;\; C[-]N\; \; \mbox{\Large{$\mid$}}\;\; VC[-]\; \; \mbox{\Large{$\mid$}}\;\; \PCFpair{C[-],N}\; \; \mbox{\Large{$\mid$}}\;\;
\PCFpair{V,C[-]}\; \; \mbox{\Large{$\mid$}}\;\;
\\
&&
\pi_l{C[-]}
\; \; \mbox{\Large{$\mid$}}\;\; \pi_r{C[-]}\; \; \mbox{\Large{$\mid$}}\;\;
\mathtt{s}(C[-])\; \; \mbox{\Large{$\mid$}}\;\; \mathtt{p}(C[-])\; \; \mbox{\Large{$\mid$}}\;\;\\
&&\PCFifzero{C[-]}{M}{N}.\phantom{\; \; \mbox{\Large{$\mid$}}\;\;}
\end{array}
\]}

\noindent
In call-by-value, $M$ rewrites to $N$, written as $M \to_{\it cbv} N$, is
defined according to the rules of Table~\ref{tab:cbvrw}.
\begin{table*}
\begin{center}
\begin{minipage}{.6\textwidth}
(1) {\em Axiom rules.}
\[
\infer{(\lambda x.M)U \to_{\it cbv} M\{x:=U\}}{}
\qquad
\infer{\pi_l{\PCFpair{U,V}} \to_{\it cbv} U}{}
\qquad
\infer{\pi_r{\PCFpair{U,V}} \to_{\it cbv} V}{}
\]
\[
\infer{\mathtt{s}(\PCFn{n}) \to_{\it cbv} \PCFn{n+1}}{}
\qquad
\infer{\mathtt{p}(\PCFn{n+1}) \to_{\it cbv} \PCFn{n}}{}
\qquad
\infer{\mathtt{p}(\PCFn{0}) \to_{\it cbv} \PCFn{0}}{}
\]
\[
\infer{\PCFifzero{\PCFn{0}}{M}{N}\to_{\it cbv} M}{}
\qquad
\infer{\PCFifzero{\PCFn{n+1}}{M}{N}\to_{\it cbv} N}{}
\]
\[
\infer{\PCFletrec{f}{x}{M}{N} \to_{\it cbv} N\{f := \lambda x.\PCFletrec{f}{x}{M}{f\,x}\}}{}
\]
(2) {\em Congruence rules.} Provided that $C[-]$ is a call-by-value context:
\[
\infer{C[M]\to_{\it cbn} C[N]}{M\to_{\it cbn} N}
\]
\end{minipage}
\end{center}
\caption{Call-by-name reduction strategy for PCF.}
\label{tab:cbvrw}
\end{table*}

\subsection{Program Nets and Register Machines}
\newcommand{\surfone}[1]{{\tt SurfOne}(#1)}
\newcommand{\syncnode}[1]{{\tt SyncNode}(#1)}
\newcommand{{\tt SyncNames}}{{\tt SyncNames}}
\newcommand{\oneindex}[1]{{\tt ind}(#1)}
\newcommand{\mapsyncname}[1]{{\tt mkname}(#1)}

\newcommand{\memories}{\mathrm{Mem}}
\newcommand{\mem}[1]{\mathbf{m}_{#1}}
\newcommand{\smem}{\mem{\mathbf{T}}}
\newcommand{\mathbf{R}}{\mathbf{R}}
\renewcommand{\S}{\mathbf{S}}
\newcommand{\mathrm{test}}{\mathrm{test}}
\newcommand{\mathrm{update}}{\mathrm{update}}
\newcommand{\mathrm{init}}{\mathrm{init}}
\newcommand{\mathrm{I}}{\mathrm{I}}
\newcommand{\mathrm{arity}}{\mathrm{arity}}
\newcommand{\nm}{\mathit{l}}
In the rest of this paper, we assume that all atomic formulas are
units (\emph{i.e.}, $1$ and $\bot$). The language of formulas is therefore $
A ::= \mathsf{1}\; \; \mbox{\Large{$\mid$}}\;\;
\bot\middA\otimesA\middA\parrA
\; \; \mbox{\Large{$\mid$}}\;\;!A\; \; \mbox{\Large{$\mid$}}\;\; ?A.$

First of all, we need the
definition of a \emph{memory}:
\begin{deff}\label{def:mem}
  Let $\mathrm{I}$ be a (possibly) infinite set whose elements are called
  \emph{addresses}. Let ${\tt SyncNames}$ be a finite set of names, where to
  each name we associate a positive number that we call {\em
    arity}. Given a set of \emph{values} $\mathbb{X}$, we define
  $\memories $ as the set $\mathrm{I}\to\mathbb{X}$ of all functions from
  $\mathrm{I}$ to $\mathbb{X}$, equipped with the following operations:
  $$
  \begin{array}{r@{{~~}:{~~}}l}
    \mathrm{test} & \mathrm{I}\times\memories \to \mathrm{Bool}\times\memories;
    \\
    \mathrm{update} &

    {\tt SyncNames}\times\displaystyle(\mathrm{I}^*)\times\memories
    \rightharpoonup \memories;
    \\
    \mathrm{init} & \mathrm{I}\times\memories \to \memories.
  \end{array}
  $$
  where the  partial function $\mathrm{update}$ is defined on a triple $(\nm,x,\mem{})$ iff
      the length of $x$ equals the arity of $\nm$.

  A \emph{memory}\footnote{An even more fitting name would be
    \emph{memory states}, but we do not want to overload too much the
    term ``state''.} is any element $\mem{}$ of $\memories$, and we say
  that $\mem{}$ \emph{has values in} $\mathbb{X}$.
\end{deff}
Intuitively, $\mem{}$ represents a set of \emph{registers} which are
referenced by the elements of $\mathrm{I}$ (the addresses). The operation
$\mathrm{test}$ is used to query the value of a register, $\mathrm{update}$ to update its
value, and $\mathrm{init}$ to set a register of the memory to a default
value. Some comments on the operations on $\memories$ are useful. The
reason why we have $\memories$ in the codomain of the operation
$\mathrm{test}$, is that we aim at a general model where $\mathrm{test}$ might have a
non-local effect on the memory, such as in a quantum setting (see
e.g.~\cite{esop}), though its implementation is beyond the scope of
this paper.  Notice also that the type of $\mathrm{update}$ is really a
dependent-type.
\subsubsection{Program Nets}
Program nets are obtained as a light and natural extension of
\textsf{SMEYLL}{} nets, as follows:
\begin{varitemize}
\item
  $\bot$-boxes\ are replaced by multi-$\bot$-boxes, which are meant to handle
  \emph{tests}.
   A
  \emph{multi-$\bot$-box} is a $\bot$ node to which we associate
  \emph{two} structures with the same conclusions $\Gamma$, as shown
  in Fig.~\ref{multibox} and~\ref{SIAMmultibox} (these figures are
  fully explained later on).
  An {\em extended {\textsf{SMEYLL}} net} is a {\textsf{SMEYLL}} net where
  multi-$\bot$-box{}es\footnote{In some example pictures, it is still
    convenient to use simple $\bot$-boxes; they can be seen as a short-cut
    for multi-$\bot$-boxes\ with the same net in both places.  } are used in
  place of $\bot$-box{}es.
\item
  Given an (extended) net $R$, let $\surfone{R}$ be the set of all
  $\mathsf{one}$ nodes at the surface, and $\syncnode{R}$ be the set of
  {\em all} sync-nodes of the extended net $R$, whether at surface
   or not.  A {\em decoration} of $R$ with names ${\tt SyncNames}$
  consists of the following two pieces of data:
  \begin{varenumerate}
  \item
    An injective partial map $\oneindex{R}:\surfone{R}\rightharpoonup
    \mathrm{I}$, \emph{i.e.}, $\mathsf{one}$ nodes are not necessarily decorated;
  \item
    A {\em total} map $\mapsyncname{R}:\syncnode{R}\to {\tt SyncNames}$,
    where ${\tt SyncNames}$ is a finite set of names. This map is simply
    naming the sync nodes appearing in the extended net $R$. We assume
    that given a name of arity $k$, all the sync nodes decorated with
    that name have the same arity $k$, where the arity of a sync node
    is the total number of $1$'s in its premisses.
  \end{varenumerate}
\end{varitemize}
\begin{deff}
   Given a  set $\memories$ as in Definition~\ref{def:mem},
  a {\em program net} is a pair $\mathbf{R}= (R,\mem{R})$, where $R$ is a
  decorated, extended net and $\mem{R}\in \memories$ is a memory.
\end{deff}
Rewriting on {\textsf{SMEYLL}} nets easily extends to program nets as shown in
Fig.~\ref{multibox} (where we adopt the convention that the memory
associated to the net is $\mem{1}$ before reduction, and $\mem{2}$
after reduction). The rules are as follows. Rule ${\it decor}$ is a
new rewriting rule which associates to a surface node $\mathsf{one}$ an
address $r\in I$; when doing this, we are \emph{linking} the $\mathsf{one}$
node to the memory. Rule ${\it bot.el}$ is modified to reflect the use
of multi-$\bot$-boxes.  As shown in Fig.~\ref{multibox}, the reduction
depends on the memory, and is determined by the result of the
operation $\mathrm{test}$. For the other reduction rules, the underlying net
is rewritten exactly as for \textsf{SMEYLL}\ nets.  Concerning the memory,
only the rule ${\it s.el}$ modifies it, as follows:
$\mem{2}=\mathrm{update}(\nm,(r_1,r_2,\dots r_k), \mem{1})$, where $k$ is the
arity of $\nm$. In all the remaining cases $\mem{1}=\mem{2}$ (i.e. the
memory is not changed)
\begin{figure}[htbp]
  \begin{center}
    \fbox{
      \begin{minipage}{.47\textwidth}
        \begin{center}
          \includegraphics[width=8.2cm]{multibox}
        \end{center}
      \end{minipage}}
\end{center}
  \caption{Program Net Rewriting.}\label{multibox}
\end{figure}
What we have introduced so far is a general schema for program nets;
in order to capture specific properties, we need to define $\memories$
and the operations on it.  In the following section, we specialize the
construction to \ensuremath{\mathsf{PCF}}.
\subsubsection{\ensuremath{\mathsf{PCF}}\ nets}\label{pcf nets}
\newcommand{\ttrue}{\mathtt{tt}} \newcommand{\tfalse}{\mathtt{ff}} To
encode \ensuremath{\mathsf{PCF}}\ programs, we use a class of program nets.  Once
$\memories$ and the operations on it are appropriately defined, we are
able to gain more expressive power than in \textsf{SMEYLL}{}, while good
computational properties will be still guaranteed by the underlying
nets. A {\em \ensuremath{\mathsf{PCF}}\ net} is a program net where
$\memories$ has values in
$\mathbb{N}$, that is, $\memories ~{:}{=}~ \mathrm{I}\to\mathbb{N}$.  The
set of sync-names is $\{\mathtt{max}, \mathtt{p}, \mathtt{s}\}$:
$\mathtt{max}$ is binary while $\mathtt{p}$ and $\mathtt{s}$ are
unary.  The operation $\mathrm{update}$ is defined as follows.  { The sync node
  of label $\mathtt{p}$ acts as the predecessor, that is $\mathrm{update}(\mathtt{è},r,\mem{1}) =
  \mem{2}$ where $\mem{2}(r)=\mem{1}(r)-1$ and $\mem{2}(k)=\mem{1}(k)$
  if $k\neq r$.  The node of label $\mathtt{s}$ acts as the successor, that is
  $\mathrm{update}(\mathtt{s},n,\mem{1}) = \mem{2}$ where $\mem{2}(r)=\mem{1}(r)+1$ and
  $\mem{2}(k)=\mem{1}(k)$ if $k\neq r$.  Finally, the sync node of
  label $\mathtt{max}$ acts as follows: $\mathrm{update}(\mathtt{max},r,q,\mem{1}) =
  \mem{2}$ where $\mem{2}(r)=\mem{2}(q)=\max(\mem{1}(r),\mem{1}(q))$
  and $\mem{2}(k)=\mem{1}(k)$ if $k\neq r$ and $k\neq q$.}  For the
other operations, $\mathrm{test}(r,\mem{})$ is defined to be $(\ttrue,
\mem{})$ if $\mem{}(r) = 0$, and $(\tfalse, \mem{})$ otherwise;
$\mathrm{init}(r,\mem{})$ is defined to be the memory $\mathbf{n}$ where
$\mathbf{n}(r) = 0$ and $\mathbf{n}(k) = \mem{}(k)$ for $k \neq r$.
Any typing derivation is encoded as a \ensuremath{\mathsf{PCF}}\ net.  Two possible
encodings will be considered: one for call-by-value, one for
call-by-name, which correspond to two translations of intuitionistic
logic into linear logic~\cite{MaraistOTW95,phdmackie}.

\subsubsection{Register Machines}
\begin{figure}
\begin{center}
  \fbox{
  \begin{minipage}{.47\textwidth}
    \begin{center}
    \includegraphics[width=7.2cm]{SIAMmultibox}
    \end{center}
  \end{minipage}}
\end{center}
\caption{Multi-$\bot$-box\ Transition for a Register Machine.}\label{SIAMmultibox}
\end{figure}
The \textsf{SIAM}{}, as we defined it in Section~\ref{SIAM}, is readily
adapted to interpret \ensuremath{\mathsf{PCF}}{} nets. Let us first sketch a general
construction for the machine which is associated to a program net.
The dynamics of the machine is mostly inherited from the \textsf{SIAM}; the
novelty is that the notion of state now includes a {memory}.  Let us
fix a set of memories $\memories{}$.  To a program net $\mathbf{R}= (R,
\mem{R})$ ($\mem{R}\in \memories$) is associated the machine $\mathcal{M}_{\mathbf{R}}$
whose memories, states and transitions are defined as follows. The
definition of position and set of positions is the same as in
Section~\ref{SIAM}.
\paragraph*{Memories}
$\memories$ and the operations on it are the same as for the program
net $\mathbf{R}$. To illustrate the machine, we need however to make the
set of addresses $\mathrm{I}$ precise. We take $\mathrm{I}$ to be the set of
positions $\mathtt{INIT}_R \cup \mathtt{ONES}_R$. We say that the access to the memory
is defined for all positions for which $\mathrm{orig} (\mathbf{p}) \in \mathtt{INIT}_R
\cup \mathtt{ONES}_R$.
\paragraph*{States}
A state of $\mathcal{M}_{\mathbf{R}}$ is a pair $(\mathbf{T}, \smem)$, where $\mathbf{T}$ is a state
in the sense of Section~\ref{SIAM}, and $\smem\in \memories{}$ is a
memory. An \emph{initial} state of $\mathcal{M}_{\mathbf{R}}$ is a pair $(\mathbf{I},
\mem{\mathbf{I}})$, where $\mem{\mathbf{I}}$ coincides with $\mem{R}$ for the
positions corresponding to decorated $\mathsf{one}$ nodes, is arbitrary on
$\mathtt{INIT}_R$, and is $0$ anywhere else.
\paragraph*{Transitions}
The transitions are the same as in \ref{SIAM}, except in the following
cases, which are defined only if the access to the memory is defined.
\begin{varitemize}
\item
  Sync nodes. When the tokens $\mathbf{p}_1, \dots, \mathbf{p}_k$ cross a sync node
  with label $\nm$ and arity $k$, the operation $\mathrm{update}(\nm,\mathbf{p}_1,
  \dots, \mathbf{p}_k, \mem{})$ opportunely modifies the memory $\mem{}$.
\item
  Multi-$\bot$-box. Let the box be as in Fig.~\ref{SIAMmultibox},
  where $S_0$ and $S_1$ are the two nets associated to it, and the
  edges $e_0,e_1$ are as indicated.  When a token is in position
  $\mathbf{p}=(e,\epsilon,\mathord{t})$ on the principal conclusion of the box, it
  moves to $ (e_0,\epsilon,\mathord{t})$ if $\mathrm{test}(\mathrm{orig}(\mathbf{p}),\smem)$ returns
  the boolean $\mathtt{ff}$ (arrow (i) in Fig.~\ref{SIAMmultibox}) and
  it moves to $(e_1,\epsilon,\mathord{t})$ if $\mathrm{test}(\mathrm{orig}(\mathbf{p}),\smem)$ returns
  $\mathtt{tt}$ (arrow (ii) in Fig.~~\ref{SIAMmultibox}). If a token
  $(f, \mathord{s}, \mathord{t})$ is on an auxiliary conclusion $f$, it moves to
  the corresponding conclusion in $S_0$ (resp. $S_1$) if $\mathord{t}\in
  \mathtt{Instances}_{\mathbf{T}}(S_0)$ (resp. $\mathord{t} \in \mathtt{Instances}_{\mathbf{T}}(S_1)$).
\end{varitemize}
\paragraph*{State Transformations}
Let $\mathbf{R}=(R,\mem{R})$ be a program net and $\mathbf{R} \rightsquigarrow \S=(S, \mem{S})$.
The transformation $\mathrm{trsf}$ described in Fig.~\ref{fig:trsfOthers}
associates \emph{positions} of $R$ to \emph{positions} of $S$; this
allows us also to specify the transformation of the memory, hence
allowing us to map a memory of $\mathcal{M}_\mathbf{R}$ into a memory of $\mathcal{M}_{\S}$.
More precisely, each state $(\mathbf{T}, \smem )$ of $\mathcal{M}_\mathbf{R}$ is mapped
into a state $(\mathrm{trsf}(\mathbf{T}), \mathrm{trsf}(\smem) )$ of  $\mathcal{M}_{\S}$.
\subsubsection{\ensuremath{\mathsf{PCF}}\ Machines}
A \ensuremath{\mathsf{PCF}}\ machine is a {register} machine where $\memories$ and the
operations on it are defined as for \ensuremath{\mathsf{PCF}}\ nets (Section \ref{pcf
  nets}).  As for the \textsf{SIAM}, we have that $\mathrm{trsf}$ maps each run of
$\mathcal{M}_\mathbf{R}$ into a run of $\mathcal{M}_{\mathbf{R}'}$ which converges/diverges/deadlocks
iff the run on $\mathcal{M}_R$ does.  By combining \ensuremath{\mathsf{PCF}}\ nets and the
\ensuremath{\mathsf{PCF}}\ machine, it is possible to establish similar results to those in
Section~\ref{interplay} and~\ref{semantics}.  \condinc{}{
\begin{lemma} Let $\mathbf{R}$ be a \ensuremath{\mathsf{PCF}}\ net where all conclusions have type $\mathsf{1}$.
  The machine $\mathcal{M}_\mathbf{R}$ terminates in a final state (say $(\mathbf{T},\smem)$)
  iff $\mathbf{R}$ reduces to a cut and sync free net (say $\mathbf S=(S, \mem{S})$).
  Moreover
  \[
  \mem{S}=\sem {\smem}
  \]

  where $\sem{\blue{\smem}}$ is the restriction of $\blue{\smem}$
  to the elements pointed to by final positions.
\end{lemma}
}
Assume $\mathbf{R}$ is a \ensuremath{\mathsf{PCF}}\ net of conclusion $\mathsf{1}$. We write $\mathbf{R}
\Downarrow n$ if $\mathbf{R}$ reduces to $\mathbf S$, where the value in the
memory corresponding to the unique $\mathsf{one}$ node in $\mathbf S$ is
$n$. Similarly we write  $\mathcal{M}_{\mathbf{R}} \Downarrow n$, where $n$ is the value pointed to by the unique final position in the final state of $\mathcal{M}_{\mathbf{R}}$.
\begin{thm}[Adequacy]
$\mathbf{R} \Downarrow n$ if and only if $\mathcal{M}_{\mathbf{R}} \Downarrow n$
\end{thm}

\subsection{The Call-by-Value Encoding}
In the call-by-value encoding of \ensuremath{\mathsf{PCF}}\ into \ensuremath{\mathsf{PCF}}\ nets, the shape of
the net corresponding to $x_1:A_1,\dots,x_n:A_n\vdash M:B$ is
\[
\includegraphics[page=2,width=5cm]{PCFcbv.pdf}
\]
where $M^\dagger$ is a net and where $(\cdot)^\dagger$ is a mapping of types to
{\textsf{SMEYLL}} formulas, defined as follows:
\begin{align*}  \mathbb{N}^\dagger&:=~\mathsf{1};\\
  (A\to B)^\dagger&:=~{!(A^\dagger\b\parr B^\dagger)};\\
  (A\times B)^\dagger&:=~{A^\dagger}\otimes{B^\dagger}.
\end{align*}

\noindent
In our translation, we have chosen to adopt an \emph{efficient}
encoding, rather than the usual call-by-value encoding. In other
words, we follow Girard's optimized translation of intuitionistic into
linear logic, which relies on properties of positive formulas
\cite{Girard87}\footnote{A good summary of the different translations
  is given at the address
  \url{http://llwiki.ens-lyon.fr/mediawiki/index.php/Translations_of_intuitionistic_logic}}.
We feel that this encoding is closer to call-by-value computation than
the non-efficient one; it however raises a small issue.  Notice in
fact that we map natural numbers into the type $1$, not $!1$. How
about duplication and erasure, then? We will handle this in the next
section, by using sync nodes, but let us first better clarify what the
issue is.

Girard's translation relies on the fact that $1$ and $!1$ are
logically equivalent (\emph{i.e.}, they are equivalent for
provability). However, this in itself is not enough to capture
duplication in our setting, because we need to also duplicate the
values in the memory, and not only the underlying net. We illustrate
this in Fig.~\ref{one_equiv}. The portion inside the dashed line
corresponds to a proof of $1\vdash {!1} $; when we look at an example
of its use (l.h.s. of the figure), we see that by using it we do
duplicate the node $\mathsf{one}$, but \emph{not} the value $n$ which is
associated to it. The value $n$ is not transmitted from the $1$ to the
$!1$ which is going to be duplicated. The logical encoding however
still correctly models weakening (r.h.s. of Fig.~\ref{one_equiv}).
\begin{figure}
\begin{center}
\fbox{
  \begin{minipage}{.47\textwidth}
    \begin{center}
    \includegraphics[width=7cm]{girardCBV}
    \end{center}
  \end{minipage}}
\end{center}
\caption{A Proof of $1\vdash {!1}$.}\label{one_equiv}
\end{figure}
\paragraph*{Exponential Rules and the Units}
The formula $\bot$ does not support contraction, weakening and
promotion ``out of the box'' in {\textsf{SMEYLL}} but it is nonetheless
possible to encode them as \ensuremath{\mathsf{PCF}}\ nets with the help of the binary sync
node {\tt max}.
\begin{figure}
\begin{center}
\fbox{
\begin{minipage}{.47\textwidth}
  \begin{center}
    \includegraphics[page=4,width=4cm]{PCFcbv-positive-nodes.pdf}
  \end{center}
\end{minipage}}
\end{center}
\caption{Syntactic Sugar: Copying $\bot$.}\label{fig:copy-node}
\end{figure}
\begin{varitemize}
\item
  {\em Contraction.} We encode contraction on $\bot$ by using a sync
  node {\tt max} and the syntactic sugar {\tt copy} defined in
  Fig.~\ref{fig:copy-node}. It duplicates the value associated to the
  incoming edge, and it does so in a call-by-value manner: it will
  only copy a $\mathsf{one}$ node (i.e. a result), not a whole
  computation. In particular, it should be noted that the rules of net
  rewriting are not modified.
\item
  {\em Promotion.} We aim at the reduction(s) shown in
  Fig.~\ref{fig:prom-one-idea}: a $\mathsf{one}$ node with memory set to $n$
  is sent to a frozen computation (inside a $!$-box) computing the
  same $\mathsf{one}$ node. Since {\textsf{SMEYLL}} features recursion in the form
  of the $Y$-box, together with the copy operation already defined it
  is possible to write a net for the formula $\bot\parr{!\mathsf{1}}$, as
  shown in Fig.~\ref{fig:prom-one-net}.
\item
  {\em Weakening.}  We can directly use the coding given on the
  r.h.s. of
  Fig.~\ref{one_equiv}.\\
\end{varitemize}
\begin{figure}
\begin{center}
\fbox{
  \begin{minipage}{.47\textwidth}
    \begin{center}
      \includegraphics[page=6,width=8.2cm]{PCFcbv-positive-nodes.pdf}
    \end{center}
  \end{minipage}}
\end{center}
\caption{Desired Behavior for the Mapping of $\mathsf{1}$ to ${!\mathsf{1}}$.}\label{fig:prom-one-idea}
\end{figure}
\begin{figure}
\begin{center}
\fbox{
  \begin{minipage}{.47\textwidth}
    \begin{center}
      \includegraphics[page=7,width=6cm]{PCFcbv-positive-nodes.pdf}
    \end{center}
  \end{minipage}}
\end{center}
\caption{\ensuremath{\mathsf{PCF}}\ Net Computing $\bot\! \parr {!1}$.}\label{fig:prom-one-net}
\end{figure}
\paragraph*{Exponential Rules for the Image $A^\dagger$ of any Type $A$}
The goal of this paragraph is to construct nets which behave like the
nodes $?c$, $?w$ and $?p$ of linear logic, this for any edge of type
$A^\dagger\b$.  For any type $A$, the formula $A^\dagger$ is a
multi-tensor of $\mathsf{1}$'s and $!$-ed types. We therefore construct the
grey contraction, weakening and promotion nodes inductively on the
structure of the type, as presented in Fig.~\ref{fig:cwp-pos-type}.
\begin{figure*}
\begin{center}
  \fbox{
    \begin{minipage}{14cm}
    \begin{center}
      \includegraphics[width=13cm,page=1]{PCFcbv-positive-nodes2}
    \end{center}
  \end{minipage}}
\end{center}
\caption{Inductive Definition of Contraction, Weakening and Promotion
  Nodes.}\label{fig:cwp-pos-type}
\end{figure*}
\paragraph*{Interpreting Typing Judgements}
Typing derivations are inductively mapped to \ensuremath{\mathsf{PCF}}\ nets as shown in
Fig.~\ref{fig:PCFcbv}. The grey nodes $\mathsf{?c}$ and $\mathsf{?w}$
were defined in Fig.~\ref{fig:cwp-pos-type} (the case of $?\bot$ has
been discussed above). The grey node ``$\mathsf{?}$'' is a shortcut
for the following construction:
\begin{center}
  \includegraphics[page=3,height=2cm]{PCFcbv-positive-nodes.pdf}
\end{center}
\begin{figure*}
\begin{center}
  \fbox{
    \begin{minipage}{15cm}
      \begin{center}
        \includegraphics[page=1,width=14cm]{PCFcbv3}
      \end{center}
    \end{minipage}}
\end{center}
\caption{Call-by-Value Translation of \ensuremath{\mathsf{PCF}}\ into \ensuremath{\mathsf{PCF}}\ Nets.}\label{fig:PCFcbv}
\end{figure*}
\paragraph*{Adequacy}
We prove the following result, which relates the call-by-value
encoding into \ensuremath{\mathsf{PCF}}\ nets and the call-by-value reduction strategy for
terms:
\begin{theorem}
  \label{th:adequacy-cbv}
  Let $M$ be a closed term of type $\mathbb{N}$. Then $M\to_{\it cbv}\PCFn{n}$
  if and only if $M^\dagger\Downarrow n$
\end{theorem}
As a corollary, we conclude that the machine on $M^\dagger$ behaves as
$M$ in call-by-value.
\begin{corollary}
  Let $M$ be a closed term of type $\mathbb{N}$. Then $M$ call-by-value
  converges if and only if $\mathcal{M}_{M^\dagger}$ itself converges
\end{corollary}

\subsection{The Call-by-Name Encoding}
Besides the encoding of call-by-value \ensuremath{\mathsf{PCF}}, which is non-standard, and
has thus been described in detail, program nets also have the
expressive power to encode call-by-\emph{name} \ensuremath{\mathsf{PCF}}. The encoding is
the usual one: a proof net corresponding to
$x_1:A_1,\dots,x_n:A_n\vdash M:B$ has conclusions
$\{?A_1^*\b,\ldots, ?A_n^*\b, B^*\}$
\[
\includegraphics[page=2,width=5cm]{PCFcbn.pdf}
\]
where $(\cdot)^*$ is a mapping
of types to {\textsf{SMEYLL}} formulas:
\begin{align*}
\mathbb{N}^*&{}:=~\mathsf{1};\\
  (A\to B)^* &{}:=~ ?(A^*)\b\parr B^*;\\
  (A\times B)^* &{}:=~ {!(A^*)}\otimes{!(B^*)}.
\end{align*}
\noindent Typing derivations are mapped to \ensuremath{\mathsf{PCF}}{} nets essentially in
the standard way, and presented in Figure~\ref{fig:PCFcbn}. Note that
unlike the call-by-value translation, since every context is always in
$?$-form, we do not need special weakening, contraction and promotion
nodes.
Then, as in the previous section, one can relate the
call-by-name encoding in \ensuremath{\mathsf{PCF}}\ nets and the call-by-name reduction
strategy for terms.

\begin{figure*}
\begin{center}
  \fbox{
    \begin{minipage}{15cm}
      \begin{center}
        \includegraphics[page=1,width=14cm]{PCFcbn}
      \end{center}
    \end{minipage}}
\end{center}
\caption{Call-by-Name Translation of \ensuremath{\mathsf{PCF}}\ into \ensuremath{\mathsf{PCF}}\ Nets.}\label{fig:PCFcbn}
\end{figure*}

\begin{theorem}[Adequacy]
  \label{th:adequacy-cbn}
  Let $M$ be a closed term of type $\mathbb{N}$. Then $M\to_{\it cbn}\PCFn{n}$
  if and only if $M^*\Downarrow n$
\end{theorem}
As a corollary, one can show that the  machine on $M^*$ behaves
as $M$ in call-by-name.
\begin{corollary}
  Let $M$ be a closed term of type $\mathbb{N}$. Then $M$ converges in
  call-by-name if and only if the register machine $\mathcal{M}_{M^*}$ itself converges.

\end{corollary}
\section{Conclusions}
We have shown how the multitoken paradigm not only works well in the
presence of exponential and fixpoints, but also allows us to treat
different evaluation strategies in a uniform way. Some other
interesting aspects which emerged along the last section are worth
being mentioned.

In the call-by-value encoding of \ensuremath{\mathsf{PCF}}, we have used binary \emph{sync
  nodes} in an essential way, to duplicate values in the register:
without them, the efficient encoding of natural numbers would not have
been possible. This shows that sync nodes can indeed have an
interesting computational role besides reflecting entanglement in
quantum computation~\cite{lics2014}. In the future, we plan to further
the potential of such an use, in particular in view of
efficient implementations.

A key feature of \textsf{SMEYLL}{} nets rewriting is that it is
\emph{surface}. Surface reduction allows us to interpret recursion,
but how much do we lose by considering surface reduction instead of
usual cut-elimination? We think that a simple way to understand the
limitations of surface reduction is to consider an analogy to
Plotkin's weak reduction. In \ensuremath{\mathsf{PCF}}, $\lambda x.\Omega$ is a normal
form. As a consequence one loses, \emph{e.g.}, some nice results about the
shape of normal forms in the $\lambda$-calculus (which, in logic,
corresponds to the subformula property). In presence of fixpoints,
however, this is a necessary price to pay. Otherwise, any term
including a fixpoint would diverge. Of course there is much more to be
said about all this, and we refer the reader to, \emph{e.g.}, the work by
Simpson~\cite{SimpsonRTA2005}.

\section*{Acknowledgments}
The first author is partially supported by the
ANR project 12IS02001 PACE. The second and third authors were supported by the project
ANR-2010-BLANC-021301 ``LOGOI''.
\bibliographystyle{abbrv}