Lionel Vaux
email: vaux@iml.univ-mrs.fr

Convolution λµ-calculus

published or not. The documents may come

Convolution lambda-bar-mu-calculus

Introduction

Herbelin's λµ-calculus [START_REF] Herbelin | Séquents qu'on calcule[END_REF] transposes the Curry-Howard correspondence between classical natural deduction and λµ-calculus to the setting of classical sequent calculus LK (in fact one of its deterministic versions: LKT [START_REF] Vincent Danos | Sequent calculi for second order logic[END_REF]). In particular, the notion of application, corresponding to the modus ponens of natural deduction, is replaced with the notion of cut between a term and a context. More precisely, λµ-calculus involves three syntactic categories -terms, contexts and commands -given by the following grammar: In the present paper, we introduce an extension of λµ-calculus, featuring a binary operation * on contexts (and the corresponding context unit 1), which bears similarities with the convolution product of distributions. For that purpose, we further endow the 1 set of terms with a structure of commutative monoid, with addition + and neutral 0, and give the following three reduction rules: The reader may check that the reduction rules of usual λµ-calculus can be simulated in this new setting.

Outline of the Paper. In the remaining of this introduction, we briefly review notions and ideas that led to the definition of convolution λµ-calculus: it is the pure calculus associated with an extension of Ehrhard-Regnier's differential nets [START_REF] Ehrhard | Differential interaction nets[END_REF], along the lines of Laurent's polarization of linear logic proof nets [START_REF] Laurent | Etude de la polarisation en logique[END_REF]. In section 2 we introduce the objects of convolution λµ-calculus, and the associated notion of reduction, for which we prove the Church-Rosser property. In section 3 we define a reflexive object D in the category of sets and relations, following [START_REF] Bucciarelli | An extensional model of the lambda-calculus in the category of sets and relations[END_REF]. Then we introduce a type-system, in which types are elements of D, along the lines of Carvalho's system R [dC06]. We conclude by proving that terms identified by reduction have exactly the same types.

Classical Logic and Co-structural Rules

Denotational semantics of linear logic gives rise to models of simply typed λ-calculus, through the Curry-Howard isomorphism and well known translations from intuitionistic logic into linear logic. This relationship may be explicited in the syntax by encodings of typed λ-calculus into linear logic proof nets, in which β-reduction of λ-terms is accurately simulated by cut-elimination in proof nets. In fact, one may also establish such a correspondence in an untyped setting: pure λ-terms are succesfully encoded into the weakly typed nets of [START_REF] Regnier | Lambda-calcul et réseaux[END_REF].

An analoguous relationship may be observed in a setting related with classical logic rather than intuitionistic logic. In [START_REF] Laurent | Etude de la polarisation en logique[END_REF], Olivier Laurent introduced polarized linear logic and polarized proof nets. Polarized linear logic is linear logic where all formulas are polarized, and weakening and contraction are allowed on every negative formula; also, promotion is allowed on any sequent formed only of negative formulas. In [START_REF] Laurent | Polarized proof-nets and λµ-calculus[END_REF], Laurent showed how to encode Parigot's λµ-calculus [START_REF] Parigot | λµ-calculus: An algorithmic interpretation of classical natural deduction[END_REF] into polarized proof nets. Since λµ-calculus lifts the Curry-Howard correspondence from intuitionistic logic to classical logic, this encoding is the counterpart of a translation from classical natural deduction into polarized linear logic. A thorough semantical investigation on the nature of this translation may be found in [START_REF] Laurent | About translations of classical logic into polarized linear logic[END_REF].

It also happens that original models of linear logic lead to novel extensions of λcalculus, using the Curry-Howard correspondence as a tool to draw semantical properties back into the syntax. In [START_REF] Ehrhard | On Köthe sequence spaces and linear logic[END_REF] and [START_REF] Ehrhard | Finiteness spaces[END_REF], Ehrhard introduced models of linear logic in which formulas are interpreted by particular vector spaces, and proofs by linear maps between these spaces. Moreover, morphisms with type !A -• B correspond to analytic functions between A and B. This not only provided a semantics of typed λ-calculus in which λ-terms are interpreted by smooth functions between vector spaces in a very natural way, but also led to the introduction of differential λ-calculus by Ehrhard and Regnier in [START_REF] Ehrhard | The differential lambda-calculus[END_REF].

Differential Nets. Here we briefly outline some features of the differential interaction nets from [START_REF] Ehrhard | Differential interaction nets[END_REF], which may be considered as a syntactic presentation of the models from [START_REF] Ehrhard | On Köthe sequence spaces and linear logic[END_REF] and [START_REF] Ehrhard | Finiteness spaces[END_REF]. For the sake of simplicity, we use a weak typing scheme: using usual linear logic connectors and modalities, introduce type o such that o = !o -• o; we will use types o, i = o ⊥ , !o and ?i = (!o) ⊥ , to type the wires of interaction nets. We do not consider criteria for well-formedness of nets; we only focus on local, weakly typed reduction rules.

Differential interaction nets extend the interaction nets for multiplicative exponential linear logic from [START_REF] Lafont | From proof nets to interaction nets[END_REF]

∂ !o o , cocontraction: m ! !o !o !o and coweakening: u ! !o .
Cells m ! and u ! have the same geometry as tensor and tensor unit respectively: m ! connects two nets together, and u ! is a net by itself.

Recall that in the formalism of interaction nets, typing depends on the orientation of wires: if a wire has type A in one orientation, it has type A ⊥ in the reverse orientation. Also, recall that each cell has exactly one principal port (this we put on the point of our triangular cells) together with any number of auxiliary ports. A redex consists of two cells connected by their respective principal ports, in accordance with typing. Among new reduction rules introduced in differential nets, interaction between cells c ? and w ? on the one hand, and m ! and u ! on the other hand, endow exponential types with a structure of bialgebra, mainly characterized by the following interaction rule:

m ! !o !o !o c ? ?i ?i → c ? ?i c ? ?i m ! !o m ! !o !o !o !o !o .
Also, dereliction d interacts with m ! as follows:

m ! !o !o d ?i i → d ?i i w ? ?i d ?i i w ? ?i + .
The idea is that d requires one copy of an argument from its principal port, which it feeds to its auxiliary port; this argument is taken nondeterministically from either auxiliary port of m ! , hence the sum. The redex between d and w ! reduces to the 0 net (which is the neutral element of sum of nets) following the same intuition. There are of course symmetric rules for interaction between derivative ∂, and c ? and w ? , that we do not explicit here.

An extensive discussion of the intuitions behind differential reduction rules may be found in [START_REF] Ehrhard | Differential interaction nets[END_REF] and the relationship between sum and nondeterminism is developped in the introduction of [START_REF] Ehrhard | The differential lambda-calculus[END_REF]. Although this is not done in [START_REF] Ehrhard | Differential interaction nets[END_REF], one may also introduce promotion boxes in differential interaction nets, along the lines of [START_REF] Lafont | From proof nets to interaction nets[END_REF], and provide appropriate reduction rules: this allows to encode differential λ-calculus.

Polarized Nets. Polarized nets are another extension of linear logic nets. Again, we only outline a weakly typed version of the polarized proof nets of [START_REF] Laurent | Polarized proof-nets and λµ-calculus[END_REF], which we present in an interaction net flavor. The main feature of polarized nets is that contraction and weakening are generalized to type o:

c o o o o and w o o .
This accounts for structural rules on output types, which is a characteristic of classical logic. Generalized structural rules give rise to a new redex between tensor and contraction c o (or weakening w o ) cells:

c o o o ⊗ i !o i → ⊗ i ⊗ i c ? ?i c o o o !o o !o and w o ⊗ i !o i → w ? ?i w o o .
Polarized proofs nets are well suited to encode classical extensions of λ-calculus: see [START_REF] Laurent | Polarized proof-nets and λµ-calculus[END_REF] for an encoding of λµ-calculus and [Lau02, Section 12.2] for an encoding of both deterministic variants of λµμ-calculus.

Differential Structures and Classical Logic. In [START_REF] Vaux | The differential λµ-calculus[END_REF], the author introduced the differential λµ-calculus, as an attempt to uncover possible interactions between differential structures and classical logic, in a purely computational setting. The result is a pure calculus which consistently extends both differential λ-calculus and λµ-calculus.

Another possible path for studying how differential and classical constructs interact with each other lies at the level of interaction nets. One may come up with a notion of differential polarized nets, with cells those of differential nets and polarized nets altogether. Then it is easily checked that the union of the reduction rules for differential nets and for polarized nets address all possible redexes.

We do not detail further this construction, but one may verify that differential λµcalculus enjoys a natural encoding into these differential polarized nets. Hence, although differential λµ-calculus introduces a new reduction rule, which was not present in λµcalculus nor in differential λ-calculus (namely that associated with the derivative of a µ-abstraction), one may claim that it is only a side-effect of the sequentiality of λcalculus. Indeed, in the more parallel syntax of interaction nets, differential cells on the one hand, and generalized structural rules on the other hand, do not interact with each other.

A Convolution Product on Contexts. The convolution λµ-calculus defined in this paper, is the pure calculus associated with the following other variant of polarized nets: together with the cells of polarized nets, introduce the abovementioned costructural cells m ! and u ! , and also generalized versions of these,

m i i i i and u i i
i.e. cocontraction and coweakening on input type i. New redexes arise and we give the following reduction rules: m i and u i interact with c o and w o the same way as m ! and u ! interact with c ? and w ? , in particular

c o o o o m i i i → m i i m i i c o o c o o o o o o ;
also, m i duplicates and u i erases , the same way as c o and w o act on ⊗ :

→ o ?i m i i i i o o m i i m ! !o !o o !o o and o ?i u i i → u i i u ! !o .
Again, we do not detail this system further: this is still the subject of ongoing work in [START_REF] Vaux | Polarized proof nets and differential structures[END_REF]. Rather, we explicit how convolution λµ-calculus stems from it. In the translation of λµ-calculus into polarized nets, the type of dangling wires (oriented outwards) is only o or ?i. Type i only occurs in the cuts involved in the translation of application. This suggests that the computational counterpart of costructural cells on type i may be more fruitfully studied in the setting of Herbelin's λµ-calculus, where cuts appear explicitly.

One may derive a translation of λµ-calculus into polarized nets from that of λµμ Tcalculus given in [START_REF] Laurent | Etude de la polarisation en logique[END_REF], in which i types the active wire of the translation of contexts. The counterpart of m i and u i is then an associative and commutative operation on contexts that we denote by * , and its unit 1. It is argued in [Ehr01, Section 5.4], that m ! acts as a convolution product on !o, with properties similar to those of convolution of distributions; in that analogy, u ! corresponds to the Dirac mass at 0 (see also [START_REF] Ehrhard | Finiteness spaces[END_REF] Section 3], in paragraph Algebraic structure). Since the behaviour of m i and u i on type i mimics that of m ! and u ! on type !o, we may call * convolution product on contexts. We will show later that, although they live in different formalisms, * actually shares a distinctive feature with the convolution product of distributions, which further enforces this designation.

From the reduction rules of nets we have outlined, one derives that β-reduction may be generalized so that:

λx s , (t • e) * (t ′ • e ′ ) → s t + t ′ /x , e * e ′ .
Recall that nondeterministic choice provides a possible computational interpretation of sum, as described in the introduction of [START_REF] Ehrhard | The differential lambda-calculus[END_REF]. Convolution product of contexts may then be interpreted as a nondeterministic intertwining of lists of arguments.

The reduction step given above, however, only amounts to usual reduction in λµcalculus, together with the identity (t • e) * (t ′ • e ′ ) = (t + t ′ ) •(e * e ′ ) which is semantically valid (see Remark 15). Moreover, it involves synchronisation between contexts: both must have a term at top-level, for a reduction to occur. In this paper, we use a finer grained notion of reduction, the basic rules of which were given in the beginning of this introduction: this matches cut elimination between and costructural cells more closely. Also, that notion will enable us to demonstrate the link with convolution of distributions in Remark 5.

Relational Semantics. In order to underline the correspondence between convolution λµ-calculus and generalized costructural rules on i, we provide it with a denotational semantics in the category of sets and relations. In the standard relational model of linear logic, formulas are interpreted as sets and proofs as relations between these sets: see, e.g., [Ehr05, Appendix A] for precise definitions. In particular, structural rules on type A , m A = c ⊥ A , and u A = w ⊥ A , it turns out that we obtain a model of differential interaction nets. This suggests that we may derive a denotational semantics of convolution λµ-calculus from a model of λµ-calculus in the category of sets and relations.

A correspond to relations d A ⊆ !A -• A = M fin (A) × A, c A ⊆ !A -• (!A ⊗ !A) = M fin (A) × (M fin (A) × M fin (A)) and w A ⊆ !A -• 1 = M fin (A) × 1,
The model we use was introduced by Bucciarelli and Ehrhard in [START_REF] Bucciarelli | An extensional model of the lambda-calculus in the category of sets and relations[END_REF], as an extensional lambda-model in the category of sets and relations. It is naturally endowed with a monoid structure, which is suitable to provide a denotational semantics of λµcalculus along the lines of [START_REF] Laurent | About translations of classical logic into polarized linear logic[END_REF]: monoid operation and unit model structural rules on o. We also use those monoid laws to handle the denotational semantics of convolution product: the same as for costructural rules, this amounts to reverse the direction of the corresponding relation.

Related Work

A system of intersection and union types for the λµ-calculus is presented [START_REF] Daniel | Intersection and union types in the lambda-bar-mu-mu-tilde-calculus[END_REF]. This system bears some similarity with the type system we present in section 3: this is underlined by the fact that all weakly normalizing terms are typable. It comes as no surprise, since our system is derived from Carvalho's system R, which is related to a system of intersection types for λ-calculus.

One important outcome of [dC06] and our paper is that they provide the aforementioned type systems with a strong grounding into well known denotational semantics of linear logic and its variants.

Syntax

In this section, we introduce the syntax of convolution λµ-calculus. Like ordinary λµcalculus, it involves three distinct syntactic categories: terms, contexts and commands. We introduce convolution product * as a commutative and associative binary operation on contexts, with unit 1.

Similarly to what is done in [START_REF] Ehrhard | The differential lambda-calculus[END_REF] and [START_REF] Vaux | The differential λµ-calculus[END_REF], each category of objects is endowed with a structure of commutative monoid, and we denote by + and 0 the corresponding operation and neutral element. Moreover, all but one syntactic construct are linear, i.e. they commute to sums: in particular, * distributes over +. In order to implement these high-level, metatheoretical requirements, we first define a basic syntax with a simple equality, then provide extended notations.

Remark 1. Since we only form sums (without coefficients) it is quite clear that our constructions are well defined, and that nothing tricky is hiding behind equality of terms. Recall from [Vau06, Section 4] that the introduction of linear combinations of terms (rather than just sums) may break normalization properties, or even trivialize β-equality [Vau06, Section 2.6], depending on the structure of the set of coefficients.

Morphology

Basic Syntax. Fix two denumerably infinite sets V (set of variables, denoted by x, y, z) and N (set of names, denoted by α, β, γ). We consider terms, commands and contexts up to permutativity of sum in the sense that, e.g., s + (s ′ + S) = s ′ + (s + S). Also, we consider simple contexts up to permutativity of convolution product: e.g., α * ((S • e) * e ′ ) = (S • e) * (α * e ′ ). Notice that these identities preserve free and bound variables and names: hence they are compatible with α-conversion. Equality of terms (resp. commands, contexts) is then given by permutativity of sum and product, together with α-equivalence.

Notations. We call simple object any simple term, simple context or simple command, and object any term, context or command. We may use greek letter θ to denote a simple object and capital Θ to denote an object. In general, if simple object θ and object Θ appear in the same sentence, it should be clear they are of the same kind: Θ is a term, context or command, if θ is a simple term, a simple context or a simple command respectively.

If θ 1 , . . . , θ n are simple objects and Θ an object, all of the same kind, we write

θ 1 + • • • + θ n + Θ for θ 1 + (• • • + (θ n + Θ) • • •).
If θ is a simple object, we may also denote by θ the corresponding object θ + 0. Hence, all object Θ may be written

Θ = θ 1 + • • • + θ n or even Θ = n i=1 θ i . Assume Θ = θ 1 + • • • + θ n and Θ ′ = θ ′ 1 + • • • + θ ′ p : we write Θ + Θ ′ for θ 1 + • • • + θ n + θ ′ 1 + • • • + θ ′ p .
Up to these conventions, sum + becomes an associative and commutative binary operation on terms, contexts and commands respectively, and object 0 is neutral.

Similarly, we identify any stack σ with the simple context σ * 1 ∈ E: then we may write any simple context e as e = σ 1 * • • • * σ n where the stacks σ i are names or of shape S • e ′ . With notations similar to those we used for sum, we consider * as an associative and commutative binary operation on simple contexts, with unit 1. Now we extend our syntactic constructs by linearity in order to be able to write λx S, µα C, S • E, E * F and S , E for all S ∈ T + , E, F ∈ E + and C ∈ C + . Definition 3. Assume s 1 , . . . , s n ∈ T , e 1 , . . . , e p , f 1 , . . . , f q ∈ E, c 1 , . . . , c r ∈ C and S ∈ T + . Then we write:

λx ( n i=1 s i ) = n i=1 λx s i ( p j=1 e j ) * q k=1 f k = p j=1 q k=1 e j * f k µα ( r l=1 c l ) = r l=1 µα c l n i=1 s i , p j=1 e j = n i=1 p j=1 s i , e j S • ( p j=1 e j ) = p j=1 S • e j .
Notice that the cons of a term and a context is not linear in the term: this is the analogue of application not being linear in the argument, in usual λ-calculus. This definition introduces some overlap of notations: e.g., λx s denotes both a simple term in our basic syntax, and the value of λx (s + 0) in the above definition. This is however harmless since both writings denote the same term.

Up to the notations we have just introduced, the set of terms (resp. contexts, commands) is endowed with a structure of commutative monoid. The set of contexts is moreover endowed with a structure of commutative rig (i.e. a commutative ring, without the condition that every element admits an opposite), with addition + and multiplication * . Also, λ-and µ-abstractions are linear, cons is linear in the context, and cut is bilinear. Then substitution of a term for a variable (resp. of a context for a name) in an object is defined as usual, by induction on objects:

y [T /x] = T if x = y y otherwise y [E/α] = y (λy s) [T /x] = λy (s [T /x]) (λy s) [E/α] = λy (s [E/α]) (µβ c) [T /x] = µβ (c [T /x]) (µβ c) [E/α] = µβ (c [E/α]) β [T /x] = β β [E/α] = E if α = β β otherwise (S • e) [T /x] = (S [T /x]) •(e [T /x]) (S • e) [E/α] = (S [E/α]) •(e [E/α]) 1 [T /x] = 1 1 [E/α] = 1 (σ * e) [T /x] = (σ [T /x]) * (e [T /x]) (σ * e) [E/α] = (σ [E/α]) * (e [E/α]) s , e [T /x] = s [T /x] , e [T /x] s , e [E/α] = s [E/α] , e [E/α] 0 [T /x] = 0 0 [E/α] = 0 (θ + Θ) [T /x] = θ [T /x] + Θ [T /x] (θ + Θ) [E/α] = θ [E/α] + Θ [E/α]
assuming usual conditions to avoid variable and name capture.

Reduction

Convolution Reduction. We call simply contextual relation any triplet r of binary relations respectively on terms, contexts and commands, all denoted r, and such that:

if s r S ′ then λx s r λx S ′ and s , e r S ′ , e ;

-if e r E ′ then s • e r s • E ′ , s , e r s , E ′ and e * f r E ′ * f ; -if c r C ′ then µα c r µα C ′ ; -if S r S ′ then S • e r S ′ • e;
and if θ 0 r Θ ′ 0 then for all Θ 1 , θ 0 + Θ 1 r Θ ′ 0 + Θ 1 .

λx s , 1 → β s [0/x] , 1 (2)
with y a fresh variable and α a fresh name in (2). where → * β denotes the reflexive and transitive closure of → β . This enlightens the fact that → β is a refined version of both usual reduction of λµ-calculus and the coarser notion of convolution reduction we first derived from cut elimination in the introduction.

Conversely, → β may be simulated by that coarse reduction, up-to the following generalization of η-expansion on commands: recalling that the analogue of η-expansion in λµ-calculus is s ← η λx µα s , x • α we set s , e * e ′ ← η ′ λx µα s , e * (x • α) , e ′ . This can be thought of as η-expansion w.r.t. only one component of a product. If e ′ actually holds an argument at top-level, i.e. e ′ = S • f , we can get back:

λx µα s , e * (x • α) , S • f → * β s , e * (S • f ) = s , e * e ′
which validates ← η ′ as a notion of η-expansion.

Remark 5. Recall (e.g., from [START_REF] Schwartz | Théorie des distributions[END_REF]) that the definition of the convolution product of distributions is as follows: if e and f are distributions with compact domains and ϕ is a test function, then e * f is such that λz ϕ(z) , e * f = λy λx ϕ(x + y) , e , f .

Analoguously, one can check that the following two commands Confluence. We prove confluence of reduction using usual Tait-Martin-Löf technique: introduce a parallel extension of one-step reduction, and prove this has the diamond property.

A binary relation r on commutative monoid A is said to be linear if: for all a 1 , . . ., a n , b 1 , . . . , b n ∈ A, if a i r b i holds for all i, then n i=1 a i r n i=1 b i also holds (in particular 0 r 0). Notice that → β is not linear: 0 → β 0. We call contextual relation any triplet r of binary relations respectively on terms, contexts and commands, all denoted r, such that each of them is reflexive and linear, and if

S r S ′ , E r E ′ , F r F ′ and C r C ′ , then λx S r λx S ′ , µα C r µα C ′ , S • E r S ′ • E ′ , E * F r E ′ * F ′ and S , E r S ′ , E ′ .
Denotational Semantics. We define the relational semantics of an object, as the set of all its typings in system Rλ µ * . More precisely: Definition 14. Assume S ∈ T + , E ∈ E + and C ∈ C + are such that FV (Θ) ⊆ {x 1 , . . . , x n } and FN (Θ) ⊆ {α 1 , . . . , α p }, for Θ = S, E, C. We define S α 1 ,...,αp x 1 ,...,xn = {(Γ(x 1 ), . . . , Γ(x n ), a, ∆(α 1 ), . . . , ∆(α p )); Γ ⊢ S : a | ∆} , E α 1 ,...,αp x 1 ,...,xn = {(Γ(x 1 ), . . . , Γ(x n ), a, ∆(α 1 ), . . . , ∆(α p )); Γ | E : a ⊢ ∆} and C α 1 ,...,αp x 1 ,...,xn = {(Γ(x 1 ), . . . , Γ(x n ), ∆(α 1 ), . there exist variable environments Γ ′ , Γ 1 , . . . , Γ n , and name environments ∆ ′ , ∆ 1 , . . . , ∆ n and types a 1 , . . . , a n ∈ D such that

• Γ = Γ ′ + Γ 1 + • • • + Γ n and ∆ = ∆ ′ ⋆ ∆ 1 ⋆ • • • ⋆ ∆ n ; • for all i = 1, . . . , n, Γ i ⊢ T : a i | ∆ i ; • and Rλ µ * (Γ ′ + x : [a 1 , . . . , a n ] , ∆ ′ , Θ, a).
Lemma 18. The following statements are equivalent:

-Rλ µ * (Γ, ∆, Θ [E/α] , a);

there exist variable environments Γ ′ and Γ ′′ , name environments ∆ ′ and ∆ ′′ , and type b ∈ D, such that

• α ∈ Supp (∆ ′ ); • Γ = Γ ′ + Γ ′′ and ∆ = ∆ ′ ⋆ ∆ ′′ ; • Γ ′′ | E : b ⊢ ∆ ′′ ;
• and Rλ µ * (Γ ′ , ∆ ′ ⋆ α : b, Θ, a).

Theorem 19. If Θ → β Θ ′ , then we have: Rλ µ * (Γ, ∆, Θ, a) iff Rλ µ * (Γ, ∆, Θ ′ , a). If moreover FV (Θ) ⊆ {x 1 , . . . , x n } and FN (Θ) ⊆ {α 1 , . . . , α p }, then Θ α 1 ,...,αp x 1 ,...,xn = Θ ′ α 1 ,...,αp x 1 ,...,xn . Proof. The proof is by induction on Θ, inspecting all possible cases for reduction Θ → β Θ ′ , and using the previous three lemmas in redex cases.

Hence the relational semantics is preserved by reduction. As a corollary, Lemma 12 implies that every object that has a normal form is typable.

Future Work

On Pure Calculi. Although grounded in ideas coming from models of differential λ-calculus, convolution λµ-calculus provides no differentiation primitive. Indeed, recall from our introduction that the nets associated with convolution λµ-calculus are polarized nets, extended with cocontraction and coweakening on types !o and i. In particular, they do not involve derivative ∂.

One may augment these nets by including ∂ and the associated cut elimination rules, but this needs caution. Uncontrolled use of ∂ breaks one essential property of polarized nets: namely, the occurrence of at most one positive type (!o or i in our setting) among all output wires. That matter is discussed in [START_REF] Vaux | Polarized proof nets and differential structures[END_REF] in more details.

This remark, however, does not hamper the fact that one may propose differential extensions of convolution λµ-calculus. Some first attempts even suggest that the introduction of convolution product of contexts actually simplifies the presentation of a would-be differential λµ-calculus.

On Denotational Semantics. In [dC06], Carvalho provides precise results relating the relational semantics of λ-terms with their normalization properties (which are very close to those we expect from an intersection type system); he also provides bounds for the execution time of terms in variants of Krivine's abstract machine, according to the size of their typing derivations in system R. We do not know yet, to which extent these results may accomodate themselves to the setting of Bucciarelli-Ehrhard's model and convolution λµ-calculus (or even usual λµ-or λµ-calculus for that matter).

Another promising direction for further research is to study more precisely how the categorical constructions of [START_REF] Laurent | About translations of classical logic into polarized linear logic[END_REF] may be extended to a setting with costructural rules.

  s, t ::= x | λx s | µα c (terms) e, f ::= α | s • e (contexts) c ::= s , e (commands) . Reduction is defined by the following two basic rules: λx s , t • e → s [t/x] , e and µα c , e → c [e/α] .

  λx s , (t • e) * f → λx µα s [t + x/x] , e * α , f λx s , 1 → s [0/x] , 1 µα c , e → c [e/α] .

  where M fin (A) denotes the set of all finite multisets of elements of A and 1 is a singleton set. One interesting feature of the relational model is that it identifies dual connectors in linear logic. In particular, if ϕ ⊆ A -• B in the relational model, then ϕ ⊥ ⊆ B -• A where ϕ ⊥ = {(b, a); (a, b) ∈ ϕ}. By setting ∂ A = d ⊥

Definition 2 .

 2 Define sets T of simple terms and T + of terms, set S of stacks, sets E of simple contexts and E + of contexts, and sets C of simple commands and C + of commands, by the following grammar: s ::= x | λx s | µα c (simple terms) σ ::= α | S • e (stacks) e ::= 1 | σ * e (simple contexts) c ::= s , e (simple commands) S ::= 0 | s + S (terms) E ::= 0 | e + E (contexts) C ::= 0 | c + C (commands) .

Definition 4 .

 4 Reduction → β is the least simply contextual relation such that: µα c , e → β c [e/α] (1) λx s , (S • e) * f → β λy µα s [y + S/x] , α * e , f

  Notice that λx s , S • e → * β s [S/x] , e and, more interestingly, λx s , (S • e) * (S ′ • e ′ ) → * β s S + S ′ /x , e * e ′

  λz s , (S • e) * (T • f ) and λy µβ λx µα s [x + y/z] , α * β , S • e , T • f are identified by reduction: both reduce to s [S + T /z] , e * f . The apparent complexity of that last identity has two main causes.First, in the formalism of distributions and test functions, ϕ is supposed to be a function with scalar values. The type corresponding to scalars is that of commands, but in λµ-calculus, as in λ-calculus, functions and values are represented by terms. Hence the µ-abstractions and the innermost cut: these handle the possible remaining arguments. Second, functions are in general considered extensionally. Expansion ← η ′ may be used to introduce sufficient extensionality: λz s , e * f ← η ′ λy µβ λz s , e * (y • β) , f → β λy µβ λx µα s [x + y/z] , α * β , e , f .

  . . , ∆(α p )); C : (Γ ⊢ ∆)} . Remark 15. The reader can easily check that (S • e) * (S ′ • e ′ ) α 1 ,...,αp x 1 ,...,xn = (S + T ) •(e * e ′ ) α 1 ,...,αp x 1 ,...,xn . The following three lemmas are proved by induction on objects. Lemma 16. We have Rλ µ * (Γ, ∆, Θ [0/x] , a) if and only if x ∈ Supp (Γ) and Rλ µ * (Γ, ∆, Θ, a). Lemma 17. Assume x ∈ FV (T ). Then the following are equivalent: -Rλ µ * (Γ, ∆, Θ [x + T /x] , a);

with y a fresh variable α a fresh name in (5).

It should be clear that → β ⊂ → / / , in the sense that if Θ → β Θ ′ then Θ → / / Θ ′ . In particular, (6) is reminiscent of the coarse version of reduction. Moreover, → / / ⊂ → * β by simple contextuality of → β . The following lemma states the essential property of parallel reduction.

Lemma 7. If Θ and Θ ′ are objects, S and S ′ ∈ T + , and E and E ′ ∈ E + , such that Θ → / / Θ ′ , S → / / S ′ and E → / / E ′ , then for every variable x and every name α, the following reductions hold:

Proof. This is a simple induction on Θ, using contextuality of → / / .

We now prove that → / / enjoys the diamond property. Assume s ∈ T and e ∈ E, and write e = ( n i=1 S i • e i ) * ( k j=1 α j ); we then define

λx s , e otherwise.

Clearly, λx s , e → / / λx s , e 0 , as a particular case of (5) or (6). Definition 8. We define full reduction as follows:

Full reduction fires all possible redexes in an object. Then one obtains the diamond property for parallel reduction:

This result is proved by inspecting all possible cases of reduction Θ → / / Θ ′ , using Lemma 7 in redex cases.

Theorem 10. Reduction is confluent.

Proof. This is a corollary of Lemma 9 and the inclusions

Relational Semantics

In this section, we adapt the system R of [dC06] to the setting of convolution λµ-calculus: we introduce a type system, the types of which are elements of the extensional λ-model described in [START_REF] Bucciarelli | An extensional model of the lambda-calculus in the category of sets and relations[END_REF].

A Reflexive Object in the Category of Sets and Relations. If X is a set, we denote by M fin (X) the set of all finite multisets [x 1 , . . . , x n ] of elements x 1 , . . . , x n ∈ X (possibly with repetitions). Also, we write (M fin (X)) (ω) for the set of all infinite sequences a = (a(i)) i∈ω of finite multisets of elements of X such that a(i) = [] holds for almost all i ∈ ω.

We define an increasing family (D n ) n∈N of sets by: D 0 = ∅ and D n+1 = (M fin (D n )) (ω) . Then we write D = n∈N D n . If A ∈ M fin (D) and a ∈ D, we write A :: a for the sequence b such that b(0) = A and b(i + 1) = a(i) for all i ∈ ω. This mapping is clearly a bijection between D and M fin (D) × D. We write ι for the sequence in which only the empty multiset occurs: ι(i) = [] for all i ∈ ω, so that ι = [] :: ι. Observe that D 1 = {ι}.

Type System. Call types the elements of D. We impose a commutative monoid structure on types as follows. For all a, b ∈ D, we define a ⋆ b as the sequence such that, for all i ∈ ω, (a ⋆ b)(i) = a(i) + b(i) where + denotes the union of multisets. Clearly ι is neutral for that associative and commutative operation.

A variable environment is a function Γ : V -→ M fin (D) such that Γ(x) = [] for almost all x ∈ V. If x ∈ V and A ∈ M fin (D), we write x : A for the variable environment Γ such that: Γ(x) = A and, for all y = x, Γ(y) = []. If Γ and Γ ′ are variable environments, we write Γ + Γ ′ for the variable environment defined by (Γ + Γ ′ )(x) = Γ(x) + Γ ′ (x). If Γ is a variable environment, we define its support Supp (Γ) = {x ∈ V; Γ(x) = []}.

Similarly, a name environment is a function ∆ : N -→ D such that ∆(α) = ι for almost all α ∈ N. If α ∈ N and a ∈ D, we write α : a for the name environment ∆ such that: ∆(α) = a and, for all β = α, ∆(β) = ι. If ∆ and ∆ ′ are name environments, we write ∆ ⋆ ∆ ′ for the name environment defined by (∆ ⋆ ∆ ′ )(α) = ∆(α) ⋆ ∆ ′ (α) and we set Supp (∆) = {α ∈ N; ∆(α) = ι}. Now we introduce type system Rλ µ * for the objects of convolution λµ-calculus. Typing judgements are of form Γ ⊢ S : a | ∆, Γ | E : a ⊢ ∆ or C : (Γ ⊢ ∆), where Γ is a variable environment and ∆ is a name environment. We may omit Γ (resp. ∆) if it is the constant function with value [] (resp. ι). The rules of system Rλ µ * are given in Fig. 1.

The reader may refer to [START_REF] Daniel | Intersection and union types in the lambda-bar-mu-mu-tilde-calculus[END_REF] and check that the rules of system Rλ µ * , restricted to the objects of ordinary λµ-calculus, are quite similar to those of system M ∩∪ . This similarity actually extends to the fact that all weakly normalizing objects are typable in system Rλ µ * , as we will show later. This feature is a characteristic of intersection type systems: this was already prominent in system R.

Example 11. The term λx µα x , x • α (the λµ-calculus variant of δ = λx (x) x) has

Figure 1: Typing rules for system Rλ µ * the following typing derivation, recalling that ι = [] :: ι:

x

Lemma 12. Every term, context or command which is in normal form is typable.

Proof. The result is proved by mutual induction on normal terms, contexts and commands. Among the typing rules in figure 1, only Cut involves some compatibility condition on the types of subobjects. Hence the only interesting induction case is that of simple commands. Simple commands in normal form are those c = s , e such that:

(i) either s is a variable and e is a simple context in normal form;

(ii) or s = λx t, where t is a simple term in normal form, and e = α 0 * • • • * α n is a product of names, with n > 0.

In both cases, it is easy to build a typing derivation using the inductive hypothesis and axiom rules (Var or Name).

Denote by FV (Θ) (resp. FN (Θ)) the set of all variables (resp. names) free in Θ. To simplify some of our next statements, we write Rλ µ * (Γ, ∆, Θ, a) for:

Lemma 13. If Rλ µ * (Γ, ∆, Θ, a), then Supp (Γ) ⊆ FV (Θ) and Supp (∆) ⊆ FN (Θ).

Proof. This is easily proved by induction on Θ.


⊥ A = {a ′ ⊆ A; ∀a ∈ F

❆❞❞✐t✐✈❡s✳ ❲❡ ♥♦✇ ✐♥tr♦❞✉❝❡ t❤❡ ❝❛rt❡s✐❛♥ str✉❝t✉r❡ ♦❢ Fin✳ ❲❡ ❞❡✜♥❡ A ⊕ B ❜② |A ⊕ B| = |A| ⊎ |B| ❛♥❞ F (A ⊕ B) = {a ⊎ b; a ∈ F (A) , b ∈ F (B)} ✇❤❡r❡ ⊎ ❞❡♥♦t❡s t❤❡ ❞✐s•♦✐♥t ✉♥✐♦♥ ♦❢ s❡ts✿ x ⊎ y = ({1} × x) ∪ ({2} × y)✳ ❲❡ ❤❛✈❡ (A ⊕ B) ⊥ = A ⊥ ⊕ B ⊥ ✳ ❚❤❡ ❝❛t❡❣♦r② Fin ✐s ❜♦t❤ ❝❛rt❡s✐❛♥ ❛♥❞ ❝♦✲❝❛rt❡s✐❛♥✱ ✇✐t❤ ⊕ ❜❡✐♥❣ t❤❡ ♣r♦❞✉❝t ❛♥❞ ❝♦✲♣r♦❞✉❝t✱ ❛♥❞ 0 t❤❡ ✐♥✐t✐❛• ❛♥❞ t❡r♠✐♥❛• ♦❜•❡❝t✳ Pr♦•❡❝t✐♦♥s ❛r❡ ❣✐✈❡♥ ❜②✿ λ A,B = {((1, α), α) ; α ∈ |A|} ∈ Fin(A ⊕ B, A) ρ A,B = {((2, β), β) ; β ∈ |B|} ∈ Fin(A ⊕ B, B) ❛♥❞ ✐❢ f ∈ Fin(C, A) ❛♥❞ g ∈ Fin(C, B)✱ ♣❛✐r✐♥❣ ✐s ❣✐✈❡♥ ❜②✿ f, g = {(γ, (1, α)) ; (γ, α) ∈ f } ∪ {(γ, (2, β)) ; (γ, β) ∈ g} ∈ Fin(C, A ⊕ B). ❚❤❡ ✉♥✐q✉❡ ♠♦r♣❤✐s♠ ❢r♦♠ A t♦ 0 ✐s t❤❡ ❡♠♣t② r❡•❛t✐♦♥✳ ❚❤❡ ❝♦✲❝❛rt❡s✐❛♥ str✉❝✲ t✉r❡ ✐s ♦❜t❛✐♥❡❞ s②♠♠❡tr✐❝❛••②✳ ❊①❛♠♣•❡ ✸✳ ❲r✐t❡ O ⊥ = {(0, ∅)} ∈ Fin(N , 1)✳ ❚❤❡♥ O ⊥ , P = {(0, (1, ∅))} ∪ {(k + 1, (2, k)); k ∈ N} ∈ Fin (N , 1 ⊕ N ) ✐s ❛♥ ✐s♦♠♦r♣❤✐s♠✳ ❊①♣♦♥❡♥t✐❛•s✳ ■❢ A ✐s ❛ s❡t✱ ✇❡ ❞❡♥♦t❡ ❜② M ✜♥ (A) t❤❡ s❡t ♦❢ ❛•• ✜♥✐t❡ ♠✉•t✐s❡ts ♦❢ ❡•❡♠❡♥ts ♦❢ A✱ ❛♥❞ ✐❢ a ⊆ A✱ ✇❡ ✇r✐t❡ a ! = M ✜♥ (a) ⊆ M ✜♥ (A)✳ ■❢ α ∈ M ✜♥ (A)✱ ✇❡ ❞❡♥♦t❡ ✐ts s✉♣♣♦rt ❜② Supp(α) ∈ P ❢ (A)✳ ❋♦r ❛•• ✜♥✐t❡♥❡ss s♣❛❝❡ A✱ ✇❡ ❞❡✜♥❡ !A ❜②✿ |!A| = M ✜♥ (|A|) ❛♥❞ F (!A) = a ! ; a ∈ F (A) ⊥⊥ ✳ ■t ❝❛♥ ❜❡ s❤♦✇♥ t❤❛t F (!A) = a ⊆ M ✜♥ (|A|) ; α∈a Supp(α) ∈ F (A) ✳ ❚❤❡♥✱ ❢♦r ❛•• f ∈ Fin(A, B)✱ ✇❡ s❡t !f = {([α 1 , . . . , α n ] , [β 1 , . . . , β n ]) ; ∀i, (α i , β i ) ∈ f } ∈ Fin(!A, !B), ✇❤✐❝❤ ❞❡✜♥❡s ❛ ❢✉♥❝t♦r✳ ◆❛t✉r❛• tr❛♥s❢♦r♠❛t✐♦♥s der A = {([α] , α); α ∈ |A|} ∈ Fin(!A, A) ❛♥❞ dig A = {( n i=1 α i , [α 1 , . . . , α n ]); ∀i, α i ∈ |!A|} ♠❛❦❡ t❤✐s ❢✉♥❝✲ t♦r ❛ ❝♦♠♦♥❛❞✳ ❊①❛♠♣•❡ ✹✳ ❲❡ ❤❛✈❡ ✐s♦♠♦r♣❤✐s♠s {([] , ∅)} ∈ Fin(!0, 1) ❛♥❞ α l + β r , α, β ; (α l , α) ∈ !λ A,B ∧ (β r , β) ∈ !ρ A,B ∈ Fin(!(A ⊕ B), !A ⊗ !B). ▼♦r❡ ❣❡♥❡r❛••②✱ ✇❡ ❤❛✈❡ ! (A 1 ⊕ • • • ⊕ A n ) ∼ = !A 1 ⊗ • • • ⊗ !A n ✳ ❆•• t❤❡ ✉s✉❛• str✉❝t✉r❡ ♦❢ ♠♦❞❡•s ♦❢ ♣r♦♣♦s✐t✐♦♥❛• ❝•❛ss✐❝❛• •✐♥❡❛r •♦❣✐❝ ✐s ♥♦✇ ✐♥tr♦❞✉❝❡❞✿ ♦♥❡ ❝❛♥ ❝❤❡❝❦ t❤❛t Fin ✐s ❛ ♥❡✇✲❙❡❡•② ❝❛t❡❣♦r②✱ ❢♦••♦✇✐♥❣ t❤❡ t❡r♠✐✲ ♥♦•♦❣② ♦❢ ❬✼(✳ Γ ⊢ s, t : A × B Γ ⊢ s : A × B ✭▲❡❢t✮ Γ ⊢ π l s : A Γ ⊢ s : A × B ✭|✐❣❤t✮ Γ ⊢ πr s : B ❋✐❣✳ ✶✳ |✉•❡s ♦❢ t②♣❡❞ λ✲❝❛•❝✉•✐ ✇✐t❤ ♣r♦❞✉❝ts ❛♥❞ Fin ! (A, B) = F (A ⇒ B)✱ ❢♦••♦✇✐♥❣ •✐r❛r❞✬s tr❛♥s•❛t✐♦♥ ♦❢ ✐♥t✉✐t✐♦♥✐st✐❝ ✐♠✲ ♣•✐❝❛t✐♦♥ A ⇒ B = !A ⊸ B✳ ❚❤❡ ✐❞❡♥t✐t② ♠♦r♣❤✐s♠ ♦❢ Fin ! (A, A) ✐s •✉st der A ✳ ■❢ f ∈ !A ⊸ B✱ t❤❡ ♣r♦♠♦t✐♦♥ ♦❢ f ✐s f ! = !f • dig A = n i=1 α i , [β 1 , . . . , β n ] ; ∀i, (α i , β i ) ∈ f ∈ !A ⊸ !B. ■❢ f ∈ A ⇒ B ❛♥❞ g ∈ B ⇒ C✱ t❤❡✐r ❝♦♠♣♦s✐t✐♦♥ ✐♥ Fin ! ✐s t❤❡♥ g • f = g • f ! ✳ |❡♠❛r❦ ✶✳ |❡❝❛••✐♥❣ t❤❡ ❝❤❛r❛❝t❡r✐③❛t✐♦♥s ♦❢ A ⊸ B ❛♥❞ !A✱ ✇❡ ❣❡t t❤❛t f ∈ F (A ⇒ B) ✐✛ ∀a ∈ F (A)✱ f • a ! ∈ F (B) ❛♥❞ ∀β ∈ |B|✱ (f ⊥ • {β}) ∩ a ! ✐s ✜♥✐t❡✳ ❚❤❡ ❝❛rt❡s✐❛♥ ♣r♦❞✉❝t ♦❢ Fin ! ✐s ♦❢ ❝♦✉rs❡ ⊕✱ ✇✐t❤ ♣r♦•❡❝t✐♦♥s π A,B l = λ A,B • der A⊕B ❛♥❞ π A,B r = ρ A,B • der A⊕B ❀ ♣❛✐r✐♥❣ ✐s t❤❡ s❛♠❡ ❛s ✐♥ Fin✳ ❚❤❡ ✐s♦♠♦r✲ ♣❤✐s♠ (A 1 ⊕ • • • ⊕ A n ) ⇒ B ∼ = A 1 ⇒ • • • ⇒ A n ⇒ A ❞❡❞✉❝❡❞ ❢r♦♠ ❊①❛♠♣•❡ ✹ s✉❜s✉♠❡s t❤❡ ❛❞•✉♥❝t✐♦♥ Fin ! (A ⊕ B, C) ∼ = Fin ! (A, B ⇒ C)✳ ❆s ❛ ♣❛rt✐❝✉•❛r ❝❛s❡✱ 0 ⇒ A ∼ = A ❛♥❞ ✇❡ ❝❛♥ ✐❞❡♥t✐❢② ❛♥② ♠♦r♣❤✐s♠ f ∈ 0 ⇒ A ✇✐t❤ t❤❡ ✜♥✐t❛r② s✉❜s❡t f • {[]} ∈ F (A)✳ ✸ ❙❡♠❛♥t✐❝s ♦❢ t②♣❡❞ λ✲❝❛•❝✉•✐ ■♥ t❤✐s s❡❝t✐♦♥✱ ✇❡ ❣✐✈❡ ❛♥ ❡①♣•✐❝✐t ❞❡s❝r✐♣t✐♦♥ ♦❢ t❤❡ ✐♥t❡r♣r❡t❛t✐♦♥ ✐♥ Fin ! ♦❢ t❤❡ ❜❛s✐❝ ❝♦♥str✉❝t✐♦♥s ♦❢ t②♣❡❞ λ✲❝❛•❝✉•✐ ✇✐t❤ ♣r♦❞✉❝ts✳ ❚②♣❡❞ λ✲❝❛•❝✉•✐✳ ▲❡t ❜❡ ❣✐✈❡♥ ❛ ❝♦••❡❝t✐♦♥ A ♦❢ ❛t♦♠✐❝ t②♣❡s ❛♥❞ ❝♦♥s✐❞❡r t❤❡ t②♣❡ ❡①♣r❡ss✐♦♥s ❣✐✈❡♥ ❜②✿ A, B ::= X | A → B | A × B | ⊤ ✇❤❡r❡ X r❛♥❣❡s ♦✈❡r A✳ ❋♦r ❡❛❝❤ t②♣❡ A✱ t❤❡r❡ ❛r❡ ❝♦✉♥t❛❜•② ♠❛♥② ❢♦r♠❛• ✈❛r✐❛❜•❡s ♦❢ t❤❛t t②♣❡✱ ❛♥❞ ❛•s♦ ❛ ❝♦••❡❝t✐♦♥ C A ♦❢ t❡r♠ ❝♦♥st❛♥ts ♦❢ t❤❛t t②♣❡✳ ❚❤❡♥ t❡r♠ ❡①♣r❡ss✐♦♥s ❛r❡ ❣✐✈❡♥ ❜②✿ s, t ::= x | a | λx s | s t | s, t | π l s | π r s | ❱❛r Γ [] , x [α] : A, ∆ [] ⊢ x α : A ❯♥✐t Γ [] ⊢ ∅ : ⊤ a ∈ CA α ∈ a ❈♦♥st Γ [] ⊢ a α : A Γ, x α : A ⊢ s β : B ❆❜s Γ ⊢ λx s (α,β) : A → B Γ0 ⊢ s ([α 1 ,...,α k ],β) : A → B Γ1 ⊢ t α 1 : A • • • Γ k ⊢ t α k : A ❆♣♣ P k j=0 Γj ⊢ s t β : B Γ ⊢ s α : A P❛✐r l Γ ⊢ s, t (1,α) : A × B Γ ⊢ t β : B P❛✐rr Γ ⊢ s, t (2,β) : A × B Γ ⊢ s (1,α) : A × B ▲❡❢t Γ ⊢ π l s α : A Γ ⊢ s (2,β) : A × B |✐❣❤t Γ ⊢ πr s β : B ❋✐❣✳ ✷✳ ❈♦♠♣✉t✐♥❣ ♣♦✐♥ts ✐♥ t❤❡ r❡•❛t✐♦♥❛• s❡♠❛♥t✐❝s ❛♥❞ ✇❡ ❞❡✜♥❡ ❢r❡❡ ❛♥❞ ❜♦✉♥❞ ✈❛r✐❛❜•❡s ❛s ✉s✉❛•✳ ❲❡ ❞❡♥♦t❡ ❜② s [x := t] t❤❡ s✉❜st✐t✉t✐♦♥ ♦❢ t ❢♦r x ✐♥ s✳ ❆ ❝♦♥t❡①t Γ ✐s ❛ ✜♥✐t❡ •✐st (x 1 : A 1 , . . . , x n : A n ) ✇❤❡r❡ t❤❡ x i ✬s ❛r❡ ♣❛✐r✇✐s❡ ❞✐st✐♥❝t ✈❛r✐❛❜•❡s ❛♥❞ A i ✐s t❤❡ t②♣❡ ♦❢ x i ✳ ❆ t②♣✐♥❣ •✉❞❣❡♠❡♥t ✐s ❛♥ ❡①♣r❡ss✐♦♥ Γ ⊢ s : A ❞❡r✐✈❡❞ ❢r♦♠ t❤❡ r✉•❡s ✐♥ ❋✐❣✉r❡ ✶✿ ✇❡ t❤❡♥ s❛② t❡r♠ s ✐s ♦❢ t②♣❡ A ✐♥ ❝♦♥t❡①t Γ ✳ ❈•❡❛r•②✱ ✐❢ ❛ t❡r♠ s ✐s t②♣❛❜•❡✱ t❤❡♥ ✐ts t②♣❡ ✐s ✉♥✐q✉❡•② ❞❡t❡r♠✐♥❡❞✱ s❛② A✱ ❛♥❞ t❤❡♥ Γ ⊢ s : A ✐✛ Γ ❝♦♥t❛✐♥s t❤❡ ❢r❡❡ ✈❛r✐❛❜•❡s ♦❢ s✳ ❚❤❡ ♦♣❡r❛t✐♦♥❛• s❡♠❛♥t✐❝s ♦❢ ❛ t②♣❡❞ λ✲❝❛•❝✉•✉s ✐s ❣✐✈❡♥ ❜② ❛ ❝♦♥t❡①t✉❛• ❡q✉✐✈❛•❡♥❝❡ r❡•❛t✐♦♥ ≃ ♦♥ t②♣❡❞ t❡r♠s✿ ✐❢ s ≃ t✱ t❤❡♥ s ❛♥❞ t ❤❛✈❡ t❤❡ s❛♠❡ t②♣❡✱ s❛② A❀ ✇❡ t❤❡♥ ✇r✐t❡ Γ ⊢ s ≃ t : A ✇❤❡♥❡✈❡r Γ ❝♦♥t❛✐♥s t❤❡ ❢r❡❡ ✈❛r✐❛❜•❡s ♦❢ s ❛♥❞ t✳ ■♥ ❣❡♥❡r❛•✱ ✇❡ ✇✐•• ❣✐✈❡ ≃ ❛s t❤❡ r❡✢❡①✐✈❡✱ s②♠♠❡tr✐❝ ❛♥❞ tr❛♥s✐t✐✈❡ ❝•♦s✉r❡ ♦❢ ❛ ❝♦♥t❡①t✉❛• r❡•❛t✐♦♥ > ♦♥ t②♣❡❞ t❡r♠s✳ ❲❡ ❞❡✜♥❡ > 0 ❛s t❤❡ •❡❛st ♦♥❡ s✉❝❤ t❤❛t✿ π l s, t > 0 s✱ π r s, t > 0 t ❛♥❞ (λx s) t > 0 s [x := t] ✭✇✐t❤ t❤❡ ♦❜✈✐♦✉s ❛ss✉♠♣t✐♦♥s ❡♥s✉r✐♥❣ t②♣❛❜✐•✐t②✮✳ ❆♥❞ ✇❡ ✇r✐t❡ ≃ 0 ❢♦r t❤❡ ❝♦rr❡s♣♦♥❞✐♥❣ ❡q✉✐✈❛•❡♥❝❡✳ |❡•❛t✐♦♥❛• ✐♥t❡r♣r❡t❛t✐♦♥ ❛♥❞ ✜♥✐t❡♥❡ss ♣r♦♣❡rt②✳ ❚❤❡ ✐♥t❡r♣r❡t❛t✐♦♥ ♦❢ s✉❝❤ ❛ ❝❛•❝✉•✉s ✐♥ Fin ! ❣♦❡s ❛s ❢♦••♦✇s✳ ❋✐rst ♦♥ t②♣❡s✿ ❛ss✉♠❡ ❛ ✜♥✐t❡♥❡ss s♣❛❝❡ X ✐s ❣✐✈❡♥ ❢♦r ❡❛❝❤ ❜❛s❡ t②♣❡ X❀ t❤❡♥ ✇❡ ✐♥t❡r♣r❡t t②♣❡ ❝♦♥str✉❝t✐♦♥s ❜② A → B = A ⇒ B ✱ A × B = A ⊕ B ❛♥❞ ⊤ = 0✳ ❋✉rt❤❡r ❛ss✉♠❡ t❤❛t ✇✐t❤ ❡✈❡r② ❝♦♥st❛♥t a ∈ C A ✐s ❛ss♦❝✐❛t❡❞ ❛ ✜♥✐t❛r② s✉❜s❡t a ∈ F ( A )✿ ✇❡ ❞❡✜♥❡ t❤❡ s❡♠❛♥t✐❝s ♦❢ ❛ ❞❡r✐✈❛❜•❡ t②♣✐♥❣ •✉❞❣❡♠❡♥t x 1 : A 1 , . . . , x n : A n ⊢ s : A✱ ❛s ❛ ✜♥✐t❛r② r❡•❛t✐♦♥ s x1:A1,...,xn:An ∈ F ( A 1 ⇒ • • • ⇒ A n ⇒ A )✳ ❲❡ ✜rst ✐♥tr♦❞✉❝❡ t❤❡ ❞❡❞✉❝t✐✈❡ s②st❡♠ ♦❢ ❋✐❣✉r❡ ✷✳ ■♥ t❤✐s s②st❡♠✱ ❞❡r✐✈❛❜•❡ •✉❞❣❡♠❡♥ts ❛r❡ s❡♠❛♥t✐❝ ❛♥♥♦t❛t✐♦♥s ♦❢ t②♣✐♥❣ •✉❞❣❡♠❡♥ts✿ x α1 1 : A 1 , . . . , x αn n : A n ⊢ s α : A st❛♥❞s ❢♦r (α 1 , . . . , α n , α) ∈ s x1:A1,...,xn:An ✇❤❡r❡ ❡❛❝❤ α i ∈ M ✜♥ (| A i |) ❛♥❞ α ∈ | A |✳ ■♥ r✉•❡s ❱❛r ✱ ❯♥✐t ❛♥❞ ❈♦♥st ✱ Γ [] ❞❡♥♦t❡s ❛♥ ❛♥♥♦t❛t❡❞ ❝♦♥t❡①t ♦❢ t❤❡ ❢♦r♠ x [] 1 : A 1 , . . . , x [] n : A n ✳ ■♥ r✉•❡ ❆♣♣ ✱ t❤❡ s✉♠ ♦❢ ❛♥♥♦t❛t❡❞ ❝♦♥t❡①ts ✐s ❞❡✜♥❡❞ ♣♦✐♥t✇✐s❡✿ ✐❢ Γ = x α1 1 : A 1 , . . . , x αn n : A n ❛♥❞ Γ ′ = x α ′ 1 1 : A 1 , . . . , x α ′ n n : A n ✱ ✇❡ s❡t Γ + Γ ′ = x α1+α ′ 1 1 : A 1 , . . . , x αn+α ′ n n : A n ✳ ❋✐♥❛••② ✇❡ ❞❡✜♥❡ t❤❡ s❡♠❛♥t✐❝s ♦❢ ❛ t❡r♠ ❛s t❤❡ s❡t ♦❢ ✐ts ❛♥♥♦t❛t✐♦♥s✿ s x1:A1,...,xn:An = (α 1 , . . . , α n , α); x α1 1 : A 1 , . . . , x αn n : A n ⊢ s α : A . ■t r❡♠❛✐♥s t♦ ♣r♦✈❡ t❤❛t s x1:A1,...,xn:An ∈ F ( A 1 ⇒ • • • ⇒ A n ⇒ A )✳ |❡♠❛r❦ ✷✳ ❚❤❡ r✉•❡s ♦❢ ❋✐❣✉r❡ ✷ ❛r❡ ❛❝t✉❛••② t❤♦s❡ ♦❢ t❤❡ r❡•❛t✐♦♥❛• s❡♠❛♥t✐❝s✿ t❤✐s ✐s t❤❡ s❡♠❛♥t✐❝s ♦❢ t②♣❡❞ λ✲❝❛•❝✉•✐ ✐♥ t❤❡ ❝❛rt❡s✐❛♥ ❝•♦s❡❞ ❝❛t❡❣♦r② Rel ! ✱ ❞❡❞✉❝❡❞ ❢r♦♠ t❤❡ r❡•❛t✐♦♥❛• ♠♦❞❡• ♦❢ •✐♥❡❛r •♦❣✐❝ ✐♥ t❤❡ ❝❛t❡❣♦r② Rel ♦❢ s❡ts ❛♥❞ r❡•❛t✐♦♥s ✭s❡❡ t❤❡ ❆♣♣❡♥❞✐① ❆ ❢r♦♠ ❬✶( ❢♦r ✐♥st❛♥❝❡✮✳ ◆♦t✐❝❡ ✐♥❞❡❡❞ t❤❛t t❤❡ ❞❡✜♥✐t✐♦♥s ♦❢ t❤❡ ♥❛t✉r❛• tr❛♥s❢♦r♠❛t✐♦♥s ♦❢ Fin ✭❛♥❞ t❤❡ ❞❡✜♥✐t✐♦♥s ♦❢ t❤❡ ♠♦r♣❤✐s♠ ❝♦♠♣♦♥❡♥t ♦❢ t❤❡ ❛ss♦❝✐❛t❡❞ ❢✉♥❝t♦rs✮ t❤❛t ♠❛❦❡ ✐t ❛ ♠♦❞❡• ♦❢ ❝•❛ss✐❝❛• •✐♥❡❛r •♦❣✐❝✱ ❛s ♣r❡s❡♥t❡❞ ✐♥ s❡❝t✐♦♥ ✷✱ ❛r❡ ❢r❡❡ ❢r♦♠ ❛♥② r❡❢❡r❡♥❝❡ t♦ t❤❡ ✜♥✐t❡♥❡ss str✉❝t✉r❡✿ t❤❡② ❛r❡ •✉st ✐♥tr♦❞✉❝❡❞ ❛s r❡•❛t✐♦♥s ♦♥ ✇❡❜s✱ ❛♥❞ ✐t s✐♠♣•② t✉r♥s ♦✉t t❤❡② ❛r❡ ✜♥✐t❛r②✱ ✇❤❛t❡✈❡r ✜♥✐t❡♥❡ss str✉❝t✉r❡ ✇❡ ❝♦♥s✐❞❡r ♦♥ t❤❡ ✉♥❞❡r•②✐♥❣ ♦❜•❡❝ts✳ ❚❤❡ ♦♥•② r❡str✐❝t✐♦♥ ✇❡ ♠❛❦❡ ✐♥ t❤❡ ✐♥t❡r♣r❡t❛t✐♦♥ ♦❢ λ✲❝❛•❝✉•✐ ✐s t❤❛t a ∈ F ( A ) ❢♦r ❛•• a ∈ C A ✳ ❚❤❡♦r❡♠ ✶ ✭❋✐♥✐t❡♥❡ss✮✳ ❚❤❡ s❡♠❛♥t✐❝s ♦❢ ❛ t②♣❡❞ t❡r♠ ✐s ✜♥✐t❛r②✿ ✐❢ x 1 : A 1 , . . . , x n : A n ⊢ s : A t❤❡♥ s x1:A1,...,xn:An ∈ F ( A 1 ⇒ • • • ⇒ A n ⇒ A )✳ Pr♦♦❢ ❚❤✐s ❤♦•❞s ❞✐r❡❝t•② ❜❡❝❛✉s❡ t❤❡ s❡♠❛♥t✐❝s ✇❡ ❤❛✈❡ ✐♥tr♦❞✉❝❡❞ ✐s •✉st r❡♣❤r❛s✐♥❣ t❤❡ ✉s✉❛• ✐♥t❡r♣r❡t❛t✐♦♥ ♦❢ t②♣❡❞ λ✲❝❛•❝✉•✐ ✐♥ ❛ ❝❛rt❡s✐❛♥ ❝•♦s❡❞ ❝❛t✲ ❡❣♦r② ❬✺(✱ ✐♥ t❤❡ ♣❛rt✐❝✉•❛r ❝❛s❡ ♦❢ Fin ! ✳ ◆♦t❛❜•②✿ r✉•❡s ❯♥✐t ✱ P❛✐r l ✱ P❛✐r r ✱ ▲❡❢t ❛♥❞ |✐❣❤t ♠❛t❝❤ t❤❡ ❞❡✜♥✐t✐♦♥ ♦❢ t❤❡ ❝❛rt❡s✐❛♥ str✉❝t✉r❡ ♦❢ Fin ! ❀ r✉•❡s ❆❜s ❛♥❞ ❆♣♣ ♠❛t❝❤ t❤❡ ❛❞•✉♥❝t✐♦♥ Fin ! (Γ ⊕ A, B) ∼ = Fin ! (Γ, A ⇒ B) ❛♥❞ t❤❡ ❞❡✜♥✐t✐♦♥ ♦❢ ❝♦♠♣♦s✐t✐♦♥ ✐♥ Fin ! ✳ ❋♦r t❤❡ r❡❛❞❡r ♥♦t ❢❛♠✐•✐❛r ✇✐t❤ t❤✐s ❝♦♥str✉❝t✐♦♥✱ ❛ ❞✐r❡❝t ♣r♦♦❢ ✐s ❛•s♦ ♣♦ss✐❜•❡ ❜② ✐♥❞✉❝t✐♦♥ ♦♥ t②♣✐♥❣ ❞❡r✐✈❛t✐♦♥s✳ ❚❤❡ ♦♥•② ♥♦♥✲tr✐✈✐❛• ❝❛s❡ ✐s t❤❛t ♦❢ ❆♣♣ ✱ ✇❤✐❝❤ ❡ss❡♥t✐❛••② ❜♦✐•s ❞♦✇♥ t♦ |❡♠❛r❦ ✶✳ ❚❤❡ ✐♥t❡r♣r❡t❛t✐♦♥ ♦❢ t❡r♠s ✇❡ ❤❛✈❡ •✉st ❞❡✜♥❡❞ ✐s ♦❢ ❝♦✉rs❡ ❛ ♠♦❞❡• ♦❢ ≃ 0 ✇❤❛t❡✈❡r t❤❡ ❝❤♦✐❝❡ ♦❢ ❜❛s❡ t②♣❡s ❛♥❞ ❝♦♥st❛♥ts✳ ❚❤❡♦r❡♠ ✷ ✭■♥✈❛r✐❛♥❝❡✮✳ ■❢ Γ ⊢ s ≃ 0 t : A t❤❡♥ s Γ = t Γ ✳ Pr♦♦❢ ❆❣❛✐♥✱ t❤✐s ❢♦••♦✇s ❞✐r❡❝t•② ❢r♦♠ t❤❡ ❢❛❝t t❤❛t ✇❡ ✉s❡❞ t❤❡ st❛♥❞❛r❞ tr❛♥s•❛t✐♦♥ ♦❢ t②♣❡❞ λ✲❝❛•❝✉•✐ ✐♥ ❝❛rt❡s✐❛♥ ❝•♦s❡❞ ❝❛t❡❣♦r✐❡s✳ ❆ ❞✐r❡❝t ♣r♦♦❢ ✐s ❛•s♦ ❡❛s②✿ ✕ ✜rst s❤♦✇ ❜② ✐♥❞✉❝t✐♦♥ ♦♥ s t❤❛t✱ ✐❢ Γ 0 , x : A [α1,...,α k ] , ∆ 0 ⊢ s β : B✱ ❛♥❞✱ ❢♦r ❛•• j ∈ {1, . . . , k}✱ Γ j , ∆ j ⊢ t αj : A✱ t❤❡♥ k j=0 Γ j , k j=0 ∆ j ⊢ s [x := t] β : B❀ ✕ t❤❡♥ ❝❤❡❝❦ t❤❛t ❢♦r ❛ ❜❛s✐❝ r❡❞✉❝t✐♦♥ Γ ⊢ s > 0 t : A✱ (α 1 , . . . , α n , α) ∈ s Γ ✐✛ (α 1 , . . . , α n , α) ∈ t Γ ✱ ✇❤✐❝❤ ✐s ❞✐r❡❝t ❜② t❤❡ r✉•❡s ♦❢ ❋✐❣✉r❡ ✷ ❛♥❞ t❤❡ ♣r❡✈✐♦✉s r❡s✉•t ♦♥ s✉❜st✐t✉t✐♦♥❀ ✕ ❝♦♥❝•✉❞❡ ❜② ❝♦♥t❡①t✉❛•✐t② ♦❢ t❤❡ s❡♠❛♥t✐❝s✳ ◆♦t✐❝❡ t❤❛t t❤❡ ✐♥✈❛r✐❛♥❝❡ ♦❢ t❤❡ s❡♠❛♥t✐❝s ❤❛s ♥♦t❤✐♥❣ t♦ ❞♦ ✇✐t❤ t❤❡ ✜♥✐t❡♥❡ss str✉❝t✉r❡✿ t❤❡ r❡s✉•t ✐s ❛❝t✉❛••② ❛ ♣r♦♣❡rt② ♦❢ t❤❡ r❡•❛t✐♦♥❛• ✐♥t❡r♣r❡t❛t✐♦♥ ♦♥•②✳ ❊①❛♠♣•❡s✳ ▲❡t ✉s ❝♦♥s✐❞❡r s♦♠❡ ♣❛rt✐❝✉•❛r ❝❛•❝✉•✐✳ P✉r❡ t②♣❡❞ λ✲❝❛•❝✉•✐ ❛r❡ t❤♦s❡ ✇✐t❤ ♥♦ ❛❞❞✐t✐♦♥❛• ❝♦♥st❛♥t ♦r ❝♦♥✈❡rs✐♦♥ r✉•❡✿ ✜① ❛ s❡t A ♦❢ ❛t♦♠✐❝ t②♣❡s✱ ❛♥❞ ✇r✐t❡ Λ A 0 ❢♦r t❤❡ ❝❛•❝✉•✉s ✇❤❡r❡ C A = ∅ ❢♦r ❛•• A✱ ❛♥❞ s ≃ t ✐✛ s ≃ 0 t✳ ❚❤✐s ✐s t❤❡ ♠♦st ❜❛s✐❝ ❝❛s❡ ❛♥❞ ✇❡ ❤❛✈❡ •✉st s❤♦✇♥ t❤❛t ✜♥✐t❡♥❡ss s♣❛❝❡s ♠♦❞❡• ≃ 0 ✳ ❇❡ ❛✇❛r❡ t❤❛t ✐❢ ✇❡ ✐♥tr♦❞✉❝❡ ♥♦ ❛t♦♠✐❝ t②♣❡✱ t❤❡♥ t❤❡ s❡♠❛♥t✐❝s ✐s ❛❝t✉❛••② tr✐✈✐❛•✿ ✐♥ Λ ∅ 0 ✱ ❛•• t②♣❡s ❛r❡ ✐♥t❡r♣r❡t❡❞ ❜② 0 ❛♥❞ ❛•• t❡r♠s ❜② t❤❡ ❡♠♣t② s❡t✳ ❇② ❝♦♥tr❛st✱ ✇❡ ❝❛♥ ❝♦♥s✐❞❡r t❤❡ ✐♥t❡r♥❛• •❛♥❣✉❛❣❡ Λ Fin ♦❢ Fin ! ✐♥ ✇❤✐❝❤ ❛•• ✜♥✐t❛r② r❡•❛t✐♦♥s ❝❛♥ ❜❡ ❞❡s❝r✐❜❡❞✿ ✜① A ❛s t❤❡ ❝♦••❡❝t✐♦♥ ♦❢ ❛•• ✜♥✐t❡♥❡ss s♣❛❝❡s ❛♥❞ C A = F ( A )✳ ❚❤❡♥ s❡t s ≃ Fin t ✐✛ s Γ = t Γ ✱ ❢♦r ❛♥② s✉✐t❛❜•❡ Γ ✳ ❚❤❡ ♣♦✐♥t ✐♥ ❞❡✜♥✐♥❣ s✉❝❤ ❛ ♠♦♥str♦✉s •❛♥❣✉❛❣❡ ✐s t♦ ❡♥❛❜•❡ ✈❡r② ♥❛t✉r❛• ♥♦t❛t✐♦♥s ❢♦r ✜♥✐t❛r② r❡•❛t✐♦♥s✿ ✐♥ ❣❡♥❡r❛•✱ ✇❡ ✇✐•• ✐❞❡♥t✐❢② ❝•♦s❡❞ t❡r♠s ✐♥ Λ Fin ✇✐t❤ t❤❡ r❡•❛t✐♦♥s t❤❡② ❞❡♥♦t❡ ✐♥ t❤❡ ❡♠♣t② ❝♦♥t❡①t✳ ■♥ t❤❛t ❝❛s❡✱ ✇❡ ♠✐❣❤t ♠❛❦❡ ❡①♣•✐❝✐t t❤❡ t②♣❡ ♦❢ ❜♦✉♥❞ ✈❛r✐❛❜•❡s✳ ❋♦r ✐♥st❛♥❝❡✱ ✇❡ ✇r✐t❡ λx A x = der A ❀ ❛♥❞ ✐❢ f ∈ Fin ! (A, B) ❛♥❞ g ∈ Fin ! (B, C)✱ ✇❡ ❤❛✈❡ λx A (g (f x)) = g • f ∈ Fin ! (A, B)✳ ❇❡❢♦r❡ ✇❡ ❛❞❞r❡ss t❤❡ ♠❛✐♥ s✉❜•❡❝t ♦❢ t❤❡ ♣❛♣❡r✱ s②st❡♠ T ✱ •❡t✬s •✉st r❡✈✐❡✇ s♦♠❡ ❡❛s② ❡①❛♠♣•❡s ♦❢ ✉s✉❛• λ✲❝❛•❝✉•✐ ❝♦♥str✉❝t✐♦♥s t❤❛t ❝❛♥ ❜❡ ♠♦❞❡••❡❞ ✐♥ Fin ! ✳ ❋✐rst✱ ❜❡✐♥❣ ❛ ❝❛rt❡s✐❛♥ ❝•♦s❡❞ ❝❛t❡❣♦r②✱ Fin ! ✐s ❛❝t✉❛••② ❛♥ ♠♦❞❡• ♦❢ ♣✉r❡ t②♣❡❞ λ✲❝❛•❝✉•✐ ✇✐t❤ ❡①t❡♥s✐♦♥❛•✐t②✱ s✉r•❡❝t✐✈❡ ♣❛✐r✐♥❣ ❛♥❞ t❡r♠✐♥❛• ♦❜•❡❝t✿ ❚❤❡♦r❡♠ ✷ st✐•• ❤♦•❞s ✐❢ ✇❡ ❛❞❞ t❤❡ r❡❞✉❝t✐♦♥s λx (u x) > 0 u✱ π l s, π r s > 0 s ❛♥❞ v > 0 ❛s s♦♦♥ ❛s x ✐s ♥♦t ❢r❡❡ ✐♥ u ❛♥❞ v ❤❛s t②♣❡ ⊤ ✭♥♦t✐❝❡✱ ❤♦✇❡✈❡r✱ t❤❛t ✐♥ t❤❛t ❝❛s❡ > 0 ✐s ♥♦ •♦♥❣❡r ❝♦♥✢✉❡♥t ❬✺(✮✳ ❲❡ ❝❛♥ ❛•s♦ ❡①t❡♥❞ t❤❡ •❛♥❣✉❛❣❡ ✇✐t❤ ♣❛rt✐❝✉•❛r ❜❛s❡ t②♣❡s ❛♥❞ ❝♦♥st❛♥ts✳ ❋♦r ✐♥st❛♥❝❡✱ ✇❡ ❝❛♥ ✐♥tr♦❞✉❝❡ ❜❛s❡ t②♣❡ Bool t♦❣❡t❤❡r ✇✐t❤ ❝♦♥st❛♥ts T ❛♥❞ F ♦❢ t②♣❡ Bool✱ ❛♥❞ D A ♦❢ t②♣❡ Bool → A → A → A✱ ✇✐t❤ t❤❡ ❛❞❞✐t✐♦♥❛• r❡❞✉❝t✐♦♥s D T s t > s ❛♥❞ D F s t > t ✭✇❡ ✇✐•• ✐♥ ❣❡♥❡r❛• ♦♠✐t t❤❡ t②♣❡ s✉❜s❝r✐♣t ♦❢ s✉❝❤ ♣❛r❛♠❡t❡r❡❞ ❝♦♥st❛♥ts✱ ✇✐t❤ t❤❡ ♦❜✈✐♦✉s ❤②♣♦t❤❡s❡s ♦♥ t②♣❛❜✐•✐t②✮ ❛♥❞ ✜① ✐♥t❡r♣r❡t❛t✐♦♥s ❛s ❢♦••♦✇s✿ ✇r✐t❡ B = 1 ⊕ 1 ❛♥❞ ✇r✐t❡ t❤❡ ♦♥•② t✇♦ ❡•❡♠❡♥ts ♦❢ |B| ❛s tt ❛♥❞ ff ❀ t❤❡♥ •❡t Bool = B✱ T = T = {tt}✱ F = F = {ff } ❛♥❞ D A = D A = {([tt] , [α] , [] , α); α ∈ A } ∪ {([ff ] , [] , [α] , α); α ∈ A }✳ ❚❤❛t t❤❡s❡ ✐♥t❡r♣r❡t❛t✐♦♥s ❛r❡ ✜♥✐t❛r② s❤♦✉•❞ ❜❡ ❝•❡❛r✳ ❚❤❡♥ ♦♥❡ r❡t❛✐♥s t❤❛t Γ ⊢ s ≃ t : A ✐♠♣•✐❡s s Γ = t Γ ✳ ❙②st❡♠ T ✳ ❚❤❡ ♠❛✐♥ ❝♦♥tr✐❜✉t✐♦♥ ♦❢ t❤❡ ♣r❡s❡♥t ♣❛♣❡r ✐s t♦ ❡st❛❜•✐s❤ t❤❛t Fin ! ♠♦❞❡•s •ö❞❡•✬s s②st❡♠ T ✱ ✇❤✐❝❤ ❝❛♥ ❜❡ ♣r❡s❡♥t❡❞ ✐♥ ✈❛r✐♦✉s ✇❛②s✳ ❚❤❡ ✐t❡r❛t♦r ✈❡rs✐♦♥ ♦❢ s②st❡♠ T ✐s t❤❡ t②♣❡❞ λ✲❝❛•❝✉•✉s ✇✐t❤ ❛♥ ❛t♦♠✐❝ t②♣❡ Nat ♦❢ ♥❛t✉r❛• ♥✉♠❜❡rs✱ ❛♥❞ ❝♦♥st❛♥ts O ♦❢ t②♣❡ Nat✱ S ♦❢ t②♣❡ Nat → Nat ❛♥❞ ❢♦r ❛•• t②♣❡ A✱ I A ♦❢ t②♣❡ Nat → (A → A) → A → A ❛♥❞ s✉❜•❡❝t t♦ t❤❡ ❢♦••♦✇✐♥❣ ❛❞❞✐t✐♦♥❛• ❝♦♥✈❡rs✐♦♥s✿ I (O) u v > v ❛♥❞ I (S t) u v > u (I t u v)✳ ❚❤❡ r❡❝✉rs♦r ✈❛r✐❛♥t ✐s s✐♠✐•❛r✱ ❜✉t t❤❡ ✐t❡r❛t♦r ✐s r❡♣•❛❝❡❞ ✇✐t❤ R A ♦❢ t②♣❡ Nat → (Nat → A → A) → A → A s✉❜•❡❝t t♦ ❝♦♥✈❡rs✐♦♥s R (O) u v > v ❛♥❞ R (S t) u v > u t (R t u v)✳ (❡t ❛♥♦t❤❡r ♣♦ss✐❜•❡ s②st❡♠ ✐s ♦❜t❛✐♥❡❞ ✇✐t❤ t❛✐• r❡❝✉rs✐✈❡ ✐t❡r❛t✐♦♥✿ t❛❦❡ J A ♦❢ t②♣❡ Nat → (A → A) → A → A ❛♥❞ •❡t J (S t) u v > J t u (u v)✳ ❚❤♦s❡ s②st❡♠s ❛••♦✇ t♦ r❡♣r❡s❡♥t ❡①❛❝t•② t❤❡ s❛♠❡ ❢✉♥❝t✐♦♥s ♦♥ t❤❡ s❡t ♦❢ ♥❛t✉r❛• ♥✉♠❜❡rs✱ ✇❤❡r❡ t❤❡ ♥✉♠❜❡r n ✐s ♦❜✈✐♦✉s•② ❞❡♥♦t❡❞ ❜② S n O✿ t❤✐s ✐s t❤❡ ❝♦♥s❡q✉❡♥❝❡ ♦❢ ❛ ♥♦r♠❛•✐③❛t✐♦♥ t❤❡♦r❡♠ ✭s❡❡ ❬✻(✮✳ ◆♦t✐❝❡ ✐♥ ♣❛rt✐❝✉•❛r t❤❛t✱ ✇❤❡♥ ❛♣♣•✐❡❞ t♦ ❛ ❝❛♥♦♥✐❝❛• ✐♥t❡❣❡r✱ I ❛♥❞ J ❝♦✐♥❝✐❞❡✿ I (S n O)uv ≃ J (S n O)uv ≃ u n v❀ t❤✐s ❞♦❡s ♥♦t ❤♦•❞ ❢♦r ❛•• t❡r♠ ♦❢ t②♣❡ Nat✱ ❤♦✇❡✈❡r✳ ❆•s♦✱ ✇❡ ❝❛♥ ❞❡✲ ✜♥❡ ❛ r❡❝✉rs♦r ✉s✐♥❣ ✐t❡r❛t✐♦♥ ❛♥❞ ♣r♦❞✉❝ts ✇✐t❤ t❤❡ st❛♥❞❛r❞ ❡♥❝♦❞✐♥❣ r❡❝ = λx λy λz π l (I x z, O λw y (π r w) (π l w), S (π r w) )✱ ❛♥❞ ✇❡ ❣❡t r❡❝ (S n O)uv ≃ R (S n O)uv✳ ❚❤❡ ✐❞❡❛ ✐s t♦ r❡❝♦♥str✉❝t t❤❡ ✐♥t❡❣❡r ❛r❣✉♠❡♥t ♦♥ t❤❡ ✢②✳ ❆❣❛✐♥✱ t❤✐s ❡♥❝♦❞✐♥❣ ✐s ✈❛•✐❞ ♦♥•② ❜② ✈❛•✉❡s ❛♥❞ r❡❝ (S t) u v ≃ u t (r❡❝ t u v) ❤♦•❞s ♦♥•② ✐❢ ✇❡ s✉♣♣♦s❡ t ✐s ♦❢ t❤❡ ❢♦r♠ S n O ✭♥♦t✐❝❡ ✇❡ ❝♦✉•❞ ❛s ✇❡•• ✉s❡ J ✐♥ t❤❡ ❞❡✜♥✐t✐♦♥ ♦❢ r❡❝✮✳ ❖♥•② t❤❡ ❡♥❝♦❞✐♥❣ ♦❢ t❤❡ ✐t❡r❛t♦r ❜② ✐t❡r = λx λy λz (R x (λx ′ y) z) ✐s ❡①t❡♥s✐♦♥❛••② ✈❛•✐❞✿ ✐t❡r O u v ≃ v ❛♥❞ ✐t❡r (S t) u v ≃ u (✐t❡r t u v)✳ ❚❤❡ ❢❛❝t t❤❛t ✐♥ ❣❡♥❡r❛• t❤❡ ❡♥❝♦❞✐♥❣ ♦❢ ♦♥❡ s②st❡♠ ✐♥t♦ t❤❡ ♦t❤❡r ❤♦•❞s ♦♥•② ♦♥ ✈❛•✉❡s ✐♥❞✐❝❛t❡ t❤❛t t❤❡✐r r❡s♣❡❝t✐✈❡ ❛•❣♦r✐t❤♠✐❝ ♣r♦♣❡rt✐❡s ♠❛② ❞✐✛❡r✳ ❆♥❞ t❤❡s❡ ❞✐✛❡r❡♥❝❡s ✇✐•• ❛♣♣❡❛r ✐♥ t❤❡ s❡♠❛♥t✐❝s✳ |❡❝❛•• ❢♦r ✐♥st❛♥❝❡ t❤❡ ❞✐s❝✉ss✐♦♥ ✐♥ ♦✉r ✐♥tr♦❞✉❝t✐♦♥✿ J ✉s❡s ✐ts ✐♥t❡❣❡r ❛r❣✉♠❡♥t •✐♥❡❛r•②✳ ❚❤✐s ❡♥❛❜•❡❞ ❊❤r❤❛r❞ t♦ ❞❡✜♥❡ ❛ s❡♠❛♥t✐❝s ♦❢ ✐t❡r❛t✐♦♥✱ ✇✐t❤ Nat = N = (N, P ❢ (N))✱ O = O = {0} ❛♥❞ S = S ! = {([n] , n + 1); n ∈ N}✳ ❙✉❝❤ ❛♥ ✐♥t❡r♣r❡t❛t✐♦♥ ♦❢ ♥❛t✉r❛• ♥✉♠❜❡rs✱ ❤♦✇❡✈❡r✱ ❢❛✐•s t♦ ♣r♦✈✐❞❡ ❛ s❡♠❛♥t✐❝s ♦❢ I ♦r R✳ ▲❡♠♠❛ ✶✳ ❆ss✉♠❡ Nat = N ✱ O = O ❛♥❞ S = S ! ✱ ❛♥❞ •❡t A ❜❡ ❛♥② t②♣❡ s✉❝❤ t❤❛t A = 0✳ ❚❤❡♥ t❤❡r❡ ✐s ♥♦ I A ∈ F (N ⇒ ( A ⇒ A ) ⇒ A ⇒ A ) s✉❝❤ t❤❛t✱ s❡tt✐♥❣ I A = I A ✱ ✇❡ ♦❜t❛✐♥ I O u v Γ = v Γ ❛♥❞ I (S t) u v Γ = u (I t u v) Γ ❛s s♦♦♥ ❛s Γ ⊢ t : Nat✱ Γ ⊢ u : A → A ❛♥❞ Γ ⊢ v : A✳ Pr♦♦❢ ❇② ❝♦♥tr❛❞✐❝t✐♦♥✱ ❛ss✉♠❡ t❤❡ ❛❜♦✈❡ ❡q✉❛t✐♦♥s ❤♦•❞✳ ❲❡ ❣❡t I (S x) (λz ′ y) z x:Nat,y:A,z:A = y x:Nat,y:A,z:A = {([] , [α] , [] , α); α ∈ | A |} . ❖♥❡ ❝❛♥ ❝❤❡❝❦ t❤❛t✿ x [] : Nat, y [α] : A, z [] : A ⊢ I (S x) (λz ′ y) z α : A ✐✛ x [] : Nat, y [α] : A ⊢ I (S x) (λz ′ y) ([],α) : A ✐✛ x [] : Nat ⊢ I (S x) ([([],α)],[],α) : A ✐✛ ⊢ I ([],[([],α)],[],α) : A ( * ) ❛♥❞ t❤❡♥ ⊢ I O ([([],α)],[],α) ❢♦r ❛•• α ∈ | A |✳ ❚❤✐s ❝♦♥tr❛❞✐❝ts t❤❡ ❢❛❝t t❤❛t✱ ❜② t❤❡ ✜rst ❡q✉❛t✐♦♥✿ I O = λy λz (I O y z) = λy λz z = {([] , [α] , α); α ∈ | A |} ❜❡❝❛✉s❡ ✇❡ s✉♣♣♦s❡❞ | A | = ∅✳ |❡♠❛r❦ ✸✳ ❚❤❡ ❡q✉✐✈❛•❡♥❝❡ ✭ * ✮ ❤♦•❞s ❜❡❝❛✉s❡ S = S ! ✐s •✐♥❡❛r✱ ❤❡♥❝❡ str✐❝t✿ t❤✐s r❡✢❡❝ts t❤❡ ❣❡♥❡r❛• ❢❛❝t t❤❛t✱ ✐❢ s ∈ F (A ⇒ B) ❝♦♥t❛✐♥s ♥♦ ([] , β) t❤❡♥✱ ❢♦r ❛•• t ∈ F (B ⇒ C)✱ ([] , γ) ✐♥ t • s ✐✛ ([] , γ) ∈ t✳ ❙✉❝❤ ❛ ♣❤❡♥♦♠❡♥♦♥ ✇❛s ❛•r❡❛❞② ♥♦t❡❞ ❜② •✐r❛r❞ ✐♥ ❤✐s ✐♥t❡r♣r❡t❛t✐♦♥ ♦❢ s②st❡♠ T ✐♥ ❝♦❤❡r❡♥❝❡ s♣❛❝❡s ❬✻(✳ ❍✐s ❡✈✐❞❡♥❝❡ t❤❛t t❤❡r❡ ✇❛s ♥♦ ✐♥t❡r♣r❡t❛t✐♦♥ ♦❢ t❤❡ ✐t❡r❛t✐♦♥ ♦♣❡r❛t♦r ✉s✐♥❣ t❤❡ •✐♥❡❛r s✉❝❝❡ss♦r r❡•✐❡❞ ♦♥ ❛ ❝♦❤❡r❡♥❝❡ ❛r❣✉♠❡♥t✳ ❚❤❡ ♣r❡✈✐♦✉s •❡♠♠❛ ✐s str♦♥❣❡r✿ ♥♦t✐❝❡ t❤❛t t❤✐s ♠❛❦❡s ♥♦ ✉s❡ ♦❢ ❤②♣♦t❤❡s❡s ♦♥ ✜♥✐t❡♥❡ss str✉❝t✉r❡s❀ ❤❡♥❝❡✱ ✐t ❤♦•❞s ✐♥ t❤❡ r❡•❛t✐♦♥❛• ♠♦❞❡• ❛s ✇❡••✱ ❛♥❞ ❛❝t✉❛••② ❛♥② ✇❡❜ ❜❛s❡❞ ♠♦❞❡• ♦❢ •✐♥❡❛r •♦❣✐❝ ✇❤❡r❡ ♣r♦♠♦t✐♦♥ ✐s ❞❡✜♥❡❞ s✐♠✐•❛r•②✱ ❛s s♦♦♥ ❛s t❤❡ ✐♥t❡r♣r❡t❛t✐♦♥ ♦❢ s✉❝❝❡ss♦r ✐s str✐❝t✳ ▲❛③② ✐♥t❡❣❡rs✳ ■♥ s❤♦rt✱ str✐❝t ♠♦r♣❤✐s♠s ❝❛♥♥♦t ♣r♦❞✉❝❡ ❛♥②t❤✐♥❣ ❡① ♥✐❤✐•♦ ❀ ❜✉t t❤❡ s✉❝❝❡ss♦r ♦❢ ❛♥② ✐♥t❡❣❡r s❤♦✉•❞ ❜❡ ♠❛r❦❡❞ ❛s ♥♦♥✲③❡r♦✱ ❢♦r t❤❡ ✐t❡r❛t♦r t♦ ❞✐st✐❣✉✐s❤ ❜❡t✇❡❡♥ ❜♦t❤ ❝❛s❡s✳ ❍❡♥❝❡ t❤❡ s✉❝❝❡ss♦r s❤♦✉•❞ ❜❡ ❛✣♥❡✿ s✐♠✐•❛r•② t♦ •✐r❛r❞✬s s♦•✉t✐♦♥✱ ✇❡ ✇✐•• ✐♥t❡r♣r❡t Nat ❜② s♦✲❝❛••❡❞ •❛③② ♥❛t✉r❛• ♥✉♠❜❡rs✳ ▲❡t N l = (|N l | , P ❢ (|N l |)) ❜❡ s✉❝❤ t❤❛t |N l | = N ∪ N > ✱ ✇❤❡r❡ N > ✐s •✉st ❛ ❞✐s•♦✐♥t ❝♦♣② ♦❢ N✳ ❚❤❡ ❡•❡♠❡♥ts ♦❢ N > ❛r❡ ❞❡♥♦t❡❞ ❜② k > ✱ ❢♦r k ∈ N✿ n > r❡♣r❡s❡♥ts ❛ ♣❛rt✐❛• ✐♥t❡❣❡r✱ ♥♦t ❢✉••② ❞❡t❡r♠✐♥❡❞ ❜✉t str✐❝t•② ❣r❡❛t❡r t❤❛♥ k✳ ■❢ ν ∈ |N l |✱ ✇❡ ❞❡✜♥❡ ν + ❛s k + 1 ✐❢ ν = k ❛♥❞ (k + 1) > ✐❢ ν = k > ✳ ❚❤❡♥ ✇❡ s❡t S l = {([] , 0 > )} ∪ {([ν] , ν + )}✱ ✇❤✐❝❤ ✐s ❛✣♥❡✳ ◆♦t✐❝❡ t❤❛t O ∈ F (N l ) ❛♥❞ S l ∈ F (N l ⇒ N l )✳ ❲❡ ✇✐•• s❤♦✇ t❤❛t t❤❡s❡ ❛••♦✇ t♦ ♣r♦✈✐❞❡ ❛♥ ✐♥t❡r♣r❡t❛t✐♦♥ ♦❢ r❡❝✉rs✐♦♥✱ ❤❡♥❝❡ ✐t❡r❛t✐♦♥✱ ✐♥ s②st❡♠ T ✿ ❢♦r ❛•• ✜♥✐t❡♥❡ss s♣❛❝❡ A✱ t❤❡r❡ ❡①✐sts R A ∈ F (N l ⇒ (N l ⇒ A ⇒ A) ⇒ A ⇒ A) s✉❝❤ t❤❛t✱ ✐♥ Λ Fin ✱ y : N l ⇒ A ⇒ A, z : N l ⊢ R O y z ≃ z : A ❛♥❞ x : N l , y : N l ⇒ A ⇒ A, z : N l ⊢ R (S l x) y z ≃ y x (R x y z) : A. ✹ ❆ r❡❝✉rs✐♦♥ ♦♣❡r❛t♦r ✐♥ ✜♥✐t❡♥❡ss s♣❛❝❡s ❋♦r ❛•• ✜♥✐t❡♥❡ss s♣❛❝❡ A✱ ✇r✐t❡ RecOp [A] = N l ⇒ (N l ⇒ A ⇒ A) ⇒ A ⇒ A✳ ❲❡ ✇❛♥t t♦ ✐♥tr♦❞✉❝❡ ❛ r❡❝✉rs✐♦♥ ♦♣❡r❛t♦r R A ∈ F (RecOp [A]) ✐♥t✉✐t✐✈❡•② s✉❜•❡❝t t♦ t❤❡ ❢♦••♦✇✐♥❣ ❞❡✜♥✐t✐♦♥✿ R t u v = ♠❛t❝❤ t ✇✐t❤ O → v S t ′ → u t ′ (R t ′ u v) . ❚❤✐s ❞❡✜♥✐t✐♦♥ ✐s r❡❝✉rs✐✈❡✱ ❛♥❞ ❛ ♥❛t✉r❛• ♠❡❛♥s t♦ ♦❜t❛✐♥ s✉❝❤ ❛♥ ♦♣❡r❛t♦r ✐s ❛s t❤❡ ✜①♣♦✐♥t ♦❢✿ λX RecOp λx N l λy N l ⇒A⇒A λz A ♠❛t❝❤ x ✇✐t❤ O → z S x ′ → y x ′ (X x ′ y z) . ✭✶✮ ❋✐①♣♦✐♥ts✳ ❚❤❡ ❝❛rt❡s✐❛♥ ❝•♦s❡❞ ❝❛t❡❣♦r② Rel ! ✐s ❝♣♦✲❡♥r✐❝❤❡❞✱ t❤❡ ♦r❞❡r ♦♥ ♠♦r✲ ♣❤✐s♠s ❜❡✐♥❣ ✐♥❝•✉s✐♦♥✳ ❍❡♥❝❡ ✐t ❤❛s ✜①♣♦✐♥ts ❛t ❛•• t②♣❡s✿ ❢♦r ❛•• s❡t A ❛♥❞ f ∈ Rel ! (A, A)✱ t❤❡ •❡❛st ✜①♣♦✐♥t ♦❢ f ✐s k≥0 f k ∅✱ ✇❤✐❝❤ ✐s ❛♥ ✐♥❝r❡❛s✐♥❣ ✉♥✐♦♥✳ ❚❤❡ •❡❛st ✜①♣♦✐♥t ♦♣❡r❛t♦r ✐s ✐ts❡•❢ ❞❡✜♥❛❜•❡ ❛s t❤❡ s✉♣r❡♠✉♠ ♦❢ ✜♥✐t❛r② ❛♣✲ ♣r♦①✐♠❛♥ts✱ Fix A = k≥0 Fix (k) A ✱ ✇❤❡r❡✿ Fix (0) A = ∅ Fix (k+1) A = λf f Fix (k) A f = [([α 1 , . . . , α n ] , α)] + n i=1 ϕ i , α ; ∀i, (ϕ i , α i ) ∈ Fix (k) A . ◆♦t✐❝❡ ✐♥❞❡❡❞ t❤❛t ✐❢ A ✐s ❛ ✜♥✐t❡♥❡ss s♣❛❝❡ t❤❡♥✱ ❢♦r ❛•• k✱ Fix (k) A = Fix

F

  ((A ⇒ A) ⇒ A)✳ ❚❤❡ ✜①♣♦✐♥t✱ ❤♦✇❡✈❡r✱ ✐s ♥♦t ✜♥✐t❛r② ✐♥ ❣❡♥❡r❛•✿ ♦♥❡ ❝❛♥ ❝❤❡❝❦ ❢♦r ✐♥st❛♥❝❡ t❤❛t Fix N l S l = N > ∈ F (N l ) ❤❡♥❝❡ Fix N l ∈ F ((N l ⇒ N l ) ⇒ N l )✳ ❙♦ ♦✉r ❞❡✜♥✐t✐♦♥ ♦❢ ❛ r❡❝✉rs♦r ♦♣❡r❛t♦r ✐s ✐♥ t✇♦ st❡♣s✿ ✇❡ ✜rst ✐♥tr♦❞✉❝❡ t❤❡ ✜♥✐t❛r② ❛♣♣r♦①✐♠❛♥ts R (k) A ∈ F (RecOp [A]) ❜② R (k) A = Step k A ∅✱ ✇❤❡r❡ Step ∈ F (RecOp [A] ⇒ RecOp [A]) ✐s ❞❡✜♥❡❞ ❛s ✐♥ ❢♦r♠✉•❛ ✭✶✮❀ t❤❡♥ ✇❡ ♣r♦✈❡ R A = k≥0 R (k) A ∈ F (RecOp [A])✳ P❛tt❡r♥ ♠❛t❝❤✐♥❣ ♦♥ •❛③② ✐♥t❡❣❡rs✳ ❲❡ ✐♥tr♦❞✉❝❡ ❛ ✜♥✐t❛r② ♦♣❡r❛t♦r Case✱ ✐♥t✉✲ ✐t✐✈❡•② ❞❡✜♥❡❞ ❛s✿ Case t u v = ♠❛t❝❤ t ✇✐t❤ O → v S t ′ → u t ′ . ▼♦r❡ ❢♦r♠❛••②✿ ❉❡✜♥✐t✐♦♥ ✶✳ ■❢ ν = [ν 1 , . . . , ν k ] ∈ M ✜♥ (|N l |)✱ ✇❡ ✇r✐t❡ ν + = ν + 1 , . . . , ν + n ✳ ❚❤❡♥ ❢♦r ❛•• ✜♥✐t❡♥❡ss s♣❛❝❡ A✱ ✇❡ •❡t Case A = {([0] , [] , [α] , α); α ∈ |A|} ∪ ([0 > ] + ν + , [(ν, α)] , [] , α); ν ∈ M ✜♥ (|N l |) ∧ α ∈ |A| ✳ ▲❡♠♠❛ ✷✳ ❚❤❡ r❡•❛t✐♦♥ Case ✐s ✜♥✐t❛r②✿ Case A ∈ F (N l ⇒ (N l ⇒ A) ⇒ A ⇒ A)✳ ▼♦r❡♦✈❡r✱ y : N l ⇒ A, z : A ⊢ Case O y z ≃ z : A ❛♥❞ x : N l , y : N l ⇒ A, z : A ⊢ Case (S l x) y z ≃ y x : A✳ Pr♦♦❢ ❚❤❛t t❤❡ ❡q✉❛t✐♦♥s ❤♦•❞ ✐s ❛ r♦✉t✐♥❡ ❡①❡r❝✐s❡✳ ❲❡ ✉s❡ |❡♠❛r❦ ✶ t♦ ♣r♦✈❡ Case ✐s ✜♥✐t❛r②✳ ❋♦r ❛•• n ∈ F (N )✱ Case A n ⊆ {([] , [α] , α); α ∈ |A|} ∪ ([(ν, α)] , [] , α); ν ∈ n ! ∧ α ∈ |A| ⊆ λy N l ⇒A λz A z ∪ λy N l ⇒A λz A (y n) ❛♥❞ t❤❡ ✉♥✐♦♥ ♦❢ t✇♦ ✜♥✐t❛r② s✉❜s❡ts ✐s ✜♥✐t❛r②✳ ■♥ t❤❡ r❡✈❡rs❡ ❞✐r❡❝t✐♦♥✱ ✇❡ ❛r❡ •❡❢t t♦ ♣r♦✈❡ t❤❛t✱ ❢♦r ❛•• (ϕ, α, α) ∈ |(N l ⇒ A) ⇒ A ⇒ A|✱ s❡tt✐♥❣ N ′ = Case ⊥ A • {(ϕ,α, α)}✱ n ! ∩ N ′ ✐s ✜♥✐t❡❀ t❤✐s ✐s ✐♠♠❡❞✐❛t❡ ❜❡❝❛✉s❡ N ′ ✐s ✜♥✐t❡ ✭✐t ❤❛s ❛t ♠♦st ♦♥❡ ❡•❡♠❡♥t✮✳

❚❤❡ ❝♦✲❑•❡✐s•✐ ❝♦♥str✉❝t✐♦♥✳ ❙✐♥❝❡ t❤❡ str✉❝t✉r❡ ✇❡ ❤❛✈❡ •✉st ❞❡s❝r✐❜❡❞ ♣r♦✈✐❞❡s ❛ ❞❡♥♦t❛t✐♦♥❛• ♠♦❞❡• ♦❢ •✐♥❡❛r •♦❣✐❝✱ t❤❡ ❝♦✲❑•❡✐s•✐ ❝♦♥str✉❝t✐♦♥ ❣✐✈❡s r✐s❡ t♦ ❛ ❝❛rt❡s✐❛♥ ❝•♦s❡❞ ❝❛t❡❣♦r②✱ ✇❤✐❝❤ ✇❡ ❞❡♥♦t❡ ❜② Fin ! ✿ ♦❜•❡❝ts ❛r❡ ✜♥✐t❡♥❡ss s♣❛❝❡s✱ ✭❱❛r✮ Γ, x : A, ∆ ⊢ x : A ✭❯♥✐t✮ Γ ⊢ : ⊤ a ∈ CA ✭❈♦♥st✮ Γ ⊢ a : A Γ, x : A ⊢ s : B ✭❆❜s✮ Γ ⊢ λx s : A → B Γ ⊢ s : A → B Γ ⊢ t : A ✭❆♣♣✮ Γ ⊢ s t : B Γ ⊢ s : A Γ ⊢ t : B ✭P❛✐r✮

❆ r❡❝✉rs♦r ✐♥ Rel ! ✳ ❲❡ ♥♦✇ ✐♥tr♦❞✉❝❡ t❤❡ ✐♥t❡r♣r❡t❛t✐♦♥ ♦❢ r❡❝✉rs♦r ❛s t❤❡ ✜①♣♦✐♥t ♦❢ t❤❡ ♦♣❡r❛t♦r ✭✶✮✳ ❉❡✜♥✐t✐♦♥ ✷✳ ❋♦r ❛•• ✜♥✐t❡♥❡ss s♣❛❝❡ A✱ ✇❡ ❞❡✜♥❡

Step A = λX RecOp[A] λx N l λy N l ⇒A⇒A λz A Case A x λx ′A (y x ′ (X x ′ y z)) z


Noël Bernard

Yves Dumond

Reification of substitutions in the asynchronous π-calculus

Keywords: concurrency, process algebra, π-calculus, explicit substitutions

In this paper, we bring in a dialect of the π-calculus, namely the π S -calculus, which involves explicit substitutions. This mechanism has the property to handle substitutions in such a way that it avoids deep parsing of the terms concerned. Then, we show that the π S -calculus can faithfully simulate the π-calculus, thus putting in evidence the fact that terms of the latter can be interpreted more efficiently.

Introduction

Name substitution is a basic feature in the semantics of the λ-calculus and of many process calculi. For instance, let us pay attention to the following reduction rule which is part of the semantics of the π-calculus:

a(r).P a(v) -→ P{v/r}
Here, the name v is received on the channel a and it is then substituted for the free occurrences of the placeholder r in the term P. Therefore, this one must be parsed in order to perform this task. Moreover, if the process P is made of a set of processes running in parallel, e.g.:

P ≡ P 1 | . . . | P n
the substitutions should normally involve several communications, which are not considered in the usual semantics. Consequently, as it stands, this mechanism might appear fairly artificial. Thus, we investigate in this paper the reification of name substitution under the form of dedicated π-processes.

Explicit substitutions are well known in the λcalculus, starting from [START_REF] Abadi | Explicit substitutions[END_REF]. The question of adding a similar construct in the π-calculus has not been so widely studied. The first attempt has been the π ξcalculus of [START_REF] Ferrari | A π-calculus with explicit substitutions: the late semantics[END_REF]. A term in this calculus consists of a pair denoted ξ :: P of an environment ξ, that is a list of equalities between names, and a process P. A closer proposal to ours can be found in [START_REF] Hirschkoff | Handling substitutions explicitely in the πcalculus[END_REF][START_REF] Stehr | CINNI -A generic calculus of explicit substitutions and its application to λ-, σand π-calculi[END_REF], where processes are ordinary processes of the π-calculus with an additional construct P [s], where s is a substitution, i.e. a correspondence between names in P and values. Explicit fusions [START_REF] Gardner | Explicit fusions[END_REF] adopt a point of view very close to that in this paper: they present an equality x = y as a process in itself. The main difference is the use of structural equivalences such as symmetry and transitivity relations between equalities, which amount to neglect of the computational aspect of explicit substitutions. The Applied π-calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF][START_REF] Abadi | Just fast keying in the pi calculus[END_REF] also introduces processes {M/x} but unlike the present paper these processes act globally on a process P not taking into account the computational content of deep propagation of substitution inside P.

Syntax

The syntax of the π-calculus widely differs from one author to another. Our point of view about this calculus is strongly influenced by the Chemical Abstract Machine [START_REF] Berry | The chemical abstract machine[END_REF]. This leads us to choose an asynchronous version of the π-calculus [START_REF] Boudol | Asynchrony and the π-calculus (note)[END_REF][START_REF] Honda | On asynchronous communication semantics[END_REF] involving guarded sums as the reference dialect. In addition, we define explicit substitutions as a specific kind of process: Definition 1 (π S -calculus syntax). The following is an inductive definition of the syntax of the π S -calculus:

The π S -terms (also called π S -processes) have to fulfill the Barendregt's hygiene condition (Bhc) [START_REF] Barendregt | The Lambda Calculus: Its Syntax and Semantics[END_REF] which prohibits name capture: for any two occurrences of a given name, either both are free or both are bound in the same binding.

The set of the π S -terms is denoted Π S . Moreover, in the explicit substitution {{r ← v}}, the name r is called the repository while v is called the value.

With regard to the Bhc, it is important to point out the fact that such a property can only be managed globally. Therefore, in this paper we study the derivation of processes considered individually but with the proviso that they are embedded in a syntactical context under the form of a π S -process that complies with the Bhc.

Action of explicit substitutions

The outer names are names which, with regard to their location in a given π S -term, are potentially subject to the action of explicit substitutions.

Definition 2 (outer names). Let P and P ′ be two π Sterms. The set O(P) of outer names of P is defined by induction on P by the following list of equations:

-O(0) = ∅ -O({{r ← v}}) = ∅ -O(āb) = {a, b} -O(a(x).P) = {a} -O(P|P ′ ) = O(P) ∪ O(P ′ ) -O(S + S ′ ) = O(S ) ∪ O(S ′ ) -O((ν x)P) = O(P) -{x} -O([x = y]P) = O(P) ∪ {x, y} -O(D( v)) = {v 1 , . . . , v n } with v = (v 1 , . . . , v n )
Definition 3 (occurrences in outer name position). Let P be a π S -term. An occurrence x of an element of O(P) is said to be in outer name position if and only if x is not in the scope of an input prefix. We denote Oc(P) the set of occurrences which are in outer name position in P.

Remark 1. For any π S -term P, O(P) is finite. Moreover, the outer names of P can be found in one step starting from the root of the syntactical tree related to this term and consequently any deep parsing of P is not necessary. This appears as a direct consequence of the syntax chosen for π S -terms, in particular the fact that sums must be guarded. Now, we have to discriminate among the explicit substitutions, those which, due to their location in a given term, are in a position to act on outer names. These are called active explicit substitutions: Definition 4 (active explicit substitutions). Let P be a π S -term. We call active explicit substitutions of P the explicit substitutions embedded in P which are not in the scope of an input prefix.

Definition 5 (set of repositories). Let P be a π S -term. We denote ρ(P) the set of the repositories of the active explicit substitutions embedded in P.

The semantic rules below give the details of implementation of the effect of active explicit substitutions on outer names as a function of the morphology of the terms concerned. This specification involves a meta-operator denoted by "≻", the corresponding meta-transitions, which are obviously not performed in the π S -calculus, being all labeled by the symbol "τ k ".

- (a 1 ) {{r ← v}} ≻ r(x).P τ k -→ v(x).P r ∈ {a, b} (a 2 ) {{r ← v}} ≻ āb τ k -→ āb{v/r} {{r ← v}} ≻ P τ k -→ P ′ ∧ x r (a 3 ) {{r ← v}} ≻ (ν x)P τ k -→ (ν x)P ′ r ∈ w ∧ w ′ = w{v/r} (a 4 ) {{r ← v}} ≻ D( w) τ k -→ D( w ′ ) {{r ← v}} ≻ S 1 τ k -→ S ′ 1 ∧ r O(S 2 ) (a 5 ) {{r ← v}} ≻ S 1 + S 2 τ k -→ S ′ 1 + S 2 {{r ← v}} ≻ S 1 τ k -→ S ′ 1 ∧ {{r ← v}} ≻ S 2 τ k -→ S ′ 2 (a 6 ) {{r ← v}} ≻ S 1 + S 2 τ k -→ S ′ 1 + S ′ 2 {{r ← v}} ≻ P τ k -→ P ′ (a 7 ) {{r ← v}} ≻ [x = y]P τ k -→ [x = y]{v/r}P ′ r ∈ {x, y} ∧ r O(P) (a 8 ) {{r ← v}} ≻ [x = y]P τ k -→ [x = y]{v/r}P {{r ← v}} ≻ P τ k -→ P ′ (a 9 ) {{r ← v}} ≻ Q | P | R τ k -→ Q | P ′ | R
These rules deserve the following comments:

(a 1 ) The process P remains unchanged. (a 3 ) Because of the Bhc, the names r and x are supposed to be different. (a 5 ) This rule is written up to left-right symmetry. (a 6 ) Occurrences of the repository r are substituted both in S 1 and in S 2 . 2

Semantics

The operational semantics for the π S -calculus is given hereafter under the form of a list of conditional term rewriting rules. The rules b 1 , b 2 and b 3 are specific to the π S -calculus. The other rules have the form which they take in usual specifications of the semantics of the asynchronous π-calculus apart from the side conditions. Indeed, while giving the π-calculus a transition semantics, side conditions are associated to some rules with the goal of imposing α-conversions which avoid name capture. There is no need to take such precautions in the π S -calculus since the Bhc radically prevents this phenomenon:

{{r ← v}} ≻ P τ k -→ P ′ ∧ r v ∧ r ∈ O(P) (b 1 ) {{r ← v}} | P τs -→ {{r ← v}} | P ′ - (b 2 ) a(r).P a(v) -→ (ν r)({{r ← v}} | P) D( u) de f = P ∧ P α { v/ u} γ -→ P ′ (b 3 ) D( v) γ -→ P ′ - (b 4 ) āb āb -→ 0 P γ -→ P ′ (b 5 ) [a = a]P γ -→ P ′ S 1 γ -→ S ′ 1 (b 6 ) S 1 + S γ -→ S ′ 1 P γ -→ P ′ (b 7 ) P | Q γ -→ P ′ | Q P γ -→ P ′ ∧ x γ (b 8 ) (ν x)P γ -→ (ν x)P ′ P āb -→ P ′ ∧ Q a(b) -→ Q ′ (b 9 ) P | Q τ -→ P ′ | Q ′ P āx -→ P ′ ∧ a x (b 10 ) (ν x)P ā(x) -→ P ′ P ā(x) -→ P ′ ∧ Q a(x) -→ Q ′ (b 11 ) P | Q τ -→ (ν x)(P ′ | Q ′ )
These rules deserve the following comments: (b 1 ) This rule, which is written up to left-right symmetry, specifies the effect of an active explicit substitution on processes of another kind. No action is possible on explicit substitutions since they have no outer names. The corresponding transition, performed in the π S -calculus, is labeled by the special action τ s . The condition r v prevents infinite derivations of the form

{{r ← v}} | P τs -→ {{r ← v}} | P τs -→ .
. . Furthermore, this rule stresses the fact that explicit substitutions are permanent processes, i.e. they do not disappear, nor are modified, after an interaction with another process. (b 2 ) When the value v is received, the explicit substitution {{r ← v}} is created and this one runs in parallel with the process P. Both the new explicit substitution and the process P are in the scope of the restricted name r which was formerly a placeholder. (b 3 ) The Bhc must be preserved by constant unfolding. Hence, all the bound names of P are first replaced by fresh names, the corresponding process, denoted P α , being obviously not unique. Then, actual parameters are substituted for formal ones. Once the corresponding process P α { v/ u} has been built up, the transition γ can be performed. Proof. Consider a π S -term P. We reason by cases on the action γ performed by P, i.e. P γ -→ P ′ : -Case γ = āb and γ is not combined with a constant unfolding. The emitting process āb is replaced by 0 in P ′ and the status of the remaining names is unchanged.

-Case γ = ā(b) and γ is not combined with a constant unfolding. Again, the emitting process āb is replaced by 0 in P ′ . In addition, the concerned restriction statement (ν b) is removed from P. Therefore, b becomes free in P ′ but remains different from the bound names of P ′ . Moreover, the status of the other names of P ′ is unchanged.

-Case γ = a(v) and γ is not combined with a constant unfolding. Then, P encompasses a process of the form S ′ + a(r).Q + S ′′ . This one is turned into (ν r)({{r ← v}} | Q) in P ′ . Hence, the name r is a placeholder before the transition and becomes a restricted name after it. Therefore, it remains a bound name different from the other bound and free names of P ′ , including the incoming name v (because of the Bhc). Moreover, the status of the other names remaining in P ′ is unchanged.

-Case γ = τ, γ is not combined with a constant unfolding and the exchanged name is free. This case is a simple combination of the first and the third ones.

-Case γ = τ, γ is not combined with a constant unfolding and the exchanged name b is bound. The process P is subject to the following modifications:

• The emitting process āb is replaced by 0.

• The scope of the restricted name b is extended and no α-conversion is required since name capture is not possible in π S . • A new explicit substitution is created and a placeholder is turned into a restricted name.

Again, the status of all the names remaining in P ′ is not modified.

-Case γ = τ s and γ is not combined with a constant unfolding. The consequence of a τ s -action consists in substituting one or several occurrences of a given repository which stand in outer name position in P, by the corresponding value. This does not bring in any new name nor modifies the status of the names remaining in P ′ .

-Case γ is combined with a constant unfolding. The process P encompasses a constant invocation D( v) and a constant defining equation, i.e. D( u)

de f
= T, is associated to the process P. First, fresh names are substituted for all the bound names of T: this generates a term T α . By definition, all the names that occur free in T appear in u. Then, these ones are replaced in T α by the names of v, i.e. by names already present in P. Let us denote Q the process P in which the term T α { v/ u} has been substituted for D( v). Then, the names of v occur free in T α { v/ u} and they have in Q the status, i.e. bound or free, that they had in P. Moreover, the only names that have appeared in Qby the fact of the unfolding process of the constant D are the fresh names. The latter are bound in T α { v/ u}, and consequently in Q, and they differ, by construction, from all the other names of Q. Furthermore, the status of the latter, in particular that of the names of v, has not been modified by the constant unfolding. Thence, Q fulfills the Bhc. At this stage, the action γ can be performed, and we are led to consider one of the previous cases.

Reduction of π-terms in π S

From now on, we focus on derivations carried out in the π S -calculus under the assumption that they start from π-terms. This criterion characterizes a specific subset among the π S -terms. In particular, all the explicit substitutions present in these terms are active: this comes from the fact that they are the result of the application of the rule b 2 .

Definition 6 (π ′

S -calculus). We denote Π ′ S the set of π Sterms which can be obtained by derivation of π-terms and we call π ′ S the calculus made of Π ′ S outfitted with the semantic rules of π S .

The next definition characterizes terms on which rule b 3 can no longer be applied.

Definition 7 (enacted processes). Let P be a π ′ S -term which encompasses the following explicit substitutions {{r 1 ← v 1 }}, . . . , {{r n ← v n }}. The process P is said to be enacted if and only if O(P) ∩ ρ(P) = ∅.

Definition 8 (enactment phase). Let P be a π ′ S -term. Any (possibly empty) sequence of τ s -actions, due to the action of the explicit substitutions of P, which turns it into an enacted process P ′ is called an enactment phase. The corresponding derivation is denoted P ❀ P ′ . We define hereafter a property which is fulfilled by the set of explicit substitutions of π ′ S -terms provided the latter are reduced according to a given strategy. This property is subsequently used to establish the termination and the confluence of the enactment phase.

Definition 9 (disjunction property). Let P be a π ′ Sterm which encompasses the following explicit substitutions

{{r 1 ← v 1 }}, . . . , {{r n ← v n }}.

The term P is said to fulfill the disjunction property on repositories and values if and only if:

-all the repositories r i are distinct, -no value v i is equal to a repository r j . We denote D(P) the fact that P abides by this property.

Lemma 1. Let P be a π ′ S -term that derives from a πterm P 0 . Then, D(P) holds provided along the derivation that leads from P 0 to P, all the actions different from τ s have been performed by enacted processes.

Proof. Consider a π ′ S -term P that encompasses the list of explicit substitutions {{r 1 ← v 1 }}, . . . , {{r n ← v n }}. We reason by induction on the length of a derivation path that complies with the aforementioned constraints.

Base case : no explicit substitution is present in P 0 and consequently D(P 0 ) is verified.

Induction step : by induction hypothesis, D(P) holds. According to the semantics of the π ′ S -calculus, active explicit substitutions are permanent processes, i.e. they cannot disappear nor be modified. Therefore, the only transitions which are worth considering are those that generate a new explicit substitution: this expels the actions āv, ā(v) and τ s . The mechanism of constant unfolding does not generate new explicit substitutions, either. Hence, in the proof below, the two actions, i.e. a(v) and τ, are considered with the proviso that they are not combined with a constant unfolding. Thus, if we denote {{r ← v}} the explicit substitution which has appeared in P ′ , then for all explicit substitution {{r i ← v i }} of P, we have to prove that r r i , r v i , r v and r i v. We proceed by cases on the action γ performed by P, i.e. P γ -→ P ′ :

-Case γ = a(v):

• r r i . The repository r i either is a placeholder present in the original term P 0 or a fresh name that has appeared due to a constant unfolding. In both cases, because of the Bhc, r r i .

• r v i . We reason ad absurdum. Assume that for some i, r = v i . Then, P necessarily encompasses:

a process S ′ + a(r).Q + S ′′ , which becomes (ν r)({{r ← v}} | Q) in P ′ , an explicit substitution {{r i ← r}} which, by hypothesis, cannot be embedded in Q since in π ′ S -terms, all the explicit substitutions are active. Here, Q is the scope of the placeholder r and this name also occurs outside Q, namely in the explicit substitution {{r i ← r}}. This is clearly in contradiction with the Bhc.

• r v. Again, we reason ad absurdum. Assume that r = v. Then, P necessarily encompasses a process

S ′ + a(v).Q + S ′′ which becomes (ν v)({{v ← v}} | Q) in P ′ .
Here, the incoming name v appears in P as a placeholder and outside P in an emitting process of the form āv. This is in contradiction with the Bhc, to which the context encompassing P is supposed to comply.

• r i v. Here, we have to prove that the incoming name v cannot be equal to one of the repositories r i . Each of them either was a placeholder in the term P 0 or has appeared as a fresh name during a constant unfolding. In both cases, it could not occur anywhere else. So, it can be received by P only if it has been previously sent out by a process from which P derives, and subsequently sent back to P. Consider the explicit substitution {{r i ← v i }}: because of the disjunction property, r i i . Under this assumption, any action ār i or ā(r i ) is prohibited because the encompassing process is not enacted: the value v i must be substituted for r i before the emission. Therefore, the received value v cannot be equal to one of the repositories of P.

-Case γ = τ and the emitted name is free:

• r r i and r v i . We can reason in the same way as in case γ = a(v): the only difference is that the emitting process is embedded in P.

• r v. We reason ad absurdum. Assume that r = v. Then, P necessarily encompasses:

a process āv, a process S ′ + a(v).Q + S ′′ which becomes

(ν v)({{v ← v}} | Q) in P ′ .
Moreover, the emitting process āv is obviously not embedded in Q. Hence, the name v occurs in Q as a placeholder and outside Q in the emitting process, which is in contradiction with the Bhc.

• r i v. Again, we reason ad absurdum. Assume that for some i, r i = v. Then, P necessarily encompasses:

a process āv, a process S ′ + a(r).Q + S ′′ , which becomes (ν r)({{r ← v}} | Q) in P ′ , an active explicit substitution {{v ← v i }} which is not embedded in Q.

Since D(P)holds, we have v v i . Here, the contradiction comes from the fact that the action τ cannot be performed because P is not enacted: v i must be substituted for v in the process āv prior to this action. As a result, the repository v cannot be emitted and ergo cannot become the value of the newly created explicit substitution.

-Case γ = τ and the emitted name is bound, i.e. is a restricted name:

• r r i , r v i and r v. We can reason as we did in the previous case.

• r i v. We reason ad absurdum. Assume that for some i, r i = v. Then, P necessarily encompasses:

-a process (ν v)(R ′ | āv | R ′′ ), -a process S ′ + a(r).Q + S ′′ , which becomes (ν r)({{r ← v}} | Q) in P ′ , -an explicit substitution {{v ← v i }} which, be- cause of the Bhc, is necessarily embedded in R ′ or R ′′ and such that v v i .
Again, we can argue that the τ-action cannot be performed if P is not enacted: the name v i has to be substituted for v before the emission.

Remark 2. If the π ′ S -term P 0 has been derived up to P according to the hypotheses made in the terms of Lemma 1, then D(P) is verified whether P is enacted or not.

Lemma 2 (finiteness of enactment phase). Let P be a π ′

S -term such that D(P) holds. Then, any enactment phase of P is finite.

Proof. If P is enacted, then the enactment phase is empty. Now, assume that P is a non enacted π ′ Sprocess. The outer names which are affected during the enactment phase are the elements of the finite set E = O(P) ∩ ρ(P). By the fact of the disjunction property, each element of E can be subject to the action of one, and one only, explicit substitution. Once the substitution(s) has (have) been performed, the names(s) appearing at the corresponding location(s) cannot be modified anymore since no value is equal to a repository. Therefore, if nb-occ(x, P) denotes the number of occurrences of x in outer names position in P, we can argue that the integer value e∈E nb -occ(e, P) strictly decreases, up to zero, at each τ s -step.

Lemma 3 (confluence of enactment phase). Let P be a π ′ S -term such that D(P) holds. Then, the enactment phase of P has the property of confluence.

Proof. Obvious: due to the disjunction property, any occurrence of an element of the set E = O(P)∩ρ(P)is subject to the action of one, and one only, explicit substitution. Hence, any τ s -action is performed in total causal independency towards the other.

Simulation of π by π ′

S

We show in this section that any π-term can be derived, respectively in π and in π ′ S , in such a way that, at each step, the terms reached are closely related, thus putting in evidence a relation of simulation between the derivations they respectively belong to. This clearly shows the possibility to interpret π-terms in an efficient way, avoiding the parsing phases of terms made necessary by in-depth substitutions.

To begin with, we need to define the two calculi, one compared to the other:

• The Bhc is assumed to be implemented both in π and in π ′ S . • The only difference between the two syntaxes resides in the fact that in π ′ S , explicit substitutions do not exist.

• From a semantic point of view the relationship between the two calculi is specified hereafter. Thus, for what concerns the π-calculus:

-Substitutions are performed in-depth after each reception, so there is no need for a meta-operation handling them. Consequently, the rule b 1 must be removed and the input rule b 2 has to be written under its usual form:

a(r).P a(v) -→ P{v/r}
-All the other semantic rules, in particular b 3 which preserves the Bhc, are unchanged.

At this point, we introduce a notion that aims at defining a morphological relation between πand π ′ S -terms. The latter are characterized by the presence of explicit substitutions and of restriction statements (ν r i ) related to the repositories. Hence, these features have to be removed in order to make the comparisons possible between terms of the two calculi.

Definition 10 (concrete term). If P is a π ′

S -term, we denote P the π-term defined by the following set of axioms, where ≡ is the syntactic identity between terms:

-P | . . . | Q ≡ P | . . . | Q -a 1 (x 1 ).P 1 + . . . + a n (x n ).P n ≡ a 1 (x 1 ). P 1 + . . . + a n (x n ). P n -∃v, {{r ← v}} is a subprocess of P ⇒ (ν r)P ≡ P -∄v, {{r ← v}} is a subprocess of P ⇒ (ν r)P ≡ (ν r) P -({{r ← v}} | P) ≡ P -[x = y]P ≡ [x = y] P -āb ≡ āb -D( w) ≡ D( w) -0 ≡ 0
We bring in below the simulation relation considered in this paper, as well as some related notions: Definition 11 (name occurrence location). Let x be an occurrence of a name n in the π ′ S -term P. We call location of x and denote loc(x, P) the number of symbols preceding x in P, the names and the constant identifiers being counted as 1.

Definition 12 (֒→-transition). If P and Q are two π ′ Sterms and γ an action different from τ s , any derivation of the form P

γ -→ P ′ ❀ Q is denoted P γ ֒→ Q.
Corollary 1. Let P 0 be a π-term and consider the following derivation P 0

γ 0 ֒→ . . . γ n-1 ֒→ P n performed in π ′ S .
Then, for all i, P i is enacted and D(P i ) holds.

Proof. Obvious since the above derivation of P 0 is in conformity with the reduction strategy defined by the terms of Lemma 1.

Definition 13 (M-equivalence). Let P be a π-term and Q an enacted π ′ S -term such that D(Q) holds. Consider the list {{r 1 ← v 1 }}, . . . , {{r n ← v n }} of explicit substitutions encompassed by Q. Then, the terms P and Q are said to be M-equivalent if and only if:

M.1 P ≡ Q {v 1 /r 1 } . . . {v n /r n } M.2 (x ∈ Oc(P) ∧ x is an occurrence of n ⇒ ∃x ′ ∈ Oc(Q) s.t. : (x ′ is an occurrence of n ∧ loc(x, P) = loc(x ′ , Q ) ) )
and conversely

The M-equivalence is denoted ∼.

Definition 14 (σ-simulation). A relation ≍ is said to be a σ-simulation of π by π ′ S if for any derivation

∆ : P ≡ P 0 γ 0 -→ P 1 γ 1 -→ . . . γ n-1
-→ P n in π there exists a derivation ∆ ′ :

P ≡ Q 0 γ 0 ֒→ Q 1 γ 1 ֒→ . . . γ n-1 ֒→ Q n in π ′
S such that for all i,

P i ≍ Q i .
Remark 3. At first sight, one may be surprised that we consider a simulation relation between derivations and not between terms as it is usually done. In fact, by explicitly considering derivations of the process P as a whole, we deal with terms which encompass all the required explicit substitutions.

Proposition 2. The relation∼ is a σ-simulation of π by π ′ S .

Proof. We reason by induction on the length of a derivation path. Moreover, in the proof below, any expression of the form [ x = x] denotes a list of adjacent matching statements [

x 1 = x 1 ] . . . [x n = x n ].
Base case : The π-terms P, P 0 and Q 0 are identical, i.e. P ≡ P 0 ≡ Q 0 and the set of explicit substitutions encompassed by Q 0 is empty. Thence P 0 ∼ Q 0 .

Induction step : We reason by cases on the transition γ n undergone by the π-term P n , i.e. P n γn -→ P n+1 :

-Case γ n = āb and γ n is not combined with a constant unfolding. By induction hypothesis, P n ∼ Q n . Therefore, the processes P n and Q n are such that they both encompass an emitting process of the form [ x = x]āb, the location of the corresponding occurrences of a being respectively the same in P n and in Q n . Hence, there exists a π ′ S -term Q n+1 for which Q n āb -→ Q n+1 . Moreover, P n+1 and Q n+1 can be respectively deduced from P n and Q n by replacing the process [ x = x]āb by 0. By induction hypothesis, Q n is enacted and since no new explicit substitution has appeared in Q n+1 , this one is enacted too. Consequently, the π ′ S -term Q n+1 is such that Q n āb ֒→ Q n+1 . Furthermore, under the assumption that P n ≡ Q n {v 1 /r 1 } . . . {v n /r n }, if we respectively replace [ x = x]āb by 0 in P n and in Q n , the location of all the occurrences of the remaining names is either unchanged or shifted symmetrically in P n and in Q n . This is in particular true for:

• the occurrences of the different repositories r i and ergo

P n+1 ≡ Q n+1 {v 1 /r 1 } . . . {v n /r n },
• the occurrences in outer name position which remain identical, at any concerned location, respectively in P n+1 and Q n+1 .

In conclusion, M.1 and M.2 hold and thence P n+1 ∼ Q n+1 .

-Case γ n = ā(b) and γ n is not combined with a constant unfolding. Here, the reasoning is basically the same as that of the previous case. The only difference lies in the fact that in addition to the emitting process, a restriction statement (ν b) disappears from P n and Q n as well.

-Case γ n = a(v) and γ n is not combined with a constant unfolding. The process P n encompasses a process of the form [ y = y](S ′ + a(ρ i ).P i n + S ′′ ). By induction hypothesis, P n ∼ Q n and consequently Q n encompasses a process of the form [ y = y](T ′ + a(ρ i ).Q i n + T ′′ ) for which:

• Q i n is a π-term such that P i n ≡ Q i n {v 1 /r 1 } . . . {v n /r n },
• the location of the corresponding occurrences of a is the same in P n and in Q n , • S ′ ∼ T ′ and S ′′ ∼ T ′′ .

After the reception of the value v on the channel a, the two receiving processes are respectively replaced by:

• P i n {v/ρ i } in P n+1 , i.e. the substitution {v/ρ i } is per- formed in-depth in the process P i n , • (ν ρ i )({{ρ i ← v}} | Q i n )
in the immediate derivative of Q n here denoted Q, i.e. a new explicit substitution {{ρ i ← v}} is created that runs in parallel with the process Q i n , the whole being in the scope of the restricted name ρ i .

By induction hypothesis, D(Q n ) holds. Thence, after Lemma 1 D(Q) does too. Moreover, after Lemma 2 and Lemma 3 the enactment phase of Q is finite and confluent. Therefore, there exists a unique enacted π ′ S -term

Q n+1 for which Q ❀ Q n+1 and Q n a(v)
֒→ Q n+1 . From a morphological point of view, the processes Q and Q n+1 do not differ since the latter can be deduced from the former by a finite set of τ s -actions. In fact, Q is subject to the action of the previously existing explicit substitutions, i.e. {{r 1 ← v 1 }}, . . . , {{r n ← v n }} plus that of the new created one {{ρ i ← v}}. Consequently, at the end of the enactment phase, the process Q i n has been turned into a process

Q i n+1 such that P i n {v/ρ i } ≡ Q i n+1 {v 1 /r 1 } . . . {v n /r n }{v/ρ i }, which, by the fact that (ν ρ i )({{ρ i ← v}} | Q i n+1 ) ≡ Q i n+1 , leads to: P i n {v/ρ i } ≡ (ν ρ i )({{ρ i ← v}} | Q i n+1 ) {v 1 /r 1 } . . . {v n /r n }{v/ρ i }
By hypothesis, Q n is an enacted process and because of the scope definition of ρ i , occurrences of its own cannot be found outside Q i n . Hence, the enactment phase of Q only affects the process Q i n . From this, we deduce:

P n+1 ≡ Q n+1 {v 1 /r 1 } . . . {v n /r n }{v/ρ i } So, M.1 holds. From P i n {v/ρ i } ≡ Q i n+1 {v 1 /r 1 } . . . {v n /r n }{v/ρ i }and by the fact that Q i
n+1 is no longer subject to the action of any explicit substitution, we can deduce that for any concerned location, the occurrences of names in outer name position are identical in P i n {v/ρ i } and in Q i n+1 . Furthermore, the processes that appear in the following couples, i.e.

(S ′ , T ′ ), (S ′′ , T ′′ )and (P i n {v/ρ i }, Q i n+1 )being all respectively made of the same number of symbols, the location of the occurrences of outer names present in P n+1 and in Q n+1 outside P i n {v/ρ i } and Q i n+1 are either unchanged or shifted symmetrically. Therefore, M.2 holds.

Again, we can assert that P n+1 ∼ Q n+1 .

-Case γ n = τ and γ n is not combined with a constant unfolding. If the name subject to the communication is free, the present case is a simple combination of the cases γ n = āb and γ n = a(b). If the emitted name is bound, i.e. is a restricted name, the reasoning is globally similar, the only difference lying in the fact that a scope extrusion must be considered, the restriction statement (ν b) remaining in P n+1 and Q n+1 .

-Case γ n is combined with a constant unfolding. By induction hypothesis, P n and Q n respectively encompass, at the same location in P n and in Q n , an occurrence of the same process D( u). This assumes the existence of a constant defining equation D( w) de f = T . At this point, consider that:

• During the constant unfolding phase, we are free to assume that D( u) is replaced by the same term T α { u/ w} both in P n and in Q n . Remember that this term is obtained by respectively substituting fresh names for all the bound names of T and the names of u for those of w. Thus, the process Q n being enacted, neither D( u) nor T α { u/ w} is subject to the action of any explicit substitution. Now, if we denote P δ n and Q δ n the terms P n and Q n in which T α { u/ w} has been substituted at the same location for D( u), then under the assumption that P n ≡ Q n {v 1 /r 1 } . . . {v n /r n }, we can state that P δ n ≡ Q δ n {v 1 /r 1 } . . . {v n /r n }, i.e. that M.1 holds for P δ n and Q δ n . • As mentioned above, the same term T α { u/ w}is substituted for D( u) both in P n and in Q n . Therefore, the respective locations of the occurrences of outer names of P δ n and Q δ n appearing respectively outside T α { u/ w} are either unchanged or shifted symmetrically. Consequently, M.2 holds for P δ n and Q δ n . We can deduce from what precedes that the Mequivalence is preserved by any constant unfolding phase, i.e. P δ n ∼ Q δ n . Note that as constant unfolding is not an actual transition, P δ n and Q δ n are not, strictly speaking, P -derivatives. Nevertheless, D(Q δ n ) holds since Q δ n and Q n encompass the same set of explicit substitutions. Therefore, while considering the transition γ n starting from P δ n and Q δ n , the same reasonings as in the previous cases can be applied, which leads to P n+1 ∼ Q n+1 .

  (b 6 ), (b 7 ), (b 9 ), (b 11 ) These rules are written up to leftright symmetry. (b 10 ) The label ā(x) denotes the emission of the restricted name x on the channel a. Proposition 1. The Bhc property is preserved in the π S -calculus.