Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination. He also introduced a new cut elimination strategy, dubbed the good strategy, and showed that its number of steps is a time cost model with polynomial overhead for the ESC/IMELL, and the first such one.

Here, we refine Accattoli's result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead.

§ INTRODUCTION

One of the advances of the last decade in the theory of $\l$-calculus is the study of reasonable cost models carried out by Accattoli, Dal Lago, and co-authors <cit.>, completing the research program started by Dal Lago and Martini almost 20 years ago <cit.>.

The General Problem.
Focusing on time, the underlying problem is whether the number of $\beta$-steps (of a fixed evaluation strategy) can be taken as a measure of time that is polynomially equivalent to that of random access machines (RAMs); or, equivalently, to that of Turing machines. This is a priori unclear because there are families of terms suffering of size explosion: the size of terms grows exponentially with the number of $\beta$-steps, independently of the adopted evaluation strategy. The difficulty is finding a strategy, together with a simulation on RAMs of the strategy, working within a overhead polynomial in:

* Length: the number of steps of the strategy, and

* Input: the size of the initial term.

When a strategy admits such a simulation we say that it is a a polynomial cost model. Note that the number of steps of the strategy can be whatever (it need not be polynomial), it is the overhead of the simulation that has to be polynomial in the above parameters.

The overhead is required to be polynomial because reasonable frameworks are not necessarily linearly related; this is the reason why the complexity class $\P$ is so important. For instance, Turing machines simulate RAMs only within a quadratic overhead. When possible, however, it is interesting to know what is the exact degree of the overhead with respect to RAMs, which are the commonly accepted abstraction of modern computers. When the overhead is linear—which is the optimal situation—then the polynomial cost model is trustable in practice: it does not hide an acceptable but possibly costly polynomial overhead.

Today, it is well-known that strategies such as weak head, head, and leftmost $\beta$-reduction provide polynomial time cost models, and that the same is true for their call-by-value and call-by-need variants <cit.>.

LSC and the Sub-Term Property.
The key tool for the polynomially bounded simulations underlying the recent advances is Accattoli and Kesner's linear substitution calculus (shortened to LSC) <cit.>, which is an intermediary setting between the $\l$-calculus and RAMs.

The LSC is a simple $\l$-calculus with explicit substitutions refining a previous calculus by Milner <cit.> and where evaluation is micro-step, that is, substitution acts on a variable occurrence at a time, rather than on all at once (which is small-step). A distinguished feature of the LSC is its rewriting rules at a distance, that is, rules where explicit substitutions do not percolate through the term structure but rather act through some contexts. The relevance of the LSC for reasonable time is linked to the sub-term property of its standard strategies <cit.>: at any point, only sub-terms of the initial term are duplicated, thus allowing one to bound the cost of each duplication with the size of the input.

No strategy of the $\l$-calculus has the sub-term property, which, as discussed by Accattoli <cit.>, is the essence of the size explosion problem. The LSC crystallizes exactly what is needed for refining the $\l$-calculus to retrieve the sub-term property and circumvent size explosion.

LSC and Abstract Machines.
It is also well-known that strategies of the LSC can usually be implemented with environment-based abstract machines whose overhead is bi-linear, that is, linear in both the input and length parameters, as shown by Accattoli et al. <cit.>. Abstract machines handle three tasks, namely the decomposition of the substitution process, the search for redexes, and $\alpha$-renaming. The difference between the LSC and abstract machines is that the LSC only handles the substitution process, the critical one for avoiding size explosion. Search and $\alpha$-renaming, indeed, tend to take only a linear overhead. That said, handling search and $\alpha$-renaming provides an in-depth understanding of evaluation and it is mandatory for obtaining precise bounds from the cost model.

Lifting to Linear Logic.
In 2022, Accattoli started a generalization of the mentioned recent results for the $\l$-calculus to the wider framework of linear logic <cit.>. Linear logic can be seen as a micro-step system with a tight control over duplications, somewhat similar to the LSC. Accattoli's starting point is the observation that, despite such similarity, no reasonable cut elimination strategy for linear logic was available. In particular, no cut elimination strategy with the sub-term property was known.

In <cit.>, he introduces a generalization of the LSC to intuitionistic multiplicative exponential linear logic (IMELL). His exponential substitution calculus (ESC) is an untyped calculus of proof terms for the sequent calculus proofs of IMELL, endowed with cut elimination at a distance and having IMELL as typing system. He then designs a new cut elimination strategy, dubbed good strategy, which has the sub-term property and which is a polynomial cost model for ESC, the first such cost model for an expressive fragment of linear logic.

This Paper.
Here, we design an environment-based abstract machine implementing the good strategy of ESC, show that it has bi-linear overhead, and provide an OCaml implementation. The result is not surprising, and yet we believe that it is interesting, for various reasons. Firstly, it is the first linear overhead result for an expressive fragment of linear logic. It allows one to extract precise time bounds from the length of cut elimination, and can thus be useful, for instance, in linear-logic-based implicit computational complexity.

Secondly, our study differs in many details from other environment-based machines. There are in fact at least two literatures related to our work (surveyed in the next paragraph). A recent one about cost analyses of machines for $\l$-calculi and an older one about machines for linear logic, here referred to as linear machines. The main differences are the following:

* Natural deduction $vs$ sequent calculus: machines usually implement calculi based on natural deduction, while ESC is based on sequent calculus, and some aspects are different. For instance, our machine has no argument stack (as it is expected, after Herbelin <cit.>).

* Micro-step source and no structural equivalence: the implemented calculus is usually small-step, while here it is micro-step. In the literature, when the calculus is micro-step it is usually implemented by the machine up to a notion of structural equivalence. Here, there is no need of structural equivalence.

* Strong $vs$ weak: our machine computes cut-free proofs, while other linear machines in the literature do not, as they usually only perform weak (or surface) evaluation (that is, they do not evaluate under abstraction and inside promotions). To our knowledge, ours is the first strong linear machine.

* Strong with no backtracking: machines for strong evaluation usually have transitions for sequentially backtracking once the evaluation of a sub-term is over. Here, we adopt a recent new technique for strong machines by Accattoli and Barenbaum <cit.>, that avoids sequential backtracking. The idea is to assign distinct jobs to each sub-term and simply jumping to the next job once the current one is over. This approach structures the machine in a very different way and provides drastically simpler strong machines.

* Complexity analysis: the complexity of linear machines is never studied in the literature.

* OCaml implementation: linear machines are usually studied theoretically and never implemented. We provide an OCaml implementation verifying our complexity analysis. In particular, it is the first implementation of the technique for strong machines of <cit.>.

Summing up, our machine is simple, given the complex setting that it implements, thanks to the absence of stacks and backtracking. In fact, it uses just one (non-trivial) data structure.

Methodologically, the main difference between our work and the literature on linear machines is that those machines were developed to provide insights about $\l$-calculi and functional programming (such as no garbage collection, in-place updates, and single pointer property) while here we proceed the other way around, using the recent theory of the $\l$-calculus to provide insights about linear logic.

Architecture of the Result.
The good strategy that we implement is a non-deterministic but diamond strategy, where diamond means that the choices do not affect termination nor evaluation lengths (otherwise the number of steps would not be a well-defined cost model). Our implementation is in two phases. The first and main one, performed by a deterministic machine dubbed SESAME (Strong Exponential Substitution Abstract Machine without Erasure), never erases. The second one is a simple garbage collection pass over the output of SESAME, that produces a cut-free term. For the correctness of SESAME, we thus need to relate a non-deterministic strategy and a deterministic machine, which is slightly unusual. For that, we follow the abstract recipe of Accattoli et al. <cit.> which is here simplified because our case is not up to structural equivalence and there is no implosiveness.

Related Work.
Accattoli and co-authors studied at length the overhead of machines for $\l$-calculi both micro-step <cit.> and small-step <cit.>. Biernacka et al. similarly studied machines for strong call-by-value <cit.> and strong call-by-need <cit.>.

Lafont considered the first linear logic (LL) machine, based on categorical combinators for intuitionistic LL (ILL) <cit.>. Abramsky considered an environment-based machine for ILL and a chemical-style machine for LL, both doing only weak evaluation <cit.>. The latter machine was then studied by Mikami and Akama <cit.> and Sato and co-authors <cit.>. Turner and Wadler study the use of IMELL for memory management and give two machines, one with the single pointer property and one without it but with a memoization mechanism <cit.>. Alberti and Ritter also deal with the single pointer property <cit.>. Bonelli gives a machine based on an unusual sequent calculus for ILL <cit.>.

The interaction abstract machine (IAM) is an unusual token-based machine for LL proofs first studied by Danos and Regnier <cit.> and Mackie <cit.>. Recent work by Accattoli et al. showed that the IAM overhead is unreasonable for both time and space <cit.>. Mackie also studied interaction nets-based implementations of LL <cit.>.

§ THE EXPONENTIAL SUBSTITUTION CALCULUS

In this section, we briefly recall Accattoli's exponential substitution calculus (ESC) <cit.> which is an untyped calculus having IMELL as system of simple types.

For more explanations, we refer the reader to <cit.>. The main differences with respect to <cit.> is that, for lack of space, we omit tensor and we only deal with micro-step rewriting rules (omitting the small-step exponential rule, which is derivable). In IMELL, linear implication is 'more important' than tensor, as tensors are not needed to simulate the $\l$-calculus. In tensorsIn Appendix B of the technical report <cit.>, we explain how to straightforwardly extend our study to tensor.

Values and Terms.
The grammars of ESC are in the upper part of esc. Variables are of two disjoint kinds, multiplicative and exponential, and we refer to variables of unspecified kind using $\var,\vartwo,\varthree$. Values are the proof terms associated to axioms or to the right rules and, beyond variables, are abstractions $\la\var\tm$ and promotions $\bang\tm$. The proof terms decorating left rules are subtractions $\suba\mvar\val\var\tm$, derelictions $\dera\evar\var\tm$,  and cuts $\cuta\val\var\tm$, which is in red because of its special role.  Note that cuts and subtractions are split, that is, have values (rather than terms) as left sub-terms.
The constructors $\la\var\tm$, $\suba\mvar\val\var\tm$, $\dera\evar\var\tm$, and $\cuta\val\var\tm$ bind $\var$ in $\tm$. We identify terms up to $\alpha$-renaming. Free variables (resp.  multiplicative/exponential variables) are defined as expected, and noted $\fv\tm$ (resp. $\mfv\tm$ and $\efv\tm$). We use $\size\tm$ for the number of constructors in $\tm$, and $\sizep\tm\var$ for the number of free occurrences of $\var$ in $\tm$.
There is a notion of proper term ensuring the linearity of multiplicative variables and the exponential boundary of promotions, detailed in escdetailed in Appendix A of the tech report <cit.>. The only relevant case is: $\bang\tm$ is proper if $\tm$ is proper and $\mfv\tm = \emptyset$. In the following, terms are assumed to be proper.

Contexts and Plugging.
The broadest notion of context that we consider is general contexts $\ctx$, which simply allow the hole $\ctxhole$ to replace any sub-term in a term. Because of split cuts and subtractions (that is, the fact that their left sub-term is a value rather than a term), the definition relies on the auxiliary notion of value context $\vctx$. The definition also uses left contexts $\lctx$, which are contexts under left constructors (or, for binary left constructors, under the right sub-term) that play a key role in the system—their use in defining $\ctx$ is just to keep the grammar compact. We also need cut contexts $\ectx$, which are noted with $\ectx$ because they shall play the role of machine environments in BAM.

A fact used pervasively is that every term $\tm$ writes, or splits uniquely as $\tm = \lctxp\val$. For instance $\dera\evar\mvar\cuta\val\mvartwo \la\evarthree\suba\mvar\mvartwo\evartwo\evartwo$ splits as $\lctx = \dera\evar\mvar\cuta\val\mvartwo\ctxhole$ and $\val =\la\evarthree\suba\mvar\mvartwo\evartwo\evartwo$.

Because of split cuts and subtractions, the definition of plugging $\ctxp\tm$ (or $\ctxp\ctxtwo$) of a term $\tm$ (or a context $\ctxtwo$) in a context $\ctx$ is slightly tricky, as it has to preserve the split shape. We refer the reader to <cit.> for such details, the definition is mostly as expected (the only two subtle cases are for $\cuta\ctxhole\var\tm$ and $\suba\mvar\ctxhole\var$). Plugging can capture variables and we use $\ctxfp\tm$ when we want to prevent it.

IMELL has a type system for ESC.

The formulas of IMELL, and the deductive rules of the sequent calculus annotated with ESC terms, are in esc-types. They are taken directly from <cit.>. The typing system for  ESC is exactly the standard sequent calculus for IMELL. Both formulas and rules are standard, but for the decoration with proof terms and the side conditions about variable names of the form $\multiForm\#\multiFormtwo$, which is a shortcut for $\dom\multiForm\cap\dom\multiFormtwo = \emptyset$. Linear implication $\lolli$ is also referred to as lolli. The only atomic formula that we consider, $\aform$, is multiplicative. There is no multiplicative unit because, in presence of the exponentials, $1$ can be simulated by $!(\aform \lolli\aform)$. We distinguish between multiplicative and exponential axioms, in order to decorate them with the corresponding kind of variable.

Note that the weakening and contraction rules do not add constructors to terms. This is crucial in order to keep the calculus manageable. Note also that the decorations of the cut and $\lolliLeftRule$ rules are split, as explained in the previous section. Clearly, typed terms are proper.

In this paper, types are only referred to in clashfree-implies-cutfree below.

Multiplicative Cut Elimination Rules.
The rewriting rules are in esc. The ESC has three multiplicative rules, in particular two for axioms, depending on whether they are acted upon ($\toaxmone$) or used to rename another multiplicative (thus linear) variable ($\toaxmtwo$). Rule $\toaxmone$ is expressed generically for multiplicative values $\mval$ (that is, multiplicative variables $\mvar$ and abstractions $\la\var\tm$). In $\toaxmone$, $\toaxmtwo$, and $\tololli$, it is silently assumed that $\ctx$ does not capture $\mvar$ in $\toaxmtwo$ and $\tololli$ (what is noted $\ctxfp\mvar$ in $\toaxmone$, while $\ctxholefp\cdot$ is not used in $\toaxmtwo$, and $\tololli$ because $\ctx$ might capture other variables in $\tm$ and $\val$). Note that, since $\ctx$ cannot capture $\mvar$ in these rules and terms are assumed to be proper, the hole of $\ctx$ cannot be contained in a $!$; this kind of context is called a multiplicative context in <cit.>.

In $\tololli$, the rule has to respect split cuts, which is why, for writing the reduct, the sub-term $\tmtwo$ is split on-the-fly. An example of $\tololli$ step follows:

\cuta{\la\evar\dera\evar\mvar\mvar}\mvartwo\suba\mvartwo{\bang\evartwo}\mvarthree\mvarthree
& \tololli &
\cuta{\bang\evartwo}\evar\dera\evar\mvar\cuta\mvar\mvarthree \mvarthree.
\end{array}$

Exponential Rules.
There are also four exponential rules, with again two rules for axioms. Replacement of variables ($\toaxeone$) and erasure ($\tow$) are expressed generically for exponential values $\exval$ (that is, exponential variables $\evartwo$ and promotions $\bang\tm$), interaction with derelictions (in $\toaxetwo$ and $\tobang$) instead requires inspecting $\exval$.
Rule $\tobang$ removes the dereliction, copies the promotion body, and puts it in a cut—in proof nets jargon, it opens the box. To preserve the split shape, the body of the promotion is split and only the value is cut. An example:

\cuta{\bang\cuta\evartwo\evarthree \evarthree}\evar \la\mvar\dera\evar{\evar'} \suba\mvar{\evar'}\mvartwo\mvartwo
& \tobang &
\cuta{\bang\cuta\evartwo\evarthree \evarthree}\evar\la\mvar\cuta\evartwo\evarthree \cuta{\evarthree}{\evar'} \suba\mvar{\evar'}\mvartwo\mvartwo.
\end{array}$

Note that $\tobang$ entangles interaction with a dereliction and duplication, which is not what proof nets usually do (but this is what the LSC does).  It is silently assumed that $\ctx$ does not capture $\evar$ in $\toaxetwo$ and $\tobang$ but it might capture other variables in $\tm$.

Comments about the Rewriting Rules.
Unsurprisingly, proper terms are stable by reduction <cit.>. We also use a notion of position in terms.

A position in a term $\tm$ is a decomposition $\tm=\ctxp\tmtwo$ such that $\tmtwo$ is a sub-term of $\tm$.

For later defining the good strategy, we identify a redex with its position, which is a context. Every step $\tm \tomsnw \tmtwo$ reduces a redex of shape $\tm=\ctxp{\cuta\val\var\ctxtwop{\tm_{\var}}}$ where $\tm_{\var}$ is an occurrence of $\var$, a sub-term of $\tm$ of shape $\var$, $\suba\var\val\vartwo\tmtwo$, or $\dera\var\vartwo\tmtwo$. The redex position of $\tomsnw$ steps is the context $\ctxp{\cuta\exval\var\ctxtwo}$. The redex position of $\tow$ steps is the context closing the root step. We write $\ctx:\tm\toesc\tmtwo$ for a redex of position $\ctx$ in $\tm$.

The presence of many constructors in an untyped setting gives rise to clashes, that is, irreducible cuts.

A clash is a term of the form $\cuta\mval\evar\tm$ or $\cuta\exval\mvar\tm$. A term $\tm$ is clashing if it has a clash as sub-term. Moreover, $\tm$ is clash-free if, co-inductively,
$\tm$ is not clashing and $\tmtwo$ is clash-free for any step $\tm \toms \tmtwo$.

Clash-freeness is guaranteed by all forms of types (simple, polymorphic, recursive, and multi types, for instance), in particular by the IMELL types in esc-types, as ensured by the next lemma. Here, we adopt the untyped calculus but consider only clash-free terms, as in <cit.>.

Let $\tm$ be a proper term.

* If $\tm$ has no clashes and $\tm \not\toms$ then $\tm$ is cut-free.

* If $\tm$ is typable (by the IMELL type system in esc-types) then $\tm$ is clash-free.

Postponement of Garbage Collection.
The erasing rule $\tow$, that models garbage collection, can be postponed. This point shall be crucial for our study.

If $\tm \toms^{*} \tmtwo$ then $\tm \tomsnw^{*} \tow^{*} \tmtwo$.

Basic Evaluation.
As an intermediary step towards our results, we consider also a restricted form of ESC evaluation, forbidding reduction under all constructors but the right sub-terms of cuts, and dub it basic evaluation. It is one possible ESC analogous of weak evaluation in the $\l$-calculus (which forbids evaluation under abstraction). In $\l$-calculi with explicit substitutions, weak normal forms of closed terms are answers, i.e. abstractions possibly surrounded by explicit substitutions. We obtain a similar property for basic evaluation.

A step $\ctx:\tm \toms \tmtwo$ (that is, a redex of position $\ctx$ in $\tm$) is basic if $\ctx$ is a cut context, which is also noted with $\tm \Rew{\symfont{b}} \tmtwo$, or $\tm \Rew{\symfont{b}a} \tmtwo$ with $a\in\set{\axmone,\axmtwo,\lolli, \axeone,\axetwo,\bang,\wsym}$ if we want to specify the kind of step. Moreover, $\Rew{\symfont{b}\neg\wsym}$ denotes a non-erasing (that is, not $\wsym$) basic step. A term $\tm$ is an answer  if $\tm = \ectxp\val$ with $\ectx$ a cut context and $\val$ not a variable.

Let $\tm$ be a closed clash-free term. Either $\tm$ has a $\Rew{\symfont{b}\neg\wsym}$-step or it is an answer.

Basic evaluation is enough to simulate in ESC the call-by-name/value weak evaluation of closed $\l$-terms, via Girard's translations to linear logic. Moreover, basic non-erasing evaluation is deterministic (and diamond, a property defined in strategy, when erasing steps are considered). We omit the proofs of these facts, because neither basic evaluation nor $\l$-terms are the focus of the paper.

Out Cuts and Garbage Collection.
We shall mainly deal with cuts that are not contained in any other cut, the out cuts, which induce a notion of out variable.

The out cuts of a term $\tm$ are those cuts in $\tm$ that are not contained in any other cut, that is, if $\tm = \ctxp{\cuta\val\var\tmtwo}$ then $\cuta\val\var\tmtwo$ is an out cut of $\tm$ if $\ctx$ cannot be written as $\ctx=\ctxtwop{\cuta\vctx\vartwo\tmthree}$ for some $\ctxtwo$, $\vctx$, $\vartwo$, and $\tmthree$. The set of out variables $\ov\tm$ of $\tm$ contains the variables having at least one occurrence out of all cuts of $\tm$.

Out variables allow us to define a lax notion of cut-free terms where there are some cuts, but they can only be garbage collection cuts, or concern variable occurrences contained in garbage, so that the term becomes cut-free after garbage collection.

A term $\tm$ is cut-free up to garbage if $\var\notin\ov\tmtwo$ for all the out cuts $\cuta\val\var\tmtwo$ of $\tm$.

§ THE GOOD STRATEGY

Here, we define the good cut elimination strategy $\tog$ for ESC, recalling the discussion from <cit.> that explains the design of the strategy.
The strategy is conceived as to have the sub-term property, which is crucial for time analyses and which is defined as follows: every duplicated (or erased) sub-term during a cut elimination sequence is a sub-term of the initial term (up to variable renamings). See <cit.> for extensive discussions about the sub-term property.

Breaking the Sub-Term Property.
When does the sub-term property not hold? One has to duplicate an exponential value $\exval$ touched by previous steps. In our setting, touched can mean two things. Either a redex fully contained in $\exval$ is reduced, obtaining $\exvaltwo$, and then $\exvaltwo$ is duplicated (or erased), as in the step marked with $\bigstar$ in the following diagram (the other, dashed path of which has the sub-term property):

at (0,0)[align = center](source)$  \cuta{\exval} \evar \ctxfp{\evar}$;
at (source.center)[right = 170pt](source-right)$\cuta{\exvaltwo} \evar \ctxfp{\evar}$;
at (source.center)[below = 25pt](source-down)$\cuta{\exval}\evar\ctxfp{\exval}$;

at (source-right|-source-down)(target)$\cuta{\exvaltwo}\evar\ctxfp{\exvaltwo}$;
at source-down.easttarget.west(fifthnode)$\cuta{\exvaltwo} \evar \ctxfp{\exval}$;

[->](source) to node[above] $\escsym $ (source-right);
[->](source-right) to node[right] $\axeone$ node[right=20pt] $\bigstar$(target);

[->, dotted](source) to node[left] $\axeone$(source-down);
[->, dotted](source-down) to node[above] $\escsym$ (fifthnode);
[->, dotted](fifthnode) to node[above] $\escsym$ (target);

Preventing these situations from happening, thus forcing evaluation to follow the other (dashed) side of the diagram, is easy. It is enough to forbid the position of the reduced redex to be inside the left sub-term of a cut—we say inside a cut value for short. It is however not enough, because cuts are also created. Consider:

\begin{array}{clllllcl}
\cuta{\la\evar\evar}\mvar\suba\mvar\exval\var\tm &\toesc&
\cuta{\la\evar\evar}\mvar\suba\mvar\exvaltwo\var\tm &\tololli
\\
&&\cuta\exvaltwo\evar\cuta\evar\var\tm &\overset\bigstar\rightarrow_{\axeone} &
\cuta\exvaltwo\evar\cuta\exvaltwo\var\tm
\end{array}

Reducing inside the subtraction value $\exval$ leads to a later breaking of the sub-term property by the $\axeone$ step, because the $\tololli$ step creates a cut with $\exvaltwo$ inside.
Preventing these cases is tricky, because forbidding reducing subtraction values leads to cut elimination stopping too soon, without producing a cut-free term. In the $\l$-calculus, it corresponds to forbidding reducing inside arguments, which leads to head reduction, that does not compute normal $\l$-terms. We shall then forbid reducing only subtraction values which are at risk of becoming cuts. In $\l$-calculus, leftmost reduction does reduce arguments but only when the left sub-term of the application is normal and not an abstraction, so that the argument is not involved in a $\beta$-redex. We shall do something similar here, but  the sequent calculus formalizes this constraint differently, by checking that some variables are not captured.

Dominating Variables.
The key notion is the one of dominating (free) variables $\dfv\ctx$ of a context (where $\ctx$ is meant to be the position of a redex), defined in strategy, the base case of which is for $\suba\mvar\vctx\var\tm$. If $\ctx$ is a position and $\var\in\dfv\ctx$ then $\cuta\val\var\ctx$ turns $\ctx$ into a dangerous position, that is, a redex of position $\cuta\val\var\ctx:\tm\toms\tmtwo$ might lead to a breaking of the sub-term property later on during cut elimination. In the example, $\evar$ belongs to $\dfv\ctx$ for every context $\ctx\defeq \dera\evar\mvar\suba\mvar\vctx\var\tmtwo$ of $\dera\evar\mvar\suba\mvar\val\var\tmtwo$, for every $\vctx$.

The Good Strategy.
These considerations lead to the notion of good contexts in strategy. A good context forbids the two ways of breaking the sub-term property: its hole cannot be in a cut value (note the absence of the production $\cuta{\vgctx}\var\tm$) nor in a subtraction value such that one of its dominating variables is cut (because of the production $\cuta\val\var\gctx$ if $\var\notin\dfv\gctx

A step $\ctx : \tm \toms \tmtwo$ is good if its position $\ctx$ is good. In such a case, we write $\tm \tog \tmtwo$. The good cut elimination strategy is simply $\tog$. We also use $\togp a$ to stress that the good step is of kind $a\in\set{\axmone,\axmtwo,\lolli, \axeone,\axetwo,\bang,\wsym}$. The non-erasing good strategy $\tognotw$ is the variant of $\tog$ excluding $\togp\wsym$ steps.

The sub-term property in the following theorem captures the quantitative aspect for cost analyses, i.e. the bound on the size of duplicated values by the size of the initial term.

* Quantitative sub-term property: if $\deriv:\tm \tog^{*} \tmtwo$ and $\val$ be a value erased or duplicated along $\deriv$, then $\size\val\leq \size\tm$.

* Diamond: if $ \tmtwo_{1} \lRew{\Gsym}\tm \tog \tmtwo_{2}$ and $\tmtwo_{1} \neq \tmtwo_{2}$ then $ \tmtwo_{1} \tog \tmthree \lRew{\Gsym}  \tmtwo_{2}$ for some $\tmthree$.

* Fullness: if $\tm$ is clash-free and not $\toms$-normal then $\tm \tog\tmtwo$ for some $\tmtwo$.

* Good polynomial cost model: if $\multiform\vdash \tm\hastype \form$ is a typed term then there exist  $k$ and a cut-free term $\tmtwo$ such that $\tm \tog^{k} \tmtwo$, and such a reduction sequence is implementable on RAMs in time polynomial in $k$ and $\size\tm$.

The algorithmic aspect of sub-term-prop.4 is proved in  <cit.> via arguments that do not establish the degree of the polynomial bound. The aim of this paper is exactly to show that a carefully designed abstract machine provides a bound that is linear in both $k$ and $\size\tm$.

The Diamond Property.
Let us provide some background about the diamond property.
Following Dal Lago and Martini <cit.>, we say that a relation $\Rew{\Rule}$ is diamond if $\tmtwo_1 \lRew{\Rule} \tm \Rew{\Rule} \tmtwo_2$ and $\tmtwo_1 \neq \tmtwo_2$ imply $\tmtwo_1 \Rew{\Rule} \tmthree \lRew{\Rule} \tmtwo_2$ for some $\tmthree$.
The terminology in the literature is inconsistent: Terese <cit.> dubs this property $\textup{CR}^1$, and defines the diamond more restrictively, without requiring $\tmtwo_1 \neq \tmtwo_2$ in the hypothesis: $\tmtwo_1$ and $\tmtwo_2$ have to join even if $\tmtwo_1 = \tmtwo_2$.

Standard corollaries of Dal Lago and Martini's notion are that, if $\Rew{\Rule}$ is diamond, then:

* Confluence:
$\Rew{\Rule}$ is confluent, that is, $\tmtwo_1  \lRewn{\Rule} \tm \Rew{\Rule}^* \tmtwo_2$  implies $\tmtwo_1 \Rew{\Rule}^* \tmthree \lRewn{\Rule} \tmtwo_2$ for some $\tmthree$;

* Length invariance: all $\Rule$-evaluations with the same start and $\Rule$-normal end terms have the same length (if $\deriv \colon \tm \Rew{\Rule}^k \tmtwo$  and $\deriv' \colon \tm \Rew{\Rule}^h \tmtwo$ with $\tmtwo$ $\Rule$-normal, then $h = k$);

* Uniform normalization: $\tm$ is weakly $\Rule$-normalizing if and only if it is strongly $\Rule$-normalizing.

Basically, the diamond property captures a more liberal form of determinism. In particular, length invariance is essential in order to take the number of steps of a strategy as a cost model. Without it, indeed, the number of steps of a non-deterministic strategy would be an ambiguously defined notion of cost.

§ PRELIMINARIES ON ABSTRACT MACHINES

Abstract Machines Glossary.
Abstract machines manipulate pre-terms, that is, terms without implicit $\alpha$-renaming. In this paper, an abstract
machine is a quadruple $\mach = (\States, \tomach, \compilrel\cdot\cdot, \decode\cdot)$ the components of which are as follows.

* States. A state $\state\in\States$ is composed by the active term $\tm$, plus one data structure which depends on the actual machine. Terms in states are actually pre-terms.

* Transitions. The pair $(\States, \tomach)$ is a transition
system with transitions $\tomach$ partitioned into principal transitions, whose union is noted $\tomachpr$ and that are meant to correspond to cut-elimination steps on the calculus, and search transitions, whose union is noted $\tomachsea$, that take care of searching for (principal) redexes.

* Initialization. The component $\compilrel{}{}\subseteq\Lambda\times\States$ is the initialization relation associating  terms to
initial states. It is a relation and not a function because $\compilrel\tm\state$ maps a $\l$-term $\tm$ (considered modulo $\alpha$) to a state $\state$ having a pre-term representant of $\tm$ (which is not modulo $\alpha$) as active term. Intuitively, any two states $\state$ and $\statetwo$ such that $\compilrel\tm\state$ and $\compilrel\tm\statetwo$ are $\alpha$-equivalent.
The initializing terms (i.e. those $\tm$ such that $\compilrel\tm\state$ for some $\state$) are always  proper and clash-free.
A state $\state$ is reachable if it can be reached starting from an initial state, that is, if $\statetwo \tomach^*\state$ where $\compilrel\tm\statetwo$ for some $\tm$ and $\statetwo$, shortened as $\compilrel\tm\statetwo \tomach^*\state$.

* Read-back. The read-back function $\decode\cdot:\States\to\Lambda$ turns reachable states into
terms and satisfies the initialization constraint: if $\compilrel\tm\state$ then $\decode{\state}=_\alpha\tm$.

Further Terminology and Notations.
A state is final if no transitions apply.
A run $\run: \state \tomach^*\statetwo$ is a possibly empty finite sequence of transitions, the length of which is noted
$\size\run$; note that the first and the last states of a run are not necessarily initial and final.
If $a$ and $b$ are transitions labels (that is, $\tomachhole{a}\subseteq \tomach$ and
$\tomachhole{b}\subseteq \tomach$) then $\tomachhole{a,b} \defeq \tomachhole{a}\cup \tomachhole{b}$ and $\sizep\run a$
is the number of $a$ transitions in $\run$, and $\sizep\run{\neg a}$ is the number of transitions in $\run$ that are
not $\tomachhole{a}$.

Well-Boundness and Renamings.
For the machines at work in this paper, the pre-terms in initial states shall be well-bound, that is, they have pairwise distinct bound names; for instance $\suba\mvar{\la\mvartwo\mvartwo}\evar\la\evartwo\evartwo$ is well-bound while $\suba\mvar{\la\mvartwo\mvartwo}\evar\la\mvartwo\mvartwo$ is not.
We shall also write $\rename{\tm}$ in a state $\state$ for a fresh well-bound renaming of $\tm$,
$\rename{\tm}$ is $\alpha$-equivalent to $\tm$, well-bound, and its bound variables
are fresh with respect to those in $\tm$ and in the other components of $\state$.

Implementation Theorem, Abstractly.
We now formally define the notion of a machine implementing a strategy. Since the good strategy is non-deterministically diamond but the machine that shall implement it is deterministic, we need a slightly unusual form of implementation theorem. As it is standard, machine transitions shall be mapped to equalities or steps on the calculus. For the other direction, however, we obtain only a big-step simulation, that is, if the strategy on the calculus terminates / diverges then the same does the machine, and with a related number of steps. But there is no step-by-step simulation of the calculus by the machine, because the non-deterministic strategy might do a step which is not the one done by the machine. Everything works fine because of the properties of diamond strategies. The general scheme is inspired by Accattoli et al.'s scheme for strong call-by-value <cit.>, but it is here simpler because of the absence of structural equivalence and implosive sharing.

It would also be possible to have a more symmetric setting by either designing a more complex diamond machine, as done by Accattoli and Barenbaum <cit.>, or by designing a deterministic variant of the good strategy. For the sake of simplicity, we prefer the asymmetric setting as to keep a simple machine and reuse the notion of good strategy from the literature.

A machine $\mach = (\States, \tomach, \compilrel\cdot\cdot, \decode\cdot)$ is a big-step implementation of a strategy $\tostrat$ on terms when, given a (proper and clash-free) term $\tm$:

* Runs to evaluations: for any $\mach$-run $\run: \compilrel\tm\statetwo \tomachine^* \state$ there is a $\tostrat$-evaluation $\deriv: \tm \tostrat^* \decode\state$ with $\sizepr\run = \size\deriv$.

* Normalizing evaluations to runs: if $\deriv \colon \tm \tostrat^* \tmtwo$ with $\tmtwo$  $\tostrat$-normal then there is a $\mach$-run $\run \colon \compilrel\tm\statetwo \tomachine^* \state$ such that $\decode\state = \tmtwo$ with $\sizepr\run = \size{\deriv}$.

* Diverging evaluations to runs: if $\compilrel\tm\state$ and $\tostrat$ diverges on $\tm$ then $\mach$ diverges on $\state$ doing infinitely many principal transitions.

Next, we isolate sufficient conditions for big-step implementations.

A lax implementation system is given by a machine $\mach = (\States, \tomach, \compilrel\cdot\cdot, \decode\cdot)$ and a strategy $\tostrat$ such that for every reachable state $\state$:$\label{def:implementation}$

*  Principal projection: if $\state \tomachpr \statetwo$ then $\decode\state \tostrat \decode\statetwo$;

*  Search transparency: if $\state \tomachsea \statetwo$ then $\decode\state  =\decode\statetwo$;

* 	Search terminates:  $\tomachsea$ terminates;

*  Halt: if $\state$ is final then $\decode\state$ is $\tostrat$-normal;

*  Diamond:  $\tostrat$ is diamond.

Let $\mach$ and  $\tostrat$ form a lax implementation system.
Then, $\mach$ is a big-step implementation of $\tostrat$.

Clash-Free and Proper States.

Note that we have not taken into account properness and clashes on states. One can say that a state $\state$ is proper (resp. clash-free) if its decoding $\decode\state$ is. In this way, these notions are trivially seen to be preserved by runs in a lax implementation system. Note, indeed, that transitions are mapped via decoding to either equalities or rewriting steps (and the proofs of these facts shall not need properness nor clash-freeness). Since states are initialized with  proper and clash-free  terms, and that these notions on terms are preserved by reduction (clash-freeness by definition, for properness see <cit.>), proper and clash-free states are preserved by transition. Therefore, we shall omit all considerations about properness and clashes for machines.

§ A MACHINE FOR THE CLOSED BASIC CASE

The Basic Abstract Machine (BAM).

Here, we study a  machine implementing basic evaluation on closed ESC terms. The aim is to give a gentle introduction to some machine concepts.

The basic abstract machine (BAM) is defined in BAM. States $\state = \twostate\ectx\tm$ are simply given by the active (pre-)term $\tm$ and a cut context $\ectx$ which is a list containing the cuts encountered so far by the search mechanism, playing the role of the (global) environment in machines such as Accattoli et al.'s Milner Abstract Machine <cit.>.

The initialization relation $\compilrel\tm{\twostate\ctxhole {\rename\tm}}$ pairs (proper and clash-free) terms $\tm$ with states composed by an empty cut context $\ctxhole$ and a well-bound renaming $\rename\tm$ of $\tm$. The BAM has six principal transitions, mimicking the ESC rewriting rules but for the weakening one (BAM never erases), plus one search transition $\tomachsea$, moving cuts from the term to the cut context.

The BAM looks at the topmost constructor of the active term and proceeds applying a transition belonging to one of the following three groups. If the constructor is:

* Search: a cut $\cuta\val\var$, the BAM adds it to the cut context, by applying $\tomachsea$;

* Computation: a subtraction $\suba\mvar\val\var$ or a dereliction $\dera\evar\var$, then the BAM looks for the associated cut in the cut context, it applies the corresponding cut elimination rule, and goes on to execute the modified active term, by applying $\tomachaxmtwo$, $\tomachlolli$, $\tomachaxetwo$, or $\tomachbang$;

* Terminal replacements: a variable $\mvar$ or $\evar$, the BAM looks for the associated cut in the cut context and it applies the matching replacement via $\tomachaxmone$ or $\tomachaxeone$. Note that terminal replacements can only be followed by further terminal replacements, hence the name.

Note that in transitions $\tomachbang$ and $\tomachaxeone$ some renaming takes place, using names that are fresh with respect to the whole state.
The domain $\domp\ectx$ of a cut context is defined as $\domp\ctxhole  \defeq  \emptyset$ and $\domp{\cuta\val\var\ectx} \defeq  \set\var\cup\domp\ectx$.

Let $\state=\twostate\ectx\tm$ be a BAM  reachable state.

Closure: $\fv\tm \subseteq \domp\ectx$ and if $\ectx=\ectxtwop{\cuta\val\var\ectxthree}$ then $\fv\val\subseteq \domp\ectxtwo$.

Well-bound: if $\la\var\tmtwo$, $\dera\evar\var\tmtwo$, $\suba\mvar\val\var\tmtwo$, or $\cuta\val\var\tmtwo$ occur in $\state$ and $\var$ has any other occurrence in $\state$ then it is a free variable of $\tm$, and if $\ectx=\ectxtwop{\cuta\val\var\ectxthree}$ and $\var$ has any other occurrence in $\state$ then it is a free variable in $\ectxthree$ or $\tm$.

Let $\state$ be a BAM  reachable state and $a\in\set{\axmone,\axmtwo, \axeone,\axetwo,\lolli,\bang}$.

* Search transparency: if $\state \tomachsea \statetwo$ then $\decode\state=\decode\statetwo$.

* Principal projection: if $\state \tomachhole{a} \statetwo$ then $\decode\state \Rew{\symfont{b}a} \decode\statetwo$.

* Search termination: transition $\tomachsea$ terminates.

* Halt: if $\state$ is final then $\state = \twostate\ectx\val$ with $\val$ not a variable, and $\decode\state$ is normal for non-erasing basic evaluation.

The BAM implements ESC non-erasing basic evaluation on closed terms.

§ SESAME

In this section, we extend the BAM as to perform the analogous of strong evaluation, that is, as to perform cut-elimination also inside values, and implement the good strategy. The obtained machine shall ignore garbage collection and—when it terminates—it returns a term that is cut-free up to garbage (cut-free-upto-gc). Garbage collection shall be addressed in gc-and-full.

The Strong Exponential Substitution Abstract Machine without Erasure (SESAME).

Pools and Jobs.
The Strong Exponential Substitution Abstract Machine without Erasure (SESAME), defined in SESAM, relies on a technique for strong evaluation recently introduced by Accattoli and Barenbaum <cit.>, which we are now going to explain.

When evaluation goes under binders, the closure invariant of the basic case (bam-invariants.1), for which free variables of the active term are associated to a cut in the cut context, is lost. Thus, when the active term is a subtraction $\suba\mvar\val\var\tm$ with no associated cut for $\mvar$,  the subtraction is kept, and the machine has to evaluate $\val$ and $\tm$. Now, the evaluations of $\val$ and $\tm$ cannot affect each other, they are independent, but one of the two sub-terms has to be evaluated first, say $\val$. Usually, strong machines (such as Crégut's <cit.>) would run through $\val$, and if such process does terminate, producing a value $\valtwo$, then they backtrack to the subtraction generating the fork by moving sequentially through $\valtwo$, and then start evaluate $\tm$.

Accattoli and Barenbaum's technique simply circumvents the sequential backtracking process by directly jumping back to the forking point. For that, the machine is equipped with a pool $\pool$ of jobs, each one paired to a unique name $\name$. In our example, there would be a job $\namctxholep\val\name$ for $\val$ and a job $\namctxholep\tm\nametwo$ for $\tm$. The idea is that when one job ends then the machine jumps to the next one, without moving through the structure of the finished job.

In <cit.>, the pool is any data structure satisfying a certain interface. The idea is that different data structures implementing the interface realize different job scheduling policies, compactly accounting for different strong strategies within the same framework. We here omit this abstract aspect and fix the pool to be the simplest such structure, namely a LIFO list of named jobs. In the $\lambda$-calculus, LIFO list pools implement leftmost evaluation <cit.>.

Another simplification with respect to <cit.> is that here jobs are simply named terms, while in <cit.> they are named pairs of a term and an applicative stack. The change induces a simpler notion of read back. This difference is not a design choice, it is simply induced by having a machine for sequent calculus terms (here) rather than natural deduction terms (in <cit.>).

A crucial point of SESAME is that job forking happens on subtractions only, that is, it does not happen on cuts $\cuta\val\var\tm$: the machine ignores $\val$ and goes straight to evaluate $\tm$. This happens in particular to prevent the breaking of the sub-term property.

We write $\fn\pool$ for the set of names associated to the jobs in $\pool$, that is, if $\pool = \namctxholep{\tm_1}{\name_1}\cons\ldots\cons \namctxholep{\tm_k}{\name_k}$ then $\fn\pool \defeq \set{\name_1,\ldots,\name_k}$.

Multi-Contexts and Approximants.
Another aspect of the technique in <cit.> is that the parts of the term that have been evaluated and that shall not be touched again by the machine—sometimes referred to as stable parts—are accumulated in the approximant $\appr$ (of the normal form), which is a multi-context (that is, a context with possibly many holes, possibly none). The idea is that the name $\name$ of a job $\namctxholep{\tm}{\name}$ in the pool is associated to a (unique) named hole $\namctxholep{\cdot}{\name}$ in $\appr$, and that, whenever a stable piece of term is produced by the job $\namctxholep{\tm}{\name}$, that piece is moved to $\namctxholep{\cdot}{\name}$ in $\appr$, incrementally building the normal form.

We follow this pattern from <cit.>, but our setting induces a few differences. Firstly, in <cit.> the machine has also a global environment, akin to the cut context of the BAM. Here, we include the environment/cut context into the approximant, having only one data structure. Thus, the approximant shall have cuts, but these cuts bind variables that have non-garbage occurrences only in the active term, i.e., only out of the approximant itself, where instead they have only garbage occurrences. At the end of a complete run, the approximant shall be normal for the non-erasing good strategy, i.e. it shall be cut-free up to garbage (cut-free-upto-gc).

Secondly, in <cit.> the machine is defined using approximants, while here we define it using the weaker notion of multi-contexts, and then prove invariants guaranteeing that the multi-contexts of reachable states are approximants.

A (named) multi-context $\namctx$ is an ESC term in which there might be
occurrences of holes $\namctxholea$ indexed with names, as follows:

$     \arraycolsep=2pt
<EMAIL_ADDRESS>l@{\hspace{.2cm}}|<EMAIL_ADDRESS>lllll}
\textsc{Names} & \name,\nametwo,\namethree, \name_1, \nametwo_2, \dots
\textsc{Value multi-ctxs} & \namvctx & \grameq & \namctxholea \mid \var \mid \la\var\namctx \mid \bang\namctx %& \ctx\rsub{}\mvar
\\
\textsc{Multi-ctxs} & \namctx & \grameq & \namvctx \mid \cuta\namvctx\var \namctx  \mid \suba\mvar\namvctx\var\namctx \mid \dera\evar\var\namctx
\end{array}$

The plugging $\namctxp{\namctxtwo}{\name}$ of $\namctxtwo$ on $\name$ in $\namctx$,
is the capture-allowing substitution of $\namctxholea$ by $\namctxtwo$ in $\namctx$. We write $\namctxp{\namctxtwo}{\mute}$ for when $\mute$ is an irrelevant name occurring exactly once in $\namctx$; this notation is meant to be used for decomposing a multi-context in two, as in $\namctx=\namctxtwop{\namctxthree}{\mute}$.
We write $\fn{\namctx}$ for the set of names that occur in $\namctx$. Out variables and out cuts extend to multi-contexts as expected.

The domain $\domp\namctx=\set{\var_1,\ldots,\var_n}$ of a multi-context $\namctx$ contains the variables on which there is a cut in $\namctx$ (the formal definition is in sesame, page def:namctx-domainAppendix E of the tech report <cit.>).

An approximant $\appr$ is a multi-context such that:

* Unique names: every name $\name\in\fn\appr$ has exactly one occurrence in $\appr$;

* Out cuts are hereditary garbage and hole-free: for every out cut $\cuta\namvctx\var\namctxtwo$ in $\appr$, if $\var\in\fv\namctxtwo$ then $\var$ occurs only inside cut values, i.e. $\var\notin\ov\namctxtwo$, and $\namvctx$ is a term.

Note that a multi-context $\namctx$ without holes is simply a term, thus the defined notion of plugging subsumes the plugging $\namctxp{\tm}{\name}$ of terms in multi-contexts.

The principal transition of SESAME are as for the BAM up to the generalization of the cut context $\ectx$ to a multi-context $\namctx$. Note the mute name $\mute$ for decomposing the multi-context in the transitions. Clearly, the name $\mute$ on the LHS and the RHS of each transition is the same. SESAME has a search transition for each constructor of the calculus. Note that transitions $\tomachaxmone$ and $\tomachaxeone$ are no longer terminal, because now they might be followed by a search transition, after which the run might jump to a different job.

Read Back.
The read back $\decode\state$ of a state $\state = \twostate\namctx\pool$ is defined in SESAM and simply plugs each job $\namctxholep\tm\name$ of the pool $\pool$ in the hole of name $\name$ of the multi context $\namctx$. We also write $\namctx\ctxholep\pool$ for $\decode\state$. Since the holes of $\namctx$ are all independent and jobs contains terms (with no holes), we have that $\namctx\ctxholep\pool = \namctx\ctxholep\pooltwo$ for any pool $\pooltwo$ obtained by permuting the elements of $\pool$.

Example of SESAME run.
As an example, we show a SESAME run on the following term:

\tm &\defeq& {\cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}\dera{\evar_1}{\mvar_2}\dera{\evar_1}{\mvar_3}\suba{\mvar_2}{\mvar_3}{\mvar_4}{\mvar_4}}
\end{array}$

that just applies an identity function to itself, by making two copies of $\bang{\la{\mvar_1}{\mvar_1}}$ and applying one to the other via the subtraction. To fit it into the margins, we use the abbreviation $\tmtwo \defeq \suba{\mvar_2}{\mvar_3}{\mvar_4}{\mvar_4}$.

\begin{array}{l|l|l}
\SetCell[c=1]{c} \textsc{Tr.} & \SetCell[c=1]{c} \textsc{MCtx} & \SetCell[c=1]{c} \textsc{Pool}
\\\hline
& \nctxhole\name & \nctxholep{\tm}\name \,\cons\, \emptylist \\
\tomachseaone & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}\nctxhole\name & \nctxholep{\dera{\evar_1}{\mvar_2}\dera{\evar_1}{\mvar_3}\tmtwo}\name \,\cons\, \emptylist \\
\tomachbang   &\cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}
\nctxhole\name & \nctxholep{\cuta{\la{\mvar_5}{\mvar_5}}{\mvar_2}\dera{\evar_1}{\mvar_3}\tmtwo}\name \,\cons\, \emptylist \\
\tomachseaone & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}
\cuta{\la{\mvar_5}{\mvar_5}}{\mvar_2}\nctxhole\name & \nctxholep{\dera{\evar_1}{\mvar_3}\tmtwo}\name \,\cons\, \emptylist \\
\tomachbang   & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}
\cuta{\la{\mvar_5}{\mvar_5}}{\mvar_2}\nctxhole\name & \nctxholep{\cuta{\la{\mvar_6}{\mvar_6}}{\mvar_3}\tmtwo}\name \,\cons\, \emptylist \\
\tomachseaone & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}
\cuta{\la{\mvar_5}{\mvar_5}}{\mvar_2}\cuta{\la{\mvar_6}{\mvar_6}}{\mvar_3}\nctxhole\name & \nctxholep{\tmtwo}\name \,\cons\, \emptylist \\
\tomachlolli   & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}
\cuta{\la{\mvar_6}{\mvar_6}}{\mvar_3}\nctxhole\name & \nctxholep{\cuta{{\mvar_3}}{\mvar_5}\cuta{{\mvar_5}}{\mvar_4}{\mvar_4}}\name \,\cons\, \emptylist \\
\tomachseaone & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}
\cuta{\la{\mvar_6}{\mvar_6}}{\mvar_3}\cuta{{\mvar_3}}{\mvar_5}\nctxhole\name & \nctxholep{\cuta{{\mvar_5}}{\mvar_4}{\mvar_4}}\name \,\cons\, \emptylist \\
\tomachseaone & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}
\cuta{\la{\mvar_6}{\mvar_6}}{\mvar_3}\cuta{{\mvar_3}}{\mvar_5}\cuta{{\mvar_5}}{\mvar_4}\nctxhole\name & \nctxholep{{\mvar_4}}\name \,\cons\, \emptylist \\
\tomachaxmone & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}\cuta{\la{\mvar_6}{\mvar_6}}{\mvar_3}\cuta{{\mvar_3}}{\mvar_5}\nctxhole\name & \nctxholep{{\mvar_5}}\name \,\cons\, \emptylist \\
\tomachaxmone & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}\cuta{\la{\mvar_6}{\mvar_6}}{\mvar_3}\nctxhole\name & \nctxholep{{\mvar_3}}\name \,\cons\, \emptylist \\
\tomachaxmone & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}\nctxhole\name & \nctxholep{\la{\mvar_6}{\mvar_6}}\name \,\cons\, \emptylist \\
\tomachseafour & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}\la{\mvar_6}\nctxhole\name & \nctxholep{{\mvar_6}}\name \,\cons\, \emptylist \\
\tomachseasix & \cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}\la{\mvar_6}{\mvar_6} & \emptylist \\
\end{array}

Note that in the last state the cut $\cuta{\bang{\la{\mvar_1}{\mvar_1}}}{\evar_1}$ is garbage but it is not removed. This shall be taken care of by an extra garbage collection phase described in gc-and-full.

§ ANALYSIS OF SESAME

As for the BAM, we prove some invariants. The first one states that the multi context of a reachable state is an approximant. A second invariant states that names in the multi context are exactly those in the pool, where they have exactly one occurrence each. Then, we need a well-bound invariant about binders, relying on a technical definition in sesame, page def:well-bound-stateAppendix E of the tech report <cit.>, along the lines of the invariant of the BAM. Lastly, the contextual decoding invariant, the most important and sophisticated invariant, states that a reachable state less the first job reads back to a good context. For the invariant to hold, the statement has to be generalized in a technical way, analogously to similar invariants in <cit.>.

Let $\state=\twostate\namctx\pool$ be a SESAME state reachable from a well-bound initial term $\tm_0$.

* Approximant: $\namctx$ is an approximant.

* Names: jobs in the pool $\pool$ have pairwise distinct names, and $\fn\namctx=\fn\pool$.

Well-bound: $\state$ is a well-bound state.

* Contextual decoding: if $\pool=\namctxholep{\tm_1}{\name_1}\cons\ldots\cons\namctxholep{\tm_k}{\name_k}$ has length $k\geq1$ then:

\defeq
\namctx\namctxholep{\tmtwo_1}{\name_1}\ldots\namctxholep{\tmtwo_{i-1}}{\name_{i-1}}\namctxholep{\ctxhole}{\name_{i}}\namctxholep{\tmtwo_{i+1}}{\name_{i+1}}\ldots\namctxholep{\tmtwo_k}{\name_k}$

is a good context for $i\in\set{1,\ldots,k}$ and any terms $\tmtwo_1,\ldots,\tmtwo_{i-1},\tmtwo_{i+1},\ldots,\tmtwo_k$ such that $\namctx^\state_{\tmtwo_1,\ldots,\tmtwo_{i-1}|\name_i|\tmtwo_{i+1},\ldots,\tmtwo_k}$ is a term.

Implementation Theorem.
The well-bound and contextual decoding invariants are used to prove principal projection. The approximant and names invariants are used to prove the halt property. Search transparency and termination are straightforward. Then we apply the abstract implementation theorem (abs-impl), and obtain the implementation theorem.

Let $a\in\set{\axmone,\axmtwo, \axeone,\axetwo,\lolli,\bang}$.

* Search transparency: if $\state \tomachsea \statetwo$ then $\decode\state=\decode\statetwo$.

* Principal projection: if $\state \tomachhole{a} \statetwo$ then $\decode\state \togp{a} \decode\statetwo$.

* Search termination: transition $\tomachsea$ terminates.

* Halt: if $\state$ is final then $\state=\twostate\tm\emptylist$ and $\decode\state=\tm$ is cut-free up to garbage.

SESAME is a big-step implementation of the non-erasing good strategy $\tognotw$ of ESC.

§.§ Complexity Analysis

The complexity analysis of SESAME amounts to bound the cost of implementing a run $\run:\compilrel\tm\state \tosesame^*\statetwo$ on random access machines (RAMs) as a function of two parameters: the number $\sizepr\run$ of principal transitions in $\run$ (which are in bijection with the number of $\tognotw$ steps) and the size $\size\tm$ of the initial term/state $\tm$/$\state$.

Sub-Term Property.
The analysis relies on the sub-term property, ensuring that the duplicating principal transitions $\tomachbang$ and $\tomachaxeone$ manipulate only sub-terms of the initial term. Therefore, the cost of duplications is connected to size of the initial term. The property for SESAME can be inferred by the one for the good strategy, but we prefer to give a direct simple proof. The statement of the related invariant is about cut values, not duplications, but note that such values are the only terms duplicated by SESAME.

Let $\run \colon \compilrel\tm\state \tosesame^* \twostate\namctx\pool$ be a SESAME run.

* Invariant: if $\val$ is a cut value in $\namctx$ or a value in $\pool$ then $\size\val \leq\size\tm$.

* Property: if $\val$ is a value duplicated along $\run$ (by $\tomachbang$ or $\tomachaxeone$) then  $\size\val \leq\size\tm$.

Since search transitions decrease the number of term constructors in the pool, which is only increased by principal transitions and of a quantity bounded by $\size\tm$ (by the sub-term invariant), we obtain the following bound.

Let $\run \colon \compilrel{\tm}\state \tosesame^* \statetwo$ be a SESAME run. Then $\sizesea\run\leq \size\tm\cdot(\sizepr\run+1)$.

Cost of Single Transitions.
For bounding the total cost, we need to make some hypotheses on how SESAME is going to be itself implemented on RAMs:

* Variable occurrences, binders, and cuts:  a variable is a memory location, a variable occurrence is a reference to it, and a cut $\cuta\val\var$ is the fact that the location associated with $\var$ contains $\val$;

* Random access to variables: the cuts in $\namctx$ can be accessed in $\bigo(1)$ by just following the reference given by the variable occurrence, with no need to search through $\namctx$;

* Named holes and jobs: a named hole $\namctxholea$ is again a memory location $\name$, and a job $\namctxholep\tm\name$ is a pointer to $\name$ and expresses the fact that location $\name$ contains $\tm$;

* Sequences of left rules: cuts have a back pointer to the constructors before them (for instance in $\dera\evar\mvar\cuta\val\var\suba\mvar\valtwo\vartwo\tm$ the cut $\cuta\val\var$ has a pointer to $\dera\evar\mvar$) so that the removal of a cut from the multi context $\namctx$ of a state—needed for the multiplicative transitions $\tomachaxmone$, $\tomachaxmtwo$, and $\tomachlolli$—can be performed in $\bigo(1)$.

As it is standard for time analyses, we also assume that pointers can be managed in $\bigo(1)$. These hypotheses mimic similar ones behind machines for $\lambda$-calculi, which are shown to be implementable in OCaml by Accattoli and Barras <cit.> and Accattoli et al. <cit.>, and are followed by the OCaml implementation outlines in ocaml. They allow us to consider search transitions as having constant cost, and principal transitions as having cost bound by the initial term, by the sub-term property.

Let $\run \colon \compilrel{\tm}\state \tosesame^* \statetwo$ be a SESAME run. Search (resp. principal) transitions of $\run$ are implementable in $\bigo(1)$ (resp. $\bigo(\size\tm)$).

Summing Up.
By putting together the bounds on the number of search transitions with the cost of single transitions we obtain the complexity of SESAME.

Let   $\run \colon \compilrel{\tm}\state \tosesame^* \statetwo$ be a SESAME run. Then $\run$ is implementable on RAMs in $\bigo\left(\size\tm\cdot(\sizepr\run+1)\right)$.

§ FINAL GARBAGE COLLECTION AND FULL CUT ELIMINATION

By the halt property (sesam-properties.4), SESAME stops on final state $\state=\twostate\appr\emptylist$ where $\appr$ is a (pre-)term $\tm$ that is cut-free up to garbage. The final garbage collection process turning $\tm$ into a cut-free proof term $\gcdec\tm$ is formalized as the following function:

\arraycolsep=2pt\begin{array}{rll<EMAIL_ADDRESS>rll<EMAIL_ADDRESS>rll}
\multicolumn{9}{c}{\textsc{Final garbage Collection}}
\\[4pt]
\gcdec\var &\defeq& \var
\gcdec{\la\var\tm} &\defeq& \la\var\gcdec{\tm}
\gcdec{\bang\tm} &\defeq& \bang\gcdec{\tm}
\\
\gcdec{\cuta\val\var\tm} &\defeq& \gcdec{\tm}
\gcdec{\suba\mvar\val\var\tm} &\defeq& \suba\mvar{\gcdec\val}\var\gcdec{\tm}
\gcdec{\dera\evar\var\tm} &\defeq& \dera\evar\var\gcdec{\tm}
\end{array}$

Clearly, $\gcdec\tm$ is cut-free. The following proposition states the qualitative and quantitative properties of garbage collection. Its first point uses the lemma before it, while the second point rests on the SESAME bi-linear bound.

Let $\tm$ be a term that is cut-free up to garbage but not cut-free.
Then in $\tm$ there is at least an out cut that is a $\togp\wsym$-redex.

Let $\run: \compilrel\tm\state \tosesame^* \twostate\tmtwo\emptylist$ a SESAME run ending on a final state.

* Good weakening steps simulate GC: $\tmtwo \togp\wsym^k \gcdec\tmtwo$ where $k$ is the number of out cuts in $\tmtwo$;

* GC is bi-linear: the final garbage collection function $\tmtwo \mapsto \gcdec\tmtwo$ can be implemented on RAMs in $ \bigo(\size\tm\cdot(\sizepr\run+1))$.

By simulating good cut-elimination via the SESAME followed by final garbage collection, we obtain our main result, which—beyond the bi-linear bound—is a further slight (but sort of obvious) refinement of Accattoli's result, as it allows one to count only non-erasing good steps, rather than general good steps.

Let   $\deriv:\tm \tog^* \tmtwo$ be a good evaluation sequence with $\tmtwo$ cut-free. Then $\tmtwo$ is computable from $\tm$ on RAMs in $\bigo\left(\size\tm\cdot(\sizep\deriv{\neg\wsym}+1)\right)$.

If $\deriv:\tm \tog^* \tmtwo$ with $\tmtwo$ cut-free then $\tognotw$ terminates, by the uniform normalization corollary of the diamond property for $\tog$ (see the end of strategy). Then there is an evaluation $\derivtwo:\tm \tognotw^* \tmtwo'$ with $\tmtwo'$ cut-free up to garbage. Since SESAME is a big-step implementation of $\tognotw$ (sesame-is-good), we obtain a SESAME run $\run :\compilrel\tm\state \tosesame^*\statetwo$ with $\decode\statetwo=\tmtwo'$, of cost $\bigo\left(\size\tm\cdot(\sizepr\run+1)\right)=\bigo\left(\size\tm\cdot(\size{\derivtwo}+1)\right)$. By the halt property of SESAME and cut-freeness up to garbage of SESAME, we obtain that $\statetwo$ is final, that is, $\statetwo=\twostate\tmthree\emptylist$ with $\tmthree =_\alpha \tmtwo'$.

Since good weakening steps simulate GC (gc-properties.1), we obtain $\derivthree: \tmthree \togp\wsym^* \gcdec{\tmtwo'}$ with $\gcdec{\tmtwo'}$ cut-free. Concatenating $\derivtwo$ and $\derivthree$ we obtain a good and normalizing evaluation sequence $\derivfour:\tm \tognotw^*\togp\wsym^*\gcdec{\tmtwo'}$. The diamond property of the good strategy (sub-term-prop.2) implies confluence and length invariance of $\tog$ (see the end of strategy), that is, we obtain $\tmtwo = \gcdec{\tmtwo'}$ and $\size\deriv=\size\derivfour$. Since computing GC is bi-linear (gc-properties.1), and precisely costs again $\bigo\left(\size\tm\cdot(\sizepr\run+1)\right)=\bigo\left(\size\tm\cdot(\size{\derivtwo}+1)\right)$, we obtain that the total cost of SESAME followed by GC is $2\cdot\bigo\left(\size\tm\cdot(\size{\derivtwo}+1)\right)= \bigo\left(\size\tm\cdot(\size{\derivtwo}+1)\right)$.

Lastly, the diamond property of the good strategy (sub-term-prop.2) as stated in <cit.> does not give information about the kinds of steps, but by looking at its proof it is easily seen that diamond diagrams preserve the kind of steps. Therefore, not only we have $\size\deriv=\size\derivfour$, but also $\sizep\deriv{\neg\wsym}=\sizep\derivfour{\neg\wsym}$. Finally, note that $\sizep\derivfour{\neg\wsym}=\size{\derivtwo}$, so the cost actually is $\bigo\left(\size\tm\cdot(\sizep\deriv{\neg\wsym}+1)\right)$.

§ IMPLEMENTATION IN OCAML

An implementation in OCaml can be found on GitHub at
<https://github.com/sacerdot/sesame/>. All the datatypes and functions
of the implementation are documented at <https://sacerdot.github.io/sesame>.

Aim and Design.

The implementation is provided to support evidence for the cost of transitions claimed by cost-single-trans. Moreover, it
allows one to easily study the computational behaviour of family of terms by observing
their evaluation.

The implementation has not been heavily optimized, in order to keep the code readable and
close to the pen-and-paper presentation. Nevertheless, the employed data structures
are reasonably close to those of an optimized implementation. Advanced recent OCaml
features, like Generalized Algebraic Data Types, could have been used to
statically enforce more invariants. We sticked instead to a simpler subset of OCaml,
to make the code readable to non experts of the language. As a consequence, in several
places there are assertions to abort the program in case the invariants
are violated (possible only in case of bugs).

The implementation consists of a Read-Eval-Print-Loop (REPL) that asks the user
to enter an IMELL term to be reduced, in ESC syntax. The accepted BNF is printed by
the executable before starting the REPL. The term is first checked to be proper,
then its strong normal form up to garbage is computed by the SESAME machine and
finally garbage is removed. All intermediate machine steps are shown.

Before starting the REPL, a few test terms are reduced and printed (among which the example at the end of sesame), to check the
machine functionalities and as examples of the input syntax. In particular, the last tests are terms from the exploding family discussed in the next section.

Data Structures.

Terms are encoded at runtime as term graphs, which are Direct Acyclic Graphs (DAG)
augmented with a few back edges. Nodes in the graph are given by constructors
of Algebraic Data Types whose arguments are mutable, to imperatively
change the graph during reduction. All type declarations are given in the
file. The data structures used in the implementation are described in ocamlAppendix H of the tech report <cit.>.

Machine Runs: Auxiliary Functions and Their Complexity.

The code that implements the runs of SESAME to normal form and the final garbage collection
process can be found in , which is independent from all the remaining
files but . Both files together amount to 412 lines of
commented OCaml code.

A quick inspection of the code in  shows only a few non-trivial
functions, all the others being constant time:

*  that copies the
DAG in input while visiting it.

A $\bigo(1)$ fresh name generator is used
to assign a new  value to copies of variables.

*  and , used respectively in the
$\bang$ and $\lolli$ transitions, that take the body of a promotion/abstraction,
traverse it to split it into a left context and a value, and build a new term
by glueing together the obtained left context, a new cut that uses the value, and
a remaining term. The two functions differ only in the fact that  also
copies ($\alpha$-renames) the term in input, calling the  functions
on the sub-terms, while  consumes the given term.

* , the SESAME main loop, that runs until the pool is empty and
a normal form is therefore reached, or it diverges otherwise.

*  that traverse in linear time the input to remove
all garbage cuts from a normal form.

Linearity for all the previous functions but  is easily established
observing that the functions are based on visits of DAGs that never visit a node twice. In particular, the functions of Point 2 are linear in the size of the given term, which, by the
sub-term invariant, is a (copy of a) sub-term of the initial term.

The only major source of technicalities—which however do not affect the complexity—is the fact that multiplicative transitions remove the acting cut from the multi context. For example, consider a multiplicative step $\dera\evar\evartwo \cuta\val\mvar \cuta\valtwo\vartwo \tm \to \dera\evar\evartwo  \cuta\valtwo\vartwo \tm'$ involving the cut on $\mvar$. To implement it, beyond manipulating $\val$, $\tm$, and $\tm'$, one also has to connect $\dera\evar\evartwo$ and $\cuta\valtwo\vartwo$. For that, cuts have a back-pointer to the preceding constructor (as mentioned at Point 4, labeled sequences of left rule, before cost-single-trans), which induces inelegant imperative manipulations of the term graph,
in particular in the copy function. The back-pointer on $\cuta\val\mvar$ is used to retrieve the dereliction $\dera\evar\evartwo$ from $\cuta\val\mvar$, while making the new connection of $\dera\evar\evartwo$ and $\cuta\valtwo\vartwo$ requires changing two pointers: the one from the dereliction to its body, which has to target $\cuta\valtwo\vartwo$, plus the back-pointer from $\cuta\valtwo\vartwo$, which now has to target $\dera\evar\evartwo$.

The general scheme for addressing this issue is to
augment the input $\tm$ of functions that take a term with the pointer to the
parent node of $\tm$, in order to be able to reassign the back-pointer when $\tm$ is
a cut.

Parsing, Pretty Printing, and Check for Properness.

We have not attempted to achieve the best asymptotic costs for these functionalities
since they are not relevant for the paper and since in practice we are manipulating
small terms in input. To keep the code reproducible in the long term, we have not
used any external library or tool for parsing and pretty-printing. The printed version of the example run at the end of sesame is shown in exampleAppendix I of the tech report <cit.>.

§ WHAT'S NEXT: AN INTERESTING FAMILY OF TERMS

We here hint at what we consider the most interesting future work, already mentioned by Accattoli in the conclusions of <cit.>. The difference is that here we provide a family of terms showing that such a future work is challenging.

The Question.
One $\beta$-step of the $\l$-calculus is simulated in IMELL by one multiplicative step (actually a $\tololli$ step) followed by possibly many exponential steps. Since for many strategies the number of $\beta$-steps is a polynomial cost model, it means that one can count only the number of multiplicative (or even $\tololli$) steps, that is, one can count zero for exponential steps. Such a surprising fact is established easily in the case of weak evaluation with closed terms (roughly, it can be proved via standard abstract machines), while for strong evaluation it requires a sophisticated additional technique called useful sharing <cit.>. A question naturally arises: is the number of ESC multiplicative/$\tololli$ good steps a polynomial time cost model as well? This question—left to future work—is far from obvious. In the $\l$-calculus, there is a strong, hardcoded correlation between multiplicatives and exponentials, not present in IMELL. In the standard call-by-name/value encodings of $\l$-calculus in IMELL, indeed, multiplicatives and exponentials connectives rigidly alternate, while IMELL also has consecutive exponentials, as in $\bang\bang\form$, enabling wilder exponential behaviour. A hint that question might have a positive answer is given by the strong normalization of untyped exponentials  in ESC/IMELL shown in <cit.> (while they are not SN in MELL, see <cit.>).

The Question is Challenging.
We here show that the question mentioned above is challenging, and—surprisingly—it is already challenging in the apparently simple setting of basic evaluation with closed terms, that is the ESC analogous of weak evaluation for the $\l$-calculus, for which instead the question has an easy answer. The challenging aspect is here shown by building a family of ESC terms $\sigma_n$ having size linear in $n$, whose evaluation is basic and made out of exponential steps only, and of a number of steps that is exponential in $n$. This is impossible in the $\l$-calculus, and it is crucially related to iterated exponential terms such as $\bang\bang\tm$. Since the evaluation of $\sigma_n$ uses 0 multiplicative steps, it suggests that the number of multiplicative steps is not a polynomial cost model. More precisely, it shows that a smart additional mechanism—akin to useful sharing—is needed in order to circumvent the exponential number of exponential steps. Useful sharing as it appears in the literature, however, cannot be the answer, since useful sharing addresses exponential inefficiencies that are induced by strong evaluation, which is an orthogonal issue.

The Exponential Exploding Family.
The family is built in three steps.

* For $k \geq 1$, define $\pi_k := \overbrace{\dera\evartwo\_ \ldots \dera\evartwo\_ \dera\evartwo\evar}^{k}\evar$, where $\_$ is an exponential variable with no occurrences, and whose name is irrelevant. These terms reduce to (the cut-free term) $\pi_{k\cdot h}$ via  exponential basic evaluation, that is, $\cuta{\bang{\pi_k}}\evartwo{\pi_h} \toe^* \pi_{k\cdot h}$.

* Define $\delta_n := \overbrace{\cuta{\bang{\pi_2}}\evartwo \ldots \cuta{\bang{\pi_2}}\evartwo}^{n-1}\pi_2$, and note that, by Point 1, one has $\delta_n \toe^* \pi_{2^n}$.

* Finally, define the exponential exploding family as $\sigma_n \defeq \cuta{\bang{\bang{\la\mvar\mvar}}}\evartwo\delta_n$. By Point 2, we have $\sigma_n \toe^* \cuta{\bang{\bang{\la\mvar\mvar}}}\evartwo \pi_{2^n}$. Then note that $\cuta{\bang{\bang{\la\mvar\mvar}}}\evartwo \pi_{2^n} \toe^{\Omega(2^n)} \bang{\la\mvar\mvar}$.

Summing up, $\sigma_n$ is an example of term of size $\bigo(n)$ that reduces in $\Omega(2^n)$ exponential steps and 0 multiplicative steps to a cut-free proof using only basic evaluation. As mentioned in the previous section, the OCaml implementation starts by running some tests, including examples of the three points above, respectively for $k=3,h=4$, for $n=3$, and for $n=3$.

§ CONCLUSIONS

§ PROOF APPENDIX

§ PROOFS AND DEFINITIONS OMITTED FROM ESC (EXPONENTIAL SUBSTITUTION CALCULUS)

Proper terms are defined by induction on $\tm$ as follows:

* Variables: $\mvar$ and $\evar$ are proper.

* Implication: $\la\var\tm$ is proper if $\tm$ is proper and if $\var$ is a multiplicative variable then $\var \in\mfv\tm$.

* Subtraction: $\suba\mvar\val\var \tm$ is proper if $\tm$ is proper, $\val$ is proper, $\mfv\val \cap (\mfv\tm\setminus\set{\var}) = \emptyset$, $\mvar \notin\mfv\tm$, and if $\var$ is a multiplicative variable then $\var \in\mfv\tm$.

* Bang: $\bang\tm$ is proper if $\tm$ is proper and $\mfv\tm = \emptyset$.

* Dereliction: $\dera\evar\var \tm$ is proper if $\tm$ is proper and if $\var$ is a multiplicative variable then $\var \in\mfv\tm$.

* Cut: $\cuta\val\var\tm$ is proper if $\tm$ is proper, $\val$ is proper, $\mfv\val \cap (\mfv\tm\setminus\set\var) = \emptyset$, and if $\var$ is a multiplicative variable then $\var \in\mfv\tm$.

Cases of $\tm$:l:basic-harmony

* Abstraction, promotion: $\tm$ is an answer and has no basic redexes.

* Par, subtraction, dereliction, variable: $\tm$ is open, against hypotheses.

* Cut: then $\tm = \cuta\valtwo\var\lctxp\val$. Two cases:

* $\lctx$ is a cut context or empty. Two cases:

* $\val$ is a variable. By closure, $\val = \var$ or it is captured by $\lctx$. In both cases $\tm$ has a basic non-erasing redex, and it is not an answer because $\var$ is captured.

* $\val$ is not a variable. Then $\tm$ is an answer and it has no non-erasing basic redex.

* $\lctx$ is non-empty and not a cut context. Then $\tm$ is not an answer, and $\lctx = \ectxp{\lctxtwo}$ with $\ectx$ cut context and $\lctxtwo$ starting with a par, a subtraction, or a dereliction on a variable $\varthree$. Since $\tm$ is closed, $\varthree$ is bound in $\cuta\valtwo\var\ectx$, and so there is a basic non-erasing redex.

§ ADDING TENSORS

The presentation of ESC in <cit.> includes two constructors $\para\mvar\var\vartwo \tm$  and $\pair\tm\tmtwo$ corresponding to the left and right sequent calculus rules of tensor. The rules decorated with proof terms follow (as explained in the previous section of the Appendix, $\multiForm\#\multiFormtwo$ means that the domains of $\multiForm$ and $\multiFormtwo$ are disjoint):

$  \multiForm, \var\hastype\form, \vartwo\hastype\formtwo \vdash \tm\hastype\formthree$
$\mvar$ fresh
$ \tensLeftRule $
$  \multiForm, \mvar\hastype\form \tens \formtwo \vdash \para\mvar\var\vartwo \tm \hastype \formthree$

$  \multiForm\vdash \tm\hastype\form$
$  \multiFormtwo\vdash \tmtwo\hastype\formtwo$
$ \tensRightRule $
$  \multiForm, \multiFormtwo\vdash \pair\tm\tmtwo \hastype\form\otimes \formtwo$

The associated rewriting rule is:

\cuta{\pair\tmtwo\tmthree}\mvar \ctxp{\para\mvar\var\vartwo\tm}
& \rtotens &
\ctxp{\lctxp{\cuta\val\var \lctxtwop{\cuta\valtwo\vartwo \tm}}}
\\[4pt]&& \mbox{with }\tmtwo = \lctxp{\val}\mbox{ and }\tmthree = \lctxtwop{\valtwo}
\end{array}$

SESAME then needs to be extended with the following transitions:

\cline{1-5}
\SetCell[c=1]{c} \textsc{MCtx} & \SetCell[c=1]{c} \textsc{Pool} &\textsc{Tran.}& \SetCell[c=1]{c} \textsc{MCtx} & \SetCell[c=1]{c}\textsc{Pool}
\\\cline{1-5}
\namctx \mbox{ with }\mvar\notin\domp\namctx & \nctxholep{\para\mvar\var\vartwo \tm}\name \cons \pool
\namctx  \nctxholep{\para\mvar\var\vartwo \nctxhole\name}\name &\nctxholep{\tm}\name \cons \pool
\\[2pt]
\namctx & \nctxholep{\pair\tm\tmtwo}\name \cons \pool
\namctx  \namctxholep{\pair{\nctxhole\name}{\nctxhole\nametwo}}\name &\nctxholep{\tm}\name \cons \nctxholep{\tmtwo}\nametwo  \cons \pool &*
\\[4pt]
\cline[dashed]{1-5}
\namctxp{\cuta\mvartwo\mvar\namctxtwo}\mute & \nctxholep{\para\mvar\var\vartwo\tm}\name \cons \pool
\namctxp\namctxtwo\mute & \nctxholep{\para\mvartwo\var\vartwo\tm}\name \cons \pool
\\[2pt]
\namctxp{\cuta{\pair\tmtwo\tmthree}\mvar\namctxtwo}\mute & \nctxholep{\para\mvar\var\vartwo\tm}\name \cons \pool
\namctxp\namctxtwo\mute &\nctxholep{\lctxp{\cuta\val\var \lctxtwop{\cuta\valtwo\vartwo \tm}}}\name \cons \pool
\\\cline{1-5}
\end{tblr}$

[c=1]l* $\nametwo$ is fresh.    # with $\tmtwo = \lctxp{\val}$ and $\tmthree = \lctxtwop{\valtwo}$.

It is easily seen that, with the assumption about how SESAME is implemented that we made in analysis, these transitions can be implemented in constant time and they do not break the sub-term invariant / property. Everything smoothly adapts as to cover the extension with tensors.

§ PROOFS FROM PREL-ABS-MACH (PRELIMINARIES ON ABSTRACT MACHINES)

Let $\mach$ and $\tostrat$ be an asymmetric implementation system.
For any state $\state$ of $\mach$, if $\decode\state \tostrat \tmtwo$ then there is a state $\statetwo$ of $\mach$
such that $\state \tomachsea^*\tomachpr \statetwo$.

For any state $\state$ of $\mach$, let $\nfsea{\state}$ be a normal form of $\state$ with respect to $\tomachsea$: such a state exists because search transitions
Since $\tomachsea$ is mapped on identities (by search transparency), one has $\decode{\nfsea{\state}} =
\decode\state$.
As $\decode\state$ is not $\tostrat$-normal by hypothesis, the halt property entails that
$\nfsea{\state}$ is not final, therefore $\state \tomachsea^* \nfsea{\state} \tomachpr \statetwo$ for some state $\statetwo$.

* Runs to evaluations: by induction on the length of the run. It follows easily from the properties of principal
projection and search transparency of lax implementation systems.

* Normalizing evaluations to runs: the statement that we need to prove is:

if $\deriv \colon \tm \tostrat^* \tmtwo$ with $\tmtwo$  $\tostrat$-normal then there is a $\mach$-run $\run \colon \compilrel\tm\statetwo \tomachine^* \state$ with $\state$ final such that $\decode\state = \tmtwo$ with $\sizepr\run = \size{\deriv}$.

We prove a more general statement where we replace the initial term $\tm$ and the initial state $\compilrel\tm\statetwo$ with
a general state $\statetwo$ and use its decoding $\decode\statetwo$ for $\tm$:

if $\deriv:\decode\statetwo \tostrat^* \tmtwo$ with $\tmtwo$
$\tostrat$-normal then there is a $\mach$-run $\run: \statetwo \tomach^* \state$ with $\state$ final such that
$\decode\state = \tmtwo$ with $\sizepr\run = \size\deriv$.

Then if we instantiate this more general statement on
initial states we obtain the official statement, because by the initialization constraint of
the machine if $\compilrel\tm\statetwo$ then $\decode{\statetwo} =_\alpha \tm$.

The proof of the generalized statement is by induction on $\size\deriv$. If $\size\deriv=0$ then consider
$\nfsea{\statetwo}$, that by search transparency satisfies $\decode{\nfsea{\statetwo}} =
\decode{\statetwo}$. Now, if $\nfsea{\statetwo}$ can do a principal transition then from $\decode{\statetwo}$ it is possible to do a $\tostrat$ step by  principal projection, which is absurd, because $\size\deriv=0$ and by the diamond property all evaluations sequences from a term have the same number and kind of steps. Then, $\nfsea{\statetwo}$ is a final state and there is a run $\run: \statetwo \tomachsea^*\nfsea{\statetwo}$ such
that $\sizepr\run= 0$. The statement holds with $\state \defeq \nfsea{\statetwo}$.

If $\size\deriv=k>0$ then $\decode\statetwo \tostrat \tmthree \tostrat^{k-1} \tmtwo$ for some
$\tmthree$. By the one-step transfer lemma (one-step-transfer), we obtain $\statetwo\tomachsea^*\tomachpr
\statethree$ for some $\statethree$. By search transparency and principal projection, we obtain
$\deriv':\decode\statetwo\tostrat\decode\statethree$. If $\tmthree = \decode\statethree$ then we have and evaluation $\derivtwo:\decode\statethree \tostrat^{k-1} \tmtwo$. If $\tmthree \neq \decode\statethree$, the diamond property of $\tostrat$ gives anyway an
evaluation $\derivtwo:\decode\statethree \tostrat^{k-1} \tmtwo$. We can then apply the , obtaining a run $\runtwo:\statethree \tomach^* \state$ with $\state$
final and such that $\decode{\state} = \tmtwo$, and with $\sizepr\runtwo = k-1$. Note that
the run $\run:\statetwo \tomachsea^*\tomachpr \statethree\tomach^* \state$ obtained by prefixing $\runtwo$ with the run given by the one-step transfer lemma satisfies the statement because $\sizepr\run = \sizepr\runtwo +1 = \size\derivtwo +1 = \size\deriv$.

* Diverging evaluations to runs: suppose that $\tostrat$ diverges on $\tm$ but $\mach$ terminates, that
is, that there is a run $\run:\compilrel\tm\statetwo \tomach^* \state$ with $\state$ final. Then the projection
$\decode\run:\tm \tostrat^*  \decode\state$ given by the run to evaluations part (of this theorem) is a normalizing sequence
by the halt property (guaranteeing that $\decode\state$ is $\tostrat$-normal). Then $\tostrat$ normalizes $\tm$ and so, by the diamond property (precisely by uniform
normalization implied by the diamond property, see esc), $\tostrat$ cannot diverge on
$\tm$—absurd. Therefore $\mach$ diverges on $\statetwo$. Now, since $\tomachsea$ terminates, the diverging run
from $\statetwo$ must have infinitely many principal transitions.

§ PROOFS OMITTED FROM BAM (BASIC ABSTRACT MACHINE)

By induction on the length of the run $\run$ leading from the initial state to $\state$. If the run is empty the invariants hold because the initial term is closed and well-bound by hypotheses. If the run is non-empty, the invariants follow very easily from the and the inspection of the transitions in BAM.

* If $\state = \twostate\ectx{\cuta\val\var \tm} \tomachsea \twostate{\ectxp{\cuta\val\var\ctxhole} }\tm = \statetwo$ then $\decode \statetwo = \ectxp{\cuta\val\var\ctxhole}\ctxholep\tm = \ectxp{\cuta\val\var\ctxholep\tm} = \ectxp{\cuta\val\var\tm} = \decode\state$.

* Straightforward. We show it for one transition, they go all in the same way. If $\state = \twostate{ \ectxp{\cuta{\mvartwo}\mvar\ectxtwo} }{ \suba\mvar\val\var\tm }
\tomachaxmtwo
\twostate{ \ectxp\ectxtwo }{ \suba\mvartwo\val\var\tm }$. Then $\decode\state = \ectxp{\cuta{\mvartwo}\mvar\ectxtwop{\suba\mvar\val\var\tm}}$. By the well-bound invariant (bam-invariants.2), there are no cuts on $\mvar$ in $\ectxtwo$ and $\ectx$. Then

$\ectxp{\cuta{\mvartwo}\mvar\ectxtwop{\suba\mvar\val\var\tm}} \toaxmtwo \ectxp{\ectxtwop{\suba\mvartwo\val\var\tm}} = \decode\statetwo$

which clearly is a basic step.

* Straightforward, since there can only be a finite number of cuts in the active term.

* Let $\state = \twostate\ectx\tm$ be a final state. Then the outermost constructor of $\tm$ is not a cut, otherwise $\tomachsea$ would apply. By the closure invariant (bam-invariants.1), the outermost constructor is not a subtraction, nor a dereliction, nor a variable, otherwise there would be a cut on the variable occurrence of that constructor, and by clash-freeness (see the last paragraph of prel-abs-mach) the machine would make a transition. Then $\tm$ is an abstraction or a bang. Then $\decode\state = \ectxp\tm$ is an answer. By the closure invariant, $\ectxp\tm$ is a closed term. By weak-harmony, $\ectxp\tm$ is normal for basic evaluation.

§ DEFINITIONS OMITTED FROM SESAME (SESAME)

The domain of a multi-context is the set of variables $\domp\namctx$ on which there is an out cut $\cuta\namvctx\var \namctxtwo$ in $\namctx$ such that there are some holes in $\namctxtwo$. Formally, it is defined as follows:

\begin{array}{rll<EMAIL_ADDRESS>rll}
\multicolumn{6}{c}{\textsc{Domain of value multi contexts}}
\\
\domp\namctxholea & \defeq & \emptyset
\domp\var & \defeq & \emptyset
\\
\domp{\la\var\namctx}  & \defeq & \domp\namctx
\domp{\bang\namctx}  & \defeq & \domp\namctx
\end{array}$

\multicolumn{4}{c}{\textsc{Domain of multi contexts}}
\\
\domp{\cuta\namvctx\var \namctx}  & \defeq & \set\var\cup\domp\namctx & \mbox{if $\namctx$ is not a term}
\\
\domp{\cuta\namvctx\var \namctx}  & \defeq & \emptyset & \mbox{if $\namctx$ is a term}
\\
\domp{ \suba\mvar\namvctx\var\namctx}  & \defeq & \domp\namvctx\cup\domp\namctx
\\
\domp{\dera\evar\var\namctx}  & \defeq & \domp\namctx
\end{array}$

A SESAME state $\state=\twostate\namctx\pool$ is well bound if:

* Term binders:  if $\la\var\tm$, $\dera\evar\var\tm$, $\suba\mvar\val\var\tm$, or $\cuta\val\var\tm$ occur anywhere in $\state$ then the only other possible occurrences of $\var$ in $\state$ are as a free variable of $\tm$;

* Context binders: if $\namctx=\namctxtwop{\cuta\val\var\namctxthree}\mute$, $\namctx=\namctxtwop{\suba\mvar\val\var\namctxthree}\mute$, $\namctx=\namctxtwop{\dera\evar\var\namctxthree}\mute$, or $\namctx=\namctxtwop{\la\var\namctxthree}\mute$ then the only other possible occurrences of $\var$ in $\state$ are as a free variable of $\namctxthree$ or of jobs $\nctxholep{\tm}\name$ of the pool $\pool$ such that $\name\in\names{\namctxthree}$.

§ PROOFS OMITTED FROM ANALYSIS (ANALYSIS OF SESAME)

Let $\gctx$ be a good context. Then:

$\gctxp{\cuta\val\var\ctxhole}$, $\gctxp{\suba\mvar\val\var\ctxhole}$, $\gctxp{\dera\evar\var\ctxhole}$, $\gctxp{\la\var\ctxhole}$, and $\gctxp{\bang\ctxhole}$ are good contexts.

If $\mvar \notin\domp\gctx$ then $\gctxp{\suba\mvar\ctxhole\var\tm}$ is a good context.

The proofs are straightforward inductions on $\gctx$. Intuitively, for the first point the statement follows from the fact that the inner extensions  of $\gctx$ have empty sets of dominating free variables (and the hole is not in the left sub-term of a cut); the second point has $\mvar$ as dominating variable, which is why the hypothesis $\mvar \notin\domp\gctx$ is needed.

Let $\ctxp{\cuta\mval\mvar\ctxtwo}$ be a good context. Then $\ctxp\ctxtwo$ is a good context.

The proof is a straightforward induction on $\ctx$. Intuitively, removing a cut makes goodness easier to establish, because the constraints on goodness are related to cuts.

Let $\namctxp{\cuta\mval\mvar\namctxtwo}\mute$ be an approximant. Then $\namctxp{\namctxtwo}\mute$ is an approximant.

The removal of $\cuta\mval\mvar$ cannot alter the uniqueness of names, nor add holes, nor create occurrences of out variables, thus $\namctxp{\namctxtwo}\mute$ is an approximant because $\namctxp{\cuta\mval\mvar\namctxtwo}\mute$ is.

l:search-is-bilinearNote that search transitions strictly decrease the size of the terms in the pool, which is increased only by principal transitions. Note also that principal transitions can increase it only of the size of a cut value, which by the sub-term invariant is bounded by $\size\tm$. Then $\sizesea\run\leq \size\tm\cdot(\sizepr\run+1)$, where the $+1$ accounts for the size of the initial term, for which there can be search transition even without any preceding principal transition.

Search transitions can be easily implemented in $\bigo(1)$ by only re-arranging pointers to sub-terms. For principal transitions, the sub-term invariant (subterm-invariant) guarantees that the size of the cut values is bound by $\size\tm$, so that their manipulations for implementing the transitions can be implemented in $\bigo(\size\tm)$. The only tricky operation is the $\alpha$-renaming in transitions $\tobang$ and $\toaxeone$, which amounts to copy sub-terms and can be done adapting the linear-time copy algorithm in Accattoli and Barras <cit.>.

The cost of implementing $\run$ is the sum of the costs of implementing its principal and search transitions on RAM:thm:sesame-overhead-bound

* Principal transitions: each one costs $\bigo(\size\tm)$ and so all together they cost $\bigo(\size\tm\cdot\sizepr{\run})$.

* Search transitions: each one costs $\bigo(1)$ and they are $\size\tm\cdot(\sizepr\run+1)$ of them by search-is-bilinear. Therefore, all together they cost $\bigo\left(\size\tm\cdot(\sizepr\run+1)\right)$.

Therefore, the cost of implementing $\run$ is $\bigo(\size\tm\cdot\sizepr{\run})+ \bigo\left(\size\tm\cdot(\sizepr\run+1)\right)=\bigo\left(\size\tm\cdot(\sizepr\run+1)\right)$.

§ PROOFS OMITTED FROM GC-AND-FULL (FINAL GARBAGE COLLECTION AND FULL CUT ELIMINATION)

If $\tm$ is not cut free then it has at leas an out cut. Let $\tm=\ctxp{\cuta\val\var\tmtwo}$ be an innermost out cut of $\tm$, that is, such that in $\tmtwo$ there are no other out cuts of $\tm$. By definition of cut-freeness up to garbage, $\var\notin\ov\tmtwo$. Note that $\tmtwo$, having no out cuts, is cut-free. Then $\var\notin\fv\tmtwo$ and $\cuta\val\var\tmtwo$ is a $\tow$-redex in $\tm$. We need to show that $\ctx$ is good. By contradiction, suppose that $\ctx$ is bad. Then there are two cases:

* The hole of $\ctx$ is in the left sub-term of a cut, that is, $\ctx=\ctxtwo{\cuta\vctx\vartwo\tmthree}$. Then $\cuta\val\var$ is not an out cut of $\tm$. Absurd.

* The hole of $\ctx$ is in a dominated sub-term, that is, $\ctx=\ctxtwop{\cuta\valtwo\vartwo\ctxthree}$ with $\vartwo\in\dfv\ctxthree$. Note that the fact that $\cuta\val\var$ is an out cut forces $\cuta\valtwo\vartwo$ to be an out cut as well. Moreover, if $\vartwo\in\dfv\ctxthree$ then $\ctxthree = \ctx_1\ctxholep{\dera\vartwo\varthree\ctx_2}$ or $\ctxthree = \ctx_1\ctxholep{\suba\vartwo\valthree\varthree\ctx_2}$ for some $\ctx_1$ and $\ctx_2$. Note, in particular, that $\dera\vartwo\varthree$ and $\suba\vartwo\valthree\varthree$ are out of all cuts, being between two out cuts. Then there is an occurrence of $\vartwo$ out of all cuts for $\cuta\valtwo\vartwo$. This contradicts cut-freeness up to garbage of $\tm$, for which the variables of out cuts have no out occurrences. Absurd.

* By induction on $k$. If $k=0$ then the statement holds with $\tmtwo\defeq \tm$. Let $k>0$. By good-w-redex-exists, there is a good $\wsym$-redex in $\tm$. Then $\tm\togp\wsym\tmthree$. By $\tmthree \togp\wsym^{k-1} \tmtwo$ with $\tmtwo$ cut-free. Then $\tm \togp\wsym^k \tmtwo$.

* By sesame-overhead-bound, the run $\run$ has  cost $\bigo\left(\size\tm\cdot(\sizepr\run+1)\right)$. Then the size of the final state $\twostate\tmtwo\emptylist$, and so of $\tmtwo$, is bound by $\bigo\left(\size\tm\cdot(\sizepr\run+1)\right)$. Since $\gcdec\tmtwo$ amounts to simply remove all out cut in a traversal of the term, this can be done in $\bigo(\size\tmtwo)$, given our hypothesis on the representation of terms (discussed just before cost-single-trans, page l:cost-single-trans). That is, the cost is $\bigo(\size\tmtwo)=\bigo\left(\size\tm\cdot(\sizepr\run+1)\right)$.

§ OVERVIEW OF THE DATA STRUCTURES USED IN THE OCAML IMPLEMENTATION

Data Structures.

Terms are encoded at runtime as term graphs, which are Direct Acyclic Graphs (DAG)
augmented with a few back edges. Nodes in the graph are given by constructors
of Algebraic Data Types whose arguments are declared as mutable to imperatively
change the graph during reduction. All type declarations are given in the

We start our description of the various shapes of nodes from the
datatype that is used for values:

type value =
| Var of var
| Abs of  var : var; mutable bo : term
| Bang of  mutable bo : term

A value is either a variable occurrence node, that points to the unique node in memory
that represents a variable, an abstraction node, that points to the node for
the bound variable and to the root node of the body of the abstraction,
or a promotion node that points to the root node of the promoted term.

and var =
mutable is : bvar option;
kind : me;
name : int;
mutable copy : var;

Variables nodes are the only kind of nodes that are shared in a term graph.
The  field holds either the value  for multiplicative
variables or the value  for exponential variables. The  field,
that plays no role during reduction, is an unique index to differentiate variables
during pretty-printing: a variable of name $i$ is printed either as $\mvar_i$ or $\evar_i$
according to its kind. The parser only accepts terms that follow the Barendregt's
convention and that are well bounded in order to have a bijection between
variables and  pairs.

The  field is necessary to implement copy ($\alpha$-renaming) in linear
time. During copy, the first time a bound variable is visited a new variable node is
allocated and  is set to it. Later, when occurrences of the variable
to be copied are found, the  field is used to retrieve the new variable
to use, preserving the sharing. Variables that have not been copied have the
field initialized to point to themselves recursively, to avoid introducing
an  type.

A variable can be globally free or bound by an abstraction, in which case the
field is , or it can be bound in a cut, a dereliction or a
subtraction. The three latter cases are represented with a  value for
holding the data for the binder. Storing the cut value associated to the
variable in the  field allows to look in $O(1)$ for cuts in a context,
a prerequisite of most SESAME rules.

In place of storing the cut value inside the variable, an alternative implementation
could have made the variable point back to the binder. Handling back-pointers in OCaml
always require some gymnicks, like creating nodes with dummy values and imperatively
updating them later to create the cycles in the graph. Our design choice, instead,
allows to keep the DAG structure, that is handled very easily.

The SESAME machine has no need to access derelictions and subtractions given their
bound variable. However, we have decided to handle cuts, derelictions and subtractions
in the same way, since they can occur in the term structure in the same position.
This leads to some simplification in the code. It is, however, a quite inessential
design decision.

and bvar =
(* ptr must point to the surrounding Bind;
it can be None in initial terms *)
| Cut of  v : value; mutable ptr : ptr option
| MElim of  mutable var : var; mutable v : value
| EElim of  mutable var : var

The  describes the binder associated to a variable, excluding the case
of abstraction.  and  are for subtractions and derelictions
and they point to the inspected variables and, in the case of subtractions, to the
node that is the root of the value.

Cut nodes point to the root of the cut value
, but they also have an optional back-pointer  that points to the
node that is the parent of the cut. For example, the node for the term
$\dera\evar\evartwo \cuta\val\var \tm$ points both to the node for the variable $\evartwo$ and to the node for the suberm $\cuta\val\var \tm$. The  pointer of the  node associated
to $\var$ points back to node for $\dera\evar\evartwo \cuta\val\var \tm$. This is necessary to remove in $O(1)$
the cut from the context in the multiplicative principal SESAME rules: the
the right child of the pointed node is mutated from a pointer to the root of
$\cuta\val\var \tm$ to a pointer of the root of $\tm$.

To simplify the implementation of the parser, cuts in the initial terms may have
the  field set to . The SESAME will set it correctly when the
cut is processed the first time, entering the approximant.

and term =
| Val of value
| Bind of  var : var; mutable t : term
(* var must have is != None *)

A term node is either a value node or a  node that points to the
bound variable  and the continuation term . As already explained,
the  field of the variable differentiates between cuts, derelictions and
subtraction, avoiding back-pointers.

When a value is used as a term, an additional indirection  is introduced.
In a more optimized implementation this indirection can be completely avoided by
merging together the  and  datatypes. The price to pay is
the introduction of more runtime invariants, i.e. places in the code where an OCaml
term of type  is actually expected to contain a value only. To mitigate
the extra checks and dead code branches, one could employ Algebraic Data Types to
parameterize the  datatype with additional information about the nature
of the term (value, variable, cut, etc.). Due to the lack of subtyping in OCaml, this
leads in turn to some gymnicks to typecheck the code (e.g. introduce formers for
existential types) and thus we avoided this solution to maintain the code simple
for non experts of the language.

and topterm = term ref

A  is just a reference to the root of a term graph and it represents
the whole term.

In OCaml it is not possible to take the address of a record/constructor field to
mutate it. One needs to have a reference to the whole record/constructor instead.
The  datatype, that we have already encountered when describing the
back-pointers inside cuts, represents a pointer inside the term graph.
It lists all the constructors (i.e. labelled records) that have fields that are
sub-terms different from variables, i.e. all the positions where an hole
can occur in an approximant.

and ptr =
| Initial of topterm (** points to the [topterm] *)
| InsideBang of value (** [value] must be a [Bang] *)
| InsideAbs of value (** [value] must be an [Abs] *)
| InsideBind of term (** [value] must be a [Bind] *)
| InsideMElim of bvar (** [bvar] must be an [MElim] *)

For example, a pointer to the term $\tm$ inside $\dera\evar\evartwo \tm$ is encoded as
where  is the node for $\dera\evar\evartwo \tm$.
If we picked a different programming language like C, not subject to mark&swepp
garbage collection, it could have been possible to just take directly pointers to
pointers to terms in memory in place of using the  type.
In the example above, we could have just used a pointer to the pointer to $\tm$ inside
the record for $\dera\evar\evartwo \tm$.

type pool = ptr list

Named holes and jobs are simply represented as pointers inside a term graph, and
the pool of jobs as a list of s.
A pointer in the pool is the position of the corresponding named hole in the
approximant, the pointed sub-term is the term to be reduced by the job and the
approximant is just the part of term outside any sub-terms pointed by the pointers
in the pool.

Thanks to this representation, reduction is implemented as local term rewriting:
at each step the unique term graph in memory is locally modified starting from the
topmost pointer in the pool, until the pool becomes empty and the term graph is the
strong normal form.

§ THE EXAMPLE OF SESAME RUN, EXECUTED BY THE OCAML IMPLEMENTATION

The OCaml implementation starts by running some tests. One of them is the example of SESAME run given at the end of sesame, whose output is given below. The names of the jobs in the pool are represented with numbers, that is, the hole name $\name$ is here represented with the index $1$. Moreover, the pool and the multi-context are represented as a single term where the job $\nctxholep{\tm}1$ is directly plugged in the multi-context at hole $\nctxholep{\cdot}1$, according to the fact that in the implementation we only keep the term graph together with a pool made of pointers into it.
Input: [!1m1-e1][e1?m2][e1?m3][m2>m3,m4]m4
Parsed: [!$\lambda$m$_1$m$_1$$\to$e$_1$][e$_1$?m$_2$][e$_1$?m$_3$][m$_2$$\triangleright$m$_3$,m$_4$]m$_4$
The term is proper.
->sea$_1$ [!$\lambda$m$_1$m$_1$$\to$e$_1$]<[e$_1$?m$_2$][e$_1$?m$_3$][m$_2$$\triangleright$m$_3$,m$_4$]m$_4$>$_1$
->!    [!$\lambda$m$_1$m$_1$$\to$e$_1$]
->sea$_1$ [!$\lambda$m$_1$m$_1$$\to$e$_1$]
->!    [!$\lambda$m$_1$m$_1$$\to$e$_1$]
->sea$_1$ [!$\lambda$m$_1$m$_1$$\to$e$_1$]
->-o   [!$\lambda$m$_1$m$_1$$\to$e$_1$]
->sea$_1$ [!$\lambda$m$_1$m$_1$$\to$e$_1$]
->sea$_1$ [!$\lambda$m$_1$m$_1$$\to$e$_1$]
->axm$_1$ [!$\lambda$m$_1$m$_1$$\to$e$_1$][$\lambda$m$_6$m$_6$$\to$m$_3$][m$_3$$\to$m$_5$]<m$_5$>$_1$
->axm$_1$ [!$\lambda$m$_1$m$_1$$\to$e$_1$][$\lambda$m$_6$m$_6$$\to$m$_3$]<m$_3$>$_1$
->axm$_1$ [!$\lambda$m$_1$m$_1$$\to$e$_1$]<$\lambda$m$_6$m$_6$>$_1$
->sea$_4$ [!$\lambda$m$_1$m$_1$$\to$e$_1$]$\lambda$m$_6$<m$_6$>$_1$
->sea$_6$ [!$\lambda$m$_1$m$_1$$\to$e$_1$]$\lambda$m$_6$m$_6$
->*GC  $\lambda$m$_6$m$_6$