Math. Struct. in Comp. Science (1993), vol. 11, pp. 1–000. Printed in the United Kingdom \begin{matrix}c \\ ◯ \end{matrix} 1993 Cambridge University Press

A Semantics for Lambda Calculi with Resources

Gérard Boudol and Pierre-Louis Curien and Carolina Lavatelli

Received 15 April 1999

We present the λ-calculus with resources λ_{r} as well as two variants, a deterministic restriction λ_{m} and an extension λ_{r}^{c} with a convergence testing operator. These calculi provide a control on the substitution process ; deadlocks may arise if not enough resources are available to carry out all the substitutions needed to pursue a computation. The design of these calculi was motivated by Milner’s encoding of the λ-calculus in the π-calculus. As Boudol and Laneve have shown elsewhere, the discriminating power of λ_{m} (given by the contextual observational equivalence) over λ-terms coincides with that induced by Milner’s π-encoding, and coincides also with that provided by the lazy algebraic semantics (Lévy-Longo trees). The main contribution of this paper is model-theoretic. We define and solve an appropriate domain equation, and show that the model thus obtained is fully abstract with respect to λ_{r}^{c}. The techniques used are in the line of those used by Abramsky for the lazy λ-calculus, the main departure being that the resource-consciousness of our calculi leads us to introduce a non-idempotent form of intersection types.

1. Introduction

In this paper, we address the problem of providing a denotational semantics for Boudol’s resource-conscious λ-calculus (Boudol 1993), defined with the aim of reducing the gap between the π-calculus (Milner 1989) and the lazy λ-calculus (Abramsky 1989).

The study of the connection between lazy λ-calculus and π-calculus has started with Milner’s encoding of λ into π (hereafter simply called the encoding), given in (Milner 1990). Milner’s encoding is adequate in the framework of a contextual operational semantics, but not fully abstract. That is, π-contexts over encoded λ-terms are strictly more discriminating than λ-contexts over the original terms. It has been observed that there are π-agents that behave over the encoding as (parallel) convergence testing combinators, which are not definable in pure lazy λ-calculus. On the other hand, as Boudol emphasized (Boudol 1993), the encoding does not verify the equality xx = x(λy.xy), though it is valid in weakly extensional models† of (extensions of) the λ-calculus (with parallel functions, non-deterministic choice, (parallel) convergence testing) (Abramsky

† By weakly extensional, we mean that the equation M = λy.(My) is valid for every term M which has a value (with y not free in M).

1989; Abramsky and Ong 1993; Boudol 1990; Boudol 1991). This indicates that, even if such extended λ-calculi enjoy adequate encodings into π (see for instance the encoding of lazy λ-calculus with non-deterministic choice and convergence testing in (Lavatelli 1996)), these encodings will not be fully abstract‡.

We argue that the failure of the aforementioned equality xx = x(λy.xy) is due to the fact that usual λ-calculi lack the possibility of raising deadlocks during evaluation. Indeed, one can build a π-context with only one available resource for x, say, the identity, such that the first occurrence of x can be substituted by the identity but the second one stands for a deadlocked term. In this context, the evaluation of the encoding of xx stops in a deadlocked term while that of x(λy.xy) ends in an abstraction (a value). This phenomenon is at the origin of the definition of the λ-calculus with resources λ_{r}, a refinement of pure lazy λ-calculus which allows us to control the availability of arguments. In this calculus, arguments are multisets of terms, called resources, of infinite or finite cardinality. Infinite homogeneous arguments correspond exactly to those of pure λ-calculus, and in this case, β-reductions can involve an arbitrary number of substitutions. The possibility of raising deadlocks is introduced through the finite arguments ; indeed, a finite number of resources implies a limited number of substitutions during β-reductions, and there may be more relevant free occurrences of a variable than there are resources for them. The calculus is non-deterministic because, by definition, the substitution mechanism does not follow any strategy for fetching resources from arguments. An interesting sub-calculus of λ_{r} is its deterministic version, called λ-calculus with multiplicities λ_{m}, where arguments are multisets of a unique term. Indeed, most of the results about the encoding of lazy λ-calculus into π were shown by Boudol and Laneve in the framework of multiplicities (Boudol and Laneve 1994; Boudol and Laneve 1995a; Boudol and Laneve 1995b).

The resource calculi admit different “may testing” observational semantics (Boudol 1993; Boudol and Laneve 1994; Boudol and Laneve 1995a; Boudol and Laneve 1995b). Two main scenarios have been considered : the standard one, which takes abstractions only as observables and does not distinguish between deadlock and divergence, verifies η-expansion ; the flat one, which allows us to observe both abstractions and deadlocks, does not. The question raised by Milner (Milner 1990), what is the semantics induced upon λ-terms by encoding them into the π calculus?, has been answered as follows by Boudol and Laneve : it is the flat semantics induced by contexts of the λ-calculus with multiplicities. Moreover, they show that this semantics over pure λ-terms coincides with Lévy’s algebraic semantics (Lévy 1976) and that, in fact, non-determinism does not add any extra discriminating power. As far as semantic equality is concerned, these results hold also in the standard scenario. The flat and the standard preorders correspond to two natural orderings on Lévy-Longo trees : the standard inclusion, and the Plotkin-Scott-Engeler ordering, which is essentially an η-extension of the first.

These results allow us to compare the expressiveness of λ_{m} (hence of λ_{r}) with that of

‡ Sangiorgi does achieve full abstraction for the encoding of an extension of the lazy λ-calculus with some form of non-determinism, but his result refers to a more powerful observational semantics (extended applicative bisimulation), intensional enough to distinguish λy.xy from x.

classical extensions of lazy λ-calculus. Ong shows in (Ong 1988) that the Plotkin-Scott-Engeler preorder over pure λ-terms is strictly more discriminating than the semantics induced by λ-contexts augmented with parallel convergence testing. Hence λ_{m}-contexts are strictly more discriminating than contexts of the lazy λ-calculus augmented with parallel convergence testing ; in particular, neither a non-deterministic feature nor a convergence testing facility are needed to recover the power of π-contexts over pure λterms. However, if we consider more widely terms with resources instead of pure λ-terms, convergence testing does separate some λ_{r}-terms that λ_{r}-contexts cannot distinguish.

The present work concerns the denotational semantics of resource calculi . We propose a domain equation for these calculi whose canonical solution has a logical presentation based on a refinement of the intersection type discipline (Sallé 1978; Coppo and Dezani 1980; Coppo and Dezani and Venneri 1980; Coppo and Dezani and Venneri 1981). In systems with intersection, types are preserved by expansion. The crucial point is to group type information through the use of a conjunction : if M[N/x] has type ϕ and σ_{1}, …, σ_{n} are the types given to N all along this derivation, then M has type ϕ under the assumption that x has type σ_{1}∧ ⋯ ∧σ_{n}. In agreement with the permanent availability of resources in classical λ-calculus, conjunction is idempotent, i.e., ϕ∧ϕ means exactly the same as ϕ. This is not longer suitable in resource calculi ; the refinement, originally proposed in (Boudol 1993), consists precisely in the elimination of the rule for contracting hypotheses. This type system induces an adequate semantics for λ_{r} with respect to the standard contextual or testing preorder. In (Boudol and Lavatelli 1996), a counterexample to full abstraction is constructed and full abstraction of the type semantics is shown for λ_{r}^{c}, which is λ_{r} augmented with convergence testing.

The domain equation introduced in this paper has the form D = (M(D) → D)_{⊥}, where M(D) stands for the “domain of multisets” of terms. From the strict point of view of semanticists, the equation is not completely satisfactory since the structure of M(D) does not allow for a direct interpretation of arguments ; actually, we interpret all finite approximations of an argument in order to recover its denotation. However, the fact that the canonical model induced by the equation is the exact counterpart of a simple and appropriate type system for our calculus justifies its study in our opinion. The tight relation with this economical type system is the key to our proof of full abstraction, as in the work of Abramsky and Ong (Abramsky and Ong 1993)

In section 2, we deal with syntactic issues : we present the λ-calculi with resources, give an operational semantics, and discuss expressiveness issues. We show in particular that λ_{r}^{c} allows for more discriminations than λ_{r} on terms with multiplicities. The domain equation and the interpretation function are presented in section 3. In sections 4 and 5, we recall Boudol’s type system and relate it to the domain introduced in section 3 : the meaning of a term coincides with the collection of its possible types. Finally, in section 6, we prove that the model is fully abstract with respect to λ_{r}^{c}, while it is only adequate with respect to λ_{r}.

2. λ-calculi with resources

In pure λ-calculus, arguments are managed as permanent resources : β-conversion of (λx.M)N gives M[N/x], a term where the argument N replaces x as many times as x occurs free in M. In other words, β-conversion transforms the argument N in an inexhaustible resource of the substitution process.

The λ-calculi with resources allow us to model non-permanent as well as permanent resources. In these calculi, infinitely available arguments come with an explicit infinite multiplicity : standard application reads MN^{∞}. The limited availability of arguments, hence the possibility of reaching a deadlock during evaluation, and non-determinism follow from the introduction of finite bags or multi-sets of terms as arguments. Bags are of the form (N_{1}^{m_{1}} | ⋯ | N_{k}^{m_{k}}) with m_{i} ∈ ℕ ∪ {∞}, where each component N_{i} is used as argument at most m_{i} times in a substitution process. The effective substitution of x by a multiset of cardinality q obeys two laws : (1) there are at most q replacements, and (2) these replacements are performed by necessity, that is, when x occurs in head position. Explicit substitutions ⟨P/x⟩ in the style of (Abadi and Cardelli and Curien and Lévy 1991) appear as a suitable computational device to model this kind of partial substitution, while keeping the lazy regime of evaluation. The following is an example of evaluation in resource calculi : assume P_{1}, …, P_{n} are bags of terms and let Q = (N_{1}^{m_{1}} | ⋯ | N_{k}^{m_{k}}) ; then

xP_{1} ⋯ P_{i}⟨Q/x⟩P_{i+1} ⋯ P_{n} →_{r} N_{j}P_{1} ⋯ P_{i}⟨Q′/x⟩P_{i+1} ⋯ P_{n}

for any j ∈ {1, …, k} where Q′ = (N_{1}^{m_{1}} | ⋯ | N_{j}^{m_{j}−1} | ⋯ N_{k}^{m_{k}}). It is worth noticing that the evaluation is non-deterministic since, above, any component may be fetched from Q. Remark also that the P_{i}’s are left untouched by the reduction: the rest Q′ of the bag is left available for when some other free occurrences of x will eventually reach a head position. Also, we assume as a side condition that x does not occur free in N_{j}, so that Q′ will not concern N_{j}.

2.1. Syntax

In this section, we define the three calculi used all along the paper : λ-calculus with multiplicities λ_{m} and λ-calculus with resources λ_{r}, both defined in (Boudol 1993), and λ-calculus with resources and convergence testing λ_{r}^{c} (Lavatelli 1996; Boudol and Lavatelli 1996).

Terms of λ_{r}^{c} are either variables taken from a countable set Var ranged over by u, v, w, x, y, z, …, or abstractions λx.M, or applications MP where P is the argument (a bag of terms), or expressions like M⟨P/x⟩ where ⟨P/x⟩ is a substitution entry for M, or expressions cP for testing the convergence of bag P. The grammar is the following :

Terms : (Λ_{rc}) M ::= x | λx.M | (MP) | M⟨P/x⟩ | cP
Bags : (Π) P ::= 1 | M | (P | P) | M^{∞} .

The terms of λ_{r} are just those of λ_{r}^{c} not containing c. As a further restriction, the definition of λ_{m} allows homogeneous bags only as arguments, with finite or infinite multiplicity.

y[z/x] = \{ \begin{matrix}z & if y = x \\ y & otherwise \end{matrix}

(λy.M)[z/x] = \{ \begin{matrix}λy.M & if y = x \\ λy′.M[y′/y][z/x] & otherwise, y′ new \end{matrix}
(MP)[z/x] = (M[z/x])(P [z/x])
(M⟨P/y⟩)[z/x] = \{ \begin{matrix}M⟨P [z/x]/y⟩ & if y = x \\ (M[z/x])⟨P [z/x]/y⟩ & otherwise \end{matrix}
(cP)[z/x] = c(P [z/x])
1[z/x] = 1
(P | Q)[z/x] = (P [z/x] | Q[z/x])
(M^{∞})[z/x] = (M[z/x])^{∞}

Fig. 1. Renaming

That is, the grammar for λ_{m}-terms is the following :

(Λ_{m}) M ::= x | λx.M | (MN^{k}) | M⟨N^{k}/x⟩ where k ∈ ℕ ∪ {∞}.

Here, the argument N^{0} stands for 1, and N^{k} with finite k > 0 stands for the bag (\underbrace{N | ⋯ | N}_{k times}). We shall omit multiplicity 1 in arguments, i.e.,MN will be used for MN^{1}.

We adopt the convention that L, M, N, … and P, Q, … denote terms and bags, respectively. Moreover, T stands indistinctly for bags or terms, and R, S … represent either arguments or substitution entries. We use R̃ as a short form for the sequence R_{1} … R_{n}, when n is not relevant or is known from the context. For sequences composed of substitution entries only, we often write ⟨P̃/x̃⟩ instead of ⟨P_{1}/x_{1}⟩ ⋯ ⟨P_{n}/x_{n}⟩.

Free variables of terms are defined as usual, with the following additions:

fv(M⟨P/x⟩) = fv(M) \ {x} ∪ fv(P) fv(cP) = fv(P)
fv(1) = ∅ fv(P | Q) = fv(P) ∪ fv(Q) fv(M^{∞}) = fv(M) .

Some special terms will be used throughout the paper. They are :

I = λx.x Ω = (λx.xx^{∞})(λx.xx^{∞})^{∞} .

We consider λ_{r}^{c}-terms up to α-conversion, whose definition involves the renaming oper-

\begin{aligned}M^{∞} & ≡ & (M | M^{∞}) & (P | Q) & ≡ & (Q | P) \\ P & ≡ & (1 | P) & (P | (Q | T)) & ≡ & ((P | Q) | T) \end{aligned}

P ≡ Q ⇒ \{ \begin{matrix}MP ≡ MQ \\ M⟨P/x⟩ ≡ M⟨Q/x⟩ \end{matrix}

Fig. 2. Structural equivalence

ation given in figure 1. The α-conversion M=_{α}N is the congruence generated by the following laws, when z ∉ var(M): λx.M = λz.M[z/x] and M⟨P/x⟩ = (M[z/x])⟨P/z⟩.

The congruence ≡, called structural equivalence, defined in figure 2 allows us to permute the resources of a bag and to develop infinite multiplicities.

2.2. Evaluation

The evaluation of λ_{r}^{c}-terms follows the lazy strategy adopted by Abramsky and Ong for the λ-calculus : neither the body of abstractions nor the arguments in application terms are evaluated. Moreover, the convergence testing combinator introduced by Abramsky and Ong (Abramsky and Ong 1993) can be defined as λx.cx. The set of evaluation rules consists of two parts and is given in figures 4 and 3, respectively. The first part formalizes weak β-reduction →_{rc} using explicit substitutions : there are five axioms and four structural rules. The second part establishes a mechanism for fetching resources, allowing us to perform substitutions in a delayed manner through an auxiliary relation ≻. As usual, →_{rc}^{⋆} stands for zero or more evaluation steps, →_{rc}^{+} stands for one or more evaluation steps.

The axiom for fetch, combined with the fact that we have defined evaluation up to the structural equivalence, allows us to encode non-deterministic choice at the level of

x⟨N/x⟩≻N

M⟨N/x⟩≻M′ ⇒ \{ \begin{matrix}MP ⟨N/x⟩≻M′P \\ (cM)⟨N/x⟩≻cM′ \\ M⟨P/z⟩⟨N/x⟩≻M′⟨P/z⟩ & if x ≠ z and z ∉ fv(N) \end{matrix}

Fig. 3. Fetching rules (β) (λx.M)P →_{rc} M⟨P/x⟩

(v) (λx.M)⟨P/z⟩ →_{rc} λx.(M⟨P/z⟩) if x ∉ fv(z) ∪ fv(P)

(c1) c(λx.M) →_{rc} I

(c2) cP →_{rc} cM if P ≡ (M | Q)

(fetch) M⟨N/x⟩≻M′ ⇒ M⟨(N | Q)/x⟩ →_{rc} M′⟨Q/x⟩ if x ∉ fv(N)

M →_{rc} M′ ⇒ \{ \begin{matrix}MP →_{rc} M′P \\ M⟨P/x⟩ →_{rc} M′⟨P/x⟩ \\ cM →_{rc} cM′ \\ N →_{rc} M′ & if M ≡ N \end{matrix}

Fig. 4. Evaluation in λ_{r}^{c}

terms (Boudol 1993). Indeed, setting (M⊕N) =^{def} x⟨(M | N)/x⟩ and using the fetch rule, we have both

(M⊕N) →_{rc} M⟨N/x⟩ and (M⊕N) →_{rc} N⟨M/x⟩,

provided that x ∉ fv(M) ∪ fv(N). The resulting terms M⟨N/x⟩ and N⟨M/x⟩ are essentially M and N, respectively (see lemma 2.5).

The first rule for c establishes that the testing is successful when a value is encountered ; the whole term becomes the identity so that evaluation can be pursued. Here is an illustration : (c(λx.M))(N | Q) →_{rc} I(N | Q) →_{rc}^{⋆} N⟨Q/x⟩ (with x ∉ fv(Q)). The second rule selects non-deterministically a component M from P discarding the rest of the bag. The term M becomes the argument of c. The structural rule for c allows us to evaluate its argument.

We next illustrate the fetch operation. If M = xR_{1} ⋯ R_{n}⟨N/x⟩, then a derivation M≻M′ has the following shape :

\begin{matrix}x⟨N/x⟩≻N \\ xR_{1}⟨N/x⟩≻NR_{1} \end{matrix} ; ⋮ ; xR_{1} ⋯ R_{n−1}⟨N/x⟩≻NR_{1} ⋯ R_{n−1} ; M = xR_{1} ⋯ R_{n}⟨N/x⟩≻M′ = NR_{1} ⋯ R_{n}

The rule involving c allows us to look for a substitution entry for x if the term M being tested has x as head variable.

The evaluation relations →_{r} and →_{m} for λ_{r} and λ_{m}, respectively, are defined by the subset of rules defining →_{rc} not dealing with c. Notice that for →_{m}, the fetch actually means

\begin{matrix}M⟨N/x⟩≻M′ (x ∉ fv(N)) \\ M⟨N^{k+1}/x⟩ →_{m} M′⟨N^{k}/x⟩ \end{matrix}

where we consider k = k +1 if k = ∞: hence it is deterministic. Also, rule (c2) boils down to cM^{k} →_{rc} cM (for k ≥ 1). Thus, unlike λ_{r} and λ_{r}^{c}, the calculus with multiplicities λ_{m} is deterministic up to α-conversion.

2.3. Operational semantics

We observed in the introduction that a terminating evaluation of a λ_{r}^{c}-term may end in an abstraction or a deadlock. Indeed, terms like xP_{1} ⋯ P_{n}⟨1/x⟩ are legal and may be reached during evaluation. Nevertheless, the operational semantics adopted here for λ_{r}^{c} takes abstractions only as values and does not provide any mean to detect deadlocks. Hereafter, V, W range over values, that is, over abstractions. The convergence predicate ⇓_{rc}^{l} is defined on closed terms by :

M ⇓_{rc}^{l} V ⟺^{def} (M →_{rc}^{⋆} V in l steps and V is an abstraction) .  (1)

That is, a term M converges whenever at least one evaluation issued from it ends in a value. We use the notations M ⇓_{rc}^{l} and M⇓_{rc} as short forms of (∃V M ⇓_{rc}^{l} V). We say that M diverges whenever it does not converge, written M⇑_{rc}. The convergence and divergence predicates for λ_{r} and λ_{m} are defined similarly ; we denote them by ⇓_{r}, ⇑_{r} and ⇓_{m}, ⇑_{m}, respectively.

We adopt as observational semantics the extensional preorder of Morris, also called testing preorder, where a term is approximated by another if it passes at least as many tests as the first one. The tests for terms are made up of the constructors of the language plus a constant [ ] (read it ”hole”). Tests are usually called contexts and are ranged over by capital letters A, B, C, D. We let C[M] denote the term of Λ_{rc} obtained by replacing in C all occurrences of [ ] by M. As a result of these replacements, free variables of M may become bound in C[M]. We say that C closes M if all free variables of M are bound in C[M]. A term M passes a test C whenever C[M] converges. Definition 2.1. (Observational Semantics) The testing preorder ⊑_{rc} is defined as follows :

(M ⊑_{rc} N) ⟺^{def} (C[M]⇓_{rc} ⇒ C[N]⇓_{rc} for all contexts C closing M, N) .

The testing preorders for λ_{r} and λ_{m}, ⊑_{r} and ⊑_{m}, respectively, have similar definitions. The testing preorder is also called the observational preorder.

The fact that contexts used for testing terms are of arbitrary kind makes the definition of the preorder ⊑_{rc} not workable, although it is a precongruence, i.e., if M ⊑_{rc} N then C[M] ⊑_{rc} C[N] for any context C. But it is possible to give an alternative presentation of ⊑_{rc} in terms of a restricted set of applicative contexts. Applicative contexts contain at most one hole, placed in head position ; their syntax is given by the following grammar :

A ::= [ ] | AP | A⟨P/x⟩ | cA .

Definition 2.2. The applicative preorder ⊑_{A} , with associated equivalence ≃_{A} , is defined by :

(M ⊑_{A} N) ⟺^{def} (A[M]⇓_{rc} ⇒ A[N]⇓_{rc} for all applicative contexts A closing M, N) .

Lemma 2.3. (Context Lemma) For all M, N ∈ Λ_{rc} :

(M ⊑_{rc} N) ⟺ (M ⊑_{A} N) .

Proof. A detailed proof can be found in (Lavatelli 1996), a short one in (Boudol and Lavatelli 1996).

The evaluation relation is decreasing w.r.t. the applicative preorder. Lemma 2.4. (M →_{rc} N) ⇒ (N ⊑_{A} M) .

Proof. Assume M →_{rc} N and A[N]⇓_{rc}V for some abstraction V. Since the term M appears at the head position in A[M], we have A[M] →_{rc} A[N] ; hence A[M]⇓_{rc}V.

Clearly, some permutations of substitution entries or garbage collection may be done in a term without affecting its computational content. To state this formally, let ≍ be the least relation containing ≡ ∪=_{α} and satisfying :

M⟨R/x⟩ ≍ M  x ∉ fv(M)
(MP)⟨R/x⟩ ≍ (M⟨R/x⟩)P  x ∉ fv(P)
M⟨P/z⟩⟨R/x⟩ ≍ M⟨R/x⟩⟨P/z⟩  z ≠ x, x ∉ fv(P), z ∉ fv(R)
(cM)⟨R/x⟩ ≍ c(M⟨R/x⟩)
M ≍ M′ ⇒ (MP) ≍ (M′P)
M ≍ M′ ⇒ (M⟨P/x⟩) ≍ (M′⟨P/x⟩)
M ≍ M′ ⇒ (cM) ≍ (cM′)

Notice that the last three implications are equivalent to stating that if M ≍ M′, then A[M] ≍ A[N] for any applicative context A. Lemma 2.5. (M ≍ N) ⇒ (M ≃_{A} N) .

Proof. The lemma is a consequence of the following easy property (Lavatelli 1996) :

(∗) (M ≍ N and M →_{rc} M′) ⇒ ∃N′ (N →_{rc} N′ and M′ ≍ N′) .

Let M ≍ N and A be an applicative context, so that A[M] ≍ A[N]. Suppose A[M]⇓_{rc}V ; by (∗), there is some N′ such that A[N] →_{rc}^{⋆} N′ ≍ V. Given that V is an abstraction, the only possible case of the definition of ≍ that can apply is the first one. Thus N′ = V ⟨R/x⟩ with x ∉ fv(V). But then, setting V = λy.N_{1}, we have N′ →_{rc} λy.N_{1}⟨R/x⟩, and hence A[N]⇓_{rc}.

From now on, substitution entries on variables that do not occur free will be often discarded for the sake of clarity (notably in the examples of section 2.4).

The following two technical lemmas will be used in the proofs of lemmas 6.14 and 6.8, respectively. Lemma 2.6. (MP ≃_{A} My^{∞}⟨P/y⟩), for y ∉ fv(M) ∪ fv(P).

Proof. If M is an abstraction, the proof relies on the following auxiliary equivalence (with y ∉ fv(M)) :

(∗) M⟨P/x⟩ ≃_{A} M⟨y^{∞}/x⟩⟨P/y⟩ .

This property is proved by tedious case inspection and induction on the length of the evaluation. The entry ⟨y^{∞}/x⟩ behaves as a buffer : each use of a resource of P on the right hand side is simulated by a use of y (which is always available due to the infinite multiplicity) immediately followed by a use of the same resource of P on the left hand side, and conversely. The detailed proof can be found in (Lavatelli 1996). Lemma 2.7. Let ⟨P_{0}/x⟩, ⟨P_{1}/x⟩, …, ⟨P_{n}/x⟩ be closed substitution entries on the same variable, and assume P ≡ (N_{1} | ⋯ | N_{n} | Q). Then

(M⟨P_{0}/x⟩)(N_{1}⟨P_{1}/x⟩ | ⋯ | N_{n}⟨P_{n}/x⟩ | Q) ⊑_{A} (MP)⟨(P_{0} | P_{1} | ⋯ | P_{n})/x⟩ .

Proof. The statement is shown together with the following two properties :

\begin{matrix}M⟨P_{1}/x⟩S̃_{0}⟨P_{2}/x⟩S̃_{1} ⊑_{A} MS̃_{0}⟨(P_{1} | P_{2})/x⟩S̃_{1} \\ M⟨(N_{1}⟨P_{1}/x⟩ | ⋯ | N_{n}⟨P_{n}/x⟩ | Q)/z⟩⟨P_{0}/x⟩ ⊑_{A} M⟨P/z⟩⟨(P_{0} | P_{1} | ⋯ | P_{n})/x⟩ . \end{matrix}

2.4. Expressiveness

Boudol and Laneve established the following result (Boudol and Laneve 1994) : λ_{m}- contexts over pure λ-terms are strictly more discriminating than λ-contexts augmented with the parallel convergence testing combinator p (Abramsky 1989; Abramsky and Ong 1993), whose behaviour is specified as follows :

\{ \begin{matrix}pMN → I & if either M or N converges \\ pMN diverges & otherwise. \end{matrix}

(Notice that the convergence testing operator is recovered from the parallel convergence testing by setting c = λx.pxx.) This is a quite powerful result since c is not definable within λ_{r} (and hence neither is p) ; this follows from example 2.12, where we exhibit two terms with multiplicities that are not separable by λ_{r}-contexts, but can be separated using a λ_{r}^{c}-context.

Examples 2.10 and 2.11 illustrate how multiplicities allow us to separate λ-terms that are naturally discriminated using convergence testing (also called sequential convergence testing) and parallel convergence testing, respectively, while example 2.8 shows that the increase of expressivity is in fact strict. Example 2.8. Let M = xx^{∞}, N = x(λy.xy^{∞})^{∞}. These (pure) λ-terms are equal in the theory induced by the applicative bisimulation (Abramsky 1989), even extended with parallel convergence testing combinators, but separable by means of resource contexts. Assume C = [ ]⟨I/x⟩ (giving multiplicity 1 to I). Then :

\begin{matrix}C[N] →_{m} I(λy.xy^{∞})^{∞}⟨1/x⟩ →_{r} z⟨(λy.xy^{∞})^{∞}/z⟩⟨1/x⟩ →_{r}^{⋆} λy.(xy^{∞}⟨1/x⟩) ⇓_{m} \\ C[M] →_{m} Ix^{∞}⟨1/x⟩ →_{r} z⟨x^{∞}/z⟩⟨1/x⟩ →_{r} x⟨x^{∞}/z⟩⟨1/x⟩ ≍ x⟨1/x⟩ ⇑_{m} \end{matrix}

where the last evaluation diverges since x⟨1/x⟩ is a deadlocked term. Notice that here the ability to stop evaluation does not depend on the non-deterministic features of some of the resource calculi. □

Remark 2.9. There exist other ways to distinguish terms like xx and x(λy.xy).

— A discipline for controlling the arity of functions rather than the uses of their arguments has been investigated independently in (Piperno 1995) and in (Curien 1998; Curien and Herbelin 1998)§. This control enforces that a substitution, say, by a function of one argument can only be carried out on those occurrences that have explicitly one argument. Under this discipline we have (xx)[I/x] → (Ix)[I/x] → x[I/x] where the last term is deadlocked. On the other hand (x(λy.xy))[I/x] converges : (x(λy.xy))[I/x] →^{⋆} (λy.xy)[I/x] → λy.y . As far as we know, the semantic aspects of arity control have not been investigated.

— The equality of Böhm trees has been characterized in (Dezani and Intriglia and Venturini 1998) observationally in an extension of the (non-lazy) λ-calculus with a nondeterministic choice operator and constants for numerals.

Example 2.10. Define B = x(λy.Ω)Ω and let

M = λx.xB(λy.Ω) and N = λx.x(λz.Bz)(λy.Ω).

Abramsky and Ong (Abramsky and Ong 1993) used these terms to show that the convergence testing combinator adds some separation power to ordinary λ-contexts. Indeed, the context A = [ ]c is such that A[N] converges and A[M] diverges :

A[N] → c(λz.c(λy.Ω)Ωz)(λy.Ω) → I(λy.Ω) → λy.Ω
A[M] → c(c(λy.Ω)Ω)(λy.Ω) → c(IΩ)(λy.Ω) → cΩ(λy.Ω) .

In λ_{m}, M and N are separated by the context C = [ ]U^{1}, where U = λvw.v :

C[N] →_{m} x(λz.Bz)(λy.Ω)⟨U/x⟩
→_{m} (λvw.v)(λz.Bz)(λy.Ω)⟨1/x⟩
→_{m}^{⋆} v⟨λz.Bz/v⟩⟨λy.Ω/w⟩⟨1/x⟩
→_{m}^{⋆} λz.(Bz⟨1/v⟩⟨λy.Ω/w⟩⟨1/x⟩) ⇓_{m}
C[M] →_{m}^{⋆} v⟨B/v⟩⟨λy.Ω/w⟩⟨1/x⟩
→_{m} x(λy.Ω)Ω⟨1/v⟩⟨λy.Ω/w⟩⟨1/x⟩ ⇑_{m} .

§ Piperno defines a restriction of the β-reduction, while Curien and Herbelin consider a stack-free abstract machine that gives rise to a natural game-theoretic interpretation. In both frameworks a type-free strong normalization result holds.

Notice that the term C[M] diverges just because the argument U can be used only once, that is, no resource is available for the second occurrence of x. □

Example 2.11. Define B = xΩΩ and let

M = λx.xB(xBΩ) and N = λx.xB(x(λy.By)Ω).

These terms, taken from (Boudol and Laneve 1994), illustrate the separation power of parallel convergence testing over pure λ-terms : M and N are not separable by contexts with sequential convergence testing, but can be separated if parallel convergence testing is allowed. We first explain informally why M and N are not separable in the lazy λ-calculus augmented with c. Below, the divergence ⇑c, the convergence ⇓c, and the observational equivalence ≃c are relative to this language. Assume A = [ ]LL_{1} ⋯ L_{n} ; then the observational equivalence of M and N follows from the following two facts :

1 (LΩΩ) ⇑c ⇒ A[M] ⇑c and A[N] ⇑c. We examine the different reasons for the divergence of LΩΩ : either L diverges, and then A[M] and A[N] diverge too. Or L takes one argument which is put in head position so that the statement holds since both A[M] and A[N] begin with L(LΩΩ). Or L takes two arguments and puts one of them in head position : if it is the first one, then both A[M] and A[N] diverge since (LΩΩ) ⇑c ; if it is the second one, the statement holds since then (L(LΩΩ)Ω) ⇑c and (L(λy.(LΩΩ)y)Ω) ⇑c.

2 (LΩΩ) ⇓c ⇒ A[M] ⇓c and A[N] ⇓c. This holds since for any closed H we have (H ⇓c) ⇒ (H ≃c λy.Hy). Therefore ML ≃c NL holds, and this implies A[M] ≃c A[N].

Fact (2) still holds for a λp-context. But (1) does not. Let A = [ ]p ; we have :

A[N] → p(pΩΩ) \underbrace{(p(λx.(pΩΩ)x)Ω)}_{converges} ⇓p  A[M] → p(pΩΩ) \underbrace{(p(pΩΩ)Ω)}_{diverges} ⇑p .

Notice that the convergence of A[N] could be achieved thanks to the ability of p to choose its second argument in p(pΩΩ)(p(λx.(pΩΩ)x)Ω), and then its first argument in p(λx.(pΩΩ)x)Ω. In the framework of multiplicities, Boudol and Laneve show how Böhm’s technique (Barendregt 1984; Krivine 1991) can be used to separate these two terms. Let C = [ ]P^{2}F K, where P = λx_{1}x_{2}x_{3}.x_{3}x_{1}x_{2} , K = λx_{1}x_{2}.x_{1} and F = λx_{1}x_{2}.x_{2}. The evaluation of C[N] converges with two uses of P, while C[M] would need three. During the evaluation of C[N] and C[M], the first use of P consumes F, bringing the subterms x(λz.Bz)Ω and xBΩ, respectively, in head position. Then P is used once again and consumes K, bringing λz.Bz and B = xΩΩ, respectively, in head position. That is, the evaluation of C[N] ends in an abstraction while that of C[M] ends in a deadlocked term :

C[N] →_{m}^{⋆} x_{3}x_{1}x_{2}⟨B/x_{1}⟩⟨x(λy.By)Ω/x_{2}⟩⟨P/x⟩⟨F/x_{3}⟩K
→_{m} F x_{1}x_{2}⟨B/x_{1}⟩⟨x(λy.By)Ω/x_{2}⟩⟨P/x⟩K
→_{m}^{⋆} x_{2}⟨x(λy.By)Ω/x_{2}⟩⟨P/x⟩K
→_{m} x(λy.By)Ω⟨P/x⟩K
→_{m} P (λy.By)Ω⟨1/x⟩K
→_{m}^{⋆} Kx_{1}x_{2}⟨λy.By/x_{1}⟩⟨Ω/x_{2}⟩⟨1/x⟩
→_{m}^{⋆} (λy.By)⟨1/x⟩
→_{m} λy.(By⟨1/x⟩) ⇓_{m}
C[M] →_{m}^{⋆} B⟨1/x⟩ = xΩΩ⟨1/x⟩ ⇑_{m} .

□

Example 2.12. Define L = (λy.Ω) and B = λzx.xz^{∞}, and let

M = BL^{m} and N = BL^{n} with n > m ≥ 1.

The terms M and N are not separable within λ_{r} : at most one resource L from the argument can be used during an evaluation (a proof of this can be found in (Lavatelli 1996)). In fact, both M and N behave as BL^{1} in any context. Let us illustrate this with an example : let C = [ ](I|Q_{1})Q_{2} ⋯ Q_{p} with p ≥ 1 and T = BL^{k}, with k ≥ 1 ; then

C[T] →_{r} (λx.xz^{∞})⟨L^{k}/z⟩(I | Q_{1})Q_{2} ⋯ Q_{p}
→_{r} xz^{∞}⟨L^{k}/z⟩⟨(I|Q_{1})/x⟩Q_{2} ⋯ Q_{p}
→_{r} Iz^{∞}⟨L^{k}/z⟩⟨Q_{1}/x⟩Q_{2} ⋯ Q_{p}
→_{r} w⟨z^{∞}/w⟩⟨L^{k}/z⟩⟨Q_{1}/x⟩Q_{2} ⋯ Q_{p}
→_{r}^{⋆} (λy.Ω)⟨z^{∞}/w⟩⟨L^{k−1}/z⟩⟨Q_{1}/x⟩Q_{2} ⋯ Q_{p} .

If p = 1, there are no more arguments to consume, and hence C[T]⇓_{r}, while if p ≥ 2, then

C[T] →_{r}^{⋆} Ω⟨z^{∞}/w⟩⟨L^{k−1}/z⟩⟨Q_{1}/x⟩⟨Q_{2}/y⟩Q_{3} ⋯ Q_{p} ⇑_{r} .

It should be clear that these evaluations are independent of k, provided k is at least 1. Therefore, no difference between M and N can be observed in λ_{r}. Instead, the λ_{r}^{c}-context A = [ ](λw.c^{n}(w)), where c^{i}(w) = \underbrace{(cw) ⋯ (cw)}_{i times} is a kind of convergence testing operator

of arity i, separates M and N :

A[N] →_{rc}^{⋆} (xz^{∞})⟨L^{n}/z⟩⟨λw.c^{n}(w))/x⟩
→_{rc} (λw.c^{n}(w))z^{∞}⟨L^{n}/z⟩⟨1/x⟩
→_{rc} c^{n}(w)⟨z^{∞}/w⟩⟨L^{n}/z⟩⟨1/x⟩
→_{rc}^{⋆} (cL)c^{n−1}(w)⟨z^{∞}/w⟩⟨L^{n−1}/z⟩⟨1/x⟩
→_{rc} Ic^{n−1}(w)⟨z^{∞}/w⟩⟨L^{n−1}/z⟩⟨1/x⟩
⋮
→_{rc} I⟨z^{∞}/w⟩⟨1/z⟩⟨1/x⟩ ⇓_{rc} .

But, since n − m ≥ 1, the evaluation of A[M] is deadlocked :

\begin{aligned}A[M] & →_{rc}^{⋆} & c^{n}(w)⟨z^{∞}/w⟩⟨L^{m}/z⟩⟨1/x⟩ \\ & →_{rc}^{⋆} & c^{n−m}(w)⟨z^{∞}/w⟩⟨1/z⟩⟨1/x⟩ ⇑_{rc} . \end{aligned}

□

3. Denotational semantics

In this section, we address the following two questions : what kind of domain equation can we associate with λ-calculi with resources, and what are the solutions like? Following Scott’s approach, we are led to consider domains isomorphic to (a variant of) their continuous function space (Scott 1982; Plotkin 1981). We first observe that the equation D = (D → D)_{⊥} for lazy λ-calculus is not suitable for resource calculi. Indeed, even if the canonical solution of this equation over complete lattices allows for an interpretation of non-determinism through the binary lub, or “join” operation (Boudol 1990)¶, this operator is idempotent and hence does not allow us to distinguish infinitely available resources from finite ones. In conclusion, the standard equation is not expressive enough for enabling the interpretation of the arguments in resource calculi.

In section 3.2 we propose the equation D = (M(D) → D)_{⊥} for resource calculi, where D is a complete prime algebraic lattice and M(D) is a domain of multisets. The choice of the category (complete lattices) does not only come from the need of interpreting non-determinism, but also from that of modeling the substitution process, as we will see in section 3.3.

3.1. Background

We recall some standard definitions of domain theory (Amadio and Curien 1998). A partial order is a pair (D, ⊑) where ⊑ is a binary relation on D which is reflexive, transitive and antisymmetric. A subset X of a partial order (D, ⊑) is directed iff X ≠ ∅ and if d, e ∈ X then there is an x ∈ X such that d ⊑ x and e ⊑ x. A cpo is a partial order with least element ⊥ such that every directed subset X has a least upper bound (l.u.b.), written ⨆ X. A continuous function between two cpo’s is a function preserving directed l.u.b.’s. An element d of a cpo D is compact iff for every directed subset X of D, d ⊑ ⨆ X implies d ⊑ x for some member x of X. For instance, ⊥ is compact. We will use K(D) to denote the set of compact elements of D. A cpo D is algebraic iff for every element x, the set {d ∈ D | d ∈ K(D) and d ⊑ x} is directed and has l.u.b. x. It is ω-algebraic if it is algebraic and has denumerably many compact elements.

A complete lattice is a partial order (D, ⊑) such that each subset X of D has a least upper bound ⨆ X. The binary l.u.b.’s are written x ⊔ y. A complete lattice has a least and a greatest element, namely ⊥ = ⨆ ∅ and ⊤ = ⨆ D. In this framework, an element c is compact iff for any X ⊆ D we have c ⊑ ⨆ X ⇒ c ⊑ ⨆ Y for some finite subset Y of

¶ The solution over the complete lattices is an adequate model of lazy λ-calculus and a fully abstract model of the lazy calculus augmented with c and ⊕.

X. An element p of a lattice is prime iff for any finite subset Y of D such that p ⊑ ⨆ Y there exists x ∈ Y such that p ⊑ x. Notice that ⊥ is not prime. We will denote by KP(D) the set of compact prime elements of D. We write KP_{⊥}(D) = KP(D) ∪ {⊥}. A prime algebraic lattice (p.a.l.) (Nielsen and Plotkin and Winskel 1981) is a complete lattice D such that any element x of D is the join of the compact primes it dominates:

x = ⨆{c | c ∈ KP(D) and c ⊑ x}.

Note that the definition of p.a.l. could have been given by replacing KP(D) with KP_{⊥}(D). A downset over a partial order (D, ⊑) is a subset X such that

x ∈ X and y ⊑ x ⇒ y ∈ X.

The downset completion of a partial order (D, ⊑) is the set of downsets of D ordered by inclusion, which is a prime algebraic lattice. The set of non-empty downsets is called the non-empty downset completion. A non-empty set X ⊆ D is an upperset over (D, ⊑) if and only if

x ∈ X and x ⊑ y ⇒ y ∈ X.

We denote by ↑ X the least upperset of D containing X ; for singletons {x} the notation becomes ↑ x. Proposition 3.1. Any prime algebraic lattice (D, ⊑) is isomorphic to the downset completion of its set of compact prime elements (KP(D), ⊑). Alternatively, any prime algebraic lattice (D, ⊑) is isomorphic to the non-empty downset completion of (KP_{⊥}(D), ⊑).

Proof. Let c and p be the transformations defined by :

x ∈ D ⇒ c(x) = {y | y ∈ KP(D) and y ⊑ x}.
d downset on KP(D) ⇒ p(d) = ⨆ d.

It is clear that c(x) is a downset and that p(d) is in D since every subset has a l.u.b. Moreover, x = ⨆{e | e ∈ KP(D) and e ⊑ x} implies p(c(x)) = x. It remains to prove c(p(d)) = d ; observe that

c(p(d)) = {y | y ∈ KP(D) and y ⊑ ⨆ d }
= {y | y ∈ KP(D) and y ⊑ x and x ∈ d}
= {y | y ∈ KP(D) and y ∈ d}  (d downset)
= d  (d ⊆ KP(D)) .

An ideal is a directed downset. The ideal completion Ideal(D, ⊑) of a partial order (D, ⊑) is the set of ideals of D ordered by inclusion, which is algebraic. Moreover, any algebraic cpo D is order-isomorphic to Ideal(K(D), ⊑). A filter is a co-directed upperset, that is, a non-empty set X ⊆ D is a filter over (D, ⊑) iff it is an upperset over this poset and

∀x, y ∈ X ∃z ∈ X (z ⊑ x and z ⊑ y).

Given a ∈ D, the least filter containing a is ↑ a = {x | a ⊑ x}.

We will be also concerned with the function space construction and with lifted domains. Given cpos D and E, their function space D → E is the cpo of all continuous functions from D to E with the pointwise ordering :

f ≤ g ⟺^{def} ∀x ∈ D f(x) ⊑_{E} g(x) .

We use a λ-like syntax to describe functions in (D → E) : λv ∈ D.e stands for the function f such that for any d ∈ D, f(d) is the element of E obtained by replacing v by d in e. The strict function space, D →_{⊥} E, is the set {f : D → E | f(⊥) = ⊥} whose elements are called strict continuous functions, with the pointwise ordering inherited from D → E. The lifting D_{⊥} of a partial order D is the set {⟨0, d⟩ | d ∈ D} ∪ {⊥} with the ordering :

x ≤ y iff (x = ⊥) or (∃d, d′ ∈ D d ⊑ d′ and x = ⟨0, d⟩ and y = ⟨0, d′⟩).

We often write simply d for ⟨0, d⟩. Two continuous functions, up and down, are associated with the lifting construction. Their type and definition are the following :

\begin{aligned}up & : & D → D_{⊥} & down & : & D_{⊥} →_{⊥} D \\ up(d) & = & ⟨0, d⟩ & down(⟨0, d⟩) & = & d , down(⊥) = ⊥_{D} . \end{aligned}

The lifted application (( )) : (D → E)_{⊥} ×D → E is the uncurried form of down : (D → E)_{⊥} →_{⊥} (D → E) :

f((d)) = down(f)(d) with f ∈ (D → E)_{⊥} and d ∈ D.

3.2. A domain equation for resource calculi

The aim of this section is to give a precise definition of the aforementioned domain equation D = (M(D) → D)_{⊥}. We base our construction of M(D) on the observation that it should represent multisets in the same way as powerdomains allow us to represent sets.

Given a set E, let M_{f}(E) denote the set of finite multisets of elements of E. The multiset union of u and v is denoted u ▪ v and we identify an element e ∈ E with the singleton multiset {e}. Then any multiset is a product u = e_{1} ▪ ⋯ ▪ e_{n} with n ≥ 0 and possibly with repetitions. The empty product is the empty multiset ∅, and the product operation ▪ is commutative and associative. We may also write multisets as monomials u = e_{1}^{m_{1}} ▪ ⋯ ▪ e_{k}^{m_{k}}, where the m_{i}’s are positive integers. Let (P, ⊑) be a poset ; we define the poset of finite multisets (M_{f}(P), ⋖) with least element ∅ as follows. The preorder ⋖ is the least precongruence containing ⊑ and the inclusion of multisets. That is, the least preorder on M_{f}(P) satisfying :

p ⋖ q  if p ⊑ q
u ⋖ u ▪ v
u ▪ v ⋖ u′ ▪ v′ if u ⋖ u′ and v ⋖ v′ .

We assume that q_{1} ▪ ⋯ ▪ q_{n} denotes the empty multiset when n = 0. This convention is similar to that already adopted for bags. It is easily checked that p_{1} ▪ ⋯ ▪ p_{k} ⋖ u if and only if

∃q_{1}, …, q_{k} ∀i (p_{i} ⊑ q_{i} and (u = q_{1} ▪ ⋯ ▪ q_{k} or ∃v u = q_{1} ▪ ⋯ ▪ q_{k} ▪ v)) .

Lemma 3.2. Let (P, ⊑) be a poset. The relation ⋖ is a partial order over M_{f}(P).

Proof. Let |u| be the cardinality of multiset u. Then u ⋖ v implies |u| ≤ |v |. We show (u ⋖ v ⋖ u ⇒ u = v) by induction on |u|. If |u| = 1, we have |v | = 1, so (u ⊑ v ⊑ u ⇒ u = v). If |u| > 1, let p be a maximal element of u with respect to ⊑ and u = p ▪ u′. There exist q and v′ such that v = q ▪ v′ where p ⊑ q and u′ ⋖ v′. There exist also p′, u′′ such that u = p′ ▪ u′′ with q ⊑ p′ and v′ ⋖ u′′. From p ⊑ q ⊑ p′, we get p = p′ = q because p is maximal. Hence u′ = u′′, and then u′ = v′, by the induction hypothesis.

It should be clear that M(D) will involve somehow the operation M_{f}( ). Instead of taking (K(D)−⊥, ⊑) as is classical in the construction of powerdomains, we assume that D is a prime algebraic lattice and then we define

M(D) = Ideal(Bag(D), ⋖) where Bag(D) = M_{f}(KP(D)).

In this construction, (Bag(D), ⋖) is the analog of the finite powerset ordered by the lower order, used to build up lower powerdomains.

An alternative presentation of (Bag(D), ⋖) in terms of non-empty multisets comes up naturally by associating the empty multiset to the bottom ⊥ of D. Given a poset (P, ⊑) with bottom element ⊥, let M_{f}^{∗}(P) be the set of finite non-empty multisets of P and let ⋖_{⊥} be the preorder defined as ⋖, plus ⊥ as neutral element, i.e., ⊥ ▪ u ⋖_{⊥} u. Notice that in this setting, ⊥ is the least non-empty multiset : ⊥ ⋖_{⊥} u for any non-empty multiset u just because ⊥ ⊑ p for any p in P. Proposition 3.3. The posets (M_{f}(P), ⋖) and (M_{f}^{∗}(P_{⊥}), ⋖_{⊥}) are isomorphic.

Proof. It is easy to see that the two injections b, b′ defined by

(M_{f}(P), ⋖) →^{b} (M_{f}^{∗}(P_{⊥}), ⋖_{⊥}) (M_{f}^{∗}(P_{⊥}), ⋖_{⊥}) →^{b′} (M_{f}(P), ⋖)
b(∅) = ⊥  b′(⊥) = ∅ b′(⊥ ▪ u) = b′(u)
b(p) = p b(p ▪ u) = p ▪ b(u)  b′(p) = p b′(p ▪ u) = \{ \begin{matrix}p ▪ b′(u) & if b′(u) ≠ ∅ \\ p & otherwise \end{matrix}

where p ∈ P and u ∈ M_{f}(P) or u ∈ M_{f}^{∗}(P), verify the following two statements :

u, v ∈ M_{f}(P) and u ⋖ v ⇒ b(u) ⋖_{⊥} b(v) and
u, v ∈ M_{f}^{∗}(P_{⊥}) and u ⋖_{⊥} v ⇒ b′(u) ⋖ b′(v) .

In view of this isomorphism, the domain equation D = (M(D) → D)_{⊥} becomes

D = (Ideal(M_{f}^{∗}(KP_{⊥}(D)), ⋖_{⊥}) → D)_{⊥} .

Our choice of compact primes instead of compacts elements to carry out the construction M(D) allows us to define a mapping j transforming an ideal of M(D) into an element of D for the interpretation of variables (see section 3.3). Recall that any p.a.l. D is isomorphic to the non-empty down-set completion of KP_{⊥}(D). Given an ideal of multisets, j forms the union of their underlying sets. Formally, if a ∈ M(D) :

j(a) = ⋃{ x ∈ KP_{⊥}(D) | ∃u ∈ a x ⋖ u } .

The mapping j on K(M(D)) has the following shape : Let a be the principal ideal ↓(d_{1} ▪ ⋯ ▪ d_{n}) with d_{i} ∈ KP_{⊥}(D), then

j(a) = d_{1} ⊔ ⋯ ⊔ d_{n}.

3.3. Interpretation

We explain in which sense the solutions of the domain equation defined in the previous section constitute models of λ-calculi with resources.

The interpretation function V[[M]]_{ρ} for λ_{r}^{c} takes as arguments a term M and an environment ρ closing M and gives back an element of D. Environments are mappings in Env = [V ar → M(D)] with a finite domain. We call CEnv the collection of compact environments, i.e., those environments defined on [V ar → K(M(D))].

Since M(D) does not have arbitrary l.u.b.’s, it does not allow for a direct interpretation of arguments. The meaning of a term relies on the meaning of the finite terms related to it. By finite terms we mean terms whose bags have a finite number of components. We define a binary relation P ∝ Q which captures the idea that every multiplicity in bag P becomes finite in bag Q : all infinite multiplicities of P are replaced in Q by finite ones and finite multiplicities in P may decrease their values in Q :

M^{n} ∝ \{ \begin{matrix}1 \\ M^{m} & for all m ∈ ℕ if n = ∞ \\ M^{m} & for all m ≤ n if n ∈ ℕ \end{matrix}

P ∝ P′ and Q ∝ Q′ ⇒ (P | Q) ∝ (P′ | Q′) .

Some additional notation is needed to define the interpretation function. For any finite collection V of variables, the environment ρ/_{V} is such that

ρ/_{V} (y) = \{ \begin{matrix}ρ(y) & if y ∉ V \\ undefined & otherwise. \end{matrix}

In order to simplify the notation let us define the product of compact environments, ρ_{m} ▪ ⋯ ▪ ρ_{n}, with m ≤ n, by :

(∀i ρ_{i} ∈ CEnv ⇒ (∀x ρ_{i}(x) = ↓u_{i} ⇒ (ρ_{m} ▪ ⋯ ▪ ρ_{n})(x) = ↓(u_{m} ▪ ⋯ ▪ u_{n}))) .

The definition of the interpretation of terms with resources is given in figure 3.3.

The usual interpretation V[[x]]_{ρ} = ρ(x) does not work, because values for variables are taken from M(D) and not from D. Whence the use of the mapping j : M(D) → D in the equation V[[x]]_{ρ} = j(ρ(x)). The interpretation of the abstraction is as usual in a lazy framework. The remaining constructs are application and explicit substitution, for which the environment (that is, the bags of terms associated to the free variables) should not be duplicated. Instead, environments are split and distributed to free occurrences of variables in all possible ways. Moreover, it should be obvious that any convergent evaluation of a term uses the arguments occurring in it only a finite number of times each ; hence it seems natural to compute its denotation in terms of its associated finite terms. All these contributions are collected together by means of a l.u.b. which due to the non-determinacy of evaluation is not directed. This is why we require that D is a complete lattice. Notice that the environments ρ_{0}, …, ρ_{n} used to give the semantics of application and explicit substitution are compact ones (see the definition of the product ρ_{m} ▪ ⋯ ▪ ρ_{n}). Certainly, we could have used arbitrary environments, but our choice eases technical proofs.

4. The model of uppersets in logical form

The aim of this section is to construct a concrete logical model of resource calculi in the style of logical filter models for pure (lazy) λ-calculus (see (Barendregt and Coppo and Dezani 1983; Coppo and Dezani and Honsell and Longo 1984; Ronchi 1993) and also (Boudol 1990; Boudol 1991; Dezani and de Liguoro and Piperno 1994; Dezani and de Liguoro and Piperno 1999a; Dezani and de Liguoro and Piperno 1999b)), which turns out to be a presentation of the canonical, or minimal, or initial, solution of the domain

V[[x]]_{ρ} = j(ρ(x))
V[[λx.M]]_{ρ} = up(λu ∈ M(D).V[[M]]_{ρ[x:=u]})
V[[MP]]_{ρ} = ⨆V[[M]]_{ρ_{0}}((↓d_{1} ▪ ⋯ ▪ d_{n}))

where \{ \begin{matrix}ρ ⊇ ρ_{0} ▪ ρ_{1} ▪ ⋯ ▪ ρ_{n}, \\ P ∝ (M_{1} | ⋯ | M_{n}) and \\ d_{i} ≤ V[[M_{i}]]_{ρ_{i}} ∩ KP_{⊥}(D) \end{matrix}

V[[M⟨P/x⟩]]_{ρ} = ⨆V[[M]]_{ρ_{0}[x:=↓d_{1}▪···▪d_{n}]}

where \{ \begin{matrix}ρ ⊇ ρ_{0}/_{x} ▪ ρ_{1} ▪ ⋯ ▪ ρ_{n}, \\ P ∝ (M_{1} | ⋯ | M_{n}) and \\ d_{i} ≤ V[[M_{i}]]_{ρ_{i}} ∩ KP_{⊥}(D) \end{matrix}

V[[cP]]_{ρ} = \{ \begin{matrix}V[[I]]_{ρ} & if P ≡ (M | Q) and V[[M]]_{ρ} ≠ ⊥ \\ ⊥ & otherwise \end{matrix}

Fig. 5. Interpretation function

equation defined in section 3.2 (Pitts 1996; Amadio and Curien 1998). We shall not prove nor even define more precisely canonicity here ; the details would closely follow the treatment given in, say, (Abramsky and Ong 1993). The underlying logic consists of a language of types together with an entailment relation between types. The meaning of a term is a set of formulas of the logic.

4.1. Type theory

The syntax for types (formulas) is determined by the following grammar :

\begin{aligned}(ft) & ϕ & ::= & ω | π → ϕ \\ (fb) & π & ::= & ϕ | (π × π) . \end{aligned}

Unless stated otherwise, ϕ, σ, δ will range over ft and π, ψ, θ will range over fb.

The type ω stands for the truth in the logic ; it is the least piece of information we can have about a term. Arrow types are in a sense implicative formulas used to give meaning to functions. The language for argument types involves a novel constructor × which is the logical counterpart of parallel composition. This “product” of types acts as a kind of conjunction, allowing us to group type information about the arguments of a function. For instance ((π → ϕ) × π) → ϕ will be among the types of λx.(xx). However, unlike conjunction, product is not idempotent, i.e., ϕ × ϕ is not equivalent to ϕ in general (this is the case for ϕ = ω only). If both ϕ_{0} and ϕ_{1} are informations about a term M, we cannot say that ϕ_{0} × ϕ_{1} is ; what we can say is that this product type is part of the meaning of the finite bag (M | M).

The entailment relation ϕ ≤ σ, which can be read as “ϕ implies σ”, is the least reflexive and transitive relation on fb verifying the usual laws for arrows in the weak theory of λ-calculus (1 to 3), together with additional laws for product (4 to 8) :

1. ϕ ≤ ω
2. π → ω ≤ ω → ω
3. π_{1} ≤ π_{0} and ϕ_{0} ≤ ϕ_{1} ⇒ (π_{0} → ϕ_{0}) ≤ (π_{1} → ϕ_{1})
4. ω × π ≤ π
5. π ≤ ω × π
6. π_{0} × π_{1} ≤ π_{1} × π_{0}
7. π_{0} × (π_{1} × π_{2}) ≤ (π_{0} × π_{1}) × π_{2}
8. π_{0} ≤ π′_{0} and π_{1} ≤ π′_{1} ⇒ π_{0} × π_{1} ≤ π′_{0} × π′_{1} .

Remark that × does not verify idempotency, i.e., we do not assume :

π ≤ π_{0} and π ≤ π_{1} ⇒ π ≤ (π_{0} × π_{1}).

However, × verifies the other usual properties of conjunction :

π_{0} × π_{1} ≤ π_{0} and π_{0} × π_{1} ≤ π_{1}.

We write ϕ ∼ σ whenever ϕ ≤ σ and σ ≤ ϕ are provable. For instance :

π → ω ∼ ω → ω , ω × π ∼ π , π_{0} × π_{1} ∼ π_{1} × π_{0} , and (π_{0} × π_{1}) × π_{2} ∼ π_{0} × (π_{1} × π_{2}).

The associativity of × allows us to discard parentheses from product types, whose general shape is σ_{1} × ⋯ × σ_{n} with n ≥ 1 and σ_{i} ∈ ft. Finally, observe that for any σ ∈ ft we have :

ω ≤ σ ⇒ σ = ω and σ ≠ ω ⇒ σ ≤ ω → ω.

The type theory verifies what we call the product and the arrow properties, which characterize formulas related by ≤. Definition 4.1. We define the relation π ▷ ϕ_{1}, …, ϕ_{m}, which expresses the fact that ϕ_{1}, …, ϕ_{m} are the meaningful factors (i.e., different from ω) of π, as follows :

− ω ▷ ε (the empty sequence)

− ψ → δ ▷ ψ → δ

− π ▷ ϕ_{1}, …, ϕ_{m} and π′ ▷ ϕ′_{1}, …, ϕ′_{k} ⇒ π × π′ ▷ ϕ_{1}, …, ϕ_{m}, ϕ′_{1}, …, ϕ′_{k} .

Proposition 4.2. (Product Property) Let π ▷ ϕ_{1}, …, ϕ_{n} and ψ ▷ σ_{1}, …, σ_{m}. The following equivalence holds :

π ≤ ψ ⟺ ∃i : [1, m] → [1, n] (i injective and (∀j ∈ [1, m] ϕ_{i(j)} ≤ σ_{j})) .

Moreover the size of the proof of ϕ_{i(j)} ≤ σ_{j} is at most equal to that of π ≤ ψ.

Proof. (⇐) If m = 0, then ψ = ω × ⋯ × ω, hence π ≤ ψ holds for any π by clauses 1,4 and 8 of the definition of ≤. Otherwise,

ϕ_{i(1)} × ⋯ × ϕ_{i(m)} ≤ σ_{1} × ⋯ × σ_{m} ∼ ψ by (8).

Moreover, π ≤ ϕ_{i(1)}×⋯×ϕ_{i(m)} by commutativity, 4 and 8. Hence π ≤ ψ by transitivity.

( ⇒) By structural induction on the size l of the derivation of π ≤ ψ : l = 1 : If π ≤ ψ is an instance of reflexivity or axioms 1 or 2, or 4 to 7, then n = m and the sequences ϕ_{1}, …, ϕ_{m} and σ_{1}, …, σ_{m} are equal up to permutations. That is there exists a bijection i : [1, m] → [1, m] such that ϕ_{i(j)} = σ_{j} for all j = 1, …, m. l > 1 : Three cases arise depending on whether the last rule used in the derivation of π ≤ ψ is 3, in which case there is nothing to prove, or 8 or transitivity. In the second case, π = π_{0} × π_{1} and ψ = ψ_{0} × ψ_{1} with π_{i} ≤ ψ_{i} in l_{i} steps, for i = 0, 1. We have l = l_{0} + l_{1}. Let

\begin{matrix}π_{0} ▷ ϕ_{1}, …, ϕ_{a} & π_{1} ▷ ϕ_{a+1}, …, ϕ_{n} \\ ψ_{0} ▷ σ_{1}, …, σ_{b} & ψ_{1} ▷ σ_{b+1}, …, σ_{m} . \end{matrix}

By the induction hypothesis, there exist injections k_{0} : [1, b] → [1, a] and k_{1} : [b+1, m] → [a+1, n] such that ϕ_{k_{h}(j)} ≤ σ_{j} in at most l_{h} steps for any j, with h = 0 or h = 1.. Define i : [1, m] → [1, n] by

i(j) = \{ \begin{matrix}k_{0}(j) & if 1 ≤ j ≤ b \\ k_{1}(j) & if b + 1 ≤ j ≤ m. \end{matrix}

Then ϕ_{i(j)} ≤ σ_{j} in less than l steps. Finally, if π ≤ ψ is proved by transitivity. then

π ≤ θ in l_{1} steps and θ ≤ ψ in l_{2} steps,

with l_{1} +l_{2} +1 = l. Let θ ▷ δ_{1}, …, δ_{p}. By induction, there exist two injections k_{1} : [1, p] → [1, n] and k_{2} : [1, m] → [1, p] such that ϕ_{k_{1}(j)} ≤ δ_{j} for all j = 1, …, p and δ_{k_{2}(j)} ≤ σ_{j} for all j = 1, …, m. Define i = k_{1} ∘ k_{2} : [1, m] → [1, n]. From the induction hypotheses,

ϕ_{k_{1}(k_{2}(j))} ≤ δ_{k_{2}(j)} in at most l_{1} steps and
δ_{k_{2}(j)} ≤ σ_{j}  in at most l_{2} steps.

By transitivity, ϕ_{k_{1}(k_{2}(j))} ≤ σ_{j} in at most l steps. Proposition 4.3. (Arrow Property) For all π, ψ, ϕ, σ :

(π → ϕ ≤ ψ → σ) ⟺ (σ ≠ ω ⇒ ψ ≤ π and ϕ ≤ σ) .

Proof. (⇐) By cases on σ. If σ = ω, we have

π → ϕ ≤ π → ω ≤ ω → ω ≤ ψ → ω

for any π, ϕ, ψ. If σ ≠ ω, the statement follows immediately by clause 3. ( ⇒) Assume σ ≠ ω ; we proceed by induction on the size l of the derivation of π → ϕ ≤ ψ → σ. If l = 1, then π → ϕ ≤ ψ → σ is established by reflexivity, hence π = ψ and ϕ = σ. Otherwise (i.e., l > 1), the derivation is either by application of clause 3 or by transitivity. The first case supposes ψ ≤ π and ϕ ≤ σ directly. In the second case, there exists θ such that

π → ϕ ≤ θ and θ ≤ ψ → σ,

with sizes l_{1} and l_{2}, respectively. The product property implies θ ▷ π′ → ϕ′ (θ has only one factor different from ω). That is, θ ∼ π′ → ϕ′. Thus we have π → ϕ ≤ π′ → ϕ′ ≤ ψ → σ. By induction, ψ ≤ π′ and ϕ′ ≤ σ hold. Moreover, ϕ′ ≠ ω since ω ≤ σ would imply σ = ω, contradicting the hypothesis. Then by induction again, we have ϕ ≤ ϕ′ and π′ ≤ π. Therefore, ψ ≤ π and ϕ ≤ σ.

4.2. Domain of uppersets

In order to solve the domain equation for the λ-calculi with resources, the model is required to be a p.a.l., that is the non-empty downset completion of some poset with bottom (cf. proposition 3.1). To this end we will use the poset (ft, ≤) which is in reverse order w.r.t. the standard convention : ϕ ≤ τ means that τ is less precise than ϕ. Therefore, we use the notion dual to that of non-empty downset : that of non-empty upperset, called simply upperset in the sequel. Definition 4.4. (Domain U) U is the collection of uppersets over (ft, ≤), ordered by set inclusion.

Introducing the ingredient of non-emptiness in the definition of upperset is in agreement with the intended meaning for the bottom element of the domain U, whose canonical representative must be ω. By construction, ⟨U, ⊆⟩ is a prime algebraic lattice. Its least element ⊥ is ↑ ω which is actually {ω}, its top element ⊤ is ft, and x⊔y = x∪y and x⊓y = x ∩ y. Given A ⊆ ft, we have ↑ A = ⨆{ ↑ a | a ∈ A} = ⋃{ ↑ a | a ∈ A}. The compact prime elements of U are its principal uppersets ↑ ϕ and its compact elements are finite unions of compact primes. Remark 4.5. For any ϕ, σ ∈ ft, we have ϕ ≤ σ iff ↑ σ ⊆ ↑ ϕ.

As a corollary, ∀π ↑ (ω → ω) = ↑ (π → ω) : the left-to-right inclusion holds by definition (rule 2) ; the right-to-left one holds because π ≤ ω for any π. Furthermore, if ϕ ≁ ω, then ↑ ϕ contains all functions types of the shape π → ω, since ϕ ≤ ω → ω.

We argue that the domain U is a suitable candidate to solve, up to isomorphism, the semantic equation for λ_{r}^{c} and that, in fact, it provides an adequate model for the resource calculi. The last point will be studied in the next sections. Here we treat the first point, that is, we show the following isomorphism :

U ∼ (M(U) → U)_{⊥}.

The proof is based on the observation that the domain M(U) has a concrete (logical) presentation over the poset (fb, ≤). Definition 4.6. (Domain U_{B}) U_{B} is the collection of filters over (fb, ≤), ordered by set inclusion. Remark 4.7. For any π, ψ ∈ fb, we have π ≤ ψ iff ↑ ψ ⊆ ↑ π.

The poset (U_{B}, ⊆) is an ω-algebraic cpo where the l.u.b.’s. of directed subsets of U_{B} are their union and whose compact filters are the principal filters ↑ π. The next proposition states that this poset gives a concrete presentation of the domain M(U). Proposition 4.8. U_{B} and M(U) are order-isomorphic.

Proof. Recall that M(U) = Ideal(M_{f}^{∗}(KP_{⊥}(U)), ⋖_{⊥}). It is enough to show that the sets of compact elements of U_{B} and M(U) are order-isomorphic. Those sets are the following :

\begin{aligned}K(U_{B}) & = & \{ ↑ π | π ∈ fb\} \\ K(M(U)) & = & \{↓(d_{1} ▪ ⋯ ▪ d_{n}) | n ≥ 1 and d_{i} ∈ KP_{⊥}(U)\}, \end{aligned}

where KP_{⊥}(U) = { ↑ ϕ | ϕ ∈ ft}. Define κ : fb → M_{f}^{∗}(KP_{⊥}(U)) as follows :

\begin{aligned}κ(ϕ) & = & ↑ ϕ & if ϕ ∈ ft \\ κ(π × ψ) & = & κ(π) ▪ κ(ψ). \end{aligned}

It is easy to check that ↑ π ∈ K(U_{B}) ⟺ ↓κ(π) ∈ K(M(U)). It remains to show that, for any π, ψ ∈ fb, we have

π ≤ ψ ⟺ κ(ψ) ⋖_{⊥} κ(π) .

( ⇒) If ψ ∼ ω, then κ(ψ) = (↑ ω)^{m} ⋖_{⊥} ↑ ω ⋖_{⊥} κ(π) for any π. Otherwise, assume π ▷ ϕ_{1}, …, ϕ_{n} and ψ ▷ σ_{1}, …, σ_{m}. By the product property, there is an injection i : [1, m] → [1, n] such that ϕ_{i(j)} ≤ σ_{j}. That is, ↑ σ_{j} ⋖_{⊥} ↑ ϕ_{i(j)}. Hence

κ(ψ) ⋖ ↑ σ_{1} ▪ ⋯ ▪ ↑ σ_{m} ⋖_{⊥} ↑ ϕ_{i(1)} ▪ ⋯ ▪ ↑ ϕ_{i(m)} ⋖_{⊥} κ(π).

(⇐) By structural induction on the derivation of κ(ψ) ⋖_{⊥} κ(π). Observe that whenever κ(θ) = u ▪ v, there exist θ_{0}, θ_{1} such that θ = θ_{0} × θ_{1}, κ(θ_{0}) = u and κ(θ_{1}) = v.

— If κ(ψ) ⋖_{⊥} κ(π) is proved by reflexivity, then ψ and π are equal up to commutativity, hence π ≤ ψ.

— If both π and ψ are in ft, then κ(ψ) ⋖_{⊥} κ(π) boils down to ↑ ψ ⊆ ↑ π, and we have π ≤ ψ.

— If κ(ψ) = κ(π) ▪ ⊥ ⋖_{⊥} κ(π), then ψ = π × ω. So π ≤ ψ holds.

— If κ(ψ) ⋖_{⊥} κ(ψ) ▪ κ(π′) = κ(π), then π = ψ × π′ ≤ ψ × ω ≤ ψ holds.

— If κ(ψ) = κ(ψ_{0}) ▪ κ(ψ_{1}) ⋖_{⊥} κ(π_{0}) ▪ κ(π_{1}) = κ(π) comes from κ(ψ_{0}) ⋖_{⊥} κ(π_{0}) and κ(ψ_{1}) ⋖_{⊥} κ(π_{1}), then we have π_{0} ≤ ψ_{0} and π_{1} ≤ ψ_{1} by induction. So π = π_{0}×π_{1} ≤ ψ_{0} × ψ_{1} = ψ holds.

— If κ(ψ) ⋖_{⊥} κ(θ) ⋖_{⊥} κ(π), the induction hypothesis gives θ ≤ ψ and π ≤ θ. Hence π ≤ ψ by transitivity of ≤.

In order to prove that U and (U_{B} → U)_{⊥} are isomorphic, we need to represent the continuous functions from U_{B} to U by elements of U. To this end, we successively define step functions (used to determine the compact elements of the domain U_{B} → U), the application operator of the model, and functions F and G which realize the isomorphism.

Definition 4.9. Step functions f_{πϕ} from U_{B} to U are given by :

f_{πϕ}(c) = \{ \begin{matrix}↑ ϕ & if ↑ π ⊆ c \\ ↑ ω & otherwise. \end{matrix}

Proposition 4.10. The compact elements of (U_{B} → U) are exactly given by finite least upper bounds of the shape ⨆_{I}f_{π_{i}ϕ_{i}}.

Proof. Let f ∈ (U_{B} → U), we show the following two properties :

1 f_{πϕ} ⊆ f ⟺ ↑ ϕ ⊆ f(↑ π) and 2 f = ⋃{f_{πϕ} | f_{πϕ} ⊆ f}.

The ( ⇒) direction of (1) is easy : f_{πϕ} ⊆ f ⇒ f_{πϕ}(↑ π) ⊆ f(↑ π) ⟺ ↑ ϕ ⊆ f(↑ π). As for (⇐), let ↑ ϕ ⊆ f(↑ π). It is enough to consider the case of ↑ π ⊆ c since ↑ ω is always included in f(c). By the monotonicity of f, we have f_{πϕ}(c) =↑ ϕ ⊆ f(↑ π) ⊆ f(c).

Remark that the domain (U_{B} → U) is a p.a.l. where the l.u.b’s are defined pointwise, that is (⋃g)(x) = ⋃g(x). Then, using (1), to prove (2) is the same as to prove the following equation for any x ∈ U_{B} :

f(x) = ⋃{f_{πϕ}(x) | ↑ ϕ ⊆ f(↑ π)}.

The right-hand side of the equation can be read as

A = ⋃{ ↑ ϕ | ∃π ↑ ϕ ⊆ f(↑ π) and ↑ π ⊆ x}.

Exploiting the fact that f is continuous and that any x is equal to the l.u.b. of the directed set { ↑ π | ↑ π ⊆ x}, we can check that A = ⋃{ ↑ ϕ | ↑ ϕ ⊆ f(x)} which is f(x) since U is a p.a.l.

Clearly, finite l.u.b.’s of step functions are compact, and it follows immediately from (2) that all compact functions have this form.

Definition 4.11. (Application in the model) The application · : U × U_{B} → U is the continuous function defined by :

x·y = \{ \begin{matrix}\{σ ∈ ft | ∃π ∈ y . (π → σ) ∈ x\} & if x ≠ ↑ ω \\ \{ω\} & otherwise. \end{matrix}

Corollary 4.12. If x ≠ ↑ ω, then ϕ ∈ x· ↑ π ⟺ π → ϕ ∈ x.

Proof. ( ⇒) By definition of application, there is ψ ∈ ↑ π such that ψ → ϕ ∈ x ; hence π ≤ ψ implies ψ → ϕ ≤ π → ϕ ∈ x, since x is upward closed. The (⇐) direction is even simpler.

Definition 4.13. Let F and G be the functions defined by :

U →^{F} (U_{B} → U)_{⊥} →^{G} U

F (x) = \{ \begin{matrix}up(λy ∈ U_{B}.x·y) & if x ≠ ↑ ω \\ ⊥ & otherwise \end{matrix}

G(f) = \{ \begin{matrix}↑ \{π → ϕ | ϕ ∈ f((↑ π))\} & if f ≠ ⊥ \\ ↑ ω & otherwise. \end{matrix}

As an immediate consequence of the definition, we have :

F (x)((d)) = \{ \begin{matrix}x·d & if x ≠ ↑ ω \\ ↑ ω & otherwise \end{matrix} \} = x·d .

We also note that application is continuous as a function of its second argument and preserves arbitrary l.u.b.’s as a function of its first argument, and that G preserves arbirtrary l.u.b.’s too.

Lemma 4.14. (Representation Lemma) For any h ∈ (U_{B} → U)_{⊥} and any d ∈ U_{B}, we have h((d)) = G(h)·d.

Proof. Let h ∈ (U_{B} → U)_{⊥} and d ∈ U_{B}. If h = ⊥ then

G(h)·d = ↑ ω·d = ↑ ω = ⊥((d)) .

If h = up(g), we have :

h((d)) = g( ⨆_{π∈d} ↑ π) = ⋃_{f_{ψϕ}≤g} ⋃_{π∈d}f_{ψϕ}(↑ π) and

G(h)·d = ⋃_{f_{ψϕ}≤g}G(up(f_{ψϕ}))· ⨆_{π∈d} ↑ π = ⋃_{f_{ψϕ}≤g} ⋃_{π∈d}G(up(f_{ψϕ}))· ↑ π.

Therefore, it is enough to prove, for any ϕ , ψ and π :

(∗) G(up(f_{ψϕ}))· ↑ π = f_{ψϕ}(↑ π).

It is easily seen that G(up(f_{ψϕ})) = ↑ (ψ → ϕ). Then we can establish (*) as follows :

↑ (ψ → ϕ)· ↑ π
= {σ | ψ → ϕ ≤ π → σ}  (by corollary 4.12)
= {σ | σ = ω or (σ ≠ ω and π ≤ ψ and ϕ ≤ σ)} (by the arrow property)
= f_{ψϕ}(↑ π).

Theorem 4.15. (Solution of the domain equation) Let F and G be as in definition 4.13. 1 G ∘ F = IU. 2 F ∘ G = I_{(U_{B} → U)_{⊥}}.

Proof. 1. Let x ∈ U. If x = ↑ ω, then G(F (↑ ω)) = G(⊥) = ↑ ω. Otherwise,

G(F (x)) = ↑ {π → ϕ | ϕ ∈ x· ↑ π} = ↑ {π → ϕ | π → ϕ ∈ x} = x.

2. Let f ∈ (U_{B} → U)_{⊥} ; for any d ∈ U_{B} we have

F (G(f))((d)) = G(f)·d = f((d))

by the representation lemma 4.14. Hence down(F (G(f)) = down(f), and F ∘ G = I_{(U_{B} → U)_{⊥}} then follows easily from the observation that ω → ω ∉ ↑ ω, and hence that G(g) ≠ ⊥ if g ≠ ⊥. Definition 4.16. (Denotational Semantics) The denotational preorder ⊑_{U} , with associated equivalence ≃_{U} , is given by :

M ⊑_{U} N ⟺^{def} ∀ρ ∈ CEnv V[[M]]_{ρ} ⊆ V[[N]]_{ρ}. .

5. Type assignment system

We show that the interpretation of a term in model U coincides with the set of types that can be assigned to it in the system P described below. On the way, we prove some syntactic properties of the type system such as subject expansion (theorem 5.10) and a property of extensionality (lemma 5.11).

5.1. Definition and properties

The functionality theory associated with the λ-calculus of resources with convergence testing is a sequent calculus extending the one for λ_{r} given in (Boudol 1993), which incorporates the entailment relation ϕ ≤ σ between types∥. The provable judgments are of the form Γ ⊢ T : τ where Γ, called a typing context, is a finite sequence of hypotheses x_{1} : π_{1}, …, x_{n} : π_{n}, T is a term (resp. bag of terms) and τ is a type in ft (resp. fb). We

∥ The functionality theory studied in (Boudol 1993) only involves a notion of equivalence between types ; entailment is not needed when discussing adequacy. Its role in the proof of full abstraction can be seen in the proof of the convergence lemma 6.13.

often write x ∈ Γ for ∃π x : π ∈ Γ. The usual structural rules are unified in a single rule allowing us to do a finite number of exchanges, weakenings and products of hypotheses. Definition 5.1. (Type System P) Let ≫ be the least reflexive, transitive relation containing the pairs :

(exchange) Γ, x : π, y : ψ, Δ ≫ Γ, y : ψ, x : π, Δ
(weakening)  Γ ≫ x : π, Γ
(product)  Γ, x : π, x : ψ, Δ ≫ Γ, x : π × ψ, Δ .

The rules of system P are shown in figure 6. They are essentially those of classical intersection type systems (Sallé 1978; Coppo and Dezani 1980). The difference is that the manipulation of the hypotheses in P has a “multiplicative character” : contractions are not authorized. This allows us to treat independently each occurrence of a variable and to associate one resource to each one. Notice that (L1) combined with (L8) give the more usual typing rule Γ ⊢ x : ϕ if x : ϕ is in Γ. Remark 5.2. Since terms are also bags, there are provable judgments Γ ⊢ M : π, with π ∈ fb, but it is straightforward to see that we then must have π ∼ ϕ for some ϕ ∈ ft, and Γ ⊢ M : ϕ (with a shorter proof). This is because the only freedom we have to apply rule (L5) is via structural equivalences of the sort P ≡ (1 | P) (cf. figure 2), and because the only possible types for 1 are the types equivalent to ω (through rule (L7)).

(L1) x : ϕ ⊢ x : ϕ  (L6) \begin{matrix}Γ ⊢ (M|M^{∞}) : π \\ Γ ⊢ M^{∞} : π \end{matrix}

(L2) \begin{matrix}x : π, Γ ⊢ N : ϕ \\ Γ ⊢ λx.N : π → ϕ \end{matrix} (x ∉ Γ)  ^{(L7) Γ ⊢ T : ω}

(L3) \begin{matrix}Γ ⊢ M : π → ϕ Δ ⊢ P : π \\ Γ, Δ ⊢ (MP) : ϕ \end{matrix}  (L8) \begin{matrix}Δ ⊢ T : τ \\ Γ ⊢ T : τ \end{matrix} (Δ ≫ Γ)

(L4) \begin{matrix}Γ ⊢ P : π x : π, Δ ⊢ M : ϕ \\ Γ, Δ ⊢ M⟨P/x⟩ : ϕ \end{matrix} (x ∉ Δ)  (L9) \begin{matrix}Γ ⊢ T : τ \\ Γ ⊢ T : σ \end{matrix} (τ ≤ σ)

(L5) \begin{matrix}Γ ⊢ P : π Δ ⊢ Q : ψ \\ Γ, Δ ⊢ (P |Q) : π × ψ \end{matrix}  ^{(L10) \begin{matrix}Γ ⊢ P : ω → ω \\ Γ ⊢ cP : ϕ → ϕ \end{matrix}}

Fig. 6. Type assignment system P

Definition 5.3. (Type Semantics) The type preorder ⊑_{P}, with associated equivalence ≃_{P}, is given by :

(M ⊑_{P} N) ⟺^{def} ∀Γ ∀ϕ (Γ ⊢ M : ϕ ⇒ Γ ⊢ N : ϕ) .

Lemma 5.4. The following rule is admissible in system P :

\begin{matrix}x : π, Γ ⊢ T : τ \\ x : ψ, Γ ⊢ T : τ \end{matrix} (ψ ≤ π)

that is, if the assumption is provable by the rules of P, then so is the conclusion.

Proof. The proof is by structural induction on the proof of x : π, Γ ⊢ T : τ. The interesting case is that of axiom (L1). We show the implication ψ ≤ ϕ ⇒ x : ψ ⊢ x : ϕ as follows : let ψ = σ_{1} × ⋯ × σ_{n} ≤ ϕ ; by the product property, there exists i such that σ_{i} ≤ ϕ. Then

\begin{matrix}\begin{matrix}\begin{matrix}x : σ_{i} ⊢ x : σ_{i} \\ x : σ_{i} ⊢ x : ϕ \end{matrix} & (L9) \\ x : σ_{1}, …, x : σ_{n} ⊢ x : ϕ \end{matrix} & (L8) \\ x : ψ ⊢ x : ϕ \end{matrix} (L8)

Lemma 5.4 allows us to perform additional weakenings during proofs. From now on, we consider relation ≫ enriched with the weakening axiom

ψ ≤ π ⇒ x : π, Γ ≫ x : ψ, Γ,

that is, we incorporate lemma 5.4 into the rule (L8). Definition 5.5.

— We shall freely manipulate contexts as multisets, i.e., up to uses of exchange.

— Let T be a term or a bag of terms and y a variable ; we define Γ_{T} and Γ/_{y} by induction on Γ as follows :

Γ empty ⇒ [ \begin{matrix}Γ_{T} & empty \\ Γ/_{y} & empty \end{matrix}

Γ = x : π, Δ ⇒ [ \begin{matrix}Γ_{T} & = & \{ \begin{matrix}x : π, Δ_{T} & if x ∈ fv(T) \\ Δ_{T} & otherwise \end{matrix} \\ Γ/_{y} & = & \{ \begin{matrix}x : π, Δ/_{y} & if x ≠ y \\ Δ/_{y} & otherwise. \end{matrix} \end{matrix}

— If Γ_{x} = x : π (there is only one occurrence of x in Γ) then we set Γ(x) = π.

— We denote by Γ^{×} the context such that if Γ_{x} = x : π_{1}, …, x : π_{n} then Γ^{×}(x) = π_{1} × ⋯ × π_{n} (for any x).

— We use Γ̃ to denote the smallest typing context (defined up to exchange) such that for any x : π ∈ Γ, if π = ϕ_{1} × ⋯ × ϕ_{n} with ϕ_{i} ∈ ft, then x : ϕ_{1}, …, x : ϕ_{n} ∈ Γ̃.

Next we state some simple properties of system P : Proposition 5.6. 1 Γ ⊢ T : τ ⇒ Γ̃ ⊢ T : τ. 2 Γ^{×} ⊢ T : τ ⇒ Γ ⊢ T : τ. 3 Γ ⊢ T : τ and y ∉ fv(T) ⇒ Γ/_{y} ⊢ T : τ. So Γ_{T} ⊢ T : τ holds too. 4 Γ ≫ Δ ⇒ Δ_{x}^{×}(x) ≤ Γ_{x}^{×}(x) (for all x). 5 Δ ≫ Γ and x : ψ ∈ Δ ⇒ x : π ∈ Γ and π ≤ ψ (for some π).

Proof. 1. By structural induction on the derivation Γ ⊢ T : τ. Besides induction hypotheses, we use the following properties : x̃ : π, Γ̃ ⊢ M : σ implies x : π, Γ̃ ⊢ M : σ by (L8) ; Γ = Γ_{1}, Γ_{2} implies Γ̃ = Γ̃_{1}, Γ̃_{2} ; Δ ≫ Γ implies Δ̃ ≫ Γ̃.

2. Assume Γ^{×} ⊢ M : ϕ. Then, from part (1) of this proposition, Γ̃^{×} ⊢ M : ϕ holds. Furthermore, Γ̃^{×} ≫ Γ̃ ≫ Γ. By (L8), we get Γ ⊢ M : ϕ.

3. Straightforward by induction on the derivation of Γ ⊢ T : τ.

4. By induction on the size of the proof of Γ ≫ Δ. We examine weakening only. Let Γ ≫ y : θ, Γ = Δ. If y ≠ x then Γ_{x} = Δ_{x}. If y = x, then Δ_{x}^{×}(x) = θ × Γ_{x}^{×}(x) ≤ ω × Γ_{x}^{×}(x) ≤ Γ_{x}^{×}(x).

5. Similar to part (4).

The following proposition states that type assignment within P is syntax-directed up to uses of rules (L8) and (L9). Proposition 5.7. 1 If Γ ⊢ P : π and π ▷ ϕ_{1}, …, ϕ_{n} with n ≥ 1, then there exist terms M_{1}, …, M_{n}, Q

and contexts Γ_{1}, … Γ_{n} such that P ≡ (M_{1} | ⋯ | M_{n} | Q), Γ_{1}, …, Γ_{n} ≫ Γ and ∀i ∈ {1, …, n} Γ_{i} ⊢ M_{i} : ϕ_{i} (with shorter proofs).

2 If Γ ⊢ M⟨P/x⟩ : ϕ and ϕ ≠ ω, there exist ψ, Γ_{1}, Γ_{2} such that

Γ_{1} ⊢ P : ψ and x : ψ, Γ_{2} ⊢ M : ϕ where x ∉ Γ_{2} and Γ_{1}, Γ_{2} ≫ Γ.

3 If Γ ⊢ MP : ϕ and ϕ ≠ ω, there exist π, Γ_{1}, Γ_{2} such that

Γ_{1} ⊢ M : π → ϕ and Γ_{2} ⊢ P : π where Γ_{1}, Γ_{2} ≫ Γ.

4 If Γ ⊢ λx.M : ϕ and ϕ ≠ ω, then there exist π, σ, Δ such that

x : π, Δ ⊢ M : σ where ϕ = π → σ , x ∉ Δ and Δ ≫ Γ.

Proof. All proofs are by structural induction. We examine one case of part 1 and one case of part 3 of the statement :

1. Suppose that Γ ⊢ P : π is derived by (L9). Then Γ ⊢ P : ψ with ψ ≤ π. By induction, ψ ▷ δ_{1}, …, δ_{r}, P ≡ (N_{1} | ⋯ | N_{r} | Q′), Γ_{i} ⊢ N_{i} : δ_{i} and Γ_{1}, …, Γ_{r} ≫ Γ. By the product property, there exists an injection b : [1, n] → [1, r] such that δ_{b(j)} ≤ ϕ_{j} for any j = 1, …, n. This implies n ≤ r and Γ_{b(j)} ⊢ N_{b(j)} : ϕ_{j} for any j = 1, …, n. Then, writing

(N_{1} | ⋯ | N_{r}) ≡ (N_{b(1)} | ⋯ | N_{b(n)} | Q′′) and Q = (Q′′ | Q′),

we have P ≡ (N_{b(1)} | ⋯ | N_{b(n)} | Q). Thus the conclusion holds with M_{j} = N_{b(j)}.

3. If the derivation of Γ ⊢ MP : ϕ ends with (L9), then Γ ⊢ MP : σ and σ ≤ ϕ. By induction, Γ_{1} ⊢ M : π → σ and Γ_{2} ⊢ P : π where Γ_{1}, Γ_{2} ≫ Γ. Since σ ≤ ϕ implies π → σ ≤ π → ϕ, we have Γ_{1} ⊢ M : π → ϕ by rule (L9).

Proposition 5.8. 1 Γ ⊢ x : ϕ ⇒ (ϕ ≠ ω ⇒ ∃x : π ∈ Γ π ≤ ϕ). 2 Γ ⊢ I : π → ϕ ⇒ π ≤ ϕ. 3 Γ ⊢ cx : ψ → σ ⇒ ∃x : π ∈ Γ π ≤ ω → ω and ψ ≤ σ. 4 Γ ⊢ x^{∞} : π ⇒ (π ≁ ω ⇒ ∃x : ψ_{1}, …, x : ψ_{n} ∈ Γ ψ_{1} × ⋯ × ψ_{n} ≤ π).

Proof. Part (4) is an easy consequence of proposition 5.7(1) and of part (1) of this statement. Parts (1), (2), and (3) are proved by structural induction. We examine a few cases.

1. If the derivation ends with (L8), we have Δ ⊢ x : ϕ for some Δ such that Δ ≫ Γ. By induction, some x : ψ exists in Δ with ψ ≤ ϕ. By proposition 5.6(5), x : π ∈ Γ for some π such that π ≤ ψ. Hence, π ≤ ϕ holds by transitivity.

2. We can assume ϕ ≠ ω for otherwise π ≤ ω for any π. Assume the last rule used in the derivation is (L2). Then x : π, Γ ⊢ x : ϕ with x ∉ Γ. By part (1) of this proposition, we have π ≤ ϕ. If the last rule is (L9), then Γ ⊢ I : δ for some δ ≤ π → ϕ. Since δ ∈ ft, it must be δ = π′ → ϕ′ for some formulas π′ and ϕ′. As ϕ ≠ ω, the arrow property guarantees ϕ′ ≠ ω, π ≤ π′ and ϕ′ ≤ ϕ. Moreover, π′ ≤ ϕ′ holds by induction, hence π ≤ ϕ by transitivity.

3. Assume rule (L10) is used last. Then ψ = σ and Γ ⊢ x : ω → ω. By part (1) of this proposition, there exists x : π in Γ such that π ≤ ω → ω.

Proposition 5.9. 1 M=_{α}M′ and Γ ⊢ M : ϕ ⇒ Γ ⊢ M′ : ϕ. 2 P ≡ P′ and Γ ⊢ P : π ⇒ Γ ⊢ P′ : π. 3 P ∝ Q and Γ ⊢ Q : π ⇒ Γ ⊢ P : π. In particular, x : π ⊢ x^{∞} : π since x^{∞} ∝ x and

x : π ⊢ x : π.

Proof. Part (1) is a consequence of the following property, which is established by a straightforward induction : if variables are consistently renamed in the context and in the term, then the resulting judgment is still provable. Part (2) follows from the observation that rule (L6) is in fact reversible (applying rule (L5) and assigning type ω to M). Also, the only types for 1 are those equivalent to ω. As for part (3), P ∝ Q implies P ≡ (Q | P′), hence the statement holds by part (2) (assigning type ω to P′).

The evaluation relation →_{rc} and the typing system P verify the important property of subject expansion : the types of the terms obtained during an evaluation of M are types of M too.

Theorem 5.10. (Subject expansion) If T →_{rc} T′ and Γ ⊢ T′ : τ, then Γ ⊢ T : τ.

Proof. We shall use the following property, which is easily checked :

(∗) (M⟨N/x⟩≻M′ and Γ ⊢ M′ : ϕ) ⇒ Γ ⊢ M⟨N/x⟩ : ϕ,

The proof of the lemma is by induction on the derivation of T →_{rc} T′. We examine a few cases :

— If T = (λx.M)P →_{rc} M⟨P/x⟩ = T′, then Γ_{1} ⊢ P : ψ and x : ψ, Γ_{2} ⊢ M : τ with Γ_{1}, Γ_{2} ≫ Γ and x ∉ Γ_{2} by proposition 5.7(2). Then Γ ⊢ (λx.M)P : τ by (L2) and (L3).

— If T = cV →_{rc} I = T′, then ϕ = π → σ and π ≤ σ hold by proposition 5.8(2). On the other side, Γ ⊢ cV : σ → σ holds for any value V, by (L10). So Γ ⊢ T : ϕ follows by (L9), since σ → σ ≤ ϕ.

— If T = M⟨P/x⟩ →_{rc} M′⟨Q/x⟩ = T′, where P ≡ (N | Q), M⟨N/x⟩≻M′ and x ∉ fv(N), then

Γ_{1} ⊢ Q : ψ and x : ψ, Γ_{2} ⊢ M′ : ϕ

with x ∉ Γ_{2} and Γ_{1}, Γ_{2} ≫ Γ by proposition 5.7(2). Then, x : ψ, Γ_{2} ⊢ M⟨N/x⟩ : ϕ by the property (∗). Since x is bound in M⟨N/x⟩, we have in fact Γ_{2} ⊢ M⟨N/x⟩ : ϕ, by proposition 5.6(3). By proposition 5.7(2) again, there exist π, Σ′, Σ′′ such that

Σ′ ⊢ N : π and x : π, Σ′′ ⊢ M : ϕ,

with x ∉ Σ′′ and Σ′, Σ′′ ≫ Γ_{2}. Since x : π, Σ′′ ≫ x : π, x : ψ, Σ′′ ≫ x : π × ψ, Σ′′, we get x : π × ψ, Σ′′ ⊢ M : ϕ by (L8). Then Σ′, Γ_{1}, Σ′′ ⊢ M⟨P/x⟩ : ϕ by (L4), since Σ′, Γ_{1} ⊢ (N | Q) : π × ψ by (L5). This implies Γ ⊢ T : ϕ by (L8).

We next prove an extensionality lemma for our typing system. In usual intersection type systems, this property is expressed as follows (cf. (Hindley 1982; Hindley 1983; Dezani and Margaria 1986)) :

(Γ ⊢ M : ϕ∧(ω → ω) and x ∉ fv(M)) ⇒ Γ ⊢ λx.Mx : ϕ.

Lemma 5.11. (Extensionality Lemma) Let x ∉ fv(M), x ∉ Γ. The following statement holds :

(Γ ⊢ M : π → σ) ⟺ (Γ ⊢ M : ω → ω and x : π, Γ ⊢ Mx^{∞} : σ) .

Proof. (⇒) If Γ ⊢ M : π → σ then we have Γ ⊢ M : ω → ω by (L9). By proposition 5.9(3), for any π we have x : π ⊢ x^{∞} : π, then x : π, Γ ⊢ Mx^{∞} : σ by (L3).

(⇐) Assume Γ ⊢ M : ω → ω and x : π, Γ ⊢ Mx^{∞} : σ with x ∉ Γ. If σ = ω, we know ω → ω ≤ π → ω ≤ π → σ so Γ ⊢ M : π → σ by (L9). Let σ ≠ ω. We prove Γ ⊢ M : π → σ by structural induction on the derivation of x : π, Γ ⊢ Mx^{∞} : σ, up to uses of (L8). One distinguishes cases according to which is the last rule applied. We examine the case (L3) only. Let Σ ⊢ M : ψ → σ and Δ ⊢ x^{∞} : ψ where Σ, Δ = x : π, Γ. If ψ ≁ ω ; then Δ_{x} = x : π and π ≤ ψ by proposition 5.8(4). If ψ ∼ ω, we have also obviously π ≤ ψ. On the other hand, since Σ ≫ x : π, Γ, we have x : π, Γ ⊢ M : ψ → σ by (L8), and Γ ⊢ M : ψ → σ since x ∉ fv(M). The conclusion follows by (L9).

5.2. Equivalence between the model and the type system

In this section, we show that the meaning of a term in the model U corresponds exactly to the set of types that can be given to this term in system P. We specialize the semantic function to the logical model U. Notice that ξ is a compact environment if and only if for any variable x in its domain ξ(x) = ↑ π for some π ∈ fb. A consequence of the isomorphism between U_{B} and M(U) is that the product of compact environments becomes

(∀i ∀x ρ_{i}(x) = ↑ π_{i}) ⇒ (ρ_{m} ▪ ⋯ ▪ ρ_{n})(x) = ↑ (π_{1} × ⋯ × π_{n}).

Because U solves the domain equation up to isomorphism, the equations defining the meaning of terms involve now functions F and G in the standard way. The interpretation function V : Λ_{rc} × Env → U is defined in figure 5.2.

V[[x]]_{ρ} = {ϕ ∈ ft | ϕ ∈ ρ(x)}
V[[λx.M]]_{ρ} = ↑ {π → ϕ | ϕ ∈ V[[M]]_{ρ[x:=↑π]}}
V[[MP]]_{ρ} = {σ | π ∈↑ ϕ_{1} × ⋯ × ϕ_{n} and (π → σ) ∈ V[[M]]_{ρ_{0}}} ∪ {ω}
where \{ \begin{matrix}ρ ⊇ ρ_{0} ▪ ρ_{1} ▪ ⋯ ▪ ρ_{n} \\ P ∝ (M_{1} | ⋯ | M_{n}) \\ ϕ_{i} ∈ V[[M_{i}]]_{ρ_{i}} \end{matrix}

V[[M⟨P/x⟩]]_{ρ} =  ⋃ V[[M]]_{ρ_{0}[x:=↑ϕ_{1}×···×ϕ_{n}]}
where \{ \begin{matrix}ρ ⊇ ρ_{0}/_{x} ▪ ρ_{1} ▪ ⋯ ▪ ρ_{n} \\ P ∝ (M_{1} | ⋯ | M_{n}) \\ ϕ_{i} ∈ V[[M_{i}]]_{ρ_{i}} \end{matrix}

V[[cP]]_{ρ} = \{ \begin{matrix}V[[I]] & if P ≡ (M | Q) and ω → ω ∈ V[[M]]_{ρ} \\ ⊥ & otherwise \end{matrix}

Fig. 7. Interpretation function over U

Lemma 5.12. Let M ∈ Λ_{rc} and ρ, ρ′ ∈ Env. The following properties hold :

— Monotonicity : ρ ⊆ ρ′ ⇒ V[[M]]_{ρ} ⊑ V[[M]]_{ρ′} .

— Continuity : τ ∈ V[[M]]_{ρ} ⟺ ∃ξ ∈ CEnv (ξ ⊆ ρ and τ ∈ V[[M]]_{ξ}) .

Proof. Straightforward induction on the definition of the interpretation function. Lemma 5.13. The preorder ⊑_{P} (cf. definition 5.3) is a precongruence and is closed w.r.t. =_{α} and ≡ :

— M ⊑_{P} N ⇒ ∀C C[M] ⊑_{P} C[N].

— (M=_{α}N or M ≡ N) ⇒ (M ≃_{P} N).

Proof. Part (1) is shown by induction on the context C, using proposition 5.7. Part (2) holds by proposition 5.9. Definition 5.14.

— Given Γ, the compact environment ρ_{Γ} is defined by

ρ_{Γ}(x) = ↑ Γ^{×}(x) for all variables x in Γ .

— Given ξ ∈ CEnv, the context Γ_{ξ} is defined by

Γ_{ξ} = {x : π | ξ(x) = ↑ π}.

Lemma 5.15. For any Δ, Γ and compact environment ξ, the following properties hold : 1 Δ ≫ Γ ⟺ ρ_{Δ}(x) ⊆ ρ_{Γ}(x) for any x in the domain of Δ. 2 ρ_{Δ,Γ} = ρ_{Δ} ▪ ρ_{Γ}. 3 ρ_{Γ_{ξ}} = ξ.

Proof. 1. By proposition 5.6.

2. By definition, ρ_{Δ,Γ}(x) = ↑ (Δ, Γ)^{×}(x) = ↑ (Δ^{×}(x) × Γ^{×}(x)) = ρ_{Δ} ▪ ρ_{Γ}.

3. We have :

ρ_{Γ_{ξ}}(x) = ↑ Γ_{ξ}^{×}(x) for any x ∈ Γ_{ξ}
= ↑ Γ_{ξ}(x) since ξ contains only one assumption on x
= ↑ π  with ξ(x) = ↑ π .

Lemma 5.16. (Γ ⊢ N : τ) ⇒ τ ∈ V[[N]]_{ρ_{Γ}}.

Proof. For τ = ω, the statement holds immediately. Assume τ ≠ ω. We proceed by structural induction on the derivation of Γ ⊢ N : τ. (L1) Here Γ = x : τ and N = x. Since V[[x]]_{ρ_{Γ}} = ↑ τ, τ ∈ V[[x]]_{ρ_{Γ}} holds. (L2) Here N = λx.M and τ = π → ϕ. Let Δ = x : π, Γ ; by induction we have ϕ ∈ V[[M]]_{ρ_{Δ}}. Moreover ρ_{Δ} = ρ_{Γ}[x :=↑ π], so π → ϕ ∈ V[[N]]_{ρ_{Γ}} by definition of the semantic function. (L3) Here N = (MP). Assume Δ ⊢ P : π and Σ ⊢ M : π → ϕ, with Γ = Σ, Δ. By induction, π → ϕ ∈ V[[M]]_{ρ_{Σ}}. Consider the case π ≁ ω. Let π ▷ ϕ_{1}, …, ϕ_{n}. Then there exist M_{1}, …, M_{n}, R and Δ_{1}, …, Δ_{n} such that P ≡ (M_{1} | ⋯ | M_{n} | R) and Δ_{i} ⊢ M_{i} : ϕ_{i} with Δ_{1}, …, Δ_{n} ≫ Δ. By the inductive hypothesis, we have ϕ_{i} ∈ V[[M_{i}]]_{ρ_{Δ_{i}}} for any i. Since Σ, Δ_{1}, …, Δ_{n} ≫ Γ implies ρ_{Γ} ⊇ ρ_{Σ} ▪ ρ_{Δ_{1}} ▪ ⋯ ▪ ρ_{Δ_{n}} by lemma 5.15, and since P ∝ (M_{1} | ⋯ | M_{n}), we have ϕ ∈ V[[MP]]_{ρ_{Γ}}. (L4) Here N = M⟨P/x⟩. Assume x : π, Σ ⊢ M : τ and Δ ⊢ P : π, with Σ, Δ ≫ Γ and x ∉ Σ. We have τ ∈ V[[M]]_{ρ_{Σ[x:=↑π]}} by induction. Let π ▷ ϕ_{1}, …, ϕ_{n} ; there exist some M_{1}, …, M_{n} and Δ_{1}, …, Δ_{n} such that P ∝ (M_{1} | ⋯ | M_{n}) and Δ_{i} ⊢ M_{i} : ϕ_{i} with Δ_{1}, …, Δ_{n} ≫ Δ. Then ϕ_{i} ∈ V[[M_{i}]]_{ρ_{Δ_{i}}} holds by induction. Since ξ_{Γ} ⊇ ρ_{Σ} ▪ ρ_{Δ_{1}} ▪ ⋯ ▪ ρ_{Δ_{n}} and π ∈ ↑ π, we have τ ∈ V[[M⟨P/x⟩]]_{ρ_{Γ}}. (L8) Follows from lemma 5.15(1) and by monotonicity (lemma 5.12). (L10) Here N = cP, τ = ϕ → ϕ and Γ ⊢ P : ω → ω. By proposition 5.7, there exist M, Q, Γ′ such that P ≡ (M | Q) and Γ′ ⊢ M : ω → ω, where Γ′ ≫ Γ. By induction, ω → ω ∈ V[[M]]_{ρ_{Γ′}}. By lemma 5.15 and by monotonicity, we have ω → ω ∈ V[[M]]_{ρ_{Γ}}. Then ϕ → ϕ ∈ V[[I]] = V[[cP]]_{ρ_{Γ}}. Lemma 5.17. Let ξ be a compact environment ; the meaning of a term N in this environment is obtained from the typing system in the following way :

V[[N]]_{ξ} = {τ | Γ_{ξ} ⊢ N : τ}.

Proof. Let Γ_{ξ} ⊢ N : τ. Then τ ∈ V[[N]]_{ρ_{Γ_{ξ}}} = V[[N]]_{ξ} by lemmas 5.16 and 5.15. We prove the other inclusion by structural induction on N. For τ = ω, the lemma holds immediately by rules (L7) and (L9). Assume τ ≠ ω and τ ∈ V[[N]]_{ξ}. N = x : Let ξ(x) = ↑ π ; since τ ∈ ξ(x), we have π ≤ τ. Moreover, x : τ ⊢ x : τ and x : τ ≫ x : π ≫ Γ_{ξ}, hence we obtain Γ_{ξ} ⊢ x : τ by (L8). N = λx.M : Let τ = π → ϕ ∈ V[[λx.M]]_{ξ}. Hence there exists ψ → σ such that

σ ∈ V[[M]]_{ξ[x:=↑ψ]} and ψ → σ ≤ π → ϕ.

By the arrow property, we have either ϕ = ω, then ϕ ∈ V[[M]]_{ξ[x:=↑ψ]} since denotations are non-empty, or σ ≠ ω, ϕ ≠ ω, π ≤ ψ and σ ≤ ϕ, hence ϕ ∈ V[[M]]_{ξ[x:=↑ψ]}. Since ↑ ψ ⊆ ↑ π, we have ϕ ∈ V[[M]]_{ξ[x:=↑π]} by monotonicity. Then Γ_{ξ[x:=↑π]} ⊢ M : ϕ holds by induction. Finally, Γ_{ξ[x:=↑π]} = Γ_{ξ/x}, x : π and Γ_{ξ/_{x}} ≫ Γ_{ξ} imply Γ_{ξ} ⊢ λx.M : π → ϕ by (L2) and (L8). N = (MP) : τ ∈ V[[MP]]_{ξ} means that there exist π, ϕ_{1}, …, ϕ_{n}, M_{1}, …, M_{n} and compact ξ_{0}, ξ_{1}, …, ξ_{n} such that P ∝ (M_{1} | ⋯ | M_{n}), ξ ⊇ ξ_{0} ▪ ⋯ ▪ ξ_{n}, (∀i ϕ_{i} ∈ V[[M_{i}]]_{ξ_{i}}), π ∈ ↑ ϕ_{1} × ⋯ × ϕ_{n}, and π → τ ∈ V[[M]]_{ξ_{0}}. We have Γ_{ξ_{i}} ⊢ M_{i} : ϕ_{i} and Γ_{ξ_{0}} ⊢ M : π → τ by induction. By (L5) and (L9), we get

Γ_{ξ_{1}}, …, Γ_{ξ_{n}} ⊢ (M_{1} | ⋯ | M_{n}) : π,

from which Γ_{ξ_{1}}, …, Γ_{ξ_{n}} ⊢ P : π follows by (L7) since P ≡ (M_{1} | ⋯ | M_{n} | Q) for some Q. By (L3), Γ_{ξ_{0}}, Γ_{ξ_{1}}, …, Γ_{ξ_{n}} ⊢ MP : τ. Finally, ξ ⊇ ξ_{0}▪⋯▪ξ_{n} implies Γ_{ξ_{0}}, Γ_{ξ_{1}}, …, Γ_{ξ_{n}} ≫ Γ_{ξ}. Then Γ_{ξ} ⊢ MP : τ follows by (L8). N = M⟨P/x⟩ : With the same assumptions as for application, except that ξ ⊇ ξ′_{0} ▪ ⋯ ▪ ξ_{n} with ξ′_{0} = ξ_{0}/_{x}, we have τ ∈ V[[M]]_{ξ_{0}[x:=↑ϕ_{1}×···×ϕ_{n}]}. We set π = ϕ_{1}×⋯×ϕ_{n}. By induction we have Γ_{ξ_{0}[x:=↑π]} ⊢ M : τ and Γ_{ξ_{i}} ⊢ M_{i} : ϕ_{i}. A derivation of Γ_{ξ_{1}}, …, Γ_{ξ_{n}} ⊢ P : π is obtained as above. Since Γ_{ξ_{0}[x:=↑π]} = Γ_{ξ′_{0}}, x : π and Γ_{ξ′_{0}}, Γ_{ξ_{1}}, …, Γ_{ξ_{k}} ≫ Γ_{ξ}, we conclude that Γ_{ξ} ⊢ N : τ by (L4) and (L8). N = cP : By definition, τ ∈ V[[I]] and ω → ω ∈ V[[M]]_{ξ}, where P ≡ (M | Q). Since τ = π → σ and σ ∈ V[[x]]_{[x:=↑π]}, we have π ≤ σ. On the other hand, Γ_{ξ} ⊢ M : ω → ω holds by induction, from which Γ_{ξ} ⊢ P : ω → ω follows, giving type ω to Q. Using (L10), we have Γ_{ξ} ⊢ cP : σ → σ, hence Γ_{ξ} ⊢ cP : π → σ holds by (L9). Theorem 5.18. For all M ∈ Λ_{rc} and ξ ∈ CEnv,

V[[M]]_{ξ} = {σ | ∃Γ Γ ⊢ M : σ and ρ_{Γ} ⊆ ξ}.

Proof. Assume Γ ⊢ M : σ and ρ_{Γ} ⊆ ξ. Then σ ∈ V[[M]]_{ρ_{Γ}} by lemma 5.16. By monotonicity of the interpretation we have σ ∈ V[[M]]_{ξ}. The other inclusion is immediate by lemma 5.17.

Theorem 5.19. (U and P are equivalent) For all M, N ∈ Λ_{rc} :

(M ⊑_{U} N) ⟺ (M ⊑_{P} N) .

Proof. Let M, N ∈ Λ_{rc} be such that M ⊑_{U} N and assume Γ ⊢ M : ϕ. We have :

ϕ ∈ V[[M]]_{ρ_{Γ}} (by lemma 5.16)
ϕ ∈ V[[N]]_{ρ_{Γ}} (since M ⊑_{U} N)
Γ_{ρ_{Γ}} ⊢ N : ϕ (by lemma 5.17)
Γ̃_{ρ_{Γ}} ⊢ N : ϕ (by proposition 5.6(1))
Γ ⊢ N : ϕ (since Γ̃_{ρ_{Γ}} = Γ̃ ≫ Γ).

The proof of the other implication is similar.

6. Full abstraction

The abstract semantics of λ_{r}^{c} in terms of typability within the system P is adequate with respect to the observational semantics we adopted for the calculus. This property extends the adequacy result proved for λ_{r} by Boudol (Boudol 1993). The proof technique consists in showing the soundness of typing with respect to a realizability predicate Γ ⊨ T : τ.

Moreover, we can establish that the abstract semantics is actually fully abstract as a consequence of a completeness result : if Γ ⊨ M : ϕ, then Γ ⊢ M : ϕ. The proof of completeness relies on the existence of characteristic terms M_{σ} for each type, with the property that, for any τ, M_{σ} has type τ if and only if σ ≤ τ.

6.1. Realizability of types

The realizability predicate ⊨ used here is the same as that given in (Boudol 1993) : Definition 6.1. For closed terms and bags of λ_{r}^{c}, predicate ⊨ is defined by :

⊨ M : ω  ⟺^{def} true
⊨ M : π → ϕ ⟺^{def} M⇓_{rc} and ∀P ( ⊨ P : π ⇒ ⊨ MP : ϕ)
⊨ P : π  ⟺^{def} π ▷ ϕ_{1}, …, ϕ_{n} and n > 0 and

∃R, M_{1}, …, M_{n} (P ≡ (M_{1} | ⋯ | M_{n} | R) and ⊨ M_{i} : ϕ_{i}) .

We now extend the predicate to the open terms of λ_{r}^{c}. Let Γ = x_{1} : π_{1}, …, x_{n} : π_{n} be a typing context without repeated variables such that fv(M) ⊆ {x_{1}, …, x_{n}} ; we define Γ ⊨ M : ϕ as follows :

Γ ⊨ M : ϕ ⟺^{def} ∀P_{1}, …, P_{n} (∀i ⊨ P_{i} : π_{i}) ⇒ ( ⊨ M⟨P_{1}/x_{1}⟩ ⋯ ⟨P_{n}/x_{n}⟩ : ϕ).

Definition 6.2. The preorder on Λ_{rc}, with associated equivalence ≃_{R} , is defined by :

(M ⊑_{R} N) ⟺^{def} ∀Γ , ϕ (Γ ⊨ M : ϕ) ⇒ (Γ ⊨ N : ϕ) .

We show that this preorder contains the applicative preorder (cf. definition 2.2).

Lemma 6.3. (M ⊑_{A} N) ⇒ (M ⊑_{R} N) .

Proof. Assume Γ = x_{1} : π_{1}, …, x_{n} : π_{n} and Γ ⊨ M : ϕ. We show Γ ⊨ N : ϕ by structural induction on ϕ. If ϕ = ω, the statement holds by definition of ⊨ . Assume ϕ = π → σ and let ⊨ P_{i} : π_{i} for i = 1, …, n and ⊨ Q : π. By assumption we have

1 M⟨P̃/x̃⟩⇓_{rc}, and 2 ⊨ M⟨P̃/x̃⟩Q : σ.

On one hand, from (1) we have N⟨P̃/x̃⟩⇓_{rc}, as M ⊑_{A} N and [ ]⟨P̃/x̃⟩ is an applicative context. On the other hand, M⟨P̃/x̃⟩Q ⊑_{A} N⟨P̃/x̃⟩Q since ⊑_{A} is a precongruence, hence ⊨ N⟨P̃/x̃⟩Q : σ by inductive hypotheses and (2).

6.2. Main results

Theorem 6.4. (Full Abstraction of the Type Semantics) For all M, N ∈ Λ_{rc} :

(M ⊑_{P} N) ⟺ (M ⊑_{rc} N) .

Proof. To show the ⇒ part, called adequacy, let M, N ∈ Λ_{rc} and C be a λ_{r}^{c}-context.

[figure: M ⊑_{P} N; and; C[M]⇓_{rc}; Lemma 5.13; Convergence Lemma 6.9; C[M] ⊑_{P} C[N]; and; ⊢ C[M] : ω → ω; ⊢ C[N] : ω → ω; Convergence Lemma 6.9; C[N]⇓_{rc}]

As for the ⇐ part, called completeness, let M, N ∈ Λ_{rc}, Γ be a set of hypotheses and ϕ ∈ ft. Then

[figure: M ⊑_{rc} N; and; Γ ⊢ M : ϕ; Lemma 6.3; Soundness Lemma 6.8; M ⊑_{R} N; and; Γ^{×} ⊨ M : ϕ; Γ^{×} ⊨ N : ϕ; Completeness Lemma 6.14; Γ^{×} ⊢ N : ϕ; Proposition 5.6; Γ ⊢ N : ϕ]

Theorem 6.5. (Full Abstraction of Model U) For all M, N ∈ Λ_{rc} :

(M ⊑_{U} N) ⟺ (M ⊑_{P} N) ⟺ (M ⊑_{rc} N) .

Proof. The equivalences hold by theorems 5.19 and 6.4. Remark 6.6. Without convergence testing, the model is only adequate. More precisely, if M, N range over Λ_{r} and contexts over λ_{r}-contexts, then a fortiori (M ⊑_{U} N) ⇒ (M ⊑_{r} N), but example 2.12 and theorem 6.5 show that the converse does not hold.

In the next three sections, we show the intermediate results (soundness, convergence, completeness). In order to establish completeness, we introduce characteristic bags and terms and justify their name in lemma 6.12.

6.3. Soundness

In order to prove the soundness of ⊨ with respect to ⊢, we need the following technical proposition. Proposition 6.7. 1 (Γ ⊨ M : ϕ and ϕ ≤ σ) ⇒ Γ ⊨ M : σ. 2 (Γ ⊨ M : ϕ and Γ ≫ Σ) ⇒ Σ^{×} ⊨ M : ϕ.

Proof. 1. We prove the statement for closed terms, by induction on σ. For σ = ω, it holds by definition of ⊨. If σ = ψ → σ′, the type ϕ must be π → ϕ′ for some π, ϕ′. By assumption, M⇓_{rc} ; this proves the statement for σ′ = ω. Otherwise, given ⊨ P : ψ, we show ⊨ MP : σ′. Assuming ψ ▷ ϕ_{1}, …, ϕ_{n}, the following is verified by definition of ⊨ :

P ≡ (M_{1} | ⋯ | M_{n} | R) and ⊨ M_{i} : ϕ_{i} for any i.

On the other hand, by the arrow property, we have ψ ≤ π and ϕ′ ≤ σ′. Let π ▷ δ_{1}, …, δ_{m}. By the product property, there is an injection i : [1, m] → [1, n] such that ϕ_{i(j)} ≤ δ_{j} for all j. By induction, ⊨ M_{i(j)} : δ_{j}. Then

⊨ (M_{i(1)} | ⋯ | M_{i(m)}) : δ_{1} × ⋯ × δ_{m}

implies ⊨ P : π, as the types composing π different from the δ_{i}’s are necessarily ω. By hypothesis, ⊨ MP : ϕ′. By induction, ⊨ MP : σ′.

For open terms, just observe that, if Γ = x_{1} : π_{1}, …, x : π_{n}, the assumption writes ⊨ M⟨P̃/x̃⟩ : ϕ for any P̃ such that ⊨ P_{i} : π_{i}. Then ⊨ M⟨P̃/x̃⟩ : σ. So Γ ⊨ M : σ by definition.

2. Let Σ^{×}(x_{i}) = π_{i}. If Γ(x_{i}) = ψ_{i}, then π_{i} ≤ ψ_{i} by proposition 5.6(4). Let ⊨ P_{i} : π_{i}. We have ⊨ M⟨P̃/x̃⟩ : ϕ since part (1) implies ⊨ P_{i} : ψ_{i}. Lemma 6.8. (Soundness) For all M, Γ, and ϕ :

(Γ ⊢ M : ϕ) ⇒ (Γ^{×} ⊨ M : ϕ) .

Proof. By structural induction on the derivation of Γ ⊢ M : ϕ. We assume that Γ^{×} = x_{1} : π_{1}, …, x_{k} : π_{k} for some k ≥ 0. The cases (L8) and (L9) have been already covered in proposition 6.7. We examine some other cases. (L1) Assume x : ϕ ⊢ x : ϕ. We must prove ⊨ x⟨P/x⟩ : ϕ for any P such that P ≡ (N | Q) and ⊨ N : ϕ. We have x⟨P/x⟩ →_{rc} N⟨Q/x⟩ ≍ N. Hence N ⊑_{A} x⟨P/x⟩ by lemmas 2.4 and 2.5, and ⊨ x⟨P/x⟩ : ϕ holds by lemma 6.3. (L2) The inductive hypothesis says that x : π, Γ^{×} ⊨ N : σ (with ϕ = π → σ and M = λx.N), with x ∉ Γ^{×}. Let closed P_{1}, …, P_{k}, P be such that ⊨ P : π and ⊨ P_{i} : π_{i} for all i. By definition we have

⊨ N⟨P/x⟩⟨P_{1}/x_{1}⟩ ⋯ ⟨P_{k}/x_{k}⟩ : σ.

Furthermore, since P̃ and P are closed and x ≠ x_{i} for any i, we have

(λx.N)⟨P̃/x̃⟩P →_{rc}^{⋆} (λx.(N⟨P̃/x̃⟩))P →_{rc} N⟨P̃/x̃⟩⟨P/x⟩ ≍ N⟨P/x⟩⟨P̃/x̃⟩.

This implies, ⊨ (λx.N)⟨P̃/x̃⟩P : σ, by lemmas 2.4, 2.5, and 6.3. Hence Γ ⊨ (λx.N) : π → σ by definition of ⊨. (L3) Assume Σ ⊢ N : π → ϕ and Δ ⊢ P : π (with M = (NP) and Γ = Σ, Δ) and let π ▷ ϕ_{1}, …, ϕ_{n}. By proposition 5.7(1), there exist some M_{1}, …, M_{n}, Q and Δ_{1}, …, Δ_{n} such that P ≡ (M_{1} | ⋯ | M_{n} | Q), Δ_{1}, …, Δ_{n} ≫ Δ, and Δ_{i} ⊢ M_{i} : ϕ_{i}, with shorter proofs than that of Δ ⊢ P : π. By induction, we have Δ_{i}^{×} ⊨ M_{i} : ϕ_{i} for i = 1, …, n and Σ^{×} ⊨ N : π → ϕ. Let P_{1}, …, P_{k} be closed bags such that ⊨ P_{i} : π_{i}. Since there exists δ_{i} such that

π_{i} ∼ Σ^{×}(x_{i}) × Δ^{×}(x_{i}) ∼ Σ^{×}(x_{i}) × Δ_{1}^{×}(x_{i}) × ⋯ × Δ_{n}^{×}(x_{i}) × δ_{i},

we can find Q_{i}, R_{j}^{i} and S_{i} such that P_{i} ≡ (Q_{i} | R_{1}^{i} | ⋯ | R_{n}^{i} | S_{i}), with ⊨ Q_{i} : Σ^{×}(x_{i}) and ⊨ R_{j}^{i} : Δ_{j}^{×}(x_{i}). Therefore, by definition of ⊨, the following holds :

⊨ N⟨Q̃/x̃⟩ : π → ϕ and ⊨ N_{j} : ϕ_{j} with N_{j} = M_{j}⟨R̃_{j}/x̃⟩.

By definition again, we have ⊨ (N_{1} | ⋯ | N_{n} | Q) : π and then

⊨ (N⟨Q̃/x̃⟩)(N_{1} | ⋯ | N_{n} | Q) : σ.

By lemma 2.7, (N⟨Q̃/x̃⟩)(N_{1} | ⋯ | N_{n} | Q) ⊑_{A} N(M_{1} | ⋯ | M_{n} | Q)⟨P̃/x̃⟩. Then Γ^{×} ⊨ (NP) : ϕ using lemma 6.3. (L10) Assume M = cP, ϕ = σ → σ, and Γ ⊢ P : ω → ω. By proposition 5.7, there exist N, Q, Δ such that P ≡ (N | Q), Δ ≫ Γ and Δ ⊢ N : ω → ω, with a shorter proof than that of Γ ⊢ P : ω → ω. By induction, Δ^{×} ⊨ N : ω → ω. Since Δ^{×} ≫ Γ^{×}, using proposition 6.7(2) we have Γ^{×} ⊨ N : ω → ω. Assume ⊨ Q_{i} : π_{i} and ⊨ R : σ. We must show

(cP)⟨Q̃/x̃⟩⇓_{rc} and ⊨ (cP)⟨Q̃/x̃⟩R : σ.

Since Δ^{×} ⊨ N : ω → ω, we have ⊨ N⟨Q̃/x̃⟩ : ω → ω, that is, N⟨Q̃/x̃⟩⇓_{rc}. Hence c(N⟨Q̃/x̃⟩) →_{rc}^{⋆} I. Since

(cP)⟨Q̃/x̃⟩ →_{rc} (cN)⟨Q̃/x̃⟩ ≍ c(N⟨Q̃/x̃⟩),

we have (cP)⟨Q̃/x̃⟩ →_{rc}^{⋆} I (cf. lemma 2.5). Then R ⊑_{A} (cP)⟨Q̃/x̃⟩R, which implies ⊨ (cP)⟨Q̃/x̃⟩R : σ by lemma 6.3.

The following lemma characterizes convergence by means of the notion of typability.

Lemma 6.9. (Convergence lemma) For all closed terms M :

M⇓_{rc} ⟺ ⊢ (M : ω → ω) .

Proof. Let M →_{rc}^{⋆} V with V a value ; it is easy to check that ⊢ V : ω → ω. Theorem 5.10 gives ⊢ M : ω → ω. To show the converse implication, assume ⊢ M : ω → ω. Then ⊨ M : ω → ω by lemma 6.8. That is, M⇓_{rc} by definition.

An immediate consequence of lemma 6.9 is that ω is the only type for a diverging term like Ω.

6.4. Characteristic bags and terms

Characteristic bags P_{τ} such that ⊢ P_{τ} : τ are defined by induction on the type τ they intend to characterize. If τ ∈ ft, M_{τ} stands for P_{τ}. At the same time as P_{τ} we construct a function T_{τ} which is meant to test if its argument has type τ.

Definition 6.10. (Characteristic Bags and Terms) We define P_{τ} and T_{τ}, by mutual induction on τ, as follows :

M_{ω} = Ω
T_{ω} = λx.I
M_{π → σ} = \{ \begin{matrix}λx.Ω & if σ = ω \\ λx.(T_{π}x^{∞})M_{σ} & otherwise \end{matrix}
T_{π → σ} = \{ \begin{matrix}λx.(cx) & if σ = ω \\ λx.T_{σ}(xP_{π}) & otherwise \end{matrix}

P_{π×ψ} = (P_{π} | P_{ψ})
T_{π} = λx.(T_{ϕ_{1}}x^{∞}) ⋯ (T_{ϕ_{n}}x^{∞}) if π ▷ ϕ_{1}, …, ϕ_{n} .

We briefly comment on the previous definition. For τ = ω, the choice is clear. The characteristic term of arrow type π → σ is the function (abstraction) that takes an argument of type π and gives back the characteristic term of type σ. In a typed calculus, M_{π → σ} would be λx:π.M_{σ}. Instead, we use T_{π} for controlling that the argument of the abstraction is of type π. Observe that in the definition of M_{π → ω} there is no control on the argument since π → ω ∼ ω → ω.

The definition of T_{π → σ} lies upon T_{σ} and P_{π}. First suppose σ ≠ ω. By proposition 5.7(3), M has type π → σ if and only if MP_{π} has type σ. If σ = ω, then π → σ ∼ ω → ω, and what we have to test then is that M converges (cf. lemma 6.9). Note that, in the setting of the lazy λ-calculus, a synthetic definition for the two cases just considered can be given by setting T_{π → σ} = λx.(cx)(T_{σ}(xP_{π})) (cf. (Abramsky and Ong 1993; Boudol 1990)). But that would not suit our paradigm with resources, because x occurs twice in this expression.

Characteristic bags for product types are built using parallel composition. Intuitively, the test for π × ψ must verify, successively, that the argument has the two types π and ψ, i.e., T_{π×ψ} = λx.(T_{π}x^{∞})(T_{ψ}x^{∞}). But this term is not suitable for π = ω, because it diverges when applied to a term of type ψ ∼ ω × ψ. The exact definition avoids any test on type ω.

We have used infinite multiplicities in the definition of characteristic bags and terms. In fact, finite multiplicities would have been enough. The test for types in ft uses its argument once : T_{π → σ} is linear in the abstracted variable. Moreover, the test for product types is made up of a finite number of “simple” tests (for arrow types). Thus, infinite multiplicities can be replaced by multiplicity 1 in T_{π}, while the characteristic term M_{π → σ} must allow for as many fetches of its arguments as types different from ω in π. Precisely, if π ▷ ϕ_{1}, …, ϕ_{n}, we can define M_{π → σ} = λx.(T_{π}x^{n})M_{σ}. Proposition 6.11. 1 ⊢ P_{τ} : τ. 2 ⊢ T_{τ} : τ → (σ → σ).

Proof. Straightforward.

Lemma 6.12. (Characterization Lemma) 1 Γ ⊢ P_{τ} : τ′ ⟺ τ ≤ τ′. 2 Γ ⊢ T_{τ} : τ′ → (ξ → σ) ⟺ τ′ ≤ τ and ξ ≤ σ.

Proof. In the proof, the notation (mτ) stands for property (m) at type τ. The ⇐ parts of (1) and (2) are consequence of proposition 6.11 and rule (L9). The proofs of the ⇒ parts are by induction on the type τ and then on the sizes of type derivations. Full details are given below for the most interesting cases.

Type inferences for M_{π → σ} and T_{π×ψ} involve the typings of their subterms T_{π}x^{∞} and T_{ψ}x^{∞}. In our induction, we shall make use of the fact that (2) implies the following property (3).

\begin{aligned}(3) & Γ ⊢ T_{τ} x^{∞} : ξ → σ ⇒ \\ & ξ ≤ σ and (τ ≁ ω ⇒ ∃x : ψ_{1}, …, x : ψ_{n} ∈ Γ ψ_{1} × ⋯ × ψ_{n} ≤ τ ). \end{aligned}

We show indeed that (2τ) implies (3τ) for all τ : If the type for T_{τ} x^{∞} is inferred by (L3), then we have Γ_{1} ⊢ T_{τ} : ψ → (ξ → σ) and Γ_{2} ⊢ x^{∞} : ψ with Γ = Γ_{1}, Γ_{2}. By (2τ), ψ ≤ τ and ξ ≤ σ hold. There are two cases to examine : if ψ ∼ ω, we have τ ∼ ω immediately. Otherwise, by proposition 5.8(4), there exist x : ψ_{1}, …, x : ψ_{n} ∈ Γ_{2} such that ψ_{1} × ⋯ × ψ_{n} ≤ ψ. Hence ψ_{1} × ⋯ × ψ_{n} ≤ τ holds by transitivity. If the proof of Γ ⊢ T_{τ} x^{∞} : ξ → σ ends with (L8), that is Δ ⊢ T_{τ} x^{∞} : ξ → σ holds for some Δ ≫ Γ, the inductive hypothesis gives ξ ≤ σ and

τ ≁ ω ⇒ ∃x : ψ′_{1}, …, x : ψ′_{m} ∈ Δ ψ′_{1} × ⋯ × ψ′_{m} ≤ τ.

Let Γ^{×}(x) = ψ_{1} × ⋯ × ψ_{n}. By proposition 5.6(4), ψ_{1} × ⋯ × ψ_{n} ≤ ψ′_{1} × ⋯ × ψ′_{m}, hence ψ_{1} × ⋯ × ψ_{n} ≤ τ by transitivity. If the derivation ends with (L9), i.e., Γ ⊢ T_{τ} x^{∞} : τ′ where τ′ ≤ ξ → σ, then τ′ ∼ ξ′ → σ′ for some ξ′ and σ′ (cf. remark 5.2). By induction, ξ′ ≤ σ′ and

τ ≁ ω ⇒ ∃x : ψ_{1}, …, x : ψ_{n} ∈ Γ ψ_{1} × ⋯ × ψ_{n} ≤ τ.

If σ = ω, then ξ ≤ σ holds immediately. Otherwise ξ ≤ ξ′ and σ′ ≤ σ hold by the arrow property, hence ξ ≤ σ follows by transitivity. This ends the proof of (3τ). Let us prove (1) and (2) : τ = ω : 1 The only type for Ω is ω, so τ ≤ τ′ = ω holds by reflexivity. 2 If the derivation of Γ ⊢ λx.I : τ′ → (ξ → σ) ends with (L2), i.e., x : τ′, Γ ⊢ I : ξ → σ,

then ξ ≤ σ by proposition 5.8(2). τ = π → ω : 1 If the derivation ends with (L2), i.e., τ′ = ψ → σ and x : ψ, Γ ⊢ Ω : σ, we have

π → ω ≤ ω → ω ≤ ψ → ω since ω is the only type for Ω. 2 When the last rule applied in the proof of Γ ⊢ λx.(cx) : τ′ → (ξ → σ) is (L2), we

derive τ′ ≤ ω → ω ∼ τ and ξ ≤ σ by proposition 5.8(3). τ = π → ϕ and ϕ ≠ ω : 1 We only consider the case where the derivation of Γ ⊢ λx.(T_{π}x^{∞})M_{ϕ} : τ′ ends with

(L3) followed by (L2), i.e., τ′ = π′ → ϕ′ and x : π′, Γ ⊢ (T_{π}x^{∞})M_{ϕ} : ϕ′ with x ∉ Γ. x : π′, Γ_{1} ⊢ T_{π}x^{∞} : ξ′ → ϕ′ and Γ_{2} ⊢ M_{ϕ} : ξ′, where Γ = Γ_{1}, Γ_{2}. Since (2π) holds by induction, (3π) gives ξ′ ≤ ϕ′ and π′ ≤ π. Moreover, ϕ ≤ ξ′ by induction, so ϕ ≤ ϕ′ by transitivity, and hence π → ϕ ≤ π′ → ϕ′.

2 We consider only the case of a derivation of Γ ⊢ λx.T_{ϕ}(xP_{π}) : τ′ → (ξ → σ), of the form :

(L2)

(L3) \begin{matrix}⋮ ; Γ_{1} ⊢ T_{ϕ} : ψ → (ξ → σ) & (L3) & \begin{matrix}⋮ ; x : τ′ ⊢ x : θ → ψ & ⋮ ; Γ_{2} ⊢ P_{π} : θ \\ x : τ′, Γ_{2} ⊢ xP_{π} : ψ \end{matrix} \\ x : τ′, Γ_{1}, Γ_{2} ⊢ T_{ϕ}(xP_{π}) : ξ → σ \end{matrix}
Γ = Γ_{1}, Γ_{2} ⊢ λx.T_{ϕ}(xP_{π}) : τ′ → (ξ → σ)

We have to show ξ ≤ σ and τ′ ≤ τ. We have :

— ψ ≤ ϕ and ξ ≤ σ by the inductive hypothesis on ϕ ;

— τ′ ≤ θ → ψ by proposition 5.8(1) ; hence

— τ′ ∼ π′ → ϕ′ for some π′, ϕ′ by the product property ;

— θ ≤ π′ and ϕ′ ≤ ψ by the arrow property (since ϕ ≠ ω implies ψ ≠ ω) ;

— π ≤ θ, by the inductive hypothesis on π.

Putting these results together, we get π ≤ π′ and ϕ′ ≤ ϕ, which implies τ′ ∼ π′ → ϕ′ ≤ π → ϕ = τ.

τ = π × ψ : 1 The statement follows easily by proposition 5.7(1) and by induction applied to π and

ψ. 2 As for the arrow case, we omit the details and analyze only the case of a derivation

for τ = ϕ_{0} × ϕ_{1} with ϕ_{i} ≠ ω, τ′ = ψ_{1} × ψ_{2}, and σ ≠ ω :

(L2)

(L3) \begin{matrix}⋮ ; x : ψ_{1}, Γ_{1} ⊢ T_{ϕ_{0}}x^{∞} : θ → (ξ → σ) & ⋮ ; x : ψ_{2}, Γ_{2} ⊢ T_{ϕ_{1}}x^{∞} : θ \\ x : τ′, Γ_{1}, Γ_{2} ⊢ (T_{ϕ_{0}}x^{∞})(T_{ϕ_{1}}x^{∞}) : (ξ → σ) \end{matrix}
Γ = Γ_{1}, Γ_{2} ⊢ λx.(T_{ϕ_{0}}x^{∞})(T_{ϕ_{1}}x^{∞}) : τ′ → (ξ → σ)

Some consequences of this derivation are :

— ψ_{1} ≤ ϕ_{0} and θ ≤ ξ → σ by (3ϕ_{0}) ; hence θ ∼ ξ′ → σ′ for some ξ′, σ′, and ξ ≤ ξ′ and σ′ ≤ σ ;

— ψ_{2} ≤ ϕ_{1} and ξ′ ≤ σ′ by (3ϕ_{1}).

Therefore, τ′ = ψ_{1} × ψ_{2} ≤ ϕ_{0} × ϕ_{1} ∼ τ and ξ ≤ ξ′ ≤ σ′ ≤ σ.

6.5. Completeness The following lemma singles out an important instance of the completeness result shown below (lemma 6.14). Lemma 6.13. (Γ ⊨ M : ω → ω) ⇒ (Γ ⊢ M : ω → ω) .

Proof. Let Γ ⊨ M : ω → ω with fv(M) ⊆ {x_{1}, …, x_{n}} and Γ(x_{i}) = π_{i} for all 1 ≤ i ≤ n. By lemma 6.11 and soundness, ⊨ P_{π_{i}} : π_{i} is verified. Then by lemma 6.9, M⟨P_{π_{1}}/x_{1}⟩ ⋯ ⟨P_{π_{n}}/x_{n}⟩⇓_{rc} implies ⊢ M⟨P_{π_{1}}/x_{1}⟩ ⋯ ⟨P_{π_{n}}/x_{n}⟩ : ω → ω. By proposition 5.7(2), there exist ψ_{1}, …, ψ_{n} such that ⊢ P_{π_{i}} : ψ_{i} for all i and x_{1} : ψ_{1}, …, x_{n} : ψ_{n} ⊢ M : ω → ω. Characterization lemma 6.12 gives π_{i} ≤ ψ_{i}. The conclusion Γ ⊢ M : ω → ω is obtained by (L8), since x_{1} : ψ_{1}, …, x_{n} : ψ_{n} ≫ x_{1} : π_{1}, …, x_{n} : π_{n} ≫ Γ. Lemma 6.14. (Completeness Lemma) For all M, Γ, ϕ :

(Γ ⊨ M : ϕ) ⇒ (Γ ⊢ M : ϕ) .

Proof. By structural induction on ϕ. If ϕ = ω, then Γ ⊢ M : ω by (L7). If ϕ = π → ω, then Γ ⊨ M : ω → ω and the statement holds by lemma 6.13. Assume ϕ = π → σ with σ ≠ ω and Γ = x_{1} : π_{1}, …, x_{n} : π_{n}. For any P_{1}, …, P_{n}, Q such that ⊨ P_{i} : π_{i} and ⊨ Q : π, we have

\begin{matrix}(∗) & M⟨P̃/x̃⟩⇓_{rc} and \\ (∗∗) & ⊨ M⟨P̃/x̃⟩Q : σ. \end{matrix}

We claim that (∗) implies Γ ⊢ M : ω → ω, and (∗∗) implies y : π, Γ ⊢ My^{∞} : σ, where y ∉ Γ and y ∉ fv(M). The conclusion will follow from these claims by the extensionality lemma 5.11.

We have, by the convergence lemma 6.9 and by the soundness lemma 6.8 :

M⟨P̃/x̃⟩⇓_{rc} ⇒ ( ⊢ M⟨P̃/x̃⟩ : ω → ω) ⇒ ( ⊨ M⟨P̃/x̃⟩ : ω → ω) .

Since this holds for all P̃, we have thus Γ ⊨ M : ω → ω by definition of ⊨ , and Γ ⊢ M : ω → ω follows by lemma 6.13.

By lemmas 2.5, 2.6, and 6.3, we have M⟨P̃/x̃⟩Q ≃_{R} (My^{∞})⟨Q/y⟩⟨P̃/x̃⟩. This equivalence together with (∗∗) imply ⊨ (My^{∞})⟨Q/y⟩⟨P̃/x̃⟩ : σ. Hence y : π, Γ ⊨ My^{∞} : σ, and the induction hypothesis gives y : π, Γ ⊢ My^{∞} : σ. This completes the proof of the two claims.

7. Conclusion

We have built up a denotational semantics for a non-confluent functional language incorporating the expression of deadlocks. A new domain equation has been proposed of the form D = (M(D) → D)_{⊥}, whose canonical solution constitutes an adequate model of the language. Moreover, completeness can be achieved by adding convergence testing facilities. Another equation of this kind, which differs in the definition of M(D), has been studied by the authors and presented in (Lavatelli 1996). Unlike the equation presented in this paper, it allows us to interpret the whole set of arguments and not only finite ones. The corresponding canonical solution is a filter model rather than an upperset model, and turns out to be adequate. Nevertheless, the fact that the type system used to characterize this model involves a standard conjunction operator besides the product complicates the task of showing a completeness result analogous to the one presented here for the language augmented with convergence testing. The definability technique is no longer suitable for showing this : indeed, the definition of characteristic bags for conjunctive types would imply the duplication of arguments, which goes against the philosophy of the language. However, we conjecture that completeness holds for the second model as well, and we have some confidence in the technique of logical relations for proving that the canonical solutions of these two domain equations induce in fact the same preorder on terms, and hence that the second model is fully abstract too. We leave this subject for further work.

Gérard Boudol and Pierre-Louis Curien and Carolina Lavatelli 44

References

M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy. Explicit Substitutions. Journal of Functional

Programming, 1. 1991. S. Abramsky. The Lazy Lambda Calculus. In D. Turner, editor, Research Topics in Functional

Programming, Addison Wesley. 1989. S. Abramsky, L. Ong. Full Abstraction in the Lazy Lambda Calculus. Information and Compu-

tation, 105(2). 1993. R. Amadio, P.-L. Curien. Domains and Lambda-Calculi. Cambridge University Press. 1998. H.P. Barendregt. The Lambda Calculus. North-Holland. 1984. H.P. Barendregt, M. Coppo, M. Dezani-Ciancaglini. A Filter Lambda Model and the Complete-

ness of Type Assignment. Journal of Symbolic Logic 48. 1983. G. Boudol. A Lambda-Calculus for Parallel Functions. Rapport de Recherche 1231, INRIA

Sophia-Antipolis. 1990. G. Boudol. Lambda-Calculi for (Strict) Parallel Functions. Information and Computation,

108(1). 1994. G. Boudol. The Lambda Calculus with Multiplicities. Rapport de Recherche 2025, INRIA Sophia-

Antipolis. 1993. G. Boudol, C. Laneve. The Discriminating Power of Multiplicities in the λ-Calculus. Information

and Computation, 126 (1). 1996. G. Boudol, C. Laneve. Termination, Deadlock and Divergence in the λ-Calculus with Multiplici-

ties. Proc. 11th Mathematical Foundations of Programming Semantics Conference. Electronic Notes in Computer Science. 1995.

G. Boudol, C. Laneve. λ-Calculus, Multiplicities and the π-Calculus. Rapport de Recherche 2581,

INRIA Sophia-Antipolis. 1995. G. Boudol, C. Lavatelli. Full Abstraction for Lambda-Calculus with Ressources and Convergence

Testing. CAAP’96. LNCS 1059. 1996. M. Coppo, M. Dezani-Ciancaglini. An Extension of the Basic Functionality Theory for the λ-

Calculus. Notre Dame Journal of Formal Logic, 21. 1980. M. Coppo, M. Dezani-Ciancaglini, F. Honsell, G. Longo. Extended Type Structures and Filter

Lambda Models. In G. Lolli, G. Longo, and A. Marcja, editors, Logic Colloquium 82. Elsevier Science Publishers B.V. (North-Holland). 1984.

M. Coppo, M. Dezani-Ciancaglini, B. Venneri. Principal Type Schemes and λ-Calculus Semantics. In J.R. Hindley and J.P. Seldin, editors, To H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press. 1980.

M. Coppo, M. Dezani-Ciancaglini, B. Venneri. Functional Characters of Solvable Terms. Zeit.

Math. Logik Grund, 27. 1981. P.-L. Curien. Abstract Böhm trees. Mathematical Structures in Computer Science 9. 1998. P.-L. Curien, H. Herbelin. Computing with abstract Böhm trees. Proceedings of the Third Fuji

International Symposium on Functional and Logic Programmming, Kyoto. 1998. M. Dezani-Ciancaglini, B. Intriglia, M. Venturni-Zilli. Böhm’s theorem for Böhm trees. Pro-

ceedings of the Sixth Italian Conference on Theoretical Computer Science. World Scientific. 1998.

M. Dezani-Ciancaglini, U. de Liguoro, A. Piperno. Fully Abstract Semantics for Concurrent

λ-Calculus. TACS’94. LNCS 789. 1994. M. Dezani-Ciancaglini, U. de Liguoro, A. Piperno. A Filter Model for Concurrent λ-Calculus.

Siam Journal on Computing, 27(5):1376-1419, 1998. M. Dezani-Ciancaglini, U. de Liguoro, A. Piperno. Filter Models for Conjunctive-Disjunctive

λ-Calculi. Theoretical Computer Science, 170(1-2):83-128, 1996.

A Semantics for Lambda Calculi with Resources 45

M. Dezani-Ciancaglini, I. Margaria. A Characterization of F-complete Type Assignments. The-

oretical Computer Science, 45. 1986. J.R. Hindley. The Simple Semantics for Coppo-Dezani-Sallé Types. International Symposium

on Programming. LNCS 137. 1982. J.R. Hindley. The Completeness Theorem for Typing λ-Terms. Theoretical Computer Science

22. 1983. J.-L. Krivine. Lambda-calcul, Types et Modèles. Masson. 1991. C. Lavatelli. Sémantique du Lambda Calcul avec Ressources. Thèse de Doctorat. Université Paris

VII. France. 1996. J.-J.Lévy. An Algebraic Interpretation of the λβK-Calculus ; and an Application of a Labelled

λ-Calculus. Theoretical Computer Science, 2(1). 1976. R. Milner, J. Parrow, D. Walker. A Calculus of Mobile Processes, Parts I and II. Information

and Computation, 100(1). 1992. R. Milner. Functions as Processes. Mathematical Structures in Computer Science, 2. 1992. J.H. Morris. Lambda Calculus Models of Programming Languages. PhD M.I.T. 1968. M. Nielsen, G. Plotkin, G. Winskel. Petri Nets, Event Structures and Domains. Theoretical

Computer Science, 13. 1981. C.-H. L. Ong. The Lazy Lambda Calculus/ An Investigation into the Foundations of Functional

Programming. PhD Thesis, Imperial College. 1988. A. Piperno. Normalization and extensionality. Proceeding of Logic in Computer Science (LICS

95), IEEE Computer Society Press. 1995. A. Pitts. Relational Properties of Domains. Information and Computation, 127. 1996. G. Plotkin. Post-Graduate Lecture Notes on Advanced Domain Theory. Department of Computer

Science, University of Edinburgh. 1981. S. Ronchi della Rocca. Basic Lambda-calculus. International Summer School in Logic for Com-

puter Science. Université de Savoie. 1993. P. Sallé. Une Extension de la Théorie des Types en λ-Calcul. LNCS 62. 1978. D. Sangiorgi. Expressing Mobility in Process Algebras : First Order and Higher Order Paradigms.

PhD. Thesis, Department of Computer Science, Edinburgh University. 1993. D. Sangiorgi. The Lazy Lambda Calculus in a Concurrency Scenario. Information and Compu-

tation, 120(1). 1994. D. Scott. Domains for Denotational Semantics. LNCS 140. 1982.