{'fraction_non_alphanumeric': 0.057945619335347434, 'fraction_numerical': 0.01095166163141994, 'mean_word_length': 3.6262054507337527, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 10, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 48, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion

We study the semantics of a resource-sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a"must"parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula. As an intermediate result we prove that the exception mechanism is not essential in the finite sub-calculus.


Introduction
In concurrent calculi like CCS [23], guarded processes are resources that can be used only once by other processes. This fundamental linearity of resources leads naturally to nondeterminism, since several agents (senders and receivers) can interact on the same channel. In general, various synchronization scenarios are possible, giving rise to different behaviours. On the other hand in the λ-calculus [1], a function (receiver) can duplicate its argument (sender) arbitrarily. Thanks to this asymmetry, the λ-calculus enjoys a strong determinism in analogy with the standard Taylor formula of the entire functions. The Taylor expansion has been studied in [14] where the authors relate it to the Böhm tree of a λ-term, giving the intuition that the former is a resource conscious improvement of the latter. The main difference between Boudol's resource λ-calculus and Ehrhard and Regnier's differential λ-calculus is that the first is lazy -this means that in many cases linear substitutions must be delayed. To that effect, the calculus features a linear explicit substitution mechanism. Moreover, it implements a fixed reduction strategy similar to linear head reduction. Therefore, Boudol's calculus is not an extension of the ordinary λ-calculus. Also, the resource λ-calculus is rather affine than linear, since depletable resources cannot be duplicated but can be erased. Another difference lies in the respective origins of these calculi: the resource λ-calculus originates from syntactical considerations related to the theory of concurrent processes, while the differential one arises from denotational models of linear logic where the existence of differential operations has been observed. These models are based on the well-known relational model of Linear Logic [17], and the interpretation of the FULL ABSTRACTION FOR RESOURCE CALCULI 3 new differential constructions is as natural and simple as the interpretation of the ordinary Linear Logic constructions.
In this paper we work with a resource-sensitive λ-calculus because our techniques depend on the linear logic structure underlying the calculus and on the presence of a Taylor expansion formula. Two main syntaxes have been proposed for the differential λ-calculus: Ehrhard and Regnier's original one [11], simplified by Vaux in [31], and Tranquilli's resource calculus of [30] whose syntax is close to Boudol's one. These calculi share a common semantical backbone as well as similar connections with differential Linear Logic and proof nets. We adopt roughly Tranquilli's syntax and call our calculus ∂λ-calculus. To avoid the problem of handling the coefficients introduced by the Taylor formula we conveniently suppose that the formal sum in the calculus is idempotent; this amounts to saying that we only check whether a term appears in a result, not how many times it appears. This is very reasonable when studying convergency properties since M + M converges exactly when M does.
Full Abstraction. A natural problem when a new calculus is introduced is to characterize when two programs are operationally equivalent, namely when one can be replaced by the other in every context without noticing any difference with respect to a given observational equivalence. In this paper we prove a full abstraction result (a semantical characterization of operational equivalence) for the ∂λ-calculus in the spirit of [5]. As in that paper, we extend the language with a convergence testing mechanism. Implicitly, this extension already appears in [10], in a differential linear logic setting: it corresponds to the 0-ary tensor and par cells. To implement the corresponding extension of the λ-calculus, we introduce two sorts of expressions: the terms (variable, application, abstraction, "throw" τ (V ) where V is a test) and the tests (empty test, parallel composition of tests and "catch" τ (M ) where M is a term). Parallel composition allows to combine tests in such a way that the combination succeeds if and only if each test succeeds. Outcomes of tests (convergence or divergence) are the only observations allowed in our calculus, and the corresponding contextual equivalence and preorder on terms constitute our main object of study.
This extended ∂λ-calculus, that we call ∂λ-calculus with tests, has a natural denotational interpretation in a model of the pure λ-calculus introduced by Bucciarelli, Ehrhard and Manzonetto in [8], which is indeed a denotational model of the differential pure nets of [10] as one can check easily. This model is a reflexive object D in the Kleisli category of the linear logic model of sets and relations where !X is the set of all finite multisets over X. An element of D can be described as a finite tree which alternates two kinds of layers: multiplicative layers where subtrees are indexed by natural numbers and exponential layers where subtrees are organized as non-empty multisets. To be more precise,`−? (negative) pairs of layers alternate with ⊗−! (positive) pairs, respecting a strict polarity discipline very much in the spirit of Ludics [18]. The empty positive multiplicative tree corresponds to the empty tensor cell and the negative one to the empty par cell. The corresponding constructions τ ,τ are therefore quite easy to interpret.
We use this logical interpretation to turn the elements of D into ∂λ-calculus terms with tests. More precisely, with each element α of D, we associate a test α + · with a hole · for a term, and we show that α belongs to the interpretation of a (closed) term M iff the test α + M converges. From this fact, we derive a full abstraction result for the fragment of the ∂λ-calculus with tests in which all ordinary applications are trivial, that we call ∂ 0 λ-calculus with tests. To extend this result to the ∂λ-calculus with tests, we use the Taylor formula introduced in [11] which allows to turn any ordinary application into a sum of infinitely many linear applications of all possible arities. One exploits then the fact that the Taylor formula holds in the model, as well as a simulation lemma which relates the head reduction of a term with the head reduction of its Taylor expansion.
Contributions. In Section 2 we provide the abstract categorical framework which is needed to interpret the ∂λ-calculus and its extension with tests. The syntax and operational semantics of the ∂ 0 λ-calculus with tests (which is the promotion-free fragment) are presented in Section 3, while its relational model D is described concretely in Section 4. The definability of the elements of D in the ∂ 0 λ-calculus with tests is the main conceptual contribution of this paper -it shows that, in this setting, the standard syntax versus semantics dichotomy is essentially meaningless. From definability it follows easily that the relational model is fully abstract for the ∂ 0 λ-calculus with tests, as shown in Section 5. This result is analyzed further in Section 6, where it is proved that in the absence of promotion the test operators do not add any discriminatory power to the contexts, thus showing that D is also fully abstract for the ∂ 0 λ-calculus without tests.
We then focus on the full ∂λ-calculus with tests. Section 7 is devoted to present its syntax, operational semantics and relational semantics. In Section 8 we consider the use of Taylor expansions to reduce the full abstraction problem for ∂λ to its "∂ 0 λ" version, thus introducing an original and promising reduction technique.

Categorical semantics of linear logic
Before introducing the syntax of our resource λ-calculus with tests, we describe the general categorical structures needed to interpret this calculus. Our goal here is to give general motivations for our syntactic constructs. In the sequel, we consider a particular model, based on the category of sets and relations, and it is not hard to check that this particular category is an instance of the general setting we present here. In Section 4, we shall present this relational interpretation concretely in order to avoid the admittedly heavy categorical formalism.
Our main reference for categorical models of linear logic (LL) is [22]. We denote by N the set of natural numbers.
Let C be a Seely category. We recall briefly that such a structure consists of a category C, whose morphisms should be thought of as linear maps, equipped with a symmetric monoidal structure for which it is closed and * -autonomous with respect to a dualizing object ⊥. The monoidal product, called tensor product, is denoted as ⊗, the linear function space object from X to Y is denoted as X Y , the composition of morphisms in C is simply denoted as juxtaposition. We use ev ∈ C((X Y ) ⊗ X, Y ) for the linear evaluation morphism and cur(f ) ∈ C(Z, X Y ) for the "linear currying" of a morphism f ∈ C(Z ⊗ X, Y ). The dual object X ⊥ is denoted as X ⊥ . We also assume that C is cartesian, with a cartesian product denoted as & and a terminal object . By * -autonomy, this implies that C is also cocartesian; we use ⊕ for the coproduct and 0 for the initial object. In any cartesian and cocartesian category, there is a canonical morphism a ∈ C(0, ) and a canonical natural transformation a X,Y ∈ C(X ⊕ Y, X & Y ). One says that the category is additive if these morphisms are isomorphisms. In that case, each homset C(X, Y ) is equipped with a structure of commutative monoid, and all operations defined so far (composition, tensor product, linear currying) are linear with respect to this structure.
If C has cartesian products of all countable families (X i ) i∈I of objects, we say that it is countably cartesian, and in that case, C is also countably cocartesian. If the canonical morphism a (X i ) i∈I ∈ C( i∈I X i ,˘i ∈I X i ) is an isomorphism, we say that C is countably additive. In that case, homsets have countable sums and composition as well as all monoidal operations commute with these sums.
Last, we assume that C is equipped with an endofunctor ! which has a structure of comonad (unit d X ∈ C(!X, X) called dereliction, multiplication p X ∈ C(!X, !!X) called digging). Moreover, this functor must be equipped with a monoidal structure which turns it into a symmetric monoidal functor from the symmetric monoidal category (C, &) to the symmetric monoidal category (C, ⊗): the corresponding isomorphisms m : ! → 1 and m X,Y : !(X & Y ) → !X ⊗ !Y are often called Seely isomorphisms. The following diagram is moreover required to be commutative.
Using this monoidal structure, we can equip the ! functor with a lax symmetric monoidal structure from the symmetric monoidal category (SMC) (C, 1, ⊗) to itself. In other words, one can define a morphism µ : 1 → !1 and a natural transformation µ X,Y : !X ⊗ !Y → !(X ⊗ Y ) which satisfy compatibility conditions with respect to the structure isomorphisms of the SMC (C, 1, ⊗). Given an object X of C and k ∈ N, this allows to define a morphism µ (k) : (!X) ⊗k → !(X ⊗k ) which is essential in the interpretation of λ-terms.
2.1. Structural natural transformations. Using these structures, we can define a weakening natural transformation w X ∈ C(!X, 1) and a contraction natural transformation c X ∈ C(!X, !X ⊗ !X) as follows. Since is terminal, there is a canonical morphism t X ∈ C(X, ) and we set w X = m !t X . Similarly, we have a diagonal natural transformation ∆ X ∈ C(X, X & X) and we set c X = m X,X !∆ X .
This contraction morphism c X : !X → !X ⊗ !X is associative, and therefore can be generalized to a unique morphism c (n) More generally we can define a morphism c (k,n) X : (!X) ⊗k → ((!X) ⊗k ) ⊗n for the generalized contraction morphism which is defined as the following composition where σ is the obvious isomorphism, defined using associativity and symmetry of ⊗.
Similarly, we define a generalized weakening morphism w (k) X as the composition where λ is the unique canonical isomorphism induced by the monoidal structure. As usual the (co)Kleisli category C ! of the comonad ! is defined as the category that has the same objects as C and C ! (X, Y ) = C(!X, Y ), with composition denoted as • and defined using the comonad. One can prove C ! is cartesian closed, with & as cartesian product and !X Y as function space object: this is a categorical version of Girard's translation of intuitionistic logic into linear logic.
Given f ∈ C((!X) ⊗k , Y ), it is standard to define f ! ∈ C((!X) ⊗k , !Y ), this operation is usually called promotion in linear logic. This morphism is defined as the following composition: The notion of categorical model recalled above allows to interpret standard classical linear logic. If one wishes to interpret differential constructs as well (in the spirit of the differential λ-calculus or of differential linear logic), more structure and hypotheses are required. Basically, we need that: • the cartesian and cocartesian category C is additive, and • the model is equipped with a codereliction natural transformation d X ∈ C(X, !X) such that d X d X = Id X . More conditions are required if one wants to interpret the full differential λ-calculus of [11] or full differential linear logic as presented in e.g. [26]: these conditions represent a categorical axiomatization of the usual chain rule of calculus and are well explained in [15]. When these conditions, that we give explicitely now, hold, we say that the chain rule holds in C.
The first condition is the following commutation.
It would be interesting to know if this condition can be reduced to a more primitive one, involving d X and the isomorphism m (of course, one can replace µ by its expression in terms of m in the diagram above, so that this diagram is actually a condition on m, but we would like to find a simpler and more elegant commuting diagram involving m).
Last we have to provide a commutation relating d X and p X . We have of course d !X d X : X → !!X. Also, µ 1 : 1 → !1 and therefore !w X µ 1 : 1 → !!X. Keeping implicit the isomorphism X ⊗ 1 X, we get (d !X d X ) ⊗ (!w X µ 1 ) : X → !!X ⊗ !!X, and we require the following diagram to commute: If C is a weak differential LL model, we can define a coweakening morphism w X ∈ C(1, !X) and a cocontraction morphism c X ∈ C(!X ⊗ !X, !X) as we did for w X and c X . Similarly we also define c (n) X ∈ C((!X) ⊗n , !X). Due to the naturality of d X we have 2.3. The Taylor formula. Let C be a weak differential LL model which is countably additive. Remember that each homset C(X, Y ) is endowed with a canonical structure of commutative monoid in which countable families are summable. We assume moreover that these monoids are idempotent. This means that, if f ∈ C(X, Y ), then f + f = f .
We say that the Taylor formula holds in C if, for any morphism f ∈ C(X, Y ), we have If the idempotency condition does not hold, one has to require the homsets to have a rig structure over the non-negative real numbers, and the Taylor condition must be written in the more familiar way !
To give a precise meaning to this kind of expressions, we need of course more structure on homsets: they need to have some completeness properties, typically expressible in topological terms.
Remark 2.2. If the chain rule holds in C, the Taylor condition reduces to the particular case of identity morphisms: one has just to require that !Id X (in the idempotent setting).

2.4.
Models of the pure differential λ-calculus. A model of the pure differential λcalculus of [11] or of the ∂λ-calculus to be introduced below, is simply a reflexive object in C ! , where C is a model of differential linear logic in which the chain rule holds. More precisely, it consists of such a category C and of a triple (U, app, lam) where U is an object of C and app ∈ C(U, !U U ) and lam ∈ C(!U U, U ) satisfy app • lam = Id !U U in C. It is crucial to take app and lam in the "linear" category C and not in C ! .
In the present paper, we concentrate on the case where U satisfies a stronger condition. We assume that C is countably cartesian, and, given an object X, we denote as X N the cartesian product˘i ∈N X i where X i = X for each i ∈ N. We consider an object U of C together with an isomorphism ϕ ∈ C(U, (!U N ) ⊥ ). We have clearly (!U N ) ⊥ by * -autonomy of C. Using ϕ, we get finally that U !U U and we define app and lam using this isomorphism.
We also assume that C is a model of the MIX rule of linear logic (see [16]). This means that ⊥ is equipped with a structure of commutative monoid in the SMC C. We use mix (n) to denote the corresponding morphism ⊥ ⊗n → ⊥ so that in particular mix (0) : 1 → ⊥ and mix (1) The interpretation of the calculi presented in this paper is based on the following toolbox. The first constructions we give deal with "terms", which are represented here by morphisms (!U ) ⊗k → U (the number k ∈ N corresponds intuitively to the number of variables on which the term depends).
• Given a family of terms f 1 , . . . , f n : (!U ) ⊗k → U , we can define a morphism [f 1 , . . . , f n ] : (a morphism of this type will be called a "bag"). • Let f : (!U ) ⊗k → U be a further term. Remember that we have defined the promotion of f , which is a bag f ! : (!U ) ⊗k → !U . Therefore we can define Finally we define the application of f to g as the term Here we present the categorical constructions required for dealing with such tests.
• Let h 1 , . . . , h n : (!U ) ⊗k → ⊥ be tests. Then we can define their parallel composition, using the mix structure of ⊥, as the test

The ∂ 0 λ-Calculus with Tests
The definition of the ∂ 0 λ-calculus with tests requires some preliminary notations that we give below.
3.1. Sets and modules. We denote by N the set of natural numbers and by 1 an arbitrary singleton set. Given a set S, we write P(S) (resp. P f (S)) for the set of all (resp. all finite) subsets of S. Given k ∈ N, we denote by S k the set of all permutations of {1, . . . , k}. Let 2 be the semiring {0, 1} with 1+1 = 1 and multiplication defined in the obvious way. For any set S, we write 2 S for the free 2-module generated by S, so that 2 S ∼ = P f (S) with addition corresponding to union, and scalar multiplication defined in the obvious way. However we prefer to keep the algebraic notations for elements of 2 S , hence set unions will be denoted by + and the empty set by 0.

3.2.
Multisets. Let S be a set. A multiset a over S can be defined as an unordered list a = [α 1 , α 2 , . . .] with repetitions such that α i ∈ S for all indices i. A multiset a is called finite if it is a finite list; we denote by #a its cardinality. We write M f (S) for the set of all finite multisets over S. Given two multisets a = [α 1 , α 2 , . . .] and b = [β 1 , β 2 , . . .] the multiset union of a, b is defined by a b = [α 1 , β 1 , α 2 , β 2 , . . .]; summing up, N S ∼ = M f (S). Given two finite sequences of multisets a, b of the same length n we define a b = (a 1 b 1 , . . . , a n b n ). Given a strict order > on S, the multiset ordering [2, Def. A.6.2] is the smallest transitive relation > m on M f (S) such that (∀β ∈ b. α > β) ⇒ (a [α] > m a b), for all α ∈ S and all a, b ∈ M f (S). Intuitively, a > m b holds if b can be obtained from a by replacing some of its elements by finitely many (possibly zero) smaller elements.
Notation on parallel composition of tests. We now introduce the ∂ 0 λ-calculus with tests which is the promotion-free fragment of the ∂λ-calculus with tests we will present in Section 7.
3.3. Syntax. The ∂ 0 λ-calculus with tests has four syntactic categories: terms that are in functional position, bags that are in argument position and represent multisets of linear resources, tests that are "corked" multisets of terms having only two possible outcomes and finite formal sums representing all possible results of a computation. Expressions are either terms, bags or tests and will be used to state results holding for all categories.
Definition 3.1. The formal grammars defining terms, bags, tests and sums are given in Figure 1(a).
Terms are the real protagonists of the ∂ 0 λ-calculus with tests. The term λx.M represents the λ-abstraction of the variable x in the term M and M P the application of a term M to a bag P of linear resources. Thus, in (λx.M )P , each resource in P is available exactly once for λx.M and if the number of occurrences of x in M "disagrees" with the cardinality of P then the result is 0 (see later, when sums of expressions are introduced). The operator τ (·) will be discussed later on, after the notion of test is explained.
As usual we assume that application associates to the left and lambda abstraction to the right. Therefore we will write λx 1 . . . x n .M P 1 · · · P k for λx 1 .(· · · (λx n .(· · · (M P 1 ) · · · P k )) · · · ). Moreover, the notation M P ∼n will stand for M P · · · P (n times). Tests are multisets of terms, the "τ " being a tag for distinguishing them from bags. Intuitively, they are expressions that can produce two results: either success, represented by ε, or failure, represented by 0.
Throughout the paper, we will enforce the distinction between bags and tests by using systematically the following notational conventions. The test V |W represents the (must-)parallel composition of V and W (i.e., V |W succeeds if both V and W succeed and the order of evaluation is inessential). We prefer to use the parallel notation as syntactic sugar in order to avoid both the explicit treatment of associativity and commutativity axioms (plus neutrality of ε). This is perfectly coherent with the implementation of tests as multisets of terms.
The operatorτ (·) allows to build a term out of a test: intuitively, the termτ (V ) may be thought of as V preceded by an infinite sequence of dummy λ-abstractions. Dually, the "cork construction" τ [L 1 , . . . , L k ] may be thought of as an operator applying to all its arguments an infinite sequence of empty bags. This suggests in particular that it is sound to reduce τ [τ (V )] to V .
Hence the termτ (V ) raises an exception encapsulating V and the test τ [L 1 , . . . , L k ] catches the exception possibly raised by, say, L i and replaces L i by the multiset of terms encapsulated in that exception. The context of the exception is thrown away by the dummy abstractions ofτ and the dummy applications of τ . A test needs to catch an exception in order to succeed; for instance, τ [M ] fails as soon as M is aτ -free, closed term.
Sums. Remember from Subsection 3.1 that 2 Λτ (resp. 2 Λ τ , 2 Λ b ) denotes the set of finite formal sums of terms (resp. tests, bags) with an idempotent sum. We also set 2 Λ e := 2 Λ τ ∪ 2 Λτ ∪ 2 Λ b . This is an abuse of notation as 2 Λ e here does not denote the 2-module generated over Λ τ ∪ Λτ ∪ Λ b , but rather the union of the three 2-modules; this means that sums should be taken only in the same sort. The typical metavariables to denote sums are given in Figure 1(a).
The α-equivalence relation and the set FV(A) of free variables of A are defined as usual, like in the ordinary λ-calculus [1]. Hereafter, (sums of) expressions are considered up to α-equivalence.
Because of the absence of promotion the number of linear resources that a term λx.M is expecting is just the number of occurrences of x in M (the degree of x in M ).
, is the number of free occurrences of x in A and is defined by induction as follows: Linear Substitution  • 3.4. Two Kinds of Substitutions. In this subsection we introduce two kinds of substitutions: the usual λ-calculus substitution and a linear one, which is proper to differential and resource calculi (see [4,11,30]). In order to proceed, we first need to introduce some notational conventions concerning the sums. Indeed the grammar for terms and tests does not include any sums, so they may arise only on the "surface". For instance, I + I is a legal sum of expressions, while λx.(x + x) cannot be generated using the grammar of Figure 1(a). Convention 3.5. As a syntactic sugar -and not as actual syntax -we extend all the constructors to sums by multilinearity, setting for instance in such a way that the equations in Figure 2(a) hold.
This kind of meta-syntactic notation is discussed thoroughly in [14].
In the following two definitions we make an essential use of the extended syntax. We recall that an operator F (−) is extended by linearity by setting Definition 3.8 (Substitution). Let A ∈ Λ e and N ∈ Λτ . The (capture-free) substitution of N for x in A, denoted by A{N/x}, is defined as usual. Accordingly, A{N/x} denotes an expression of the extended syntax. Finally, we extend this operation to sums as in A{N/x} by linearity in A. Definition 3.9 (Linear Substitution). The linear (capture-free) substitution of N for x in A, denoted by A N/x , is defined in Figure 2(b). The expression A N/x belongs to the extended syntax. We extend this operation to sums as in A N/x by linearity in A, as we did for usual substitution.
Roughly speaking, the linear substitution A N/x replaces exactly one free occurrence of x in A with the term N . If there is no occurrence of x in A then the result is 0. In presence of multiple occurrences, all possible choices are made and the result is the sum of terms corresponding to them.
The above notation A P/x makes sense because, by Theorem 3.12, the expression A L 1 /x · · · L k /x is actually independent from the enumeration of L 1 , . . . , L k in P . Moreover recall that we use α-equivalence, so that bound variables can be renamed in order to avoid capture of free variables during substitution.
3.5. The Operational Semantics. In this section we are going to introduce the reduction rules defining the operational semantics of the ∂ 0 λ-calculus with tests.
Definition 3.14. The reduction semantics of the ∂ 0 λ-calculus with tests is generated by the rules in Figure 3(a).
The reduction preserves the sort of an expression in the sense that terms rewrite to (sums of) terms and tests to (sums of) tests.
The left side of a reduction rule in Figure 3(a) is called a redex while the right side is its contractum. Redexes are classified, depending on their kind, as follows.
The following remark gives a more explicit characterization of a β-contractum. Remember that the degree of x in M has been defined in Definition 3.4.
Remark 3. 16. If M has k free occurrences of x (represented by x 1 , . . . , x k ) then we have From Remark 3.16 it is clear that, because of the presence of linear substitution, the β-reduction is a relation from terms to sums of terms, namely → β ⊆ Λτ × 2 Λτ .
containing R and respecting the rules of Figure 3 We now provide some examples of reduction. Note that parallel composition is treated From Definition 3.19 we have that 0 is in normal form. The following lemma gives an explicit characterization of terms in normal form.
Lemma 3.20. If a term M ∈ Λτ is in normal form then 1. either M = λ x.yP 1 · · · P n for some n ≥ 0 and each P i is a bag of terms in normal form, where n ≥ 0, k i ≥ 0 and each P i,j is a bag of terms in normal form.
3.6. Operational properties. In this subsection we show that the ∂ 0 λ-calculus enjoys Church-Rosser and strong normalization, even in the untyped version of the calculus.
The proof of strong normalization is purely combinatorial, based on a measure given in the following definition.
Definition 3.21. The size of an expression A, written size(A), is defined by induction as follows: The intuition behind strong normalization is that size m (A) becomes smaller by replacing one (or more) of its elements by an arbitrary number of smaller elements, i.e., with respect to the multiset ordering > m induced on M f (N) by the usual order > of N. It is well known that > m is well-founded.
Proof. The fact that there are no infinite reduction chains is trivial, since every reduction step decreases the size of an expression. In other words For the Church-Rosser property just check local confluence and conclude by Newman's lemma.
The following lemma formalizes our intuition behind the behaviour of the cork τ (·). As a corollary we get that a closed test can only reduce either to ε or to 0. Proof. As ∂ 0 λ-calculus with tests is strongly normalizing, we have that , and this latter expression reduces to a finite (possibly empty) sum of ε's, which is thus equal either to 0 or to ε.
Therefore, it makes sense to define the convergence of a test as follows.
It is easy to check that a test V can converge only if it is closed; indeed, a free variable x occurring in V cannot be erased during the reduction.

3.7.
Operational Pre-order. A term-context D · is a term having one occurrence of a hole, denoted by · , appearing in term-position; a test-context C · is a test having one occurrence of a hole, still appearing in term-position.
Definition 3.26. Term-contexts D · and test-contexts C · are defined by the following grammar: The set of term-contexts is denoted by Λτ · and the set of test-contexts by Λ τ · . Given M ∈ Λτ we indicate by C M the test resulting by blindly replacing M for the hole (allowing capture of free variables) in C · . Similarly, given a term-context D · , D M denotes the term obtained by blindly substituting M for the hole in D · .
We say that a test-context C · (resp. a term-context Definition 3.28. The operational pre-order τ O on the ∂ 0 λ-calculus with tests is defined as follows (for all M, N ∈ Λτ ): This coincides with a standard idea of operational preorder. The restriction of observations to test-contexts deserves however a discussion. First, note that tests provide a canonical notion of observation since -by design -they either converge (to ε) or reduce to 0. Hence, the choice of test-convergence as the basic observation in our calculus is very natural.
A second motivation comes a posteriori. Indeed, as we will prove in Section 6 (Theorem 6.14), for test-free terms M, N we have M τ O N exactly when, for all test-free term-contexts D · , D M is solvable entails D N is solvable (the notion of solvability for test-free terms is given in Definition 6.2).

A Relational Semantics
This section is devoted to build a relational model D of ∂ 0 λ-calculus with tests, that has been first introduced in [8] as a model of the ordinary λ-calculus.
We first give a sketchy presentation of the Cartesian closed category where D lives. We recall that the definitions and notations concerning multisets have been introduced in Subsection 3.2.
4.1. The Category MRel. The category MRel is the co-Kleisli category for the finitemultiset comonad on the category Rel of sets and relations. This category can be described directly as follows: • The objects of MRel are all the sets.
Given two sets S, T , we denote by Hereafter we adopt the following convention.
It is easy to check that this is actually the categorical product of S and T in MRel; given s : U → S and t : U → T , the corresponding morphism s, t : U → S & T is given by: Given two objects S and T , the exponential object [S ⇒ T ] is M f (S) × T and the evaluation morphism is given by: Again, it is easy to check that in this way we defined an exponentiation. Indeed, given any set U and any morphism s : As shown in [20], MRel is actually a Cartesian closed differential category [3]. It is not difficult to check that it is moreover an instance of the categorical framework presented in Section 2.

4.2.
An Extensional Reflexive Object. We build a reflexive object D, which is extensional in the sense that D ∼ = [D ⇒ D]. The elements of D are infinite sequences of multisets, that are quasi-finite in the following sense.  We build a family of sets (D n ) n∈N as follows: Since the operation mapping a set S into M f (S) (ω) is monotonic with respect to inclusion 1 and D 0 ⊆ D 1 , we have D n ⊆ D n+1 for all n ∈ N. Finally, we set D = n∈N D n .
To define an isomorphism between D and M f (D) × D just note that every element α = (a 1 , a 2 , a 3 , . . .) ∈ D stands for the pair (a 1 , (a 2 , a 3 , . . .)) and vice versa. From this simple remark, it follows that D ∼ = [D ⇒ D] (we have a canonical bijection between these two sets, and therefore an isomorphism in MRel).  = (a 1 , a 2 , a 3 , . . .) ∈ D and a ∈ M f (D), we write a :: α for the element (a, a 1 , a 2 , a 3  Remark that [] :: * = * .

4.3.
Interpreting the ∂ 0 λ-calculus with tests. We now define the interpretation of an expression A of the ∂ 0 λ-calculus with tests in the model D. As usual, an expression A will be interpreted by a morphism of the category MRel.
For all terms M , bags P , tests Q and repetition-free sequences x, y, z respectively containing the free variables of M, P, Q, we define by mutual induction the interpretations M x : D n → D, P y : D m → M f (D) and Q z : D k → 1 (1 is a singleton set and n, m, k are the lengths of x, y, z) as follows 2 : The interpretation is then extended to the elements of 2 Λ e by setting Σ k Since every test V is of the form τ [L 1 , . . . , L k ] we might define its interpretation directly by setting V   Clearly the interpretation is monotonic, in the sense expressed by the following lemma.
Lemma 4.9. For any test-context C · (resp. term-context D · ) with free variables y, if M x ⊆ N x then C M x, y ⊆ C N x, y (resp. D M x, y ⊆ D N x, y ).
Proof. By a straightforward mutual induction on C · , D · .
The substitution lemmas above generalize straightforwardly to sums. Although Lemma 4.11 is stated in full generality, for the ∂ 0 λ-calculus with tests is only useful for N = 0. We keep this formulation since it is closer to the one needed in Section 7 for the full ∂λ-calculus with tests. Proof. It is easy to check that the interpretation is contextual. The fact that the semantics is invariant under reduction follows from Lemmas 4.10 and 4.11.

Full Abstraction for ∂ 0 λ-Calculus with Tests
A model is equationally fully abstract if the equivalence induced on terms by their interpretations is exactly ≈ τ O ; it is inequationally fully abstract if the induced preorder is τ O . Obviously, every inequationally fully abstract model is also equationally fully abstract.
In this section we prove that D is inequationally fully abstract for the ∂ 0 λ-calculus with tests (Theorem 5.

Building Separating Test-Contexts.
We are going to associate a test-context α + · with each element α ∈ D, the idea being that -for every closed term M -we have α ∈ M if and only if α + M converges.
By Corollary 3.24, we know that α + βreduces either to ε or to 0. The result follows by soundness (Theorem 4.12). Proof. The result follows by applying n times (one for each variable in x) Lemma 4.10 and Corollary 5.5.
The ensuing proposition is the key argument for proving that the model D is inequationally fully abstract. (i) ( a, α) ∈ M x , (ii) α + M a -/ x ε.
Proof. We have the following chain of equivalences: ( a, α) ∈ M x ⇔ a ∈ α + M x , by Corollary 5.5, ⇔ α + M a -/ x = ∅ and deg x i (M ) = #a i , by Lemma 5.8, using Remark 5.9, ⇔ α + M a -/ x ε, by Corollary 3.24, i.e. the fact that closed tests can only reduce to either ε or 0, and Theorem 4.12, i.e. the soundness of the model.
We are now able to prove the main result of the section.
Theorem 5.11. D is inequationally fully abstract for the ∂ 0 λ-calculus with tests (for all M, N ∈ Λτ ): (⇒) Assume that M x ⊆ N x , and let C · be a test-context closing both M and N and such that C M ε. By Theorem 4.12, C M = ε = {()}. By monotonicity of the interpretation we get C M ⊆ C N , thus C N = ∅. By Corollary 3.24 this entails that C N ε. (⇐) Suppose, by the way of contradiction, that M τ O N holds but there is an element ( a, α) ∈ M x − N x . Then the test-context C · = α + (λ x. · ) ais such that C M α + M a -/ x ε and C N ε by Proposition 5.10, which is a contradiction. The reader who is only interested in the extension of Theorem 5.11 (and of its corollary) to the full ∂λ-calculus with tests can skip safely the next section.

Full Abstraction for ∂ 0 λ-Calculus without Tests
In this section we are going to prove that tests do not add any discriminatory power to the contexts already present in the ∂ 0 λ-calculus. This means that whenever there is a test-context C · separating two test-free terms M, N (sending, say, M to ε and N to 0) there exists also a term-context D · that is still able to separate M from N , without using the operators τ andτ . (As we will discuss in Section 9, this is not the case for the full ∂λ-calculus with tests.) From this syntactic result and the full abstraction for the ∂ 0 λ-calculus with tests (Theorem 5.11) we conclude that the model D is also inequationally fully abstract for its test-free fragment (Theorem 6.14, below).
6.1. The ∂ 0 λ-Calculus (Without Tests). The ∂ 0 λ-calculus is a restriction of the ∂ 0 λcalculus with tests presented in Section 3. The restriction is obtained by erasing from the syntax the constructors τ andτ and the corresponding reduction rules, i.e. (τ ), (τ ) and (γ). In other words the tests are no longer part of the language and → β is the only reduction rule of the system. This description is enough to completely characterize the system -for a more detailed description, see [13,14]. Notation 6.1. We write Λ r (resp. 2 Λ r ) for the set of (resp. finite sums of) terms of the ∂ 0 λ-calculus. The set of all (term-)contexts of the ∂ 0 λ-calculus will be denoted by Λ r · . We still write M, N, L, H for terms in Λ r , M, N, L, H for sums of terms in 2 Λ r , P, Q for bags and D · for contexts. This will not create confusion because we will always specify the set they belong to.
In order to properly define the operational pre-order in this setting, we first need to introduce the notion of solvable term.
6.2. Solvability in the ∂ 0 λ-Calculus. In λ-calculus [1] a term M is solvable whenever there exist suitable arguments that, once supplied to M , make it reduce to the identitythis means that M it is able to interact operationally with the environment.
In resource calculi solvability has been thoroughly studied by Pagani and Ronchi Della Rocca in [27,28]. Their work needs to be adapted because of the absence of promotion in our system. For the ∂ 0 λ-calculus the good notion of solvable term is the following. Definition 6.2. A term M ∈ Λ r is solvable if there is a term-context D · such that D M β I. We say that M is unsolvable otherwise. Reading [27,28] one may wonder why in the previous definition we do not ask more generally that D M β I + N for some N ∈ 2 Λ r . This is due to the fact that in our ∂ 0 λ-calculus the two definitions are equivalent, as shown in the next lemma. (So we choose the easier formulation.) Lemma 6.3. Let M ∈ Λ r be a closed term. If M β I + M for some M ∈ 2 Λ r , then there exists a sequence P of closed bags such that M P β I.
Proof. Suppose M closed such that M β I + M. Then M is also closed and normalizes to a sum M = Σ j=1 λ y j .M j such that each M j is not an abstraction itself. Now, if M = I then we are done as M β I + M β I + I = I. Otherwise, let h be the maximum among the lengths of the sequences y j . Then M [I] ∼h is again a sum of closed terms and normalizes to a sum M of closed abstraction terms whose size is strictly smaller than M . The reason is that for each summand (λ y j .M j )[I] ∼h which does not reduce to 0, M j must contain exactly one occurrence of each variable in y j . Hence M j [I]/ y j {0/ y j } has the same size as (λ y j .M j ) but it reduces (via contraction of the I that has replaced the head variable of M j ) to a term having a strictly smaller size, unless λ y j .M j ≡ I. Iterating this reasoning for at most a number of times equal to k = size(M) + [27,28] we are going to characterize solvability from both a syntactic and a semantic point of view (Theorem 6.5).
Proposition 6.4. Let M ∈ Λ r and let FV(M ) = x. If M reduces to a normal form different from 0, then there are two sequences P , P of closed bags such that: Proof. By induction on the size of M . Let x = x 1 , . . . , x n and suppose that M β λy 1 . . . y m .yQ 1 · · · Q q + M where m, q ∈ N, Q i = [M i,1 , . . . , M i,k i ] for all 1 ≤ i ≤ q, each M i,j is in normal form for every 1 ≤ j ≤ k i and M ∈ 2 Λ r . For the sake of simplicity, assume y = y h for some 1 ≤ h ≤ m (the proof is analogous when y ∈ x).
By induction hypothesis, for all 1 ≤ i ≤ q and 1 ≤ j ≤ k i there are sequences P i,j , P i,j , P i,j of closed bags such that M i,j P i,j P i,j / y P i,j / x {0/ y, x} β I + M i,j for some M i,j ∈ 2 Λ r . In the following, we will denote by σ i,j the substitution P i,j / y P i,j / x {0/ y, x}.
Note that in the statement above M must be closed because M P P / x {0/ x} is. Theorem 6.5. Let M ∈ Λ r , then the following three sentences are equivalent.
(i) M is solvable, Proof. (i ⇒ ii) Suppose by contradiction that there is no normal N such that M β N + N for some N ∈ 2 Λ r . Since the ∂ 0 λ-calculus is strongly normalizing, the only possibility is that M β 0. Therefore, for every term-context D · we would have D M β D 0 = 0. This is a contradiction since the calculus is Church-Rosser and by hypothesis there should be a term-context D · such that D M β I. Induction case p > 0. By induction hypothesis, there exist ( c i,j , β i,j ) ∈ L i,j x, z for each 1 ≤ i ≤ p and 1 ≤ j ≤ k p . Let b i = [β i,1 , . . . , β i,k i ] for every 1 ≤ i ≤ p and a 0 = ( [], [b 1 :: · · · :: b p :: α], []) ∈ M f (D) n+m where the only non-empty multiset is in n + h position. Then ( a 0 , b 1 :: · · · :: b p :: α) ∈ z h x, z and ( a i , b i ) ∈ P i x, z for a i = k i j=1 c i,j . It follows that ( a 0 a 1 · · · a p , α) ∈ z h P 1 · · · P p x, z . We conclude since z h P 1 · · · P p x, z = ∅ if and only if λz 1 . . . z m .z h P 1 · · · P p x = ∅.
(iii ⇒ ii) Suppose that M β 0. Then by Theorem 4.12 we have M x = 0 x = ∅, which is a contradiction. Definition 6.6. The operational pre-order O on the ∂ 0 λ-calculus is defined as follows (for all M, N ∈ Λ r ): Let us consider the restriction of the preorder O (see Definition 3.28) to the terms of the ∂ 0 λ-calculus (without tests). Theorem 5.11 shows that for all terms M, N of the ∂ 0 λ-calculus (without tests) we have M x ⊆ N x ⇔ M τ O N . Later in this section (Theorem 6.14) we will prove that M x ⊆ N x ⇔ M O N . Hence the preorder O coincides, on the test-free language, with τ O . This is an a fortiori justification of Definition 6.6, which was anyway supported by the intuition that solvable ∂ 0 λ-terms are a kind of arenas over which the solvability game can be successfully played and simulated by the throw/catch game of the test constructions.
6.3. Full Abstraction via Test Expansion. As mentioned in Section 3, the termτ (V ) roughly corresponds to V preceded by an infinite sequence of dummy λ-abstractions; dually, the test τ [L 1 ]| · · · |τ [L k ] corresponds to providing each L i with an infinite sequence of empty bags. (This is also clear from the reduction rules (τ ) and (τ ).) In this section we show that the infinite nature of these sequences is not essential in the ∂ 0 λ-calculus. Roughly speaking, one can find an n such that λx 1 . . . x n .V has the same behaviour ofτ (V ) and n i 's such that each L i [] ∼n i has the same behaviour of τ [L i ]. The parallel composition V = V 1 | · · · |V k can be simulated in the ∂ 0 λ-calculus by M = λx.x[V 1 , . . . , V k ] in the sense that V converges iff each V i converges and, similarly, M is solvable iff each V i is solvable.
We then define a test-expansion (Definition 6.10), from terms of the ∂ 0 λ-calculus with tests to test-free terms, formalizing this intuition. In order to expand the correct number of times the occurrences ofτ and of the elements of a test, we first need to "name" each occurrence in a different way. For this reason we label such occurrences with pairwise distinct indices. Definition 6.7. A labelled expression A is an expression of the ∂ 0 λ-calculus with tests such that every occurrence of aτ and every element of a test have been decorated with distinct natural numbers (called indices). We denote by (Λτ ) lab , (Λ b ) lab , (Λ τ ) lab , (Λ e ) lab , (Λ τ · ) lab the set of labelled terms, labelled bags, labelled tests, labelled expressions, labelled termcontexts, respectively.
Let A ∈ 2 (Λ e ) lab be a sum of labelled expressions. We writeÃ for its underlying expression; in other wordsÃ is obtained stripping off all indices from A. We write dom(A) for the set of indices occurring in A. Note that the domains of two summands A, A ∈ A may have a non-empty intersection. From (2) we note thatÃ = A for all test-free labelled expressions. From (5) we note that in a labelled bag the labels actually occur within its elements.
Definition 6.9. The reduction semantics for labelled expressions is inherited straightforwardly from the ∂ 0 λ-calculus with tests. In the β-rule, the terms are substituted together with their indices.
Since there is no duplication during the reduction, if A is a labelled expression reducing to A then A is a sum of labelled expressions (that is, all the indices occurring within each A ∈ A are pairwise distinct). Definition 6.10. Let A ∈ (Λ e ) lab be a labelled expression and be a function from N to N. The -expansion A of A is an expression of the ∂ 0 λ-calculus without tests, defined by induction on A as follows: In particular ε = λx.
x[] for all . This is extended to sums by setting ( i A i ) = i A i and to contexts by setting · = · .
Obviously, for all test-free labelled expressions A we have A = A for all . The proofs of the following lemmas are given in the technical Appendix A. Lemma 6.12. Let V ∈ 2 (Λ τ ) lab be a sum of labelled closed tests. If V ε then there exists a map : N → N such that V ( +k) is solvable for all k ∈ N. Lemma 6.13. Let V ∈ 2 (Λ τ ) lab be a sum of labelled closed tests. If V 0 then there exists a natural number k such that V ( +k) 0 for all : N → N.
We are now ready to state and prove the main theorem of this section, from which immediately follows the equational full abstraction result for the ∂ 0 λ-calculus. Theorem 6.14. D is inequationally fully abstract for the ∂ 0 λ-calculus (for all M, N ∈ Λ r ): (⇐) Suppose, by the way of contradiction, that M O N holds but there is an element ( a, α) ∈ M x − N x . By Proposition 5.10 the test-context C · = α + (λ x. · ) ais such that C M α + M a -/ x ε and C N ε (therefore C N 0 by Lemma 3.23). Let C · ∈ (Λ r · ) lab such thatC · = C · . By Lemma 6.12 there exists such that (C M ) ( +k ) is solvable for every k ∈ N. By Lemma 6.13 there exists k ∈ N such that (C N ) ( +k) is unsolvable. From Remark 6.11 (1) we get (C M ) ( +k) = C ( +k) M ( +k) and (C N ) ( +k) = C ( +k) N ( +k) . Since M, N are test-free we have M ( +k) = M and N ( +k) = N . We conclude because we found a term-context C ( +k) such that C ( +k) M is solvable and C ( +k) N is unsolvable, which is a contradiction.
Remark 6.16. A direct proof of Corollary 6.15 might be obtained exploiting a corollary of the Böhm Theorem for the ∂λ-calculus proved in [21]. We preferred to provide this proof based on test-expansion because it clarifies the behaviours of our test operators and works also in the inequational case.
The rest of the paper is devoted to extend the full abstraction results of Subsection 5.2 to the ∂λ-calculus with tests. The main ingredients will be the head reduction introduced in Subsection 7.5 and the Taylor expansion we define in Subsection 8.1.

The ∂λ-Calculus with Tests
The ∂λ-calculus with tests is an extension of the ∂ 0 λ-calculus with tests with a promotion operator available on resources. In this calculus a resource can be linear (it must be used exactly once) or not (it can be used ad libitum) and in the latter case it is decorated with a "!" superscript. 7.1. Syntax. The grammar generating the terms, the tests and the expressions of the ∂λcalculus with tests, is given in Figure 4(a). Note that such grammar is equal to the one for the ∂ 0 λ-calculus with tests (in particular tests are still plain multisets of linear resources), except for the rule concerning bags which becomes: where N is a finite sum of terms of this new syntax. We write Λτ ! for the set of terms generated by this new grammar, Λ τ ! for the set of tests, Λ b ! for the set of bags, Λ e ! for the set of expressions.
It should be clear that from now on bags are no more plain multisets of terms: they are compound objects, consisting of a multiset of terms [L 1 , . . Remark 7.1. The ∂ 0 λ-calculus with tests is the sub-calculus of the ∂λ-calculus with tests in which all bags have the shape [L 1 , . . . , L k , 0 ! ], and this identification is compatible with the reduction rules.
As in the ∂ 0 λ-calculus with tests, we extend this syntax by multilinearity to sums of expressions with the only exception that the bag [L 1 , . . . , L k , (N + M) ! ] is not required to be equal to [L 1 , . . . , L k , N ! ] + [L 1 , . . . , L k , M ! ]. The intuition is that in the first expression N+M can be used several times and each time one can choose non-deterministically N or M, whereas in the second expression one has to choose once and for all one of the summands, and then use it as many times as needed.
Linear Substitution (New Rule)

7.2.
Substitutions. Linear substitution is denoted and defined as in the ∂ 0 λ-calculus with tests ( Figure 2(b)), except of course for bags, where we use the rule of Figure 4(b). Linear substitution is extended to sums, as in A N/x , by bilinearity in both A and N. We also define the regular substitution A{N/x} for the ∂λ-calculus with tests, by simply replacing each occurrence of x in the expression A with N -in that way we get an expression FULL ABSTRACTION FOR RESOURCE CALCULI 29 of the extended syntax, since N is a sum in general. This operation is then extended to sums, as in A{N/x}, by linearity in A.
A Schwarz Theorem, analogous to Theorem 3.12, holds for the ∂λ-calculus with tests. Hence, given a sum of expressions A and a bag P = [L 1 , . . . , L k ] with x / ∈ FV(P ), it still makes sense to set A P/x := A L 1 /x · · · L k /x because this expression does not depend on the enumeration of L 1 , . . . , L k in P . In particular A []/x = A. 7.3. Operational semantics. The reduction rules of ∂λ-calculus extend those of the ∂ 0 λcalculus with tests in the sense that they are equivalent on !-free expressions.
Definition 7.4. The rules (τ ) and (γ) are exactly the same as the corresponding rules of the ∂ 0 λ-calculus, while the β-reduction andτ -reduction are rephrased as in Figure 4(c). In this setting, their contextual closure needs to be closed also under the rule of Figure 4(d).
The ∂λ-calculus with tests is still Church-Rosser (just adapt the proof in [29]), while it is no more strongly normalizing. For instance the term Ω := ∆[∆ ! ], for ∆ := λx.x[x ! ], has an infinite reduction chain, just like the paradigmatic homonymous unsolvable λ-term. Indeed, the usual λ-calculus can be embedded into the ∂λ-calculus with tests by translating every application M N into M [N ! ].
Remark 7.5. Reductions in the ∂λ-calculus with tests may be tricky, due to the combination of linear and non linear resources and substitutions. For instance, we can obtain eight Ω-like terms of the ∂λ-calculus with tests, of the form M [N (!) ] where M, N ∈ {D, ∆} and (!) denotes the optional presence of the promotion. Not surprisingly all these terms, except for Ω, reduce to 0. E.g., Here are some other examples of reductions, involving tests.
In this framework a test-context C · (resp. term-context D · ) is a test (resp. term) of the ∂λ-calculus with tests having a single occurrence of its hole, appearing in term-position. Definition 7.7. Term-contexts D · and test-contexts C · are defined by the following grammar: The set of term-contexts is denoted by Λτ ! · and the set of test-contexts is denoted by Λ τ ! · . Definition 7.8. A test V converges, notation V ↓, if there exists a (possibly empty) sum V such that V ε + V.
Convergence should not be confused with normalization. Note that Definition 7.8 is the natural extension of Definition 3.25; in presence of promotion, ε and 0 are not the only possible "outcomes" of closed tests because there are looping terms that may never interact with an outer cork τ [·]. That case represents "failure", i.e., a scenario where there is no possible sequence of choices (among summands of terms resulting from reduction) leading to the positive test ε.
Definition 7.9. The operational pre-order τ ! O on the ∂λ-calculus with tests is defined by: The comparison between D (Example 4.7(3)) and ∆ (item (1)) gives a grasp on the semantic counterpart of non-linearity.
It is easy to check that both the linear and the classic substitution lemmas generalize to this context. While we can keep the same statement for Lemma 4.11, Lemma 4.10 must be rephrased as follows (indeed, deg x (M ), deg x (V ) are undefined when M, V contain non linear resources). Lemma 7.11 (Linear Substitution Lemma). Let M, L 1 , . . . , L k ∈ Λτ ! , Q ∈ Λ τ ! and P = [L 1 , . . . , L k ] (with y ∈ FV(P )). Then we have: (i) (( a, b), α) ∈ M P/y x,y iff there exist ( a i , β i ) ∈ L i x (for i = 1, . . . , k) and a 0 ∈ M f (D) n and b ∈ M f (D) such that (( a 0 , [β 1 , . . . , β k ] b), α) ∈ M x,y and k i=0 a i = a. (ii) ( a, b) ∈ Q P/y x,y iff there exist ( a i , β i ) ∈ L i x (for i = 1, . . . , k) and a 0 ∈ M f (D) n and b ∈ M f (D) such that ( a 0 , [β 1 , . . . , β k ] b) ∈ Q x,y and k i=0 a i = a. From these lemmas it ensues that D is also a model of the ∂λ-calculus with tests.
Theorem 7.12. D is a model of ∂λ-calculus with tests. 7.5. Head Reduction. We now provide a notion of head reduction for the ∂λ-calculus with tests. Intuitively, head reduction is obtained by reducing a head redex, that is a redex occurring in head position in an expression A. The main interest of introducing this reduction strategy is that it "behaves well" with respect to Taylor expansion in the sense of Proposition 8.6.
The definition of term-and test-redexes is inherited from Definition 3.15. Among these redexes we distinguish those that are in "head" position.
Definition 7.13. A head redex is defined inductively as follows: -every test-redex V is a head redex, -a term-redex H is a head redex in both the term λ y.H P and the test τ [H P ]|V . Definition 7.14. We say that A → B is a step of head reduction if B is obtained from A by contracting a head redex. If A → B is a step of head reduction then also A + A → B + A is.
One-step head reduction is denoted by → h , while h indicates its reflexive and transitive closure.
Remark 7.15. Unlike in ordinary λ-calculus, an expression A may have more than one head redex, hence there may be more than one head reduction step starting from A.
Head reduction induces a notion of head normal form on (sums of) expressions.
This notion of head normal form differs from that given by Pagani and Ronchi Della Rocca in [28]. We keep this name because their definition captures the notion of "outernormal form" rather than that of head normal form, and in fact they changed terminology in [27].
The following lemma gives a characterization of terms and tests in head normal form.  The following two lemmas concern reduction properties of promotion-free closed tests.
Lemma 7.18. Let V ∈ Λ τ . If V is closed and V = ε then it has a head redex (hence, V → h V for some V).
Proof. By structural induction on V . It suffices to consider the case V = τ [M ]. We then proceed by cases on the structure of M (which must be closed). If M = λx.N then V head reduces using (τ ). If M is an application then it must be written either as M = (λy.N )P 1 · · · P k or as M =τ [W ]P 1 · · · P k (in both cases k ≥ 1) and hence V head reduces using either (β) or (τ ), respectively. If M =τ (W ) then V head reduces using (γ). 18.
An analogous proof shows that V 0 entails V h 0. (⇐) Trivial since h ⊆ . Head reduction will play an essential role in the next section.

Full Abstraction via Taylor Expansion
In this section we are going to define the Taylor expansion of terms and tests of the ∂λcalculus with tests. We will then use this expansion, combined with head-reduction, to generalize the full abstraction results obtained in Subsection 5.2 to the framework of ∂λcalculus with tests. 8.1. Taylor Expansion. The (full) Taylor expansion was first introduced in [11,12], in the context of λ-calculus. The Taylor expansion M • of an ordinary λ-term M gives an infinite formal linear combination of terms (equivalently, a set of terms) of the ∂ 0 λ-calculus. In the case of ordinary application it looks like: in accordance with the intended meaning and the denotational semantics of application in the resource calculus. In the syntax of Ehrhard-Regnier's differential λ-calculus the above formula looks like ∞ n=0 1 n! M (n) (0)(N, . . . , N ), hence the connection with analytical Taylor expansion is evident.
Following [21], we extend the definition of Taylor expansion from ordinary λ-terms to expressions of the ∂λ-calculus with tests. Since in our context the sum is idempotent, the coefficients disappear and our Taylor expansion corresponds to the support of the actual Taylor expansion.
As the set 2 Λ e ∞ of possibly infinite formal sums of expressions is isomorphic to P(Λ e ), in the following we feel free of using sets instead of sums.
The (full) Taylor expansion of A is the set A • ⊆ Λ e which is defined (by structural induction on A) in Figure 5.
The following are examples of Taylor expansion of terms and tests. In (1) and (2) we see that the Taylor expansion of an expression A can be infinite. In (3) we have an example of two different terms sharing the same Taylor expansion.  In [20] it is proved that the Taylor formula holds in MRel. This property entails that Taylor expansion preserves the meaning of an expression in D, as expressed in the next theorem.
Proof. By adapting the proof in [20] of the analogous theorem for the differential λ-calculus.
We now need the following technical lemma stating the commutation of Taylor expansion with respect to ordinary and linear substitutions. The proof is lengthy but not difficult and is provided in Appendix A. For the sake of readability, in the next statements we use sums and unions interchangeably.
The next proposition is devoted to show how Taylor expansion interacts with headreduction. To ease the formulation of the next proposition we assimilate 2 Λ e ! to P f (Λ e ! ). Proposition 8.6. Let A ∈ Λ e ! and let A ∈ A • be such that A → h B , for some B . Then there exists B such that A → h B and B ⊆ B • .
Proof. The idea is that the syntactic tree of A has the same structure as that of A and we can define a surjective mapping of the redexes of A into those of A.
We only treat the case A = λ x.H P 1 · · · P p where H = (λy.M )P is a head-redex. From A ∈ A • we get A = λ x.HP 1 · · · P p for some H such that H ∈ H • . Hence We can conclude that λ x.M P /y {0/y}P 1 · · · P p ⊆ (λ x.M [ L]/y {N/y}P 1 · · · P p ) • . All other cases are simpler. Proof. Suppose that there exists V ∈ V • such that V ε. By Lemma 7.19 there is a head-reduction chain of the form V → h V 1 → h · · · → h V n = ε. By iterated application of Corollary 8.8 there are tests V i (for i = 1, . . . , n) such that We conclude since ε ∈ V • n is only possible when ε ∈ V n .

8.2.
Full Abstraction for the ∂λ-Calculus with Tests. We are now going to prove that the relational model D is inequationally fully abstract for the ∂λ-calculus with tests.
(ii ⇒ i) Suppose that α + M a -/ x ε + V, for some V; then α + M a -/ x x = ∅. Hence, by Theorem 8.4, there is a closed test V ∈ (α + M a -/ x ) • such that V = ∅. By Lemma 8.10 V = α + M a -/ x for some M ∈ M • and since its interpretation is nonempty we have V ε. By applying Proposition 5.10 we get ( a, α) ∈ M x ⊆ M x (by Theorem 8.4).
Theorem 8.12. D is inequationally fully abstract for the ∂λ-calculus with tests (for all M, N ∈ Λτ ! ): ε+V, for some V, we have C M = ∅. Thus, by monotonicity of the interpretation we get C M ⊆ C N = (C N ) • = ∅. By Corollary 3.24 there is V ∈ (C N ) • such that V ε and we conclude that C N ↓ by applying Proposition 8.11. (⇐) Suppose by contradiction that M τ ! O N , but there is an ( a, α) ∈ M x − N x . By Proposition 8.11 α + M a -/ x ↓ and since M τ ! O N we have α + N a -/ x ↓. Again, by Proposition 8.11 ( a, α) ∈ N x . Contradiction. Corollary 8.13. D is equationally fully abstract for the ∂λ-calculus with tests.

Conclusions and Further Works
In this paper we defined the interpretation of several resource calculi into the relational model D and characterized the equality induced on the terms from an operational point of view. The analogous question for untyped λ-calculus was addressed in [19], where it is shown that the λ-theory induced by D is H , therefore D is fully abstract for λ-calculus.
In the first result of our paper we proved that the model D is also (in)equationally fully abstract for the ∂ 0 λ-calculus with tests. Such a proof is simplified by the absence of promotion in the calculus, which allows us to work in a strongly normalizing framework. The interest of this proof is that it generalizes along two directions.
The first direction aims to get rid of the tests, while remaining in the promotion-free fragment of the calculus. To extend this result to the ∂ 0 λ-calculus without tests we defined the test-expansion -a translation from tests to terms replacing every occurrence of a test operator τ,τ by a suitable number of empty applications or dummy lambda abstraction. By applying this translation to a test-context separating two terms, we obtain a term-context having the same discriminatory power. This is not surprising since everything is finite in the ∂ 0 λ-calculus (finite sums, finite reduction chains) therefore the infinitary nature of our test operators can be simulated by terms whose size is big enough.
The second direction aims to extend the full abstraction result to the ∂λ-calculus with tests (and promotion available on resources). The main contribution of the paper is to show that this generalization can be done just by combining the properties of the head reduction and of the Taylor Expansion.
It is worth to notice that the test expansion method cannot be applied in presence of promotion because D is not fully abstract for the ∂λ-calculus; in other words the tests are necessary to obtain the last result. This has been recently showed by Breuvart [6], who exhibited two terms of the ∂λ-calculus being observationally equivalent, but having different interpretations in D. The idea of the counterexample is to build, using fixpoint combinators, a term M reducing (eventually) to an infinite sum of terms whose head variable is preceded by an increasing number of lambda abstractions. This term is annihilated by the context τ [ · [τ (ε)]] because the operator τ "eats" all the lambda abstractions and substitutes the head-variable of each component of the sum by 0, while we know that the same context sends I to ε. The author then proved that no context of the ∂λ-calculus can simulate this behaviour.
The following table summarizes all these results. The definition of ! O is analogous to O with the definition of may-solvable given in [28]; the definition of is the usual one given in [25].

Calculus
Operational Breuvart's counterexample raises the problem of finding a model that is actually fully abstract for the ∂λ-calculus without tests. It is known that the structure of the underlying Cartesian closed category may effect the theories of all models living in it. For instance in [20] it is shown that terms having the same Taylor expansion are equated in all models living in MRel. It is therefore possible that Question 9.1 admits a negative answer. If this is the case, then the following question becomes interesting. Question 9.2. Is it possible to find a new comonad T , such that the (co)Kliesli Rel T contains a fully abstract model of ∂λ-calculus?
Indeed, the comonad M f (−) of finite multisets is not the only one that leads to models of ∂λ-calculus. For instance it has been shown by Carraro, Ehrhard and Salibra in [9] that one can consider exponential functors with infinite multiplicities. However, their models do not even validate the Taylor expansion, therefore are not suitable to solve Question 9.2. The challenge is to find other kinds of comonads.
Let be a function from N to N. Given a natural number k ∈ N we write [n := k] for the map which coincides with , except on n, where takes the value k. We let ( + k) denote the function defined by (x) = (x) + k.
In the following proofs we write A n h B if A reduces to B in n steps of head reduction, which is introduced in Section 7.5 for the full ∂λ-calculus with tests. Lemma A.3. (Lemma 6.12) Let V ∈ 2 (Λ τ ) lab be a sum of labelled closed tests. If V ε then there exists a map : N → N such that V ( +k) is solvable for all k ∈ N.
Proof. In the proof we use the characterization of solvable given in Theorem 6.5(ii). We proceed by induction on the length n of a head reduction V h ε (by Lemma 7.19). For the sake of simplicity we assume that in the sum V we first reduce a component that head reduces to ε (only when V = ε + W we start reducing within W).
x[] independently from . Case n > 0. We have V → h V n−1 h ε. The proof is divided into sub-cases depending on the redex that is contracted.