Beniamino Accattoli
email: beniamino.accattoli@inria.fr

Proof Nets and the Call-by-Value λ-Calculus

Keywords: Curry-Howard isomorphism, call-by-value λ-calculus, linear logic, graphical syntaxes, proof nets, explicit substitutions, correctness criteria 1

This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize an isomorphism between the two systems: every single rewriting step on the calculus maps to a single step on proof nets, and viceversa. In this way, we obtain an algebraic reformulation of proof nets. Moreover, we provide a simple correctness criterion for our proof nets, which employ boxes in an unusual way, and identify a subcalculus that is shown to be as expressive as the full calculus.

Introduction

A key feature of linear logic (LL for short) is that it is a refinement of intuitionistic logic, i.e. of λ-calculus. In particular, one β-reduction step in the λ-calculus corresponds to the sequence of two cut-elimination steps in linear logic, steps which are of a very different nature: the first is multiplicative and the second is exponential. The Curry-Howard interpretation of this fact is that λ-calculus can be refined adding a constructor t[x s] for sharing annotations called explicit substitution, and decomposing a β-step (λx.t)s → β t{x s} into the sequence (λx.t)u → m t[x s] → e t{x s}.

Another insight due to linear logic is that proofs can be represented graphically, in a formalism called proof nets, and the reformulation of cut-elimination on proof nets takes a quite different flavor with respect to cut-elimination in sequent calculus. The parallel nature of the graphical syntax makes commutative cut-elimination steps-which are the annoying burden of every proof of cut-admissibility-(mostly) disappear.

These two features of LL have influenced the theory of explicit substitutions in various ways [START_REF] Di | Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract)[END_REF][START_REF] Di | Proof Nets And Explicit Substitutions[END_REF][START_REF] Kesner | Resource operators for lambdacalculus[END_REF][START_REF] Kesner | The Prismoid of Resources[END_REF], culminating in the design of the structural λcalculus [START_REF] Accattoli | The Structural λ-Calculus[END_REF], a calculus isomorphic (more precisely strongly bisimilar 1 ) to its representation in a variant of LL proof nets [START_REF] Accattoli | Jumping Boxes[END_REF]1]. Such a calculus can be seen as an algebraic reformulation of proof nets for λ-calculus [START_REF] Danos | La Logique Linéaire appliqué à l'étude de divers processus de normalisation (principalement du λ-calcul)[END_REF][START_REF] Regnier | Lambda-calcul et réseaux[END_REF], and turned out to have a simpler meta-theory than previous calculi with explicit substitutions.

Girard's seminal paper on linear logic [START_REF] Girard | Linear Logic[END_REF] presents two translations of λcalculus into LL. The first one follows the typed scheme (A ⇒ B) n = !A n

B n , and it is the one to which the previous paragraphs refer to. It represents the ordinary-or call-by-name (CBN)-λ-calculus. The second one, identified by

(A ⇒ B) v = !(A v B v
), was qualified as boring by Girard and received little attention in the literature [START_REF] Maraist | Call-by-name, Call-by-value, Call-by-need and the Linear lambda Calculus[END_REF][START_REF] Pravato | The call-by-value λ-calculus: a semantic investigation[END_REF][START_REF] Danos | Reversible, Irreversible and Optimal lambda-Machines[END_REF][START_REF] Fernández | Call-by-Value lambda-Graph Rewriting Without Rewriting[END_REF][START_REF] Fernández | Labelled Lambda-calculi with Explicit Copy and Erase[END_REF][START_REF] Mackie | Encoding Strategies in the Lambda Calculus with Interaction Nets[END_REF]. Usually, it is said to represent Plotkin's call-by-value (CBV) λ βv -calculus [START_REF] Plotkin | Call-by-Name, Call-by-Value and the lambda-Calculus[END_REF]. These two representations concern typed terms only, but it is well-known that they can be extended to represent the whole untyped calculi by considering linear recursive types (o = !o o for call-by-name and and o = !(o o) for call-by-value). Surprisingly, the extension of the CBV translation to the untyped λ βv calculus introduces a violent unexpected behavior: some normal terms in λ βv map to (recursively typed) proof nets without normal form, as we will point out here. A possible interpretation of this fact is that there is something inherently wrong in the CBV translation.

In this paper we show how to refine the three actors of the play (the CBV λ-calculus, the translation, and the proof nets presentation) in order to obtain a perfect match between terms and proof nets. Technically, we show that the new translation is an isomorphism of rewriting systems, and since isomorphisms preserve reductions length (in both directions), the normalization mismatch vanishes.

Interestingly, to obtain an isomorphism we have to make some radical changes to both the calculus and the presentation of proof nets. The calculus, that we call the value substitution kernel λ vker , is a subcalculus of the value substitution calculus λ vsub studied in [START_REF] Accattoli | Call-by-Value Solvability, Revisited[END_REF], which is a CBV λ-calculus with explicit substitutions. Such a kernel-as we will show-is as expressive as the full calculus.

Our contributions are:

1. Graphical Syntax and Algebraic Formalism. It is far from easy to realize an isomorphism between terms and nets, as it is necessary to take care of many delicate details about weakenings, contractions, representation of variables, administrative reduction steps, and so on. The search for an isomorphism may seem a useless obsession, but it is not. Operational properties as confluence and termination then transfer immediately from graphs to terms, and vice versa. More generally, such a strong relationship turns the calculus into an algebraic language for proof nets, providing a handy tool to reason by structural induction over proof nets. 2. Correctness Criterion. We provide a characterization of the system of proof nets representing λ vker based on graph-theoretical principles and which does not refer to λ vker , that is, we present a correctness criterion.

Surprisingly, the known criteria for the representation of the call-by-name λ-calculus (with explicit substitutions) fail to characterize the fragment encoding the call-by-value λ-calculus. Here we present a simple and nonstandard solution to this problem. We hack the usual presentation of proof nets so that Laurent's criterion for polarized nets [START_REF] Laurent | Polarized Proof-Nets: Proof-Nets for LC[END_REF][START_REF] Laurent | Polarized proof-nets and λµ-calculus[END_REF][START_REF] Laurent | Étude de la polarisation en logique[END_REF]-the simplest known correctness criterion-captures the fragment we are interested in. The hacking is about explicit boxes: they are usually attached to !-links, while we put them on `-links. An interesting point is that the fragment we deal with is not polarized in Laurent's sense, despite being polarized in the intuitionistic/Lamarche sense [START_REF] Lamarche | Proof Nets for Intuitionistic Linear Logic: Essential Nets[END_REF]. [START_REF] Accattoli | Proof nets and the call-by-value lambdacalculus[END_REF]. The Kernel Calculus. The kernel subcalculus is new. We provide a detailed study of the relationship with the value substitution calculus, showing that they are equivalent from the point of view of termination, which is the property used to define most notions of programs equivalence. Moreover, the two systems simulate each other with only a linear overhead.

In Sect. 7, we complement the results of the paper with 1) a discussion aimed to show that the use of boxes for `-links is natural rather than ad-hoc, and 2) an account of the technical points concerning the representations of terms with proof nets, and how they have been treated in the literature.

This paper is a longer version of the workshop paper [START_REF] Accattoli | Proof nets and the call-by-value lambdacalculus[END_REF]. Apart from updating the notation of [START_REF] Accattoli | Proof nets and the call-by-value lambdacalculus[END_REF] to that of other recent papers using the same formalism [START_REF] Accattoli | Distilling abstract machines[END_REF][START_REF] Accattoli | Beta reduction is invariant, indeed[END_REF][START_REF] Accattoli | On the Value of Variables[END_REF], it extends it with the detailed relationship between the value substitution calculus and the kernel calculus in Sect. 8.

The Problem with Plotkin's Calculus

Plotkin's call-by-value (CBV for short) λ-calculus λ βv is obtained by restricting the β-rule (λx.t)s → β t{x s} (where {x s} denotes the usual meta-level substitution) so that s is a value v, i.e. a variable or an abstraction. The value substitution calculus, similarly to other variations on the CBV λ-calculus as e.g. the one by Herbelin and Zimmerman [START_REF] Herbelin | An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction[END_REF], implements the restriction in a different way. Every β-redex (λx.t)s, independently of the shape of s, is fired, but substitution is delayed by introducing an explicit substitution (or, equivalently, a let expressions), obtaining t[x s] (aka let x = s in t). Then, only explicit substitutions containing values are actually substituted, by means of an additional rewriting rule.

Before giving the details, let us point out what is the problem with Plotkin's calculus λ βv . Essentially, it is about open terms, and shows up as soon as one does evaluate under abstraction or does not restrict to closed terms. While weak evaluation and closed terms are common practice hypothesis for an evaluation strategy, a calculus should be more liberal and not rely on them. Now, consider a term like t := (λx.λy.y)sv where s is an irreducible open application, say, s := zz. Note that the redex (λx.λy.y)s cannot be fired. Rather than a problem in itself, the issue is that such a blocked redex forbids the reduction of the future redex (λy.y)v, that would appear if the first redex was to be somehow reduced (i.e. it forbids what Lévy calls creations of type 1 [START_REF] Lévy | Réductions correctes et optimales dans le lambda-calcul[END_REF]). Preventing these redexes to take place ruins the relationships between the rewriting and the semantics, see [START_REF] Paolini | Call-by-value Solvability[END_REF][START_REF] Accattoli | Call-by-Value Solvability, Revisited[END_REF]. In particular, a term like u := (λz.δ)(yy)δ (where δ := λx..xx is the usual term whose auto application Ω := δδ diverges) is a normal form in λ βv , because the first argument yy of λz.δ is not a value. From a semantical point of view, however, such a term is unsolvable (roughly, it is equivalent to Ω) and should diverge. A similar but different example of discrepancy between Plotkin's calculus and proof nets is given by u := δ((λz.δ)(yy)), where now it is the evaluation of the argument-rather than the function-that is stuck, forbidding the creation of a redex. This kind of redex creation is different from the previous one, and typical of the CBV λ-calculus. It can be called creation of type 4, as it does not appear in Lévy's classification, that is only concerned with the three kinds of creation of the CBN λ-calculus.

The value substitution calculus λ vsub provides a compact solution to the problem of stuck redex and creations of type 1 and 4. It employs explicit substitutions and it adopts carefully crafted contextual rewriting rules, also known as at a distance. We will see that in λ vsub the terms u and u diverge, as required.

Another solution is provided by Carraro and Guerrieri in [START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF], where rather than adding explicit substitution the authors extend Plotkin's λ βv with two rewriting rules permuting constructors, so that blocked redexes can be enabled. Their approach essentially adapts Regnier's σ-equivalence [START_REF] Regnier | Une équivalence sur les lambda-termes[END_REF] to CBV.

The Value Substitution Calculus and its Kernel

The language of the value substitution calculus λ vsub is given by Terms t, s, u, r

::= v | ts | t[x s] Values v ::= x | λx.t
where t[x s] is an explicit substitution. Both λx.t and t[x s] bind x in t, and we silently work modulo α-equivalence. We shall use contexts (noted C, D, E) extensively, in particular substitution contexts (noted L, L , L ) so let us define them formally:

Contexts C, D, E ::= • | λx.C | vC | Ct | C[x s] | t[x C] Substitution Contexts L, L , L ::= • | L[x t]
The plugging C t (resp. C D ) of a term t (resp. context D) in a context C is defined as t := t (resp. D := D), (λx.C) t := λx.C t (resp. (λx.C) D := λx.C D ), (Cs) t := C t s (resp. (Cs) D := C D s), and so on. Note that plugging in a context can capture variables.

As usual, the rewriting rules of λ vsub are obtained by first defining the rewriting rules at top level (noted → m and → e ), and then taking their closure by contexts (noted → m and → e ). It is less common, instead, that contexts are also used to specify the top-level rules, as we do here, that is the essence of rewriting at a distance. The multiplicative and exponential rewriting rules are given by:

Rule at Top Level Contextual Closure Multiplicative L λx.t s → m L t[x s] C t → m C s iff t → m s Exponential t[x L v ] → e L t{x v} C t → e C s iff t → e s
the fact that in the lhs of → e the context L appears inside [ ] while in the rhs it appears outside { } is not a typo. We write → λ vsub for the union of → m and → e .

Theorem 3.1 ( [START_REF] Accattoli | Call-by-Value Solvability, Revisited[END_REF]). The value substitution calculus λ vsub is confluent.

Let us show that in λ vsub the two problematic terms u and u (discussed in the previous section) diverge in λ vsub , as required:

u := (λz.δ)(yy)δ → m δ[z yy]δ → m (xx)[x δ][z yy] → e (δδ)[z yy] → m . . . and
u := δ((λz.δ)(yy)) → m δ(δ[z yy]) → m (xx)[x δ[z yy]] → e (δδ)[z yy] → m . . .
Essentially, the problems with creations are solved by 1. turning generic β-redexes (i.e. not only CBV β-redexes) into ES, 2. allowing such an action to be possible up to ES, i.e. by turning to rewriting at a distance, 3. restricting ES to substitute when they contain a value up to ES.

Note that the problem illustrated by u, i.e. stuck creations of type 1, is solved by points 1 and 2, while the problem showcased by u , i.e. stuck creations of type 4, is solved by points 1 and 3.

As hinted at in [START_REF] Accattoli | Call-by-Value Solvability, Revisited[END_REF], the value substitution calculus λ vsub is designed around the CBV translation of λ-calculus to proof nets (extended to untyped terms by means of recursive types). This shows a serious mismatch between Plotkin's calculus and proof nets, with respect to termination. However, in [START_REF] Accattoli | Call-by-Value Solvability, Revisited[END_REF] the relationship between λ vsub and proof nets was not shown. One of the reasons is that such a relationship-with respect to the usual presentation of the translationis complex, as term redexes and proof nets redexes do not match very nicely. This paper addresses this point, providing a new and simpler relationship, identifying a subcalculus λ vker of λ vsub which perfectly represents the image of the translation to proof nets. How λ vsub is related to proof nets is studied in Sect. 8.

The relationship between the value substitution calculus λ vsub and Plotkin's calculus λ βv has been treated indirectly in [START_REF] Accattoli | Call-by-Value Solvability, Revisited[END_REF]. Therein, λ vsub is related to another call-by-value calculus, Herbelin and Zimmermann's λ CBV [START_REF] Herbelin | An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction[END_REF], whose equational theory is shown to be strictly contained in the theory of λ vsub . In turn, λ CBV is related to Plotkin's λ βv in [START_REF] Herbelin | An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction[END_REF], where it is shown that the equational theory of λ βv is strictly contained in the theory of λ CBV .

The Kernel Calculus λ vker . The value substitution calculus λ vsub is somewhat redundant. In fact, there is a subcalculus, the value substitution kernel λ vker , which is as expressive as the whole of λ vsub , and that is what exactly corresponds to proof nets, as we will show. Its syntax is:

Terms t, s, u, r ::= v | vs | t[x s] Values v ::= x | λx.t
The distinguished feature of the value substitution kernel is that iterated applications as (ts)u are not part of the language, because the left subterm of an application can only be a value. Contexts are defined similarly as for λ vsub (with the obvious restriction on applications). The rewriting rules of λ vker are those of λ vsub restricted to the new syntax. Explicitly:

Rule at Top Level Contextual Closure Multiplicative (λx.t)s → m t[x s] C t → m C s iff t → m s Exponential t[x L v ] → e L t{x v} C t → e C s iff t → e s
Note that → m does no longer need the substitution context around the abstraction. Note also that λ vker is stable under reduction because only values are substituted, and so a substitution can never turn an application of the form xu into a term of the form (ts)u . Since λ vsub is confluent and λ vker is a closed subcalculus of λ vsub , we immediately obtain Theorem 3.2. The value substitution kernel λ vker is confluent.

In Sect. 8.2, we will show that λ vsub can be represented inside λ vker . The idea is that applications as (ts)u are rather represented as (xu)[x ts] with x fresh. We will prove that a term t of λ vsub and its representation t k in λ vker are equivalent from the point of view of termination.

In the next three sections, instead, we will show that λ vker has an isomorphic representation as a variant of linear logic proof nets.

The results of this paper are complemented by those in [START_REF] Accattoli | Evaluating functions as processes[END_REF], where it is shown that λ vker has an isomorphic representation inside the π-calculus as well.

Proof Nets: Definition

Introduction. Our presentation of proof nets is nonstandard in at least four points (we suggest to have a quick look to Fig. 1. Hypergraphs: we use directed hypergraphs (for which formulas are nodes and links-i.e. logical rules-are hyperedges) rather than the usual graphs with pending edges (for which formulas are edges and links are nodes). We prefer hypergraphs-that despite the scaring name are nothing else but bipartite graphs-because (a) contraction is represented modulo commutativity, associativity, and permutation with box borders for free, by admitting that exponential nodes can have more than one incoming link, (b) cut and axiom links are represented implicitly, collapsing them on nodes. This is analogous to what happens in interaction nets. Essentially, our multiplicative nodes are wires, with exponential nodes being hyper wires, i.e. wires involving an arbitrary number of ports; (c) subnets can be elegantly defined as subsets of links, that would not be possible by adopting other approaches as generalized ?-links. The choice of hypergraphs, however, has various (minor) technical consequences, and the formulation of some usual notions (e.g. the nesting condition for boxes) will be slightly different with respect to the literature. 2. `-boxes: we use boxes for `-links and not for !-links. This choice is discussed in Sect. 7, and it allows to use a very simple correctness criterioni.e. Laurent's criterion for polarized nets [START_REF] Laurent | Polarized proof-nets and λµ-calculus[END_REF][START_REF] Laurent | Étude de la polarisation en logique[END_REF]-without losing any property. 3. Polarity: we apply a polarized correctness criterion to a setting which is not polarized in the usual sense. 4. Syntax tree: since we use proof nets to represent terms, we will dispose them on the plane according to the syntax tree of the corresponding terms, and not according to the corresponding sequent calculus proof. Moreover, the orientation of the links does not reflect the usual premise-conclusion orientation of proof nets.

Nets. Nets are directed and labeled hypergraphs G = (V (G), L(G)), i.e., graphs where V (G) is a set of labeled nodes and L(G) is a set of labeled and directed hyperedges, called links, which are edges with 0, 1, or more sources and 0, 1, or more targets 2 . Nodes are labeled with a type in {e, m}, where e stands for exponential and m for multiplicative. If a node u has type e (resp. m) we say that it is a e-node (resp. m-node). The label of a node will usually be left implicit, as e and m nodes are distinguished graphically, using both colors and different shapes: e-nodes are cyan and white-filled, while m-nodes are brown and dot-like. We shall consider hypergraphs whose links are labeled from {!, d, w, `, ⊗}. The label of a link l forces the number and the type of the source and target nodes of l, as shown in Fig. 1 (the types will be discussed later, and the figure also contains the -link, which is not used to define nets: it will be used later to define the correction graph). Similarly to nodes, we use colors and shapes for the type of the source/target connection of a link to a node: e-connections are cyan and dotted, while m-connections are brown and solid. Our choice of shapes allows to read the paper also if printed in black and white. A node is:

Initial, if it is not the target of any link,
Terminal, if it is not the source of any link, Isolated, if it is initial and terminal, Internal, if it is not initial nor terminal.

Note that every link (except ) has exactly one connection with a little circle: it denotes the principal node, i.e. the node on which the link can interact. Remark the principal node for tensor and !, which is not misplaced. Moreover, every `-link has an associated box, i.e., a sub-hypergraph of P (have a look to Fig. 3). Formally: Definition 4.1 (Net). A pre-net P is a triple (|P |, fv(P ), r P ), where |P | = (V (P ), L(P )) is a hypergraph whose nodes are labeled with either e or m and whose hyperedges are {!, d, w, `, ⊗}-links, and such that: Interface: Root: r P ∈ V (P ) is a non-isolated initial e-node of P , called the root of P .

Free Variables: fv(P ) is the set of terminal nodes of P , also called free variables of P , which are targets of {d, w}-links (i.e. they are not allowed to be targets of ⊗-links, nor to be isolated).

Nodes:

Multiplicative: m-nodes have at most one incoming and at most one outgoing link.

Exponential: an e-node has at most one outgoing link, and if it is the target of more than one link then they all are d-links.

target of a hyperedge.

A net P is a pre-net together with a function box P (or simply box) associating to every `-link l a subset box(l) of L(P ) \ {l} (i.e. the links of P except l itself ) s. t. box(l) is a pre-net with a distinguished free variable called the variable of l, and verifies: Border: the root r box(l) and the free variable x are respectively the target and source e-nodes of l, and any free variable = x of box(l) is not the target of a weakening.

Nesting: for any `-box box(h) if ∅ = I := |box(l)| ∩ |box(h)|, |box(l)| ⊆ |box(h)|,

Internal Closure:

Contractions: h ∈ box(l) for any link h of P having as target an internal e-node of box(l).

Boxes: box(h) ⊆ box(l) for any `-link h ∈ box(l).
Comments on the Definition.

Weakenings and Box Borders: in the border condition for nets the fact that the free variables = x are not (the target) of a weakening means that weakenings are assumed to be pushed out of boxes as much as possible (of course the rewriting rules will have to preserve this invariant).

Weakenings are not Represented as Nullary Contractions: given the representation of contractions, it would be tempting to define weakenings as nullary contractions. However, such a choice would be problematic with respect to correctness (to be defined soon), as it would introduce many initial e-nodes in a correct net and thus blur the distinction between the root of the net, supposed to represent the output and to be unique (in a correct net), and substitutions on a variable with no occurrences (i.e. weakened subterms), that need not to be unique.

Internal Closure wrt Contractions: it is a by-product of collapsing contractions on nodes, which is also the reason for the unusual formulation of the nesting condition. In fact, two boxes that are morally disjoint can in our syntax share free variables, because of an implicit contraction merging two of them.

Boxes as Nets: note that a box box(l) in a net P is only a pre-net, by definition. Every box in a net P , however, inherits a net structure from P . Indeed, one can restrict the box function box P of P to the `-links of box(l), and see box(l) as a net, because all the required conditions are automatically satisfied by the internal boxes closure and by the fact that such boxes are boxes in P . Therefore, we will freely consider boxes as nets. Terminology about Nets. The level of a node/link/box is the maximum number of nested boxes in which it is contained3 (a `-link is not contained in its own box). Two links are contracted if they share an e-target. Note that the exponential condition states that only derelictions (i.e. d-links) can be contracted.

In particular, no link can be contracted with a weakening. A free weakening in a net P is a weakening whose node is a free variable of P . Sometimes (e.g. the bottom half of Fig. 3), the figures show a link in a box having as target a contracted e-node x which is outside the box: in those cases x is part of the box, it is outside of the box only in order to simplify the representation. Let us explain the types in Fig. 1. They have to be read bottom-up, and thus negated (to match the usual typing for links) if the conclusion of the logical rule is the bottom node of the link, as it is the case for the {w, d, ⊗}-links, while ! and `have their logical conclusion on the top node, and so their type does not need to be negated.

Induced !-boxes. Note that a !-link is always applied to something (m-nodes cannot be free variables), and there is not so much freedom for this something: either it is a dereliction link or a `with its box. Note also that in these cases we obtain (what would usually be) a valid content for a !-box, i.e. something ending on e-nodes. For the dereliction case it is evident, and for the `case it is guaranteed by the border condition in the definition of nets: the content of a `-box ends on e-nodes. Hence, any !-link has an associated box, possibly induced by a `-box, that needs not be represented explicitly. Such induced !-boxes will play a role in Sect. 6, where proof nets cut-elimination is studied.

Translation. Nets representing terms have the general form in Fig. 2.a, also schematized as in Fig. 2.b. The translation • from terms to nets is in Fig. 3 (the original boring translation is sketched in Fig. 6, page 23). A net which is the translation of a term is a proof net. Note that in some cases there are various connections entering an e-node, that is the way we represent contraction. In some cases the e-nodes have an incoming connection with a perpendicular little bar: it represents an arbitrary number (> 0) of incoming connections. The net corresponding to a variable is given by a !-link on a dereliction and not by an (exponential) axiom, as it is sometimes the case [START_REF] Fernández | Labelled Lambda-calculi with Explicit Copy and Erase[END_REF]. The reason is that an axiom (in our case a node, because axioms are collapsed on nodes) would not reflect on nets some term reductions, as x[x v] → e v, for which both the redex and the reduct would be mapped on the same net.

Extended Translation. The translation • is refined to a translation • ∆ , where ∆ is a set of variables, in order to properly handle weakenings during cut-elimination. The reason is that an erasing step on terms simply erases a subterm, while on nets it also introduces some weakenings: without the refinement the translation would not be stable by reduction. The clause defining t ∆∪{y} when y / ∈ fv(t) is the second on the first line of Fig. 3, the definition is then completed by the following two clauses: t ∅ := t and t ∆∪{y} := t ∆ if y ∈ fv(t).

α-Equivalence. To circumvent an explicit and formal treatment of α-equivalence we assume that the set of e-nodes and the set of variable names for terms coincide. This convention removes the need to label the free variables of t ∆ with the name of the corresponding free variables in t or ∆. Actually, before translating a term t it is necessary to pick a well-named α-equivalent term t , i.e. a term such that any two different variables (bound or free) have different names.

Remark 4.2. The translation of terms to nets is not injective. By simply applying the translation it is easily seen that the following pairs of terms are sent on the same net:

t[x s][y u] ∼ vo CS t[y u][x s] if x / ∈ fv(u) & y / ∈ fv(s) vu[x s] ∼ vo1 (vu)[x s] if x / ∈ fv(v) t[x s[y u]] ∼ vo2 t[x s][y u] if y / ∈ fv(t) (1)
Let ≡ vo be the reflexive, symmetric, transitive, and contextual closure of ∼ vo CS ∪ ∼ vo1 ∪ ∼ vo2 . In the proof of Lemma 6.1, we will use the fact that if t ≡ vo s then t and s are mapped on the same net. We also claim-without proving it-that ≡ vo is exactly the quotient induced on terms by the translation to nets.

Paths. A path τ of length k ∈ N from u to w, noted τ : u → k w, is an alternated sequence of nodes and links

u = u 1 , l 1 , . . . , l k , u k+1 = w s.t. link l i has source u i and target u i+1 for i ∈ {1, . . . , k}. A cycle is a path u → k u with k > 0. ' & $ % x = if y / ∈ fv(t) ∪ ∆ then t ∆∪{y} = ! d t ∆ w if x ∈ fv(t), λx.t = if x / ∈ fv(t), λx.t = ! t `! t w ìf x ∈ fv(s), xs = if x / ∈ fv(s), xs = ⊗ s d ⊗ s d if x ∈ fv(t), (λx.t)s = if x / ∈ fv(t), (λx.t)s = ⊗ s t `. . . { fv(t)∩fv(s) ⊗ s t w `. . . { fv(t)∩fv(s) if x ∈ fv(t), t[x s] = if x / ∈ fv(t), t[x s] = t s . . . { fv(t)∩fv(s) t w s . . . { fv(t)∩fv(s)
Figure 3: the translation from terms to nets.

Correctness. The correctness criterion is based on the notion of correction graph, which-as usual for nets with boxes-is obtained by collapsing boxes into generalized axiom links, i.e. our -links (see Fig. 1).

Definition 4.3 (Correction Graph). Let P be a net. The correction graph P 0 of P is the directed hypergraph obtained from P by collapsing each `-box at level 0 in P into a -link (with the same interface) by applying the rule in Fig. 2.c.

Definition 4.4 (Correctness).

A net P is correct if:

Root: the root of P induces the only initial node of P 0 .

Acyclicity: P 0 is acyclic.

Recursive Correctness: the box of every `-link at level 0 is correct.

As usual an easy induction on the translation shows that the translation of a term is correct, i.e. that: Lemma 4.5. Every proof net is correct, i.e. t ∆ is a correct net for every term t and set of variables ∆.

Note that the root correctness condition forbids the existence of isolated nodes. In logical terms, it forbids isolated axioms. Such a restriction is not ad-hoc, as it is also used in the call-by-name translation of λ-calculus to proof nets. Additional shape constraints are indeed required when proof nets are supposed to represent terms: some nets that would be considered correct proofs do not represent any λ-term and have to be rejected. Another shape constraint is the requirement that nets free variables are weakenings and derelictions (see Definition 4.1).

Proof Nets: Sequentialization

In this section we show how to extract a term t from every correct net P in such a way that t translates back to P , i.e. we show that every correct net is a proof net. The proof of such a sequentialization theorem is based on the notion of kingdom, along the lines of the proof for polarized nets by Olivier Laurent, see [START_REF] Laurent | Étude de la polarisation en logique[END_REF], pp. 57-63.

The study relies on the notion of subnet Q of a correct net P , that is a subset of the links of P plus some closure conditions, avoiding that Q prunes the interior of a box in P , or takes part of the interior without taking the whole box, or takes only some of the premises of an internal contraction. Definition 5.1 (Subnet). Let P be a correct net. A subnet Q of P is a subset of its links s.t. it is a correct net (wrt the box function inherited from P ) and satisfies the following closure conditions: Contractions: l ∈ Q for any link l ∈ P having as target an internal e-node of Q.

Boxes:

Root: box(h) ⊆ Q for any `-link h ∈ Q. Free variables: box(l) ⊆ Q if a free variable of box(l) is internal to Q.
To ease the language, we also give a name to the nodes that can be the root of a subnet. Definition 5.2 (Royal Node). Let P be a net. A royal node x of P is a e-node such that it is not a free variable of P (i.e. x / ∈ fv(P )) and it is not the variable (i.e. not the e-source) of a `-link, or-equivalently-such that it is the source of a !-link or of a ⊗-link.

Next, we define the kingdom of a royal node x, that will be proved to be the smallest subnet of root x (forthcoming Lemma 5.6). Definition 5.3 (Kingdom). Let P be a correct net and x one of its royal nodes. The kingdom king P (x) of x in P is the set of links defined by case analysis on the link l of source x: l is a !-link: king P (x) is given by l plus the d-link or the `-box on the m-target of l. l is a ⊗-link: king P (x) is given by l plus the d-link or the `-box on the m-target of l plus king P (y), where y is the e-target of l.

It is easily seen that king P (x) does not really depend on P , in the following sense.

Lemma 5.4. Let P be a correct net, Q be a subnet of P , and x be a royal node of Q (and thus of P ). Then king P (x) = king Q (x).

Proof. By induction on the length of the maximum directed path from x in Q 0 . Therefore, most of the time we will simplify and simply write king(x) (instead of king P (x)).

To characterize kingdoms the following definitions are required.

Definition 5.5 ((Free/Ground) Substitution). Let P be a correct net. An enode x of P is:

a substitution if it is the target of a {w, d}-link (or, equivalently, if it is not the target of a ⊗-link nor the root) and the source of some link;

a ground substitution if it is a substitution which is a node of P 0 (i.e. it is not internal to any `-box 4 ); a free substitution if it is a ground substitution and there is no ground substitution of P to which x has a path (in P 0 ). Now, we show that kingdoms are indeed minimal subnets. At the same time, we prove some additional properties of kingdoms to be used in the next lemmas.

Lemma 5.6 (Kingdom). Let P be a correct net and x one of its royal nodes. Then king(x) is the smallest subnet of P of root x. Moreover, it has no free substitutions, no free weakenings, and whenever y ∈ fv(king(x))

1. Connected Interface: x has a path to y in king(x) 0 ; 2. Atomicity: if y is internal to a subnet Q of P then king(x) ⊆ Q.

Proof. Let R be a correct subnet of P rooted at x. By induction on the length of the maximum directed path from x in P 0 (that exists because by correctness P 0 is acyclic) we show that king(x) ⊆ R and that king(x) is correct. Let l be the link of source x. Cases of l:

Base case: l is a !-link. By the free variables condition for pre-nets R has to contain the d-link h or the `-link on the m-target of l. In the case of a `link the box root condition for subnets implies that the whole box B is in R, hence king(x) ⊆ R. In the case of a d-link correctness is obvious, in the case of a `-box it follows by the correctness of the box itself, guaranteed by the recursive correctness condition. Moreover, no free substitutions and no free weakenings belong to king(x) (by the border condition for nets boxes cannot close on weakenings). Pick y ∈ fv(king(x)), which in the d-link case is the target of h and in the other case is a free variable of the `-box B. Now, 1. Connected Interface: if y is the target of the d-link then there is a path from x to y, given by the only path going through the !-link and the d-link. If y is a free variable of the `-box, then there is a path from x to y in king(x) 0 , the one which goes through the !-link and the -link replacing the `-box in king(x) 0 . 2. Atomicity: if y is internal to a given subnet Q then the contractions condition for subnets guarantees that h or B are in Q. Then clearly king(x) ⊆ Q.

Inductive case: l is a ⊗-link. As in the previous case, R has to contain the d-link or the `-box on the m-target of l (by the free variables condition for pre-nets). Consider the e-target z of l, that is a royal node of both P and R (by the free variables condition for pre-nets it cannot be a free variable). By i.h., king R (z) ⊆ R and by Lemma 5.4 (stating king R (z) = king P (z), simply noted king(z)) it follows king(z) ⊆ R, in turn implying king(x) ⊆ R. By i.h., king(z) is also correct, hence z verifies the root correctness condition for king(z), and so does x for king(x). Acyclicity follows by correctness of P . Recursive correctness follows from the box closure condition for subnets and correctness of P . Thus king(x)

is the smallest subnet of P of root x. Moreover by i.h., king(z)-and so king(x)-has no free substitutions and no free weakenings. Connected interface and atomicity follow from the i.h. for the free variables of king(z) and from the conditions for a subnet (as in the previous case) for the other free variables.

A key property for the read-back of a correct net as a term is given by the following lemma, that is a sort of splitting tensor lemma, stating that free substitutions are splitting.

Lemma 5.7 (Substitution Splitting). Let P be a correct net with a free substitution x. Then 1. The free variables of king(x) are free variables of P . 2. P \ king(x) is a subnet of P .

Proof.

1. Suppose not. Then there is a free variable y of king(x) which is not a free variable of P . There are two possible cases:

y is a substitution of P . By the connected interface part of Lemma 5.6, x has a path to y in king(x) 0 , i.e. to a substitution in P 0 , which is also a path in P 0 . But such a path contradicts the hypothesis that x is a free substitution, absurd.

y is the distinguished free variable of a `-box B. Thus, y is internal to some `-box B and so it is not a node of P 0 . By the atomicity part of Lemma 5.6, king(x) ⊆ B and so x is not a node of P 0 , against the definition of free substitution, absurd.

2. By point 1 the removal of king(x) cannot create new initial nodes. Being a substitution, x is the target of some link. Therefore the removal of king(x) cannot remove the root of P . It is also clear that the removal cannot create cycles, and the box closure condition for subnets guarantees that the recursive correctness of P implies the one of P \ king(x).

Of course, we need to show that as long as there are substitutions out of boxes (i.e. ground substitutions) there are free substitutions, i.e. that the substitution splitting lemma can be applied. Lemma 5.8. Let P be a correct net with a ground substitution. Then P has a free substitution.

Proof. Consider the following order on the elements of the set S g of ground substitutions of P : z ≤ y if there is a path from z to y in P 0 . Acyclicity of P 0 implies that S g contains maximal elements with respect to ≤, if it is nonempty. Note that a maximal element of S g is a free substitution in P . Now, if P has a ground substitution x then S g is non-empty. Thus, P has a free substitution.

The two previous lemmas together imply that ground substitutions can be removed one after the other, by repeatedly selecting a free one, until none of them are left. The next lemma show that what is left after these removals is exactly the kingdom of the root. Lemma 5.9 (Kingdom Characterization). Let P be a correct net. Then P = king(r P ) iff P has no free substitutions nor free weakenings.

Proof. ⇒) By Lemma 5.6. ⇐) By Lemma 5.6, king(r P ) ⊆ P . If the two do not coincide then by the contractions condition for subnets, the multiplicative condition on nets, and the fact that they share the same root, it follows that P contains a ground substitution x on a free variable of king(r P ). Then, P contains a free substitution by Lemma 5.8, absurd.

We conclude the section with the sequentialization theorem, that relates terms and proof nets at the static level.

Theorem 5.10 (Sequentialization). Let P be a correct net and ∆ be the set of e-nodes of its free weakenings. Then there is a term t s.t. t ∆ = P (and fv(P ) = fv(t) ∪ ∆).

Proof. By induction on the number of links of P . By the root and free variables conditions the minimum number of links is 2 and the two links are necessarily a !-link on top of a d-link. Let x be the e-node of the d-link. Then x = P . We now present each inductive case. After the first one we assume that the net has no free weakenings.

There is a free weakening l of e-node x. Then P = P \{l} is still a correct net and by i.h. there exist t s.t. t ∆\{x} = P . Then t ∆ = P .

There is a free substitution x. Then by Lemma 5.6 and Lemma 5.7 king(x) and P \ king(x) are correct subnets of P . By the i.h. there exist s and u s.t. s = king(x) and u {x} = P \ king(x) (note that if x ∈ fv(u) then

u {x} = u ∅ = u). Then u[x s] = P .
No free substitutions: by Lemma 5.9 P = king(r P ). For the root link l of P , of source r P , there are three cases: l is a !-link over a d-link : base case, already treated. l is a !-link over a `-link : let Q be the box of the `-link and x its distinguished free variable. By the border condition for a net the set of free weakenings of Q either is empty or it contains only x. If x is (resp. is not) the node of a free weakening then by i.h. there exists t s.t.

t {x} = Q (resp. t = Q). Then λx.t = P .
l is a ⊗-link : let x be its e-target and a its m-target. Note that P = king(r P ) implies that P is composed by l, king(x) and either the d-link or the `-link (plus its box) on a. By i.h. there exists s s.t. s = king(x). Now, if a is the source of a d-link of e-node y we Let us prove that Q and king(x) can only share free variables, as the translation prescribes: no link at level 0 of king(x) can be in Q, and no box at level 0 of king(x) can intersect Q other than on free variables, by the nesting condition. By reasoning about the distinguished free variable of Q as in the previous case we then obtain (λy.u)s = P .

' & $ % ⊗ `→m w ! Q . . . m 1 m k → e w w . . . m 1 m k . . . x d d ! Q . . . m 1 m k → e Q 1 Q k . . . . . . m 1 m k

Proof Nets: Dynamics

The rewriting rules are in Fig. 4. Let us explain them. First of all, note that the notion of cut in our syntax is implicit, because cut-links are not represented explicitly. A cut is given by a node whose incoming and outgoing connections are principal (i.e. with a little dot on the line).

Rule → m is nothing but the usual elimination of a multiplicative cut, except that the step also opens the box associated with the `-link.

The two → e rules reduce the exponential redexes. Let us explain how to read them. The graph noted Q in Fig. 4 is the induced box of the !-link (see the paragraph induced !-boxes in Sect. 4). There are in fact two possibilities: either it is simply a d-link or it is a `-link with its box, so there is no ambiguity on what to duplicate/erase. Every pair of short gray lines denotes the sequence (of length m i , with i ∈ {1, . . . , k}) of boxes closing on the corresponding links. The rule has two cases, one where !-link is cut with k ∈ {1, 2, . . .} derelictions and one where it is cut with a weakening. In the first case the subgraph Q is copied k times (if k = 1 no copy is done) as Q 1 , . . . Q k and each copy enters the m i boxes enclosing the corresponding (and removed) dereliction. Moreover, the k copies of each free variable of Q are contracted together, i.e. the nodes are merged. In the case of a cut with a weakening, Q is erased and replaced by a set of weakenings, one for every free variable of Q. Note that the weakenings are also pushed out of all boxes closing on the free variables of Q5 . This is done to preserve the invariant that weakenings are always pushed out of boxes as much as possible. Such an invariant is also used in the rule: note that the weakening is at the same level of Q. Last, if the weakenings created by the rule are contracted with any other link then they are removed on the fly, because by definition weakenings cannot be contracted. Now, we establish the relationship between terms and nets at the level of reduction. Essentially, there is only one fact which is not immediate, namely that → e actually implements the → e rule on terms, as it is proved by the following lemma.

Lemma 6.1 (Substitution). Let t = s[x L v ] then t ∆ → e L s{x v}
∆ for any set of names ∆ ⊇ fv(t).

Proof. First of all observe that t = s[x L v ] and L s[x v] both reduce to L s{x v} and by Remark 4.2 both translate to the same net. Hence it is enough to prove that L s[x v]

∆ → e L s{x v} ∆ . We prove it by induction on L. For L = • the proof is by induction on the number n of free occurrences of x in s. Cases:

n = 0) In s[x L v ]
∆ the !-link associated to v is cut with a weakening. The elimination of the cut produces a net P without the !-link and the `-box associated to v, leaving a free weakening for every free variable of the box, i.e. of every free variable of v: then P is exactly s{x v} ∆∪fv(v) = s ∆∪fv(v) .

n > 1) Write s = C x for some occurrence of x. Now, consider u = C y [y v][x v] and note that:

u → C v [x v] → C v {x v} = s{x v}
The difference between P = u ∆ and P

= s[x v]
∆ is that one of the occurrences of x in P has been separated from the others and cut with a copy of v. Consider the step P → Q which reduces the cut on x in P and the sequence P → Q y → Q y,x which first reduces the cut on y in P and then reduces in Q the (unique) residual of the cut on x in P . By the definition of reduction in nets Q = Q y,x . Now, the i.h. applied to u and y gives The next theorem expresses the perfect match between rewriting steps on terms and rewriting steps on proof nets, and it is the main result of the paper. Strong bisimulations preserve reduction lengths, so they preserve divergent/normalizing reductions, and termination properties in general. Corollary 6.3. Let t ∈ λ vker and ∆ a set of variables. Then t is weakly normalizing/strongly normalizing/a normal form/weakly divergent/strongly divergent iff t ∆ is.

C v [x v] ∆ = Q y and the i.h. applied to C v [x v] and x provides C v {x v} ∆ = Q y,x . From Q = Q y,
Actually, the translation is more than a strong bisimulation: the reduction graphs6 of t and t are isomorphic, not just strongly bisimilar. An easy but tedious refinement of the proof of Theorem 6.2 (consisting in specifying the bijection of redexes) proves: Theorem 6.4 (Dynamic Isomorphism). Let t be a term and ∆ a set of variables containing fv(t). The translation induces a bijection φ between the redexes of t and the redexes of t ∆ s.t. R : t → a t if and only if φ(R) : t ∆ → a t ∆ , where a ∈ {m, e}.

A nice by-product of our approach is that preservation of correctness by reduction comes for free, since any reduct of a proof net is the translation of a term. Corollary 6.5 (Preservation of Correctness). Let P be a proof net and P → P . Then P is correct.

Note that there is no contradiction between 1) the fact that the translation is not injective, and 2) the dynamic isomorphism between terms and proof nets. As pointed out in Remark 4.2, the lack of injectivity of the translation induces a quotient on terms: each equivalence class contains all and only the different sequentialization of a proof net, or, equivalently, all the terms translating to the same proof net. This does not forbid every term in the class to behave isomorphically to the corresponding proof net (and thus, by transitivity, isomorphically to any other term in its class).

A strong bisimulation is enough for transporting termination properties between the two systems. For confluence, instead, a priori the situation is slightly different. In general, both strong bisimulations and dynamic isomorphisms transport confluence only modulo the quotient induced by the translation. Mild additional hypothesis allow to transfer plain confluence, see [1] (pp. 83-86) for more details. Our case however is simpler, as we want to transport confluence from terms to proof nets and the quotient induced on proof nets is the identity, i.e. here confluence modulo actually coincides with plain confluence. Then from confluence of λ vker it follows that: Theorem 6.6. Proof nets are confluent.

The Original Boring Translation. For the sake of completeness, Fig. 6 sketches the ordinary CBV translation from λ-terms (possibly with iterated applications) to proof nets (including the case for explicit substitutions and using a traditional syntax with boxes on !-links). An easy computation shows that the term t = (λz.δ)(yy)δ, where δ = λx.xx maps to a net without normal form, while t is a λ βv -normal form. As already mentioned, this mismatch is the motivation behind our work.

Proof Nets: Comments and Literature

Motivating `-boxes

The call-by-name (CBN) and call-by-value (CBV) encodings of λ-calculus into linear logic (LL) can be seen as fragments of Intuitionistic Multiplicative and Exponential LL (IMELL). Let us stress that in IMELL what we noted ⊗ and `correspond to the right and left rules for the linear implication , and not to the left and right rules for ⊗. The four rules for ⊗ and are collapsed in LL but not in Intuitionistic LL, in particular our `acts on the output of the term, i.e. on the right of the sequent, and corresponds to the right rule for .

Our argument is that in IMELL there is no correctness criterion unless the syntax is extended with boxes for both ! and (our `), as we shall explain in

' & $ % x = λx.t = ts = t[x s] = ! t ! `⊗ s d t . . . { fv(t)∩fv(s) t s . . . { fv(t)∩fv(s)
Figure 6: the ordinary CBV translation from terms to nets.

the next paragraphs. In particular, the two encodings of λ-calculus turn out to be dual special cases with respect to the use of boxes, in the following sense

• The fragment of IMELL encoding the CBN λ-calculus is a special case where the box for needs not be represented.

• The fragment of IMELL encoding the CBV λ-calculus is a special case where the box for ! needs not be represented.

Therefore, our use of `-boxes actually unveils a nice symmetry, rather than being ad-hoc. In the literature there are occurrences of explicit boxes for abstractions (at least in [START_REF] Mackie | Efficient lambda-Evaluation with Interaction Nets[END_REF][START_REF] Hendriks | adbmal[END_REF]), but none of these works studies correctness.

The difficulty of designing a correctness criterion for IMELL is given by the presence of weakenings, that break connectedness. In most cases weakenings simply prevent the possibility of a correctness criterion. The fragment encoding the CBN λ-calculus, and more generally Polarized Linear Logic, are notable exceptions. For the encoding of the CBN λ-calculus there exist two correctness criteria. Let us show that none of them works for the CBV λ-calculus: 1. Danos and Regnier's criterion, in the variant replacing connectedness with the requirement that the number of connected components of every switching graph is 1 + #w, where #w is the number of weakenings at level 0 (after the collapse of boxes) [START_REF] Regnier | Lambda-calcul et réseaux[END_REF]. In our case this criterion does not work: the net in Fig. 7.a verifies the requirement while it does not represent any proof or term. Note that adding boxes to the !-links of the example does not change anything. 2. Laurent's polarized criterion [START_REF] Laurent | Polarized proof-nets and λµ-calculus[END_REF][START_REF] Laurent | Étude de la polarisation en logique[END_REF], because the CBN encoding is polarized. In its original formulation it cannot be applied to the encoding of the CBV λ-calculus, because such a fragment is not polarized (there can be a weakening as a premise of a tensor, which is forbidden in polarized logic).

' & $ % a) w ⊗ ! d w ⊗ ! d `! d b) ⊗ ! d
Our re-formulation of Laurent's criterion (Definition 4.4, page 13) rejects the net in Fig. 7.a (because the two `-links form a cycle), but without using `-boxes it would accept the net in Fig. 7.b, which is not correct7 .

Thus, the known criteria do not work and-more generally-there is no criteria for IMELL. The usual way to circumvent problems about correctness is to add some information to the graphical representation, under the form of boxes (as in this paper) or jumps (i.e. additional connections). It is well known that in these cases various criteria can be used, but this extra information either is not canonical or limits the degree of parallelism. Another possible solution is to modify the logical system adding the mix rules. However, such rules are debatable, and also give rise to a bad notion of subnet (for details see [1], pp. 199-201).

Let us stress that our counterexamples to the known criteria do not rely on the exponentials (i.e. non-linearity): it is easy to reformulate them in Intuitionistic Multiplicative Linear Logic (IMLL) with unit(s) 8 , for which then there is no correctness criterion.

In the case studied in this paper the use of `-boxes does not affect the level of parallelism in a considerable way. Indeed, in IMELL the parallelism of proof nets concerns the left rules (of ⊗ and , plus contractions and weakenings) and cuts: in our case there is no ⊗ (remember our ⊗ and `rather correspond to the rules for ), our technical choices for variables keep the parallelism for contraction and weakenings, and the parallelism of the left rule for (our ⊗) and cuts is preserved (it is given by the equations in (1), page 11).

To best of our knowledge, the observations reported here-in particular those about the lack of correctness criteria-are an original contribution of this work.

Literature on Term Representations

The relationship between λ-terms and proof nets presents a number of technical choices:

1. Explicit Substitutions, or Sharing: proof nets implement a β-step by (at least) two cut-elimination steps. This refined evaluation can be seen on the calculus only if the syntax is extended with explicit substitutions, that are nothing else but explicit sharing annotations. 2. Variables: to properly represent variables it is necessary to work modulo associativity and commutativity of contractions, neutrality of weakening with respect to contraction, and permutations of weakenings and contractions with box-borders. In the literature there are two approaches: to explicitly state all these additional congruences or to use a syntax naturally quotienting with respect to them. Such a syntax uses n-ary ?-links collapsing weakening, dereliction and contractions and delocalizing them out of boxes. It is sometimes called nouvelle syntaxe. 3. Axioms: various complications arise if proof nets are presented with explicit axiom and cut links. They can be avoided by working modulo cuts on axioms, which is usually done by employing an interaction nets presentation of proof nets. 4. Exponential Cut-Elimination: cut-elimination rules for the exponentials admit many presentations. Most of the time, either they are small-step, i.e. an exponential cut is eliminated in one shot (making many copies of the !-premise of the cut), or they are micro-step, with a rule for each possible ?-premise (weakening, dereliction, contraction, axiom, box auxiliary port).

Let us classify our study along these axes. We employ explicit substitutions and small-step exponential cut-elimination. For the representation of variables and axioms, instead, we depart from the literature and propose an alternative approach, the use of hypergraphs. Hypergraphs allow at the same time to mimic n-ary ?-links and collapse axioms and cut links as if we were using interaction nets. More precisely, we represent n-ary ?-links by allowing e-nodes to have more than one incoming link. This choice overcomes some technicalities about gluing and degluing of ?-links. Such technicalities are always omitted, but they are in fact necessary to properly define subnets and cut-elimination. In particular, with n-ary ?-links subnets cannot be defined as subsets of links (because of (de)gluing), that turns out to be technically quite annoying (unless one is deliberately less precise and forgets to deal with (de)gluing altogether). Of course, everything we did here could be also done using n-ary ?-links and interaction nets, it is rather a matter of taste.

We now list the works in the literature which are closer in spirit to ours, i.e. focusing on the representation of λ-calculi into proof nets (and thus we omit many other interesting works, as for instance [START_REF] Mackie | Encoding Strategies in the Lambda Calculus with Interaction Nets[END_REF], which studies the representation of strategies, not of calculi ).

The first such works were the PhD thesis of Vincent Danos [START_REF] Danos | La Logique Linéaire appliqué à l'étude de divers processus de normalisation (principalement du λ-calcul)[END_REF] and Laurent Regnier [START_REF] Regnier | Lambda-calcul et réseaux[END_REF], that focused on the call-by-name (CBN) translation. Danos and Regnier avoid explicit substitutions, use n-ary contractions, explicit axioms, and small-step exponential rules, see also [START_REF] Danos | Proof-nets and the Hilbert Space[END_REF]. They characterize the image of the translation using the variant of the Danos-Regnier correctness criterion requiring that any switching graph has #w + 1 connected components, where #w is the number of weakenings. In [START_REF] Danos | Reversible, Irreversible and Optimal lambda-Machines[END_REF], Danos and Regnier use the CBV translation 9 . Both translations are injective.

In [START_REF] Laurent | Polarized proof-nets and λµ-calculus[END_REF][START_REF] Laurent | Étude de la polarisation en logique[END_REF] Olivier Laurent extends the CBN translation to represent (the CBN) λµ-calculus. He does not use explicit substitutions nor n-ary ?-links, while he employs explicit axiom links and micro-step exponential rules. His work presents two peculiar points. First, the translation of λµ-terms is not injective, because-depending on the term-the µ-construct may have no counterpart on proof nets. This induces some mismatches at the dynamic level. Second, Laurent finds a simpler criterion (which is the one we used-adapted-in this paper), exploiting the fact that the fragment encoding (the CBN) λµ-calculus is polarized. In [START_REF] Laurent | Étude de la polarisation en logique[END_REF] Laurent also show how to represent the CBV λµ-calculus. However, such a representation does not use the same types as the boring translation, since A → B maps to ?!(A B), and not to !(A B). Lionel Vaux [START_REF] Vaux | λ-calcul différentiel et logique classique: interactions calculatoires[END_REF] and Paolo Tranquilli [START_REF] Tranquilli | Nets Between Determinism and Nondeterminism[END_REF][START_REF] Tranquilli | Intuitionistic differential nets and lambda-calculus[END_REF] study the relationship between the differential λ-calculus and differential proof nets. Vaux also extends the relationship to the classical case (thus encompassing a differential λµ-calculus), while Tranquilli refines the differential calculus into a resource calculus that better matches proof nets. They do not use explicit substitutions, nor n-ary contractions, while they use interaction nets (so no explicit axioms and cut link) and micro-step exponential rules. Both Tranquilli and Vaux rely on the Danos-Regnier criterion, despite the fragment encoding their calculi is polarized and can be captured using Laurent's criterion by using boxes for coderelictions; in the context of λ-calculus such boxes do not reduce the parallelism of the representation.

Delia Kesner and co-authors [START_REF] Di | Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract)[END_REF][START_REF] Di | Proof Nets And Explicit Substitutions[END_REF][START_REF] Kesner | Resource operators for lambdacalculus[END_REF] study the relationship with explicit substitutions in the CBN case. The main idea here is that explicit substitutions correspond to exponential cuts. They use explicit axiom links and micro-step exponential rules, but they do not employ n-ary contractions (and so they need additional rules and congruences). Because of explicit substitutions the translation is not injective: now different terms may map to the same proof net, as in this paper. They do not deal with correctness criteria.

In none of these works the translation is an isomorphism of rewriting systems nor a strong bisimulation. In [START_REF] Accattoli | Jumping Boxes[END_REF] Stefano Guerrini and the author use a syntax inspired by proof nets (and extended with jumps) to represent the CBN λcalculus with explicit substitutions. That work is the only one employing at the same time (the equivalent of) n-ary ?-links and (the equivalent of) micro-step exponential rules. In [START_REF] Accattoli | Jumping Boxes[END_REF] the correctness criterion is a variation over Lamarche's criterion for essential nets [START_REF] Lamarche | Proof Nets for Intuitionistic Linear Logic: Essential Nets[END_REF], which relies in an essential way on the use of jumps. A reformulation in the syntactic style of this paper of both [START_REF] Accattoli | Jumping Boxes[END_REF] and of Danos and Regnier's proof nets for the CBN λ-calculus can be found in [1], together with a detailed account of the strong bisimulation.

Last, a nice and detailed introduction to the relationship between λ-terms and proof nets is Guerrini's [START_REF] Guerrini | Proof nets and the lambda-calculus[END_REF].

Terms: Relating λ vsub and λ vker

In this section we study the relationship between λ vsub and λ vker . The results of this paper actually allow to read this section as if we were relating λ vsub and proof nets, given that λ vker and proof nets are isomorphic. In particular, by composing the (forthcoming) translation from λ vsub to λ vker and the translation from λ vker to proof nets (Sect. 4) one obtains a translation from λ vsub to proof nets. We believe, actually, that our isomorphism between terms and proof nets shines at its best here: having an algebraic language for proof nets we can relate them to λ vsub at a level of detail and rigor that would be impossible if we had to deal directly with the graphical syntax.

Projecting λ vsub on λ vker

This subsection shows that λ vsub has an interpretation inside λ vker .

Notation: when we want to stress that a term is in λ vker we use capital letters.

Any term M ∈ λ vker is a term of λ vsub . Moreover, on λ vker terms the rules of λ vsub collapse on the rules of λ vker . Then, M → λ vker N iff M → λ vsub N , for any M ∈ λ vker . Hence, λ vker is a subcalculus of λ vsub which is stable by reduction, and so Lemma 8.1. M ∈ λ vker is λ vker -strongly (resp. weakly) normalizing iff λ vsubstrongly (resp. weakly) normalizing.

However, there are terms of λ vsub which are not terms of λ vker . The purpose of this section is to show that these terms can be faithfully simulated in λ vker via an appropriate translation.

The translation • k : λ vsub → λ vker is defined as follows:

x k := x (λx.t) k := λx.t k t[x s] k := t k [x s k ] (L v s) k := L k v k s k (L ts u) k := (xu k )[x L ts k ]
where x is fresh

• k := • L[x t] k := L k [x t k ]
There is a slight mismatch between reductions in λ vsub and in λ vker . Sometimes a → m step in λ vsub is simulated by a single → m step in λ vker , while sometimes it requires an additional → e step. Consider t := (λx.λy.t)su, that translates to t k = (zu k )[z (λx.λy.t k )s k ] with z fresh. We have:

t → m (λy.t)[x s]u =: t But t k → m (zu k )[z (λy.t k )[x s k ]] → e ((λy.t k )u k )[x s k ] = t k
It is quite obvious that λ vker can simulate λ vsub with only a linear overhead (in terms of number of rewriting steps), because every step in λ vsub can be simulated by at most two steps in λ vker . We shall however prove this formally in the rest of this section. It is less obvious that any reduction sequence in λ vker can be extended with a linear number of steps so that it represents a reduction sequence in λ vsub . This will be shown in the next section, and will require some commutation properties. The two results together will provide the equivalence with respect to termination of λ vsub and λ vker , as we will show in Sect. [START_REF] Accattoli | The Structural λ-Calculus[END_REF] The left subterm is a value in a substitution context, i.e. s = L v . Then:

t{x v} k = (L v u){x v} k let L := L{x v} = (L v {x v} u{x v}) k let L := L k {x v k } = L v {x v} k u{x v} k = i.h. L v k {x v k }u k {x v k } = L k v k u k {x v k } = t k {x v k } 3.
Projection and reflection of a → e step. The reasoning is analogous to the case t = u[x r].

The left subterm is an application in a substitution context: t = L up r and t k = (yr k )[y L up k ], with y fresh. If the reduction takes place in u, p, r, L, u k , p k , r k , or L k then it follows from the i.h.. Otherwise:

1. Projection of a → m step. If u = L λx.q then t → m L L q[x p] r = s and

t k = (yr k )[y L L λx.q p k ] = (yr k )[y L k L k (λx.q k )p k ] → m (yr k )[y L k L k q k [x p k ] ] = N
Now, there are two cases, depending on the shape of q: (a) q is a value in a substitution context, i.e. q = L v . Then

s = L L q[x p] r = L L L v [x p] r and N = (yr k )[y L k L k L v k [x p k ] ] = (yr k )[y L k L k L k v k [x p k ] ] → e L k L k L k v k r k [x p k ] = s k (b) q is an application in a substitution context, i.e. u = L qm : then s = L L L qm [x p] r and N = (yr k )[y L k L k L qm k [x p k ] ] = s k 2. Reflection of a → m step. If t k = (yr k )[y L k u k p k ]
has a mredex not contained in one of the subterms then necessarily u k = L λx.Q and so u = L λx.q with q k = Q and L k = L . Then the proof repeats the reasoning of the previous point. The relationship between → m steps in the two calculi (given by Point 1 and Point 2 of Theorem 8.3) then becomes:

1. If t → m s then either t k → m s k or t k → m → adj s k . 2. If t k → m N then there exists s s.t. t → m s and either s k = N or N → adj s k .
Let us explain the technical difficulty in reflecting reductions from λ vker to λ vsub . Suppose that:

1. t k → λ vker s 1 → +
λ vker s is a reduction sequence whose first step t k → λ vker s 1 requires an adjusting step s 1 → adj u in order to be the simulation of a step t → m r on λ vsub (with r k = u), and that 2. this adjusting step s 1 → adj u is not the first step of the suffix s 1 → + λ vker s. In terms of diagrams we have:

t k s 1 s u m + adj
Then we have to show that the reduction sequence s 1 → + λ vker s and the adjusting step s 1 → adj u commute, i.e. that there exists p s.t. i.e. that doing first the adjusting step we do not forbid the computation in the suffix s 1 → + λ vker s to take place (translated as a reduction sequence u → * λ vker p). However, to later relate termination properties of λ vsub and λ vker we need a bit more than that. In fact, commutation of → adj and → λ vker is in itself trivial, because → e commutes with → λ vker and a → adj step is a → e step. What we need to show is that this commutation does not change the length of reduction sequences in a way which may affect termination. Technically, this will be given by the fact that commutation with → adj does not change the number of m-steps (in contrast to commutation with → e ).

= s k 1 or u 1 → adj s k 1 . Cases:
No need of an adjusting step, i.e. u 1 = s k 1 . Then by i.h. applied to s k 1 = u 1 → k-1 N there exists s s.t. s 1 → ≤k-1 s, N → * adj s k , and the two derivations s 1 → ≤k-1 s and s k 1 = u 1 → k-1 N have the same number of m-steps. Then t → λ vsub s 1 → ≤k-1 s has length ≤ k and we conclude, because the step t k → λ vker u 1 is a m-step iff t → λ vsub s 1 is.

An adjusting step is required, i.e. u 1 → adj s k 1 . Then both t k → λ vker u 1 and t → λ vsub s 1 are m-steps. By Lemma 8.7 applied to u 1 → adj s k 1 and the suffix u 1 → k-1 λ vker N there exists Q s.t. s k 1 → ≤k-1 λ vker Q and N → * adj Q, and moreover both derivations s k 1 → ≤k-1 λ vker Q and u 1 → k-1 λ vker N have the same number of m-steps. Now, let's apply the i.h. to s k 1 → ≤k-1 λ vker Q: we obtain s s.t. s 1 → ≤k-1 λ vsub s and Q → * adj s k , and moreover both derivations s k 1 → ≤k-1 λ vker Q and s 1 → ≤k-1 λ vsub s have the same number of m-steps, which is the same of u 1 → k-1 λ vker N . We have proved the statement, because 1. N → * adj Q and Q → * adj s k , i.e. N → * adj s k ; 2. t → m s 1 → ≤k-1 λ vsub s has length ≤ k, and 3. this derivation has the same number of m-steps of t k → m u 1 → k-1 λ vker N .

Relating Normalization Properties

Here we use the results of this section to relate termination properties in λ vsub and λ vker , in particular we show that the translation • k of λ vsub to λ vker preserves λ vsub -strong normalization. Weak Reduction. In CBV an important notion of evaluation is weak reduction, which contracts only the redexes which are not under abstractions. We now show that Theorem 8.9 holds also for weak reduction. Formally, a weak context is given by:

W ::= • | W t | tW | W [x t] | [x W ]
Weak reduction → w is defined as the union of → wm and → we , which are obtained as the closure by weak contexts of → m and → e . Weak reduction → w has the diamond property [START_REF] Accattoli | Call-by-Value Solvability, Revisited[END_REF], i.e. if s 1 w ← t → w s 2 and s 1 = s 2 then there exists u s.t. s 1 → w u w ← s 2 .

By looking at its proof it is easy to see that Theorem 8.3 holds also if any step in the statements is a weak step, because the map • k is defined on abstraction as (λx.s) k := λx.s k and so any step under a λ in a term t is mapped to a step under a λ in t k , and viceversa. In particular, t is a weak normal form iff t k is (so also Theorem 8.9.1 adapts to weak reduction). The lifting lemma (Lemma 8.8) is based on Theorem 8.3 and the commutation property of Lemma 8.7. The diamond property of weak reduction is stronger than the property in Lemma 8.7, thus the lifting lemma holds also with respect to weak reductions.

Then, all the reasoning in Theorem 8.9.2 is also valid with respect to weak reductions and gives the following theorem (whose statement is simpler than Theorem 8.9.2 because the diamond property implies that strong and weak normalization are equivalent for → w ): Theorem 8.10. Let t ∈ λ vsub . Then t has a weak normal form iff t k has a weak normal form.

Stratified Weak Reduction. The main result of [START_REF] Accattoli | Call-by-Value Solvability, Revisited[END_REF] is that a term of λ vsub is solvable if and only if it has a normal form with respect to a notion of reduction therein called stratified weak. A natural question is if such a characterization is stable by • k . Let us define stratified weak reduction. Define head contexts as:

H ::= • | Ht | λx.H | H[x t]
Note that head contexts are not weak, as they go under abstractions. Now, define stratified weak reduction → sw as the union of → swm and → swe , defined as follows The idea is that stratified weak reduction allows weak reduction to go under abstraction, but only under head abstractions. While → sw -steps are reflected by • k , it is easily seen that they are not projected. The However, it is true that t ∈ λ vsub has a → sw -normal form iff t k ∈ λ vker has a → sw -normal form. The point is that in order to prove this result one needs to pick a particular → sw -evaluation to normal form. Let us sketch the idea.

Rule
By using the axioms of [START_REF] Accattoli | An Abstract Factorization Theorem for Explicit Substitutions[END_REF], one can easily show that → sw factors by levels: any derivation t → * sw s can be reorganized so that one first reduces all the → swredexes out of all abstractions, then those under the first head abstraction, and so on. In particular, if there is a derivation to → sw -normal form then there is one of this shape. Now, → sw -derivations by levels to normal form do project via • k , roughly because the counterexample we showed is ruled out (note that it lies under a → swm redex at a lower level).

Acknowledgements. To Stefano Guerrini, for introducing me to proof nets, correctness, and the representation of λ-terms; to Giulio Guerrieri, who took a very close look to this work and pointed out many inaccuracies; to the reviewers, who provided useful comments and corrections.

[1] Beniamino Accattoli (2011): Jumping around the box: graphical and operational studies on λ-calculus and Linear Logic. PhD thesis, La Sapienza University of Rome.

  e ⊥ `e ⊗ m = e ⊥ `e e e ⊥ `m e e . . .

Figure 1

 1 Figure 1: links.

  and |box(h)| ⊆ |box(l)| then all the nodes in I are free variables of both box(l) and box(h).

Figure 2 :

 2 Figure 2: various images.

Typing.

  Nets are typed using a recursive type o = !(o o), that we rename e = !(e e) = !(e ⊥ `e) because e is a mnemonic for exponential. Let m := e e = e ⊥ `e, where m stands for multiplicative. Note that e = !m and m = !m !m. This shows that the two translations of λ-calculus into linear logic identified by the two recursive types e = !(e e) and m = !m !m are in fact the same. Links are typed using m and e, but the types are omitted by all figures except Fig. 1 because they are represented using colors and with different shapes (m-nodes are brown and dot-like, e-nodes are white-filled cyan circles).

Figure 4 :

 4 Figure 4: proof nets cut-elimination rules

  x and C v {x v} = s{x v} we obtain s{x v} ∆ = Q and conclude. n = 1) By induction on s. Some cases: Abstraction. If s = λy.u then by i.h. u[x v] ∆∪{y} → e u{x v} ∆∪{y} and so we obtain λy.(u[x v]) ∆∪{y} → e λy.(u{x v}) ∆∪{y} . Now, observe that λy.(u{x v}) = (λy.u){x v} = t{x v} and that the two nets λy.(u[x v]) ∆∪{y} and (λy.u)[x v] ∆∪{y} have the same reduct after firing the exponential cut on x, and so we obtain (λy.u)[x v] ∆∪{y} → e (λy.u){x v} ∆∪{y} Explicit Substitution. If s = r[y u] then either x ∈ u or x ∈ r. In the first case by Remark 4.2 we obtain that s[x v] ∆ = r[y u][x v] ∆ = r[y u[x v]] ∆ . Now by i.h. u[x v] → e u{x v}. Then we have s[x v] ∆ → e r[y u{x v}] ∆ = r[y u]{x v} ∆ = s{x v} ∆ . The second case is analogous. Application which is an m-redex. If s = (λy.r)u. The case x ∈ u uses Remark 4.2 and the i.h. as in the s = r[y u] case. The case x ∈ r is slightly different. As before ((λy.r)u)[x v] and ((λy.r[x v])u) have the same reduct. By i.h. hypothesis r[x v] → e r{x v} and thus (λy.r[x v])u ∆ → e (λy.r{x v})u ∆ . We conclude since ((λy.r)u)[x v] ∆ → e ((λy.r{x v})u) ∆ = ((λy.r)u){x v} ∆ For L = L [y r] the i.h. gives L s[x v] ∆ → e L s{x v} ∆ . By definition of the translation and of graph reduction it follows that L s[x v] [y r] ∆ → e L s{x v} [y r] ∆ .

Figure 5 :

 5 Figure 5: A →m-step on terms and on nets.

Figure 7 :

 7 Figure

Lemma

  • k translation may in fact place head abstractions into explicit substitutions. For instance, t := (λx.((λy.t)s))ur → swm (λx.(t[y s]))ur =: t But (with z fresh) t k = (zr k )[z λx.((λy.t k )s k )] → swm (zr k )[z λx.(t k [y s k ])] = t k

  Theorem 6.2 (Strong Bisimulation). Let t be a term and ∆ a set of variables containing fv(t). The translation is a strong bisimulation between t and t ∆ , i.e. t → a t if and only if t ∆ → a t ∆ , for a ∈ {m, e}. Proof. By induction on the translation. Cases: 1. Variable, i.e. t = x. Trivial, as both t and t ∆ have no redexes. 2. Abstraction or variable application, i.e. t = λx.s or t = xs. The statement immediately follows by the i.h., since all the redexes of t and t ∆ are contained in s and s ∆ , respectively.

	'				$
	(λx.t)s	→ m		t[x s]
		⊗
				t
	s { `. . . t	→ m	s	. . . { fv(t)∩fv(s)
	&	fv(t)∩fv(s)			%

  .3. Lemma 8.2 (Properties of • k ). The translation • k has the following properties:1. Values: t is a value iff t k is a value. 2. Substitutivity: t{x v} k = t k {x v k }. It is immediate that v k is a value. If t kis a value then either t k = x and thus t = x, or t k = λx.N , but by definition of the translation this is only possible if t = λx.s and s k = N . 2. By induction on t. The variable case is trivial and the abstraction case follows from the i.h.. The application case t = su splits into two subcases.

	Proof.
	1.

Notation: given L we define L{x v} as follows • {x v} := • and L[y t] := L{x v}[y t{x v}]. Moreover, to diminish the use of parentheses, we use t{x s} k for (t{x s}) k (as in the statement of Point 2). Subcases:

  3. Projection and reflection of a → e step. The reasoning is analogous to the case t = u[x r]. Corollary 8.4 (λ vker Linearly Simulates λ vsub ). Let t ∈ λ vsub and t → k λ vsub s. Then there exists j s.t. k ≤ j ≤ 2k and t k → j λ vker s k . 8.2. Reflecting λ vker reductions in λ vsub Corollary 8.4 projects reduction sequences in λ vsub on sequences in λ vker . Here we study the converse simulations, i.e. how to simulate an evaluation sequence in λ vker in λ vsub , which is more complex because the relation between m-steps may involve an additional step in λ vker . Let us give a status to such additional steps. Definition 8.5 (Adjusting Reduction). The adjusting rewriting relation t → adj s is defined as follows:

	Rule at Top Level
	(xu)[x L v ] → adj L vu with x / ∈ fv(u)
	Contextual Closure
	C t → adj C s	iff t → adj s
	An immediate consequence is:

  8.6 (Commutations of → adj ). Let t ∈ λ vker . Then: 1. Span of → e and → adj : By induction on t → e s 1 . The case s 1 = s 2 is given by the case in which the → e step is t → adj s 2 . 2. By induction on the length of t → * adj s 2 , using Point 1. 3. By induction on t → m s 1 . 4. By induction on the length of t → * adj s 2 , using Point 3. We can now show the required commutation property. Lemma 8.7 (Commutation of → λ vker and → adj ). Let t ∈ λ vker . Then Moreover, the two derivations t → k s 1 and s 2 → ≤k u have the same number of m-steps. Proof. Simple induction on k, using Lemma 8.6. Now, we are ready to lift reduction sequences from t k to t. As expected they are lifted only modulo an extension by adjusting steps. Lemma 8.8 (Lifting Reduction Sequences from t k to t). Let t ∈ λ vsub and t k → k λ vker N . Then there exists s s.t. t → ≤k λ vsub s and N → * adj s k . Moreover, the derivations t k → k λ vker N and t → ≤k λ vsub s have the same number of m-steps. Proof. By induction on k. If k = 0 there is nothing to prove. Then let k > 0, i.e. t k → λ vker u 1 → k-1 λ vker N . By Theorem 8.3.2 there is a term s 1 s.t. t → λ vsub s 1 and either u 1

	t	e	s 1				t	e	s 1
						implies that either s 1 = s 2 or exists u s.t.
	s 2 adj						s 2 adj	e	adj* u
	2. Span of → e and → * adj :
	t	e	s 1				t	e	s 1
						implies that either s 1 = s 2 or exists u s.t.
	s 2 adj*						s 2 adj*	e	adj* u
	3. Span of → m and → adj :
			t		m	s 1	t	m	s 1
						implies that exists u s.t.
			s 2 adj			s 2 adj	m	adj u
	4. Span of → m and → * adj :
			t		m	s 1	t	m	s 1
						implies that exists u s.t.
			s 2 adj*		s 2 adj*	m	adj* u
	Proof.
	1. t	k	s 1	t	k	s 1
						implies that exists u s.t.
		s 2 adj*			s 2 adj*	u adj* ≤ k

  Theorem 8.9 (• k and Normalization). Let t ∈ λ vsub . 1. t is a normal form iff t k is a normal form. 2. t is strongly (resp. weakly) normalizing iff t k is strongly (resp. weakly) normalizing. Notations: we use d, e, f, g for derivations (i.e. reduction sequences), and note |d| m (resp. |d|) the number of m-steps (resp. steps) in d. . 1. By Theorem 8.3 if t has a redex then t k has a redex, and viceversa. 2. ⇒) we split strong and weak normalization: Strong Normalization. Suppose that t k is not strongly normalizing. Then there is an infinite derivation from t k , i.e. there is a sequence of derivations d k : t k → k λ vker N k for any k ∈ N. By Lemma 8.8 there is a sequence of derivations e k : t → k λ vsub u k from t s.t. |e k | m = |d k | m for k ∈ N. Since → e is strongly normalizing we obtain that the sequence {|d i | m } i∈N cannot be bounded. But |e i | ≥ |e i | m = |d i | m , and so there is an infinite derivation from t, absurd. Weak Normalization. Let t → * λ vsub u and u be a normal form. By Corollary 8.4 there is a reduction t k → * λ vker u k , and by Point 1 u k is a normal form. ⇐) Analogously: Strong Normalization. By Corollary 8.4 any derivation d from t in λ vsub induces a derivation e from t k in λ vker s.t. |d| ≤ |e|, so there cannot be infinite derivations from t. Weak Normalization. Let t k → * λ vker N a reduction to normal form. By Lemma 8.8 there is s s.t. t → * λ vsub s and N → * adj s k . But N is a normal form, and so N = s k . By Point 1 s is a normal form.

	Proof

  at Top Level Contextual Closure L λx.t s → m L t[x s] H W t → m H W s iff t → m s t[x L v ] → e L t{x v} H W t → e H W s iff t → e s

A hypergraph G can be understood as a bipartite graph B G , where V 1 (B G ) is V (G) and V 2 (B G ) is L(G), and the edges are determined by the relations being a source and being a

Here the words maximum and nested are due to the fact that the free variables of `-boxes may belong to two not nested boxes, because of the way we represent contraction.

Note that our collapsed representation of contractions and cuts does not allow to simply say that x is a node at level 0: indeed the free variables of a `-box can have level > 0 and yet belong to P 0 .

Note that, for the sake of a simple representation, the figure of the weakening cutelimination rule is slightly wrong: given free a variable x i of Q, the links l 1 , . . . , l j having x i as target (i.e. l 1 , . . . , l j are all contracted together) are not necessarily all inside m i boxes, as each one can be inside a different number of boxes.

Reduction graphs, which are the graphs obtained considering all reductions starting from a given object, are not nets.

The net in Fig.7.b would be rejected by the original version of the criterion, which is based on a different orientation. But the original orientation cannot be applied to the fragment under study.

Just replace each sequence of a ! over a dereliction with an axiom, and the weakenings with ⊥-links.

Let us point out that[START_REF] Danos | Reversible, Irreversible and Optimal lambda-Machines[END_REF] presents an oddity that we believe deserves to be clarified. The authors show that an optimized geometry of interaction for the proof nets of the CBVtranslation is isomorphic to Krivine Abstract Machine (KAM): this is quite puzzling, because the KAM is CBN, while they use the CBV translation.

The left subterm is an application in a substitution context, i.e. s = L rp . Then:

The next theorem relates the reductions of t and t k .

Proof. By induction on (•) k . The variable case is trivial and the abstraction case follows from the i.h.. The other cases:

If the reduction takes place in u, r, u k , or r k then it follows from the i.h.. Note that → m steps can only take place in subterms of t, so we have proved Point 1 and Point 2. Point 3:

L, and we conclude using the reasoning for the other direction.

Application: two subcases, depending on the shape of the left subterm:

The left subterm is a value in a substitution context: t = L v r and

Reflection of a → m step. If v k = λx.u then v = λx.u with u k = u, and we repeat the same reasoning.