S Ghilezan

J Ivetić

P Lescanne

S Likavec

Resource control and intersection types: an intrinsic connection

Keywords:

In this paper we investigate the λ -calculus, a λ-calculus enriched with resource control. Explicit control of resources is enabled by the presence of erasure and duplication operators, which correspond to thinning and contraction rules in the type assignment system. We introduce directly the class of λ -terms and we provide a new treatment of substitution by its decomposition into atomic steps. We propose an intersection type assignment system for λ -calculus which makes a clear correspondence between three roles of variables and three kinds of intersection types. Finally, we provide the characterisation of strong normalisation in λ -calculus by means of an intersection type assignment system. This process uses typeability of normal forms, redex subject expansion and reducibility method.

Introduction

The notion of resource awareness and control has gained an important role both in theoretical and applicative domains: in logic and lambda calculus as well as in programming langugages and compiler design.The idea to control the use of formulae is present in Gentzen's structural rules ( [START_REF] Gentzen | Unterschungen über das logische Schliessen[END_REF]), whereas the idea to control the use of variables can be traced back to Church's λI-calculus (e.g. [START_REF] Barendregt | The Lambda Calculus: its Syntax and Semantics[END_REF]). The augmented ability to control the number and order of uses of operations and objects has a wide range of applications which enables, among others, compiler optimisations and memory management that prevents memory leaking (e.g. [START_REF] Walker | Substructural type systems[END_REF]).

In this paper, we investigate the control of resources in the λ-calculus. We propose the λ -calculus, a λ-calculus enriched with resource control operators. The explicit control of resources is enabled by the presence of erasure and duplication operators, which correspond to thinning and contraction rules in the type assignment system. Erasure is the operation that indicates that a variable is not present in the term anymore, whereas duplication indicates that a variable will have two occurrences in the term which receive specific names to preserve the "linearity" of the term. Indeed, in order to control all resources, in the spirit of the λI-calculus (see e.g. [START_REF] Barendregt | The Lambda Calculus: its Syntax and Semantics[END_REF]), void lambda abstractions are not acceptable, so in order to have λx.M well-formed the variable x has to occur in M. But if x is not used in the term M, one must perform an erasure by using the expression x ⊙ M. In this way, the term M does not contain the variable x, but the term x ⊙ M does. Similarly, a variable should not occur twice. If nevertheless, we want to have two positions for the same variable, we have to duplicate it explicitly, using fresh names. This is done by using the operator x < x 1

x 2 M, called duplication which creates two fresh variables x 1 and x 2 .

Outline of the paper We first introduce the syntax and reduction rules of the λ -calculus (Section 1). We then introduce intersection types into the λ -calculus (Section 2). Finally, by means of intersection types, we completely caracterise strong normalisation in λ (Section 3).

Section 1 We first introduce the syntax and reduction rules of the λ -calculus. Explicit control of erasure and duplication leads to decomposition of reduction steps into more atomic steps, thus revealing the details of computation which are usually left implicit. Since erasing and duplicating of (sub)terms essentially changes the structure of a program, it is important to see how this mechanism really works and to be able to control this part of computation. We chose a direct approach to term calculi rather than taking a more common path through linear logic [START_REF] Abramsky | Computational interpretations of linear logic[END_REF][START_REF] Benton | A term calculus for intuitionistic linear logic[END_REF].

Although the design of our calculus has been motivated by theoretical con-siderations, it may have practical implications as well. Indeed, for instance in the description of compilers by rules with binders [START_REF] Rose | CRSX -Combinatory Reduction Systems with Extensions[END_REF][START_REF] Rose | Implementation Tricks That Make CRSX Tick[END_REF], the implementation of substitutions of linear variables by inlining 1 is simple and efficient when substitution of duplicated variables requires the cumbersome and time consuming mechanism of pointers and it is therefore important to tightly control duplication. On the other hand, a precise control of erasing does not require a garbage collector and prevents memory leaking.

Section 2 Intersection types were introduced in [START_REF] Coppo | A new type-assignment for lambda terms[END_REF][START_REF] Coppo | An extension of the basic functionality theory for the λ-calculus[END_REF][START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF][START_REF] Sallé | Une extension de la théorie des types en lambda-calcul[END_REF] to overcome the limitations of the simple type discipline in which the only forming operator is an arrow →. The newly obtained intersection type assignment systems enable a complete characterisation of termination of term calculi [START_REF] Van Bakel | Complete restrictions of the intersection type discipline[END_REF][START_REF] Gallier | Typing untyped λ-terms, or reducibility strikes again![END_REF][START_REF] Ghilezan | Strong normalization and typability with intersection types[END_REF]. Later on, intersection types became a powerful tool for characterising strong normalisation in different calculi [START_REF] Dougherty | Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage[END_REF][START_REF] Kikuchi | Simple proofs of characterizing strong normalisation for explicit substitution calculi[END_REF][START_REF] Matthes | Characterizing strongly normalizing terms of a calculus with generalized applications via intersection types[END_REF][START_REF] Neergaard | Theoretical pearls: A bargain for intersection types: a simple strong normalization proof[END_REF].

We propose an intersection type assignment system λ ∩ that integrates intersection into logical rules, thus preserving syntax-directedness of the system. We assign a restricted form of intersection types to terms, namely strict types, therefore minimizing the need for pre-order on types.

Intersection types in the presence of resource control operators were firstly introduced in [START_REF] Silvia Ghilezan | Intersection types for the resource control lambda calculi[END_REF], where two systems with idempotent intersection were proposed. Later, non-idempotent intersection types for contraction and weakening are treated in [START_REF] Bernadet | Non-idempotent intersection types and strong normalisation[END_REF]. In this paper, we treat a general form of intersection without any assumptions about idempotence. As a consequence, our intersection type system can be considered both as idempotent or as non-idempotent, both options having their benefits depending on the motivation.

Intersection types fit naturally with resource control. Indeed, the control allows us to consider three roles of variables: variables as placeholders (the traditional view of λ-calculus), variables to be duplicated and variables to be erased because they are irrelevant. For each kind of a variable, there is a kind of type associated to it, namely a strict type for a placeholder, an intersection type for a variable to-be-duplicated, and a specific type ⊤ for an erased variable.

Section 3 By the means of the introduced intersection type assignment system λ ∩, we manage to completely characterise strong normalisation in λ , i.e. we prove that terms in the λ -calculus enjoy strong normalisation if and only if they are typeable in λ ∩. First, we prove that all strongly normalising terms are typeable in the λ -calculus by using typeability of normal forms and redex subject expansion. We then prove that terms typeable in λ -calculus are strongly normalising by adapting the reducibility method for explicit resource control operators.

Main contributions

The main contributions of this paper are: (i) an improved presentation of resource control lambda calculus syntax with a direct definition of the syntax of resource control terms. Other presentations define first an unconstrainted syntax of terms with duplication and erasure which is later restricted to linear terms;

(ii) a new treatment of substitution and its decomposition into more atomic steps;

(iii) an intersection type assignment system for resource control lambda calculus which makes explicit the intrinsic correspondence between three kinds of variables and three kinds of intersection types;

(iv) a characterisation of strong normalisation in λ -calculus by means of an intersection type assignment system, by using typeability of normal forms, redex subject expansion and reducibility. The resource control lambda calculus, λ , is an extension of the λ-calculus with explicit erasure and duplication.

Syntax

Terms and lists, respectively sets, of free variables in λ are mutually recursively defined.

Definition 1.

(i) The set of λ -terms, denoted by Λ , is defined by inference rules given in Figure 1.

(ii) The list of free variables of a term M, denoted by Fv[M], is defined by inference rules given in Figure 2.

(iii) The set of free variables of a term M, denoted by Fv(M), is obtained from the list Fv[M] by unordering.

x ∈ Λ (var)

M ∈ Λ x ∈ Fv(M) λx.M ∈ Λ (abs) M ∈ Λ N ∈ Λ Fv(M) ∩ Fv(N) = / 0 MN ∈ Λ (app) M ∈ Λ x / ∈ Fv(M) x ⊙ M ∈ Λ (era) M ∈ Λ x 1 , x 2 ∈ Fv(M) x 1 = x 2 x / ∈ Fv(M) \ {x 1 , x 2 } x < x 1 x 2 M ∈ Λ (dup)
Figure 1: Λ : the set of λ -terms A λ -term, ranged over by M, N, P, ..., M 1 , ..., can be a variable from an enumerable set Λ (ranged over by x, y, z, x 1 , . . .), an abstraction, an application, an x 2 M binds the variables x 1 and x 2 in M and introduces a free variable x. The erasure x ⊙ M introduces also a free variable x. In order to avoid parentheses, we let the scope of all binders extend to the right as much as possible.

Fv[x] = [x] Fv[M] = [x 1 , x 2 , ..., x m ] Fv[λx i .M] = [x 1 , x 2 , ...x i-1 , x i+1 , ..., x m ] Fv[M] = [x 1 , ..., x m ] Fv[N] = [y 1 , ..., y n ] Fv[MN] = [x 1 , ..., x m , y 1 , ..., y n ] Fv[M] = [x 1 , ..., x m ] Fv[x ⊙ M] = [x, x 1 , ..., x m ] Fv[M] = [x 1 , ..., x m ] Fv[x < x i x j M] = [x, x 1 , ...x i-1 , x i+1 , ......x j-1 , x j+1 , ..., x m ]
Informally, we say that a term is an expression in which every free variable occurs exactly once, and every binder binds (exactly one occurrence of) a free variable. Our notion of terms corresponds to the notion of linear terms in [START_REF] Kesner | Resource operators for lambda-calculus[END_REF]. In that sense, only linear expressions are in the focus of our investigation. In other words, a term is well-formed in λ if and only if bound variables appear actually in the term and variables occur at most once. This assumption is not a restriction, since every pure λ-term has a corresponding λ -term and vice versa, due to the embeddings given in Definition 2 and 3 and illustrated by Example 5.

Definition 2. The mapping [ ] rc : Λ → Λ is defined in the following way:

[x] rc = x [λx.t] rc = λx.[t] rc , x ∈ Fv(t) λx.x ⊙ [t] rc , x / ∈ Fv(t) [MN] rc = [t] rc [s] rc , Fv(t) ∩ Fv(s) = / 0 x < x 1 x 2 [t[x 1 /x]s[x 2 /x]] rc , x ∈ Fv(t) ∩ Fv(s)
Reciprocally, a λ -term has a corresponding λ-term.

Definition 3. The mapping [ ] : Λ → Λ is defined in the following way:

[x] = x [λx.M] = λx.[M] [M N] = [M] [N] [x < x 1 x 2 M] = [M] [x/x 1 ][x/x 2 ] [x ⊙ M] = [M] Proposition 4. (i) For each pure lambda term t ∈ Λ there is a term M ∈ Λ such that [t] rc = M. (ii) For each resource lambda term M ∈ Λ there is a term t ∈ Λ such that [M] = t.
Example 5. Pure λ-terms λx.y and λx.xx are not λ -terms, whereas

[λx.y] rc = λx.(x ⊙ y) and [λx.xx] rc = λx.x < x 1 x 2 (x 1 x 2 ) are both λ -terms. (var) y ∈ Λ x / ∈ Fv(y) (era) x ⊙ y ∈ Λ x ∈ Fv(x ⊙ y) (abs) λx.x ⊙ y ∈ Λ . . . x 1 x 2 ∈ Λ x / ∈ Fv(x 1 x 2 ) \ {x 1 , x 2 } x 1 , x 2 ∈ Fv(x 1 x 2 ) (dup) x < x 1 x 2 (x 1 x 2 ) ∈ Λ x ∈ Fv(x < x 1 x 2 (x 1 x 2 )) (abs) λx.x < x 1 x 2 (x 1 x 2 ) ∈ Λ
In the sequel, we use the following abbreviations:

• x 1 ⊙ ... x n ⊙ M is abbreviated to X ⊙ M, when X is the list [x 1 , x 2 , ..., x n ]; • x 1 < y 1 z 1 ... x n < y n z n M is abbreviated to X < Y Z M if X is the list [x 1 , x 2 , ..., x n ], Y is the list [y 1 , y 2 , ..., y n ] and Z is the list [z 1 , z 2 , ..., z n ].
Notice that X , Y and Z are lists of equal length. If n = 0, i.e. if X , Y and Z are the empty lists, then X ⊙ M = X < Y Z M = M. Note that later on due to the equivalence relation defined in Figure 7, in X ⊙ M we can take X to be the set

{x 1 , x 2 , ..., x n }.
In what follows we use Barendregt's convention [START_REF] Barendregt | The Lambda Calculus: its Syntax and Semantics[END_REF] for variables: in the same context a variable cannot be both free and bound. This applies to binders like λx.M which binds x in M and x < x 1

x 2 M which binds x 1 and x 2 in M.

Substitution

At this point, we chose to introduce a substitution operator to define substitution in Λ . Due to its interference with the linearity of terms and its slight difference with the standard substitution of the λ-calculus, the concept of substitution has to be carefully defined in the λ -calculus. For that reason, in Definition 6 we first make precise the syntax of λ , i.e. the language λ extended with a substitution operator, by providing mutually recursive definitions of λ -terms and lists (respectively sets) of free variables (see Figures 3 and4). Definition 6.

(i) The set of λ -terms, denoted by Λ , is defined by inference rules given in Figure 3.

(ii) The list of free variables of a λ -term M, denoted by Fv [M], is defined by inference rules given in Figure 4.

(iii) The set of free variables of a λ -term M, denoted by Fv (M), is obtained from the list Fv [M] by unordering.

Notice that the set Λ is a strict subset of the set Λ , Λ ⊂ Λ , and that N in M[N/x] is substitution free, therefore we can write both Fv (N) and Fv(N) for N in M[N/x]. Also, notice that if a term M is substitution free, then Fv (M) = Fv(M). Barendregt's convention applies to the substitution operator as well, where M[N/x] can be seen as a binder for x in M. Definition 7.

x ∈ Λ (var) ---→, is defined by the rules given in Figure 5. As usual, it is closed under α-equivalence and regular contexts. In the last row in Figure 5, terms N 1 and N 2 are obtained from the term N by renaming of its free variables, i.e. by substitution of all free variables of N by fresh variables, respectively.

M ∈ Λ x ∈ Fv (M) λx.M ∈ Λ (abs) M ∈ Λ N ∈ Λ Fv (M) ∩ Fv (N) = / 0 MN ∈ Λ (app) M ∈ Λ x / ∈ Fv (M) x ⊙ M ∈ Λ (era) M ∈ Λ x / ∈ Fv (M) \ {x 1 , x 2 } x 1 , x 2 ∈ Fv (M) x 1 = x 2 x < x 1 x 2 M ∈ Λ (dup) M ∈ Λ x ∈ Fv (M) N ∈ Λ Fv (M) \ {x} ∩ Fv(N) = / 0 M[N/x] ∈ Λ (sub) Figure 3: Λ : the set of λ -terms Fv [x] = [x] Fv [M] = [x 1 , x 2 , ..., x m ] Fv [λx i .M] = [x 1 , x 2 , ...x i-1 , x i+1 , ..., x m ] Fv [M] = [x 1 , ..., x m ] Fv [N] = [y 1 , ..., y n ] Fv [MN] = [x 1 , ..., x m , y 1 , ..., y n ] Fv [M] = [x 1 , ..., x m ] Fv [x ⊙ M] = [x, x 1 , ..., x m ] Fv [M] = [x 1 , ..., x m ] Fv [x < x i x j M] = [x, x 1 , ...x i-1 , x i+1 , ......x j-1 , x j+1 , ..., x m ] Fv [M] = [x 1 , ..., x m ] Fv[N] = [y 1 , ..., y n ] Fv [M[N/x i ]] = [x 1 , x 2 , ...x i-1 , x i+1 , ..., x m , y 1 , ..., y n ]
(ii) ----→ → is the reflexive, transitive closure of ---→.

x[N/x] ---→ N (λy.M)[N/x] ---→ λy.M[N/x], x = y (MP)[N/x] ---→ M[N/x]P, x ∈ Fv (M) (MP)[N/x] ---→ MP[N/x], x ∈ Fv (P) (y ⊙ M)[N/x] ---→ y ⊙ M[N/x], x = y (x ⊙ M)[N/x] ---→ Fv(N) ⊙ M (y < y 1 y 2 M)[N/x] ---→ y < y 1 y 2 M[N/x], x = y (x < x 1 x 2 M)[N/x] ---→ Fv[N] < Fv[N 1 ] Fv[N 2 ] M[N 1 /x 1 ][N 2 /x 2 ]
Figure 5: Evaluation of the substitution operator in the λ -calculus For a full understanding of the role of λ , we would like to stress two facts:

• ---→ is the operational definition of the substitution in Λ .

• ---→ is used with a higher priority than the reductions of λ given in Figure 6 (because it is used to define substitution in Λ ).

To summarise, we have added a new operator to the syntax of λ called substitution operator and denoted by [ / ], and defined the evaluation of the substitution operator, which brings us to λ -calculus.

We prove the following safety property.

Proposition 8.

(i) If Q ----→ → R and Q ∈ Λ , then R ∈ Λ . (ii) If Q ----→ → R then Fv (Q) = Fv (R).
Proof. These properties are preserved by context. Therefore we can restrict our proof to the case where Q is the instance of the left-hand side of a rule in Figure 5 and consider only one-step reduction ---→. We consider only two paradigmatic rules.

•

(M P)[N/x] ---→ M[N/x] P with x ∈ Fv (M).
-We know that x ∈ Fv (M). Then

(M P)[N/x] ∈ Λ means that M ∈ Λ , P ∈ Λ , Fv (M) ∩ Fv (P)= / 0, N ∈ Λ and (Fv (M) ∪ Fv (P)) \ {x} ∩ Fv(N) = / 0. On the other hand, M[N/x] P ∈ Λ means M ∈ Λ , N ∈ Λ , P ∈ Λ and Fv (M[N/x]) ∩ Fv (P) = / 0.
Since Fv (M) ∩ Fv (P)= / 0 and ((Fv (M)∪Fv (P))\{x})∩Fv(N) = / 0, this implies Fv (M[N/x])∩ Fv (P) = / 0, hence the condition on free variables for M[N/x] P is fulfilled.

-

Fv ((M P)[N/x]) = Fv (M P) \ {x} ∪ Fv(N) = (Fv (M) ∪ Fv (P)) \ {x} ∪ Fv(N) = (Fv (M) ∪ Fv(N)) \ {x} ∪ Fv (P) = Fv (M[N/x] P). • (x ⊙ M)[N/x] ---→ Fv(N) ⊙ M. -(x ⊙ M)[N/x] ∈ Λ means M ∈ Λ , x / ∈ Fv (M), N ∈ Λ and Fv (M) ∩ Fv(N) = / 0. On the other hand, Fv(N) ⊙ M ∈ Λ means M ∈ Λ and Fv(N) ∩ Fv (M) = / 0. -Fv ((x ⊙ M)[N/x]) = Fv (M) ∪ Fv(N) = y∈Fv(N) {y} ∪ Fv (M) = Fv (Fv(N) ⊙ M).
Figure 5 defines the evaluation of substitution in Λ . Indeed, the reduction ----→ → terminates (Proposition 10) and when it terminates it yields actually a term in Λ , i.e. there is no more substitution operator in the resulting term (Proposition 14). Therefore, there is no need for defining evaluation of M[N/x] in case of M ≡ Q[P/y], because Propositions 10 and 14 guarantee that Q[P/y] will be evaluated to some

Q ′ ∈ Λ , thus Q[P/y][N/x] ----→ → Q ′ [N/x] ----→ → Q ′′ , for some Q ′′ ∈ Λ .
In order to prove normalisation in Proposition 10, we introduce the following measure.

Definition 9. The measure || • || on λ -terms is defined as follows:

||x|| = 1 ||λx.M|| = ||M|| + 1 ||M N|| = ||M|| + ||N|| + 1 ||x ⊙ M|| = ||M|| + 1 ||x < y z M|| = ||M|| + 1 ||M[N/x]|| = ||M|| .
Proposition 10. The reduction ----→ → terminates.

Proof. The proof of the termination of the relation ----→ → is based on the measure || • || defined in Definition 9. We associate with each term M a multiset M ul(M) of natural numbers as follows:

M ul(x) = {{ }} M ul(λy.M) = M ul(M) M ul(M P) = M ul(M) ∪ M ul(P) M ul(x ⊙ M) = M ul(M) M ul(x < y z M) = M ul(M) M ul(M[N/x]) = {{||M|| }} ∪ M ul(M)
Notice that if a term P does not contain any substitution, then M ul(P) = {{ }}.

The multiset order is defined for instance in [START_REF] Baader | Term Rewriting and All That[END_REF] and is denoted by ≫. The rules in Figure 5 yield the following inequalities.

{{||x|| }} ≫ M ul(N) {{||M|| + 1}} ∪ M ul(M) ≫ {{||M|| }} ∪ M ul(M) {{||M|| + ||P|| + 1}} ∪ M ul(M) ∪ M ul(P) ≫ {{||M|| }} ∪ M ul(M) ∪ M ul(P) {{||M|| + ||P|| + 1}} ∪ M ul(M) ∪ M ul(P) ≫ {{||P|| }} ∪ M ul(M) ∪ M ul(P) {{||M|| + 1}} ∪ M ul(M) ≫ {{||M|| }} ∪ M ul(M) {{||M|| + 1}} ∪ M ul(M) ≫ M ul(M) {{||M|| + 1}} ∪ M ul(M) ≫ {{||M|| }} ∪ M ul(M) {{||M|| + 1}} ∪ M ul(M) ≫ {{||M|| , ||M|| }} ∪ M ul(M) ∪ M ul(M)
Two inequalities require discussion. The first comes from x[N/x] ---→ N and is satisfied because N is substitution free, therefore M ul(N) = {{ }}. The second comes from

(x < x 1 x 2 M)[N/x] ---→ Fv(N) < Fv(N 1 ) Fv(N 2 ) M[N 1 /x 1 ][N 2 /x 2 ] and is satisfied because ||x < x 1
x 2 M|| = ||M|| + 1 is larger than ||M|| and than any ||P|| for P subterm of M.

This shows that ----→ → is well-founded, hence that ----→ → terminates.

Proposition 11. The reduction ----→ → is confluent.

Proof. There is no superposition between the left-hand sides of the rules of Figure 5, therefore there is no critical pair. Hence, the rewrite system is locally confluent. According to Proposition 10 it terminates, hence it is confluent by Newman's Lemma [START_REF] Baader | Term Rewriting and All That[END_REF].

Definition 12 ( ---→ Normal forms). Starting from M and reducing by ----→ →,

the irreducible term we obtain is called the ---→-normal form of M and denoted by M ↓ .

Every λ -term has a unique normal form, the existence is guaranteed by Proposition 10, whereas the uniqueness is a consequence of confluence (Proposition 11).

Proposition 13. If Q ∈ Λ then Q[N/x] ↓ ∈ Λ .
Proof. Let us look at all the terms of the form Q[N/x] and their evaluation by the rules in Figure 5.

• Q is a variable. Due to rule (sub) in Figure 3, x ∈ Fv (Q), hence Q must be x.
Therefore, all the cases when Q is a variable are exhausted.

• Q is an abstraction, then one rule is enough.

• Q is an application MP, then either x ∈ Fv (M) or x ∈ Fv (P), hence the two rules exhaust this case.

• Q is an erasure y ⊙ M, then either y = x or y = x and the two cases are considered.

• Q is a duplication x < x 1 x 2 M, then again either y = x or y = x and the two cases are considered.

Proposition 14. If M ∈ Λ then M ↓ ∈ Λ .
Proof. By induction on the number of substitutions in M, Proposition 13 being the base case.

The substitution of n different variables in the same term is denoted by

M[N 1 /x 1 ]...[N n /x n ] ↓ .
These substitutions are actually performed in "parallel" since we prove that they commute in the following proposition.

Proposition 15. If M ∈ Λ and x i ∈ Fv(M) for i ∈ {1, ..., n}, n ≥ 1 with x i = x j for i = j, then M[N 1 /x 1 ]...[N n /x n ] ↓ = M[N p(1) /x p(1) ]...[N p(n) /x p(n) ] ↓ , where (p(1), ..., p(n)) is a permutation of (1, ..., n).
Proof. We prove the proposition by induction on the structure of M,

• For M = x 1 the statement holds since the only permutation is the identity, namely,

p(1) = 1, therefore x 1 [N 1 /x 1 ] ↓ = N 1 = x 1 [N p(1) /x p(1) ] ↓ .
• If M = λy.Q then this works by induction. Notice that y = x i , for i ∈ {1, ..., n}.

• If M = QR then we distinguish two cases:

some of {x 1 , ..., x n } belong to Fv(Q), whereas the others belong to Fv(R). Without loss of generality we can assume that for some k such that 1

≤ k < n, {x 1 , ..., x k } ∈ Fv(Q) and {x k+1 , ..., x n } ∈ Fv(R). Then (QR)[N 1 /x 1 ]...[N n /x n ] reduces to Q[N 1 /x 1 ]...[N k /x k ] ↓ R[N k+1 /x k+1 ]...[N n /
x n ] ↓ , and the result follows by two applications of induction hypothesis.

-If M = QR and {x 1 , ..., x n } all belong to either Fv(Q) or to Fv(R), the result follows by induction.

• If M = y ⊙ Q with y = x i for i ∈ {1, ..., n}, then the result follows by induction.

• If M = x j ⊙ Q then (x j ⊙ Q)[N 1 /x 1 ]...[N j /x j ]...[N n /x n ] reduces to Fv(N j ) ⊙ Q[N 1 /x 1 ]...[N j-1 /x j-1 ][N j+1 /x j+1 ]...[N n /x n ] ↓ .
On the other hand, given an arbitrary permutation p, let us call k the index such that p(k) = j. Then,

(x j ⊙Q)[N p(1) /x p(1) ]...[N p(k) /x p(k) ]...[N p(n) /x p(n) ] reduces to Fv(N p(k) )⊙Q[N p(1) /x p(1) ]...[N p(k)-1 /x p(k)-1 ][N p(k)+1 /x p(k)+1 ]...[N p(n) /x p(n) ] ↓ . Since N j = N p(k) then Fv(N j ) = Fv(N p(k)
) and the result follows by induction.

• If M = y < y 1 y 2 Q where y = x i for i ∈ {1, ..., n}, then the result follows by induction.

• If M = x j < x ′ j x ′′ j Q then (x j < x ′ j x ′′ j Q)[N 1 /x 1 ]...[N j /x j ]...[N n /x n ] reduces to Fv(N j ) < Fv(N ′ j ) Fv(N ′′ j ) Q[N 1 /x 1 ]...[N ′ j /x ′ j ][N ′′ j /x ′′ j ]...[N n /x n ] ≡ M 1 .
On the other hand, given an arbitrary permutation p, let us call k the index such that p(k) = j. We have that

(x p(k) < x ′ p(k) x ′′ p(k) Q)[N p(1) /x p(1) ]...[N p(k) /x p(k) ]...[N p(n) /x p(n) ] reduces to Fv(N k ) < Fv(N ′ k ) Fv(N ′′ k ) Q[N p(1) /x p(1) ]...[N ′ p(k) /x ′ p(k) ][N ′′ p(k) /x ′′ p(k) ]...[N p(n) /x p(n) ] ≡ M 2 . By induction hypothesis (recall that j = p(k)), Q[N 1 /x 1 ]...[N ′ j /x ′ j ][N ′′ j /x ′′ j ]...[N n /x n ] and Q[N p(1) /x p(1) ]...[N ′ p(k) /x ′ p(k) ][N ′′ p(k) /x ′′ p(k) ]...[N p(n) /x p(n) ] have the same normal forms, therefore M 1 ↓ = M 2 ↓ .
Finally, we can formally define substitution in Λ and simultaneous substitution in Λ via λ -normal forms.

Definition 16 (Substitution in Λ ). If M ∈ Λ and N ∈ Λ then M| | | [N// /x] | | | M[N/x] ↓ . Notice that M| | | [N// /x] | | | is well-defined, since M| | | [N// /x] | | | ∈ Λ ,
M| | | [N 1 // /x 1 , . . . , N p // /x p ] | | | = M| | | [N 1 // /x 1 ] | | |...| | | [N p // /x p ] | | |. provided that Fv(N i ) ∩ Fv(N j ) = / 0 for i = j.

Operational semantics

The operational semantics of λ is defined by a reduction relation →, given by the set of reduction rules in Figure 6. In the λ -calculus, one works modulo the structural equivalence ≡ λ , defined as the smallest equivalence that satisfies the axioms given in Figure 7 and is closed under α-conversion. The reduction relation → is closed under ≡ λ and contexts. Its reflexive, transitive closure will be denoted by → →. As usual, a term is a redex if it has the form of a term on the left-hand side of a rule in Figure 6, whereas its contractum is the term on the right-hand side of the same rule. The reduction rules are divided into four groups. The main computational step is β-reduction. The group of (γ) reductions perform propagation of duplications into the expression. Similarly, (ω) reductions extract erasures out of expressions. This discipline allows us to optimise the computation by delaying duplication of terms on the one hand, and by performing erasure of terms as soon as possible on the other. Finally, the rules in the (γω) group explain the interaction between the explicit resource operators that are of different nature. Notice that in the rule (γω 2 ) the substitution in Λ is actually a syntactic variable replacement, i.e., renaming. 2(β) • For all terms M and N such that M → N, if M ∈ Λ , then N ∈ Λ .

(λx.M)N → M| | | [N// /x] | | | (γ 1 ) x < x 1 x 2 (λy.M) → λy.x < x 1 x 2 M (γ 2 ) x < x 1 x 2 (MN) → (x < x 1 x 2 M)N, if x 1 , x 2 ∈ Fv(N) (γ 3 ) x < x 1 x 2 (MN) → M(x < x 1 x 2 N), if x 1 , x 2 ∈ Fv(M) (ω 1 ) λx.(y ⊙ M) → y ⊙ (λx.M), x = y (ω 2 ) (x ⊙ M)N → x ⊙ (MN) (ω 3 ) M(x ⊙ N) → x ⊙ (MN) (γω 1 ) x < x 1 x 2 (y ⊙ M) → y ⊙ (x < x 1 x 2 M), y = x 1 , x 2 (γω 2 ) x < x 1 x 2 (x 1 ⊙ M) → M| | | [x// /x 2 ] | | | Figure 6: Reduction rules (ε 1 ) x ⊙ (y ⊙ M) ≡ λ y ⊙ (x ⊙ M) (ε 2 ) x < x 1 x 2 M ≡ λ x < x 2 x 1 M (ε 3 ) x < y z (y < u v M) ≡ λ x < y u (y < z v M) (ε 4 ) x < x 1 x 2 (y < y 1 y 2 M) ≡ λ y < y 1 y 2 (x < x 1 x 2 M), x = y 1 , y 2 , y = x 1 , x 2
• For all terms M and N such that M → → N, if M ∈ Λ , then N ∈ Λ .

In particular, in the case of (β)-reduction if (λx.M)N ∈ Λ , then

M| | | [N// /x] | | | = M[N/x] ↓ ∈ Λ by Proposition 14.
No variable is lost during the computation, which is stated by the following proposition.

Proposition 19 (Preservation of free variables by

→ →). If M → → N then Fv(M) = Fv(N).
Proof. The proof is by case analysis on the reduction rules and uses Proposition 8 (ii).

First, let us observe the structure of the λ -normal forms, given by the following abstract syntax. As usually, a term is a normal for if it does not have any redex as subterm.

Definition 20 (Set of Normal Forms). The set N F of normals forms is generated by the following abstract syntax:

M n f ::= λx.M n f | λx.x ⊙ M n f | xM 1 n f . . . M n n f | x < x 1 x 2 M n f in the last case M n f ≡ P n f Q n f , x 1 ∈ Fv(P n f ), x 2 ∈ Fv(Q n f ) E n f ::= x ⊙ M n f | x ⊙ E n f
where n ≥ 0. It is necessary to distinguish normal forms E n f separately because the term λx.y⊙M n f is not a normal form, since λx.y⊙M n f → ω 1 y ⊙ λx.M n f . Also, in the last case the term x

< x 1 x 2 P n f Q n f , where x 1 ∈ Fv(P n f ), x 2 ∈ Fv(Q n f ) is not necessarily a normal form since P n f Q n f can be a redex, in turn M n f ≡ P n f Q n f
guarantees that the application is a normal form.

Next we define the set of strongly normalising terms S N .

Definition 21 (Strongly normalising terms). The set of strongly normalising terms

S N is defined as follows:

M ∈ N F M ∈ S N ∀N ∈ Λ . M → → N ⇒ N ∈ S N M ∈ S N Lemma 22
. Every term has one of the following forms, where n ≥ 0:

(Abs) λx.N, (AbsApp) (λx.N)PT 1 . . . T n (Var) xT 1 . . . T n (DupApp) (x < x 1 x 2 N)T 1 . . . T n (Era) x ⊙ N (EraApp) (x ⊙ N)PT 1 . . . T n
Proof. These terms are well-formed according to Definition 1 (we did not explicitly write the conditions, since we work with linear terms). The proof is by induction on the structure of the term M ∈ Λ .

• If M is a variable, this case is covered by Var for n = 0.

• If M is an abstraction λx.Q, then by induction Q has one of the given forms, hence λx.Q is covered by Abs.

• If M is an application then M is of the form M ≡ QP 1 . . . P n , for n ≥ 1 and Q is not an application. We proceed by subinduction on the structure of Q.

Accordingly, Q is one of the following:

-Q is a variable, then we have the case Var, with n ≥ 1;

-Q is an abstraction, then we have the case AbsApp;

-Q is an erasure, then we have the case EraApp;

-Q is a duplication, then we have the case DupApp, with n ≥ 1.

• If M is an erasure x ⊙ Q, then by induction Q has one of the given forms, hence x ⊙ Q is covered by Era. • If M is a duplication x < x 1 x 2 Q, then by induction Q has one of the given forms, hence x < x 1 x 2 Q is covered by DupApp for n = 0.
2 Intersection types for λ

In this section we introduce an intersection type assignment λ ∩ system which assigns strict types to λ -terms. Strict types were proposed in [START_REF] Van Bakel | Complete restrictions of the intersection type discipline[END_REF] and used in [START_REF] Espírito | Characterising strongly normalising intuitionistic terms[END_REF] for characterisation of strong normalisation in λ Gtz -calculus. The syntax of types is defined as follows:

Strict types σ :

:= p | α → σ Types α ::= ∩ n i σ i
where p ranges over a denumerable set of type atoms and

∩ n i σ i = σ 1 ∩ . . . ∩ σ n for n > 0 ⊤ for n = 0
⊤ being the neutral element for the intersection operator, i.e. σ ∩ ⊤ = σ. We denote types by α, β, γ..., strict types by σ, τ, υ... and the set of all types by Types. We assume that the intersection operator is commutative and associative. We also assume that intersection has priority over arrow. Hence, we will omit parenthesis in expressions like (∩ n i τ i ) → σ.

The type assignment system

Definition 23. (i) A basic type assignment (declaration) is an expression of the form x : α, where x is a term variable and α is a type.

(ii) Consider a finite set Dom(Γ) of variables. A basis is a function

Γ : Dom(Γ) → Types.
A basis extension of Γ is a function Γ, x : α : Dom(Γ) ∪ {x} → Types:

y → Γ(y) if y ∈ Dom(Γ) α if y = x
(iii) Given Γ and ∆ such that Dom(Γ) = Dom(∆), the bases intersection of Γ and ∆ is the function Γ ⊓ ∆ : Dom(Γ) → Types, such that:

Γ ⊓ ∆(x) = Γ(x) ∩ ∆(x). (iv) Γ ⊤ is the constant function Γ ⊤ : Dom(Γ) → {⊤}.
In what follows we assume that the bases intersection has priority over the basis extension, hence the parenthesis in Γ, (∆ 1 ⊓ . . . ⊓ ∆ n ) will be omitted. It is easy to show that Γ ⊤ ⊓ ∆ = ∆ for arbitrary bases Γ and ∆ that can be intersected, hence Γ ⊤ is the neutral element for the intersection of bases of domain Dom(Γ).

x : σ ⊢ x : σ (Ax) The type assignment system λ ∩ is given in Figure 8. It is syntax directed and the rules are context-splitting. The axiom (Ax) ensures that void λ-abstraction cannot be typed, i.e. in a typeable term each free variable appears at least once. The context-splitting rule (→ E ) ensures that in a typeable term each free variable appears not more than once.

Γ, x : α ⊢ M : σ Γ ⊢ λx.M : α → σ (→ I ) Γ ⊢ M : ∩ n i τ i → σ ∆ 0 ⊢ N : τ 0 . . . ∆ n ⊢ N : τ n Γ, ∆ ⊤ 0 ⊓ ∆ 1 ⊓ ... ⊓ ∆ n ⊢ MN : σ (→ E ) Γ, x : α, y : β ⊢ M : σ Γ, z : α ∩ β ⊢ z < x y M : σ (Cont) Γ ⊢ M : σ Γ, x : ⊤ ⊢ x ⊙ M : σ (T hin)
Assume that we implement these properties in the type system with (Ax), (→ E ) and (→ I ), then the combinators K = λxy.x and W -1 = λxy.xyy would not be typeable. This motivates and justifies the introduction of the operators of erasure and duplication and the corresponding typing rules (T hin) and (Cont), which further maintain the explicit control of resources and enable the typing of K and W -1 , namely of their corresponding λ -terms λxy.y ⊙ x and λxy.y < y 1 y 2 xy 1 y 2 , respectively. Let us mention that on the logical side, structural rules of thinning and contraction are present in Gentzen's original formulation of LJ, Intuitionistic Sequent Calculus, but not in NJ, Intuitionistic Natural Deduction [START_REF] Gentzen | Untersuchungen über das logische schließen[END_REF][START_REF] Gentzen | Unterschungen über das logische Schliessen[END_REF]. Here instead, the presence of the typing rules (T hin) and (Cont) completely maintains the explicit control of resources in λ .

In the proposed system, intersection types occur only in two inference rules. In the rule (Cont) the intersection type is created, this being the only place where this happens. This is justified because it corresponds to the duplication of a variable. In other words, the control of the duplication of variables entails the control of the introduction of intersections in building the type of the term in question. In the rule (→ E ), intersection appears on the right hand side of the turnstyle ⊢ which corresponds to the usage of the intersection type after it has been created by the rule (Cont) or by the rule (T hin) if n = 0.

The role of ∆ 0 in the rule (→ E ) should be emphasized. It is needed only when n = 0 to ensure that N has a type, i.e. that N is strongly normalising as would be seen below. Then, in the conclusion of the rule, the types of the free variables of N can be forgotten, hence all the free variables of N receive the type ⊤. All the free variables of the term must occur in the environment Γ (see Lemma 28), therefore useless variables occur with the type ⊤. When n > 0, ∆ 0 can be any of the other environments and the type of N the associated type. Since ∆ ⊤ is a neutral element for ⊓, when n > 0, ∆ ⊤ disappears in the conclusion of the rule. The case n = 0 resembles the rules (drop) and/or (K-cup) in [START_REF] Lengrand | Intersection types for explicit substitutions[END_REF] and was used to present the two cases, n = 0 and n = 0 in a uniform way. In the rule (T hin) the choice of the type of x is ⊤, since this corresponds to a variable which does not occur anywhere in M. The remaining rules, namely (Ax) and (→ I ) are traditional, i.e. they are the same as in the simply typed λ-calculus. Notice however that the type of the variable in (Ax) is a strict type.

Roles of the variables

In the syntax of λ , there are three kinds of variables according to the way they are introduced, namely as a placeholder (associated with the typing rule (Ax)), as the result of a duplication (associated with the typing rule (Cont)) or as the result of an erasure (associated with the typing rule (Thin)). Each kind of variable receives a specific type:

• variables as placeholders have a strict type,

• variables resulting from a duplication have an intersection type,

• variables resulting from an erasure have the type ⊤.

In order to emphasize the sensitivity of the system λ ∩ w.r.t. the role of a variable in a term, we provide the following examples in which variables change their role during the computation process. Our goal is to show that when the role of a variable changes, its type in the type derivation changes as well, so that the correspondence between particular roles and types is preserved.

Example 24. A variable as a "placeholder" becomes an "erased" variable: this is the case with the variable z in (λx.x ⊙ y)z, because

(λx.x ⊙ y)z → β (x ⊙ y)| | | [z// /x] | | | (x ⊙ y)[z/x] ↓ = z ⊙ y.
Since z : ⊤, y : σ ⊢ z ⊙ y : σ, we want to show that z : ⊤, y : σ ⊢ (λx.x ⊙ y)z : σ. Indeed:

(Ax)

y : σ ⊢ y : σ (Weak) x : ⊤, y : σ ⊢ x ⊙ y : σ (→ I ) y : σ ⊢ λx.x ⊙ y : ⊤ → σ (Ax) z : τ ⊢ z : τ (→ E ). z : ⊤, y : σ ⊢ (λx.x ⊙ y)z : σ
In the rule (→ E ), we have n = 0, ∆ 0 = z : τ and ∆ ⊤ 0 = z : ⊤. Thus, in the previous derivation, the variable z changed its type from a strict type to ⊤, in accordance with the change of its role in the bigger term.

Example 25. A variable as a "placeholder" becomes a "duplicated" variable: this is the case with the variable v in (λx.x < y z yz)v, because

(λx.x < y z yz)v → β (x < y z yz)| | | [v// /x] | | | (x < y z yz)[v/x] ↓ = = Fv[v] < Fv[v 1 ] Fv[v 2 ] (yz)[v 1 /y][v 2 /z] ↓ = v < v 1 v 2 v 1 v 2 . Since v : (τ → σ) ∩ τ ⊢ v < v 1 v 2 v 1 v 2 : σ, we want to show that v : (τ → σ) ∩ τ ⊢ (λx.x < y z yz)v : σ. Indeed: . . . (→ I ) ⊢ λx.x < y z yz : ((τ → σ) ∩ τ) → σ (Ax) v : τ ⊢ v : τ (Ax) v : τ → σ ⊢ v : τ → σ (→ E ). v : (τ → σ) ∩ τ ⊢ (λx.x < y z yz)v : σ
In the rule (→ E ), we have n = 2, therefore ∆ 0 ⊢ N : τ 0 can be one of the two existing typing judgements, for instance v : τ ⊢ v : τ. In this case ∆ ⊤ 0 disappears in the conclusion, because

∆ ⊤ 0 ⊓∆ 1 ⊓∆ 2 = v : ⊤⊓v : τ → σ⊓v : τ = v : ⊤∩(τ → σ)∩τ = v : (τ → σ)∩τ.
Again, we see that the type of the variable v changed from strict type to (intersection) type.

Example 26. A "duplicated" variable becomes an "erased" variable: this is the case with the variable z in (λx.x ⊙ y)(z < u v uv), because

(λx.x ⊙ y)(z < u v uv) → β (x ⊙ y)| | | [z < u v uv// /x] | | | (x ⊙ y)[z < u v uv/x] ↓ = = Fv(z < u v uv) ⊙ y = z ⊙ y.
Like in the previous examples, both z : ⊤, y : σ ⊢ z ⊙ y : σ and z : ⊤, y : σ ⊢ (λx.x ⊙ y)(z < u v uv) : σ can be shown.

Example 27. An "erased" variable becomes a "duplicated" variable: this is the case with the variable u in (λx.x < y z yz)(u ⊙ v), because

(λx.x < y z yz)(u ⊙ v) → β (x < y z yz)| | | [u ⊙ v// /x] | | | (x < y z yz)[u ⊙ v/x] ↓ = Fv[u ⊙ v] < Fv[u 1 ⊙v 1 ] Fv[u 2 ⊙v 2 ] (yz)[u 1 ⊙ v 1 /y][u 2 ⊙ v 2 /z] ↓ = u < u 1 u 2 v < v 1 v 2 (u 1 ⊙ v 1 )(u 2 ⊙ v 2 ).
The situation here is slightly different. Fresh variables u 1 and u 2 are obtained from u using the substitution in Λ . The variable u is introduced by thinning, so its type is ⊤. Substitution in Λ does not change the types, therefore both u 1 and u 2 have the type ⊤. Finally, u in the resulting term is obtained by contracting u 1 and u 2 , therefore its type is ⊤ ∩ ⊤ = ⊤. Thus we have an interesting situationthe role of the variable u changes from "to be erased" to "to be duplicated", but its type remains ⊤.

However, this paradox (if any) is only apparent, as well as the change of the role. Unlike the previous three examples, in which we obtained normal forms, in this case the computation can continue

: u < u 1 u 2 v < v 1 v 2 (u 1 ⊙ v 1 )(u 2 ⊙ v 2 ) → (ω 2 +ε 4 ) v < v 1 v 2 u < u 1 u 2 u 1 ⊙ v 1 (u 2 ⊙ v 2 ) → γω 2 v < v 1 v 2 v 1 ((u 2 ⊙ v 2 ))| | | [u// /u 2 ] | | | = v < v 1 v 2 v 1 (u ⊙ v 2 ).
So, we see that the actual role of the variable u in the obtained normal form, is "to be erased", as indicated by its type ⊤.

To conclude the analysis, we point out the following key points:

• The type assignment system λ ∩ is constructed in such way that the type of a variable always indicates its actual role in the term. Due to this, we claim that the system λ ∩ fits naturally to the resource control calculus λ .

• Switching between roles is not reversible: once a variable is meant to be erased, it cannot be turned back to some other role. Moreover, the information about its former role cannot be reconstructed from the type.

A note about idempotence and identity rule

Recall that the typing tree of a term is dictated by the syntax: → is introduced by (→ I ), ∩ is introduced by (Cont) and ⊤ is introduced by (T hin). In this context it would not pertain to remove an intersection by idempotence or identity rule. This is why they are not considered here.

Structural properties

Lemma 28 (Domain correspondence for λ ∩). Let Γ ⊢ M : σ be a typing judgment. Then x ∈ Dom(Γ) if and only if x ∈ Fv(M).

Proof. The rules of Figure 8 belong to three categories.

1. The rules that introduce a variable. These rules are (Ax), (Cont) and (T hin).

One sees that the variable is introduced in the environment if and only it is introduced in the term as a free variable.

2. The rules that remove variables. These rules are (→ I ) and (Cont). One sees that the variables are removed from the environment if and only if they are removed from the term as a free variable.

The rule that neither introduces nor removes a variable. This rule is (→ E ).

Notice that (Cont) introduces and removes variables.

The Generation Lemma makes somewhat more precise the Domain Correspondence Lemma.

Lemma 29 (Generation lemma for λ ∩).

(i) Γ ⊢ λx.M : τ iff there exist α and σ such that τ ≡ α → σ and Γ, x : α ⊢ M : σ.

(ii) Γ ⊢ MN : σ iff and there exist ∆ i and τ i , i ∈ {0, . . ., n} such that Γ ′ ⊢ M : ∩ n i τ i → σ and for all i ∈ {0, . . . , n}, ∆ i ⊢ N : τ i and

Γ = Γ ′ , ∆ ⊤ 0 ⊓ ∆ 1 ⊓ . . . ⊓ ∆ n . (iii) Γ ⊢ z < x y M : σ iff there exist Γ ′ , α, β such that Γ = Γ ′ , z : α ∩ β and Γ ′ , x : α, y : β ⊢ M : σ. (iv) Γ ⊢ x ⊙ M : σ iff Γ = Γ ′ , x : ⊤ and Γ ′ ⊢ M : σ.
Proof. The proof is straightforward since all the rules are syntax directed, and relies on Lemma 28.

In the sequel, we prove that the proposed system satisfies the following properties: Substitution lemma for λ ∩ (Proposition 35) and Subject reduction and equivalence (Proposition 36).

In order to prove the Substitution lemma we extend the type assignment system λ ∩ with a new rule for typing the substitution operator, thus obtaining an auxiliary system λ ∩ that assigns types to λ -terms.

Definition 30. (i) The type assignment system λ ∩ consists of rules from Fig-

ure 8 plus the following (Subst) rule:

Γ, x : ∩ n i τ i ⊢ M : σ ∆ 0 ⊢ N : τ 0 ... ∆ n ⊢ N : τ n Γ, ∆ ⊤ 0 ⊓ ∆ 1 ⊓ ... ⊓ ∆ n ⊢ M[N/x] : σ (Subst)
(ii) Typing judgements in the system λ ∩ are denoted by Γ ⊢ M : σ.

The system λ ∩ is also syntax-directed, and assigns strict types to λ -terms. Therefore, it represents a conservative extension of the system λ ∩, meaning that if Γ ⊢ M : σ and M ∈ Λ (i.e. M is substitution-free), then Γ ⊢ M : σ and the two derivations coincide.

It is easy to adapt Lemma 28 and Lemma 29 to prove the corresponding properties of the system λ ∩.

Lemma 31 (Domain correspondence for λ ∩). Let Γ ⊢ M : σ be a typing judgment. Then x ∈ Dom(Γ) if and only if x ∈ Fv (M).

The proof is the same as the proof of Lemma 28, having in mind the definition of Fv (M) and the fact that the rule (Subst) belongs to the category of rules that remove variables.

Lemma 32 (Generation lemma for λ ∩). (i) Γ ⊢ λx.M : τ iff there exist α and σ such that τ ≡ α → σ and Γ, x : α ⊢ M : σ.

(ii) Γ ⊢ MN : σ iff there exist ∆ i and τ i , i = 0, . . ., n such that Γ ′ ⊢ M :

∩ n i τ i → σ and for all i ∈ {0, . . ., n}, ∆ i ⊢ N : τ i and Γ = Γ ′ , ∆ ⊤ 0 ⊓ ∆ 1 ⊓ . . . ⊓ ∆ n . (iii) Γ ⊢ z < x y M : σ iff there exist Γ ′ , α, β such that Γ = Γ ′ , z : α ∩ β and Γ ′ , x : α, y : β ⊢ M : σ. (iv) Γ ⊢ x ⊙ M : σ iff Γ = Γ ′ , x : ⊤ and Γ ′ ⊢ M : σ. (v) Γ ⊢ M[N/
x] : σ iff there exist ∆ i and τ i , i = 0, . . ., n such that Γ ′ , x :

∩ n i τ i ⊢ M : σ and for all i ∈ {0, . . ., n}, ∆ i ⊢ N :

τ i and Γ = Γ ′ , ∆ ⊤ 0 ⊓ ∆ 1 ⊓ . . . ⊓ ∆ n .
Proof. The proof is straightforward since all the rules are syntax directed, and relies on Lemma 31.

To prove Lemma 34 we will need the definition of contexts.

Definition 33 (λ -Contexts).

C ::= [ ] | λx.C | MC | C M | x ⊙ C | x < x 1 x 2 C | C [N/x]
Lemma 34 (Type preservation under ----→ →).

(i) For all M, M ′ ∈ Λ , N ∈ Λ , if Γ ⊢ M[N/x] : σ and M[N/x] ----→ → M ′ , then Γ ⊢ M ′ : σ. (ii) For all M, M ′ ∈ Λ , N ∈ Λ , if Γ ⊢ C [M[N/x]] : σ and C [M[N/x]] ----→ → C [M ′ ], then Γ ⊢ C [M ′ ] : σ.
Proof. (i) The proof is by case analysis on ---→ (Figure 5). We consider only some representative rules. The other rules are routine and their proofs are analogous to the second rule we consider.

• Rule x[N/x] ---→ N. In this case n = 1 and Γ is empty. Recall that

∆ ⊤ ⊓ ∆ = ∆.
On one hand we have

x : τ ⊢ x : τ (Ax) ∆ ⊢ N : τ ∆ ⊢ N : τ ∆ ⊢ x[N/x] : τ (Subst)
and on the other hand we have ∆ ⊢ N : τ by assumption.

• Rule (MP)[N/x] ---→ M[N/x]P, x ∈ Fv (M). On one hand we have:

Γ, x : ∩ n i υ i ⊢ M : ∩ m i ρ i → σ Θ 0 ⊢ P : ρ 0 . . . Θ m ⊢ P : ρ m Γ, x : ∩ n i υ i , Θ ⊤ 0 ⊓ Θ 1 ⊓ ... ⊓ Θ m ⊢ M P : σ → E ∆ 0 ⊢ N : τ 0 ... ∆ n ⊢ N : τ n Γ, Θ ⊤ 0 ⊓ Θ 1 ⊓ ... ⊓ Θ m , ∆ ⊤ 0 ⊓ ∆ 1 ⊓ ... ⊓ ∆ n ⊢ (M P)[N/x] : σ (Subst)
One the other hand we have:

Γ, x : ∩ n i υ i ⊢ M : ∩ m i ρ i → σ ∆ 0 ⊢ N : τ 0 ... ∆ n ⊢ N : τ n Γ, ∆ ⊤ 0 ⊓ ∆ 1 ⊓ ... ⊓ ∆ n ⊢ M[N/x] : ∩ m i ρ i → σ (Subst) Θ 0 ⊢ P : ρ 0 . . . Θ m ⊢ P : ρ m Γ, Θ ⊤ 0 ⊓ Θ 1 ⊓ ... ⊓ Θ m , ∆ ⊤ 0 ⊓ ∆ 1 ⊓ ... ⊓ ∆ , n ⊢ M[N/x] P : σ (→ E ) • Rule (x ⊙ M)[N/x] ---→ Fv(N) ⊙ M.
In this case n = 0. On one hand we have:

Γ ⊢ M : σ (T hin) Γ, x : ⊤ ⊢ x ⊙ M ∆ 0 ⊢ N : τ 0 (Subst) Γ, ∆ ⊤ 0 ⊢ (x ⊙ M)[N/x] : σ
On the other hand we have:

Γ ⊢ M : σ (T hin) . . . (T hin) Γ, ∆ ⊤ 0 ⊢ Fv(N) ⊙ M : σ • Rule (x < x 1 x 2 M)[N/x] ---→ Fv[N] < Fv[N 1 ] Fv[N 2 ] M[N 1 /x 1 ][N 2 /x 2 ]
. In order to make the proof tree readable, we adopt the following abbreviations:

τ 1 ∩ n 1 i τ 1,i τ 2 ∩ n 2 i τ 2,i ∆ 1 ∆ 1,1 ⊓ ... ⊓ ∆ 1,n 1 ∆ 2 ∆ 2,1 ⊓ ... ⊓ ∆ 2,n 2 L 1 ∆ 1,1 ⊢ N : τ 1,1 ... ∆ 1,n 1 ⊢ N : τ 1,n 1 L 2 ∆ 2,1 ⊢ N : τ 2,1 ...∆ 2,n 2 ⊢ N : τ 2,n 2
Since N 1 and N 2 are obtained from N only by renaming the free variables with fresh variables of the same type, for each derivation ∆ 1,i ⊢ N : τ 1,i where i ∈ {1, ..., n 1 } we have ∆ ′ 1,i ⊢ N 1 : τ 1,i , where ∆ 1,i and ∆ ′ 1,i differ only in variables names. Analogously, for each derivation ∆ 1, j ⊢ N : τ 1, j where i ∈ {1, ..., n 2 } we have ∆ ′′ 1, j ⊢ N 2 : τ 1, j , where ∆ 1, j and ∆ ′′ 1, j differ only in variables names. Now, we also adopt the following abbreviations:

∆ ′ 1 ∆ ′ 1,1 ⊓ ... ⊓ ∆ ′ 1,n 1 ∆ ′′ 2 ∆ ′′ 2,1 ⊓ ... ⊓ ∆ ′′ 2,n 2 L ′ 1 ∆ ′ 1,1 ⊢ N 1 : τ 1,1 ... ∆ ′ 1,n 1 ⊢ N 1 : τ 1,n 1 L ′′ 2 ∆ ′′ 2,1 ⊢ N 2 : τ 2,1 ...∆ ′′ 2,n 2 ⊢ N 2 : τ 2,n 2
Moreover, we do not consider the environment ∆ 0 since it is useless here. Now, on one hand we have:

Γ, x 1 : τ 1 , x 2 : τ 2 ⊢ M : σ (Cont) Γ, x : τ 1 ∩ τ 2 ⊢ x < x 1 x 2 M : σ L 1 L 2 (Subst) Γ, ∆ 1 ⊓ ∆ 2 ⊢ (x < x 1 x 2 M)[N/x] : σ
On the other hand we have

Γ, x 1 : τ 1 , x 2 : τ 2 ⊢ M : σ L ′ 1 (Subst) Γ, ∆ ′ 1 , x 2 : τ 2 ⊢ M[N 1 /x 1 ] : σ L ′′ 2 (Subst) Γ, ∆ ′ 1 , ∆ ′′ 2 ⊢ M[N 1 /x 1 ][N 2 /x 2 ] : σ (Cont) . . . (Cont) Γ, ∆ 1 ⊓ ∆ 2 ⊢ Fv[N] < Fv[N 1 ] Fv[N 2 ] M[N 1 /x 1 ][N 2 /x 2 ] : σ (ii) We will denote by Q ≡ C [M[N/x]] and Q ′ ≡ C [M ′ ]. If Q ----→ → Q ′ this means that M[N/x] ----→ → M ′ .
We prove the statement by induction on the structure of a context containing a redex. We provide the proof for the basic case C = [ ] and three additional cases C = λx.C ′ , C = x ⊙C ′ and C = C ′ [P/y], the proof being similar for the remaining context kinds.

• Case C = [ ]
. This is the first part of this lemma (i).

• Case C = λx.C ′ . Then Q = λx.C ′ [M[N/x]] and Q ′ = λx.C ′ [M ′ ]. By assump- tion Γ ⊢ Q : σ, i.e. Γ ⊢ λx.C ′ [M[N/x
]] : σ. Using Generation lemma for λ ∩ (Lemma 32(i)) we obtain that there exist α and τ such that σ = α → τ and Γ, x :

α ⊢ C ′ [M[N/x]] : τ. Since M[N/x] ----→ → M ′ by IH we have that Γ, x : α ⊢ C ′ [M ′ ] : τ. Using rule (→ I ) we can conclude that Γ ⊢ λ.C ′ [M ′ ] : α → τ = σ. • Case C = x ⊙ C ′ . Then Q = x ⊙ C ′ [M[N/x]] and Q ′ = x ⊙ C ′ [M ′ ]. By as- sumption Γ ⊢ Q : σ, i.e. Γ ⊢ x⊙C ′ [M[N/x]] : σ. Using Generation lemma for λ ∩ (Lemma 32(iv)) we obtain that Γ = Γ ′ , x : ⊤ and Γ ′ ⊢ C ′ [M[N/x]] : σ. Since M[N/x] ----→ → M ′ by IH we have that Γ ′ ⊢ C ′ [M ′ ] : σ. Using rule (T hin) we can conclude that Γ ⊢ x ⊙ C ′ [M ′ ] : σ. • Case C = C ′ [P/y]. Then Q = C ′ [P/y][M[N/x]] and Q ′ = C ′ [P/y][M ′ ]. By assumption Γ ⊢ Q : σ, i.e. Γ ⊢ C ′ [P/y][M[N/x]] : σ. Using Generation lemma for λ ∩ (Lemma 32(v)
) we obtain that there exist ∆ i and τ i , i = 0, . . ., n such that Γ ′ , y :

∩ n i τ i ⊢ C ′ [M[N/
x]] : σ and for all i ∈ {0, . . ., n},

∆ i ⊢ P : τ i and Γ = Γ ′ , ∆ ⊤ 0 ⊓ ∆ 1 ⊓ . . . ⊓ ∆ n . Since M[N/x] ----→ → M ′ by IH 29 we have that Γ ′ , y : ∩ n i τ i ⊢ C ′ [M ′ ] : σ. Using rule (Subst) we can conclude that Γ ⊢ C ′ [P/y][M ′ ] : σ. Lemma 35 (Substitution lemma for λ ∩). If Γ, x : ∩ n i τ i ⊢ M : σ and ∆ i ⊢ N : τ i , for all i ∈ {0, . . . , n}, then Γ, ∆ ⊤ 0 ⊓ ∆ 1 ⊓ ... ⊓ ∆ n ⊢ M| | | [N// /x] | | | : σ.
Proof. From assumptions Γ, x : ∩ n i τ i ⊢ M : σ and ∆ i ⊢ N : τ i , for all i ∈ {0, . . ., n}, we get that Γ, x : ∩ n i τ i ⊢ M : σ and for all i ∈ {0, . . ., n},

∆ i ⊢ N : τ i . Applying (Subst) rule we get Γ, ∆ ⊤ 0 ⊓ ∆ 1 ⊓ ... ⊓ ∆ n ⊢ M[N/
x] : σ. Now, using termination and confluence of ---→ reduction (Proposition 10 and Proposition 11) and preservation of type under the ---→ reduction (Lemma 34) we obtain that the

unique normal form M| | | [N// /x] | | | exists and that Γ, ∆ ⊤ 0 ⊓ ∆ 1 ⊓ ... ⊓ ∆ n ⊢ M| | | [N// /x] | | | : σ. Since M| | | [N// /x] | | | ∈ Λ (Proposition 14), having that λ ∩ is conservative extension of λ ∩, we finally get that Γ, ∆ ⊤ 0 ⊓ ∆ 1 ⊓ ... ⊓ ∆ n ⊢ M| | | [N// /x] | | | : σ.
Proposition 36 (Type preservation under reduction and equivalence in λ ∩). For every

λ -term M: if Γ ⊢ M : σ and M → → M ′ or M ≡ λ M ′ , then Γ ⊢ M ′ : σ.
Proof. The proof is done by case analysis on the applied reduction. Since the property is stable by context, we can without loss of generality assume that the reduction takes place at the outermost position of the term. Here we just show several cases. We will use GL as an abbreviation for Generation lemma (Lemma 29).

• Case (β): Let Γ ⊢ (λx.M)N : σ. We want to show that

Γ ⊢ M| | | [N// /x] | | | : σ.
From Γ ⊢ (λx.M)N : σ and from GL(ii) it follows that Γ = Γ ′ , ∆ ⊤ 0 ⊓∆ 1 ⊓. . .⊓ ∆ n , and that there is a type ∩ n i τ i such that for all i = 0, . . ., n, ∆ i ⊢ N : τ i , and Γ ′ ⊢ λx.M : ∩ n i τ i → σ. Further, by GL(i) we have that Γ ′ , x : ∩ n i τ i ⊢ M : σ. Now, all the assumptions of Substitution lemma 35 hold, yielding

Γ ′ , ∆ ⊤ 0 ⊓ ∆ 1 ⊓ . . . ⊓ ∆ n ⊢ M| | | [N// /x] | | | : σ which is exactly what we need, since Γ = ∆ ⊤ 0 ⊓ Γ ′ , ∆ 1 ⊓ . . . ⊓ ∆ n . • Case (γω 2 ): Let Γ ⊢ x < x 1 x 2 x 1 ⊙ M : σ. We are showing that Γ ⊢ M| | | [x// /x 2 ] | | | : σ. From the first sequent by GL(iii) we have that Γ = Γ ′ , x : α ∩ β and Γ ′ , x 1 : α, x 2 : β ⊢ x 1 ⊙ M : σ. Further, by GL(iv) we conclude that α ≡ ⊤, x : ⊤ ∩ β ≡ β and Γ ′ , x 2 : β ⊢ M : σ. Since β = ∩ n i τ i for some n ≥ 0, by applying Substitution lemma 35 to Γ ′ , x 2 : β ⊢ M : σ and x : τ i ⊢ x : τ i , i = 0, . . . , n we get Γ ⊢ M| | | [x// /x 2 ] | | | : σ.
• The other rules are easy since they do not essentially change the structure of the term.

Due to this property, equivalent (by ≡ λ ) terms have the same type.

3 Characterisation of strong normalisation in λ

3.1 SN ⇒ Typeability in λ ∩
We want to prove that if a λ -term is strongly normalising (SN), then it is typeable in the system λ ∩. We proceed in two steps:

1. we show that all λ -normal forms are typeable and 2. we prove the redex subject expansion.

Proposition 37. λ -normal forms are typeable in the system λ ∩.

Proof. By induction on the structure of M n f and E n f , given in Definition 20.

The basic case is a variable, namely xM 1 n f . . . M n n f , where n = 0. It is typeable by (Ax). Cases involving duplication and erasure operators are easy, because the associated type assignment rules (Cont) and (T hin) preserve the type of a term. If M n f = λx.x ⊙ N n f , then by the induction hypothesis Γ ⊢ N n f : σ, hence Γ, x : ⊤ ⊢ x ⊙ N n f : σ and Γ ⊢ λx.x ⊙ N n f : ⊤ → σ. Further, we discuss the case xM 1 n f . . . M n n f , where n ≥ 1. In this case, M 1 n f , . . . , M n n f are typeable by the induction hypothesis, say Γ i j ⊢ M i n f : σ i j , i ∈ {1, ..., n}, j ∈ {1, ..., m i }. Then, since x is a fresh variable, taking x :

∩ m 1 j σ 1 j → (∩ m 2 j σ 2 j → . . . (∩ m n j σ n j → τ) . . .) and apply- ing (→ E ) rule n times, we obtain Γ ⊢ xM 1 n f . . . M n n f : τ, where Γ = x : ∩ m 1 j σ 1 j → (∩ m 2 j σ 2 j → . . . (∩ m n j σ n j → τ) . . .), Γ 1⊤ 0 ⊓ Γ 1 1 ⊓ ... ⊓ Γ 1 m 1 , . . ., Γ n⊤ 0 ⊓ Γ n 1 ⊓ ... ⊓ Γ n m n . Lemma 38. For all M, M ′ ∈ Λ and N ∈ Λ , if Γ ⊢ M ′ : σ, M[N/x] ---→ M ′ , and N is typeable, then Γ ⊢ M[N/x] : σ.
Proof. The proof is by case analysis on the applied ---→ reduction. We consider only some interesting rules.

• Rule (x ⊙ M)[N/x] ---→ Fv(N) ⊙ M.
Let Fv(N) = {x 1 , ..., x m }. By assumption N is typeable, thus ∆ 0 ⊢ N : τ 0 for some ∆ 0 = {x 1 : τ 1 , ..., x m : τ m }. If Γ ⊢ Fv(N) ⊙ M : σ, then by applying m times the Generation Lemma 32(iv), we get Γ ′ ⊢ M : σ, where Γ = Γ ′ , ∆ ⊤ 0 . On the other hand

Γ ′ ⊢ M : σ (T hin) Γ ′ , x : ⊤ ⊢ x ⊙ M : σ ∆ 0 ⊢ N : τ 0 (Subst) Γ ′ , ∆ ⊤ 0 ⊢ (x ⊙ M)[N/
x] : σ. Notice that the rule (Subst) can be applied because ⊤ = ∩ n i τ i for n = 0.

• Rule (x < x 1 x 2 M)[N/x] ---→ Fv[N] < Fv[N 1 ] Fv[N 2 ] M[N 1 /x 1 ][N 2 /x 2 ]. Let Fv[N] = [
⊢ Fv[N] < Fv[N 1 ] Fv[N 2 ] M[N 1 /x 1 ][N 2 /x 2 ] : σ, by m applications of Lemma 32(iii), we obtain that Γ = Γ ′ , y 1 : τ 1 ∩ ρ 1 , ..., y m : τ m ∩ ρ m and that Γ ′ , ∆ ′ , ∆ ′′ ⊢ M[N 1 /x 1 ][N 2 /x 2 ] : σ, where ∆ ′ = {y ′ 1 : τ 1 , ...,
∆ ′ = ∆ ′ 0 ⊤ ⊓ ∆ ′ 1 ... ⊓ ∆ ′ n 1 , ∆ ′′ = ∆ ′′ 0 ⊤ ⊓ ∆ ′′ 1 ... ⊓ ∆ ′′ n 2 , where ∆ ′ i = {y ′ 1 : τ 1,i , ..., y ′ m : τ m,i } for i ∈ {0, ..., n 1 }, ∆ ′′ j = {y ′′ 1 : ρ 1, j , ..., y ′′ m : ρ m, j } for j ∈ {0, ..., n 2 }, ∆ ′ i ⊢ N 1 : ∩ m k τ k,i , ∆ ′′ j ⊢ N 2 : ∩ m k ρ k, j
, and finally Γ ′ , x 1 : ∩ n 1 i τ i , x 2 : ∩ n 2 j ρ j ⊢ M : σ (we used the following abbreviations: ∩ m k τ k,i ≡ τ i , ∩ m k ρ k, j ≡ ρ j ). Now, since N 1 and N 2 are obtained from N by renaming, for each derivation of the type of N 1 (respectively N 2 ) we can write an analogous derivation of the type of N, i.e. ∆ i ⊢ N : τ i for i ∈ {0, ..., n 1 } and ∆ j ⊢ N : ρ j for j ∈ {0, ..., n 2 }, where ∆ i differ from ∆ ′ i (and respectively ∆ j from ∆ ′′ j ) only by the domain (Dom(∆ i ) = Dom(∆ j ) = {y 1 , ..., y m }). If we adopt abbreviations L 1 for the array of the first n 1 derivations, and L 2 for the array of the latter n 2 derivations, we have:

Γ ′ , , x 1 : ∩ n 1 i τ i , x 2 : ∩ n 2 j ρ j ⊢ M : σ (Cont) Γ ′ , x : (∩ n 1 i τ i ) ∩ (∩ n 2 j ρ j ) ⊢ x < x 1 x 2 M : σ L 1 L 2 (Subst) Γ ⊢ (x < x 1 x 2 M)[N/x] : σ. The left hand side of the latter assignment holds because Γ ′ , ∆ ⊤ 0 ⊓ ∆ 1 ⊓ ... ⊓ ∆ n 1 +n 2 = Γ ′ , y 1 : ⊤∩(∩ n 1 i τ 1,i )∩(∩ n 2 j ρ 1, j ), ..., y m : ⊤∩(∩ n 1 i τ m,i )∩(∩ n 2 j ρ m, j ) = Γ ′ , y 1 : τ 1 ∩ ρ 1 , ..., y m : τ m ∩ ρ m = Γ.
Proposition 39 (Redex subject expansion). From Γ ⊢ M[N/x] : σ by Lemma 32(v) (Generation lemma) it follows that there exist ∆ i and τ i , i = 0, . . . , n such that Γ ′ , x : ∩ n i τ i ⊢ M : σ and for all i ∈ {0, . . ., n},

∆ i ⊢ N : τ i and Γ = Γ ′ , ∆ ⊤ 0 ⊓ ∆ 1 ⊓ . . . ⊓ ∆ n . Now: Γ ′ , x : ∩ n i τ i ⊢ M : σ (→ I ) Γ ′ ⊢ λx.M : ∩ n i τ i → σ ∆ 0 ⊢ N : τ 0 ... ∆ n ⊢ N : τ n (→ E ) Γ ⊢ (λx.M)N : σ Since M, N ∈ Λ we have that Γ ⊢ (λx.M)N : σ.
(ii) By case analysis according to the applied reduction, similar to the proof of Proposition 36.

Theorem 40 (SN ⇒ typeability). All strongly normalising λ -terms are typeable in the λ ∩ system.

Proof. The proof is by induction on the length of the longest reduction path out of a strongly normalising term M, with a subinduction on the structure of M.

• If M is a normal form, then M is typeable by Proposition 37. • Next, suppose that M itself is neither a redex nor a normal form. Then, according to Lemma 22, M has of one of the following forms:

• If M is a λ -redex, i.e. M → M ′ , then let M ′ be its contractum. M ′ is
λx.N (where N = y ⊙ P and y = x, since in this case M would be a redex and previous case would apply),

-xT 1 . . . T n , -x ⊙ N, -(λx.N)PT 1 . . . T n , -(x ⊙ N)PT 1 . . . T n , -(x < x 1 x 2 N)T 1 . . . T n ,
where N, P, T 1 , . . . , T n , are not all normal forms. We can classify these forms into the following two categories:

1) Terms with internal redexes: λx.N, xT 1 . . . T n , x⊙N and (x < x 1 x 2 N)T 1 . . . T n when duplication cannot be propagated further into N, i.e. N ≡ PQ, x 1 ∈ Fv(P), x 2 ∈ Fv(Q). In all these cases, we proceed by subinduction on the structure of M, since the length of the longest reduction path out of a subterm that contains a redex is equal to the length of the longest reduction path out of M.

2) Terms with a leftmost redex: (λx.N)PT 1 . . . T n , (x ⊙ N)PT 1 . . . T n and (x < x 1 x 2 N)T 1 . . . T n when duplication can be propagated further into N. In these cases, by applying the leftmost reduction, we obtain a term with smaller length of the longest reduction path, therefore we can proceed using induction.

In all the cases, after the application of induction (respectively subinduction) hypothesis in order to conclude typeability of subterms of M, it is easy to build the type of M. We will prove some illustrative cases from both categories, the rest being similar.

-M ≡ λx.N. Then, the only way to reduce M is to reduce N and the number of reductions in N is equal to the number of reductions in M. Since M is SN, N is also SN. Since N is a subterm of M, N is typeable by subinduction and λx.N is typeable by (→ I ).

-M ≡ xT 1 . . . T n . Then T 1 , . . . , T n must be SN by subinduction, hence typeable. Then we build the type for M by multiple application of the rule (→ E ), as in Proposition 37.

-M ≡ (x < x 1 x 2 PQ)T 1 . . . T n with x 1 ∈ Fv(P), x 2 ∈ Fv(Q). Again, each of P, Q, T 1 , . . . , T n must be SN by subinduction, hence typeable. We first use the rule (Cont) to type x < x 1

x 2 PQ and then we use the rule (→ E ), as in Proposition 37 to type M.

-M ≡ (λx.N)PT 1 . . . T n . Then M → M ′ where M ′ ≡ N| | | [P// /x] | | |T 1 . . . T n . M ′ is

Typeability ⇒ SN in λ ∩

In various type assignment systems, the reducibility method can be used to prove many reduction properties of typeable terms. It was first introduced by Tait [START_REF] Tait | Intensional interpretations of functionals of finite type I[END_REF] for proving the strong normalisation of simply typed λ-calculus, and developed further to prove strong normalisation of various calculi in [START_REF] Tait | A realizability interpretation of the theory of species[END_REF][START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse, et son application à l'elimination des coupures dans l'analyse et la théorie des types[END_REF][START_REF] Krivine | Lambda-calcul types et modèles[END_REF][START_REF] Ghilezan | Strong normalization and typability with intersection types[END_REF][START_REF] Ghilezan | Reducibility: A Ubiquitous Method in Lambda Calculus with Intersection Types[END_REF], confluence (the Church-Rosser property) of βη-reduction in [START_REF] Koletsos | Church-Rosser theorem for typed functionals[END_REF][START_REF] Statman | Logical relations and the typed λ-calculus[END_REF][START_REF] Mitchell | Type systems for programming languages[END_REF][START_REF] Mitchell | Foundation for Programmimg Languages[END_REF][START_REF] Ghilezan | Reducibility: A Ubiquitous Method in Lambda Calculus with Intersection Types[END_REF] and to characterise certain classes of λ-terms such as strongly normalising, normalising, head normalising, and weak head normalising terms (and their persistent versions) by their typeability in various intersection type systems in [START_REF] Gallier | Typing untyped λ-terms, or reducibility strikes again![END_REF][START_REF] Dezani-Ciancaglini | Compositional characterization of λ-terms using intersection types[END_REF][START_REF] Dezani-Ciancaglini | Two behavioural lambda models[END_REF][START_REF] Dezani-Ciancaglini | Behavioural Inverse Limit Models[END_REF].

The main idea of the reducibility method is to interpret types by suitable sets of lambda terms which satisfy some realisability properties and prove the soundness of type assignment with respect to these interpretations. A consequence of soundness is that every typeable term belongs to the interpretation of its type, hence satisfying a desired reduction property.

In the sequel, we adapt the reducibility method in order to prove that terms typeable in λ ∩ are strongly normalising.

Definition 41. For M , N ⊆ Λ , we define M / / N ⊆ Λ as M / / N = {M ∈ Λ | ∀N ∈ M MN ∈ N }.
(I2) [[α → σ]] = [[α]] / / [[σ]]; (I3) [[∩ n i σ i ]] = ∩ n i [[σ i ]] for n > 0 S N for n = 0.
Next, we introduce the notions of variable property, β-expansion property, ω-expansion property, γ-reduction property, thinning property and contraction property. The variable property and the β-expansion property correspond to the saturation property given in [START_REF] Barendregt | Lambda calculi with types[END_REF].

Definition 43.

• A set X ⊆ Λ satisfies the variable property, notation VAR(X ), if X contains all the terms of the form xM 1 . . . M n , where n ≥ 0 and M i ∈ S N , i = 1, . . ., n.

• A set X ⊆ Λ satisfies the β-expansion property, notation EXP β (X ) if M 1 ∈ S N . . . M n ∈ S N N ∈ S N M| | | [N// /x] | | |M 1 . . . M n ∈ X EXP β (X ) (λx.M) N M 1 . . . M n ∈ X . • A set X ⊆ Λ satisfies the ω-expansion property, notation EXP ω (X ) if M 1 ∈ S N . . . M n ∈ S N N ∈ S N x ⊙ (MN)M 1 . . . M n ∈ X EXP ω (X ) (x ⊙ M) N M 1 . . . M n ∈ X . • A set X ⊆ Λ satisfies the γ-reduction property, notation RED γ (X ) if M 1 ∈ S N . . . M n ∈ S N N ∈ S N x < x 1 x 2 (MN)M 1 . . . M n ∈ X RED γ (X ) (x < x 1 x 2 M) N M 1 . . . M n ∈ X . • A set X ⊆ Λ satisfies the thinning property, notation THIN(X ) if: M ∈ X THIN(X ) x ⊙ M ∈ X . • A set X ⊆ Λ satisfies the contraction property, notation CONT(X ) if: M ∈ X CONT(X ) x < y z M ∈ X . • RED γ (M ∩ N ). Suppose that x < x 1 x 2 (MN) ∈ M ∩ N . Since both M and N are -saturated RED γ (M ) and RED γ (N ) hold, hence (x < x 1 x 2 M)N ∈ M and (x < x 1 x 2 M)N ∈ M , i.e. (x < x 1 x 2 M)N ∈ M ∩ N . • THIN(M ∩N ). Let M ∈ M ∩N and x ∈ Fv(M). Then M ∈ M and M ∈ N .
Since both M and N are -saturated THIN(M ) and THIN(N ) hold, hence (iv) By induction on the construction of ϕ ∈ Types.

x ⊙ M ∈ M and x ⊙ M ∈ N , i.e. x ⊙ M ∈ M ∩ N . • CONT(M ∩ N ). Suppose that M ∈ M ∩ N , y = z, y, z ∈ Fv(M), x ∈ Fv(M) \
• If ϕ ≡ p, p a type atom, then [[ϕ]] = S N , so it is -saturated using (i).

• If ϕ ≡ α → σ, then [[ϕ]] = [[α]] / / [[σ]]. Since [[α]] and [[σ]
] are -saturated by assumption, we can use (ii).

• If ϕ ≡ ∩ n i σ i , then we distinguish two cases:

-for n > 0, [[ϕ]] = [[∩ n i σ i ]] = ∩ n i [[σ i ]
] and for all i = 1, . . . , n, [[σ i ]] are -saturated by assumption, so we can use (iii).

for n = 0, ϕ ≡ ∩ 0 i σ i , then [[ϕ]] = S N and we can use (i). Finally, we can give a characterisation of strong normalisation in λ -calculus.

We further define a valuation of terms [[-]]

Theorem 52. In λ -calculus, the term M is strongly normalising if and only if it is typeable in λ ∩.

Proof. Immediate consequence of Theorems 51 and 40.

Related work and conclusions

The idea to control the use of variables can be traced back to Church's λI-calculus [START_REF] Barendregt | The Lambda Calculus: its Syntax and Semantics[END_REF] and Klop's extension of λ-calculus [START_REF] Willem | Combinatory reduction systems[END_REF]. Currently, there are several different lines of research in resource aware term calculi.

Van Oostrom [54] and later Kesner and Lengrand [START_REF] Kesner | Resource operators for lambda-calculus[END_REF], applying ideas from linear logic [START_REF] Girard | Linear logic[END_REF], proposed to extend λ-calculus with explicit substitution [START_REF] Kesner | Resource operators for lambda-calculus[END_REF] with operators to control the use of variables (resources). Their linear λlxr-calculus is an extension of the λx-calculus [START_REF] Bloo | Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection[END_REF][START_REF] Rose | On explicit substitution with names[END_REF] with operators for linear substitution, erasure and duplication, preserving at the same time confluence and full composition of explicit substitutions. The simply typed version of this calculus corresponds to the intuitionistic fragment of linear logic proof-nets, according to Curry-Howard correspondence, and it enjoys strong normalisation and subject reduction. Generalising this approach, Kesner and Renaud [START_REF] Kesner | The prismoid of resources[END_REF][START_REF] Kesner | A prismoid framework for languages with resources[END_REF] developed the prismoid of resources, a system of eight calculi parametric over the explicit and implicit treatment of substitution, erasure and duplication.

On the other hand, process calculi and their relation to λ-calculus by Boudol [START_REF] Boudol | The lambda-calculus with multiplicities[END_REF] initialised investigations in resource aware non-deterministic λ-calculus with multiplicities and a generalised notion of application [START_REF] Boudol | A semantics for lambda calculi with resources[END_REF]. The theory was connected to linear logic via differential λ-calculus by Ehrhard and Regnier in [START_REF] Ehrhard | The differential lambda-calculus[END_REF] and typed with non-idempotent intersection types by Pagani and Ronchi Della Rocha in [START_REF] Pagani | Solvability in resource lambdacalculus[END_REF]. An account of this approach is given in [START_REF] Alves | Linearity: A roadmap[END_REF].

Resource control in sequent calculus corresponding to classical logic was proposed by Žunić in [START_REF] Žunić | Computing with sequents and diagrams in classical logic -calculi * X , d X and c X[END_REF]. Resource control in sequent λ-calculus was investigated in [START_REF] Ghilezan | Intuitionistic sequentstyle calculus with explicit structural rules[END_REF].

Intersection types in the presence of resource control were first introduced in [START_REF] Silvia Ghilezan | Intersection types for the resource control lambda calculi[END_REF]. Later on non-idempotent intersection types for λlxr-calculus were introduced by Bernadet and Lengrand in [START_REF] Bernadet | Non-idempotent intersection types and strong normalisation[END_REF]. Their proof of strong normalisation takes advantage of intersection types being non-idempotent.

Our contribution extends the work of [START_REF] Silvia Ghilezan | Intersection types for the resource control lambda calculi[END_REF], accordingly we follow the notation of [START_REF] Žunić | Computing with sequents and diagrams in classical logic -calculi * X , d X and c X[END_REF] and [START_REF] Silvia Ghilezan | Intersection types for the resource control lambda calculi[END_REF], along the lines of [54]. We have proposed an intersection type assignment system for the resource control lambda calculus λ , which gives a complete characterisation of strongly normalising terms of the λ -calculus. The proofs do not rely on any assumption about idempotence, hence they can be applied both to idempotent and non-idempotent intersection types.

This paper expands the range of the intersection type techniques and combines different methods in the strict type environment. It should be noticed that the strict control on the way variables are introduced determines the way terms are typed in a given environment. Basically, in a given environment no irrelevant intersection types are introduced. The flexibility on the choice of a type for a term, as it is used in rule (→ E ) in Figure 8, comes essentially from the choice one has in invoking the axiom.

The presented calculus is a good candidate to investigate the computational content of substructural logics [START_REF] Schroeder-Heister | Substructural Logics[END_REF] in natural deduction style and relation to substructural type systems [START_REF] Walker | Substructural type systems[END_REF]. The motivation for these logics comes from philosophy (Relevant Logics), linguistics (Lambek Calculus), computing (Linear Logic).

Since the basic idea of resource control is to explicitly handle structural rules, the control operators could be used to handle the absence of (some) structural rules in substructural logics such as thinning, weakening, contraction, commutativity, associativity. This would be an interesting direction for further research. Another direction involves the investigation of the use of intersection types, being a powerful means for building models of lambda calculus [START_REF] Barendregt | A filter lambda model and the completeness of type assignment[END_REF][START_REF] Dezani-Ciancaglini | Behavioural Inverse Limit Models[END_REF], in constructing models for substructural type systems. Finally, one may wonder how the strict control on the duplication and the erasure of variables influences the type reconstruction of terms [START_REF] Boudol | On type inference in the intersection type discipline[END_REF][START_REF] Kfoury | Principality and type inference for intersection types using expansion variables[END_REF].

Contents 1 Resource control lambda calculus λ 5 1 . 1 16 2 24 3 35 4work and conclusions 44 1

 11116243544 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.3 Operational semantics . . . . . . . . . . . . . . . . . . . . . . . . Intersection types for λ 19 2.1 The type assignment system . . . . . . . . . . . . . . . . . . . . 19 2.2 Structural properties . . . . . . . . . . . . . . . . . . . . . . . . . Characterisation of strong normalisation in λ 31 3.1 SN ⇒ Typeability in λ ∩ . . . . . . . . . . . . . . . . . . . . . 31 3.2 Typeability ⇒ SN in λ ∩ . . . . . . . . . . . . . . . . . . . . . Related Resource control lambda calculus λ

Figure 2 :

 2 Figure 2: List of free variables of a λ -term

Figure 4 :

 4 Figure 4: List of free variables of a λ -term

Figure 7 :

 7 Figure 7: Structural equivalence

Figure 8 :

 8 Figure 8: λ ∩: λ -calculus with intersection types

  (i) If Γ ⊢ M| | | [N// /x] | | | : σ and N is typeable, then Γ ⊢ (λx.M)N : σ. (ii) Let M be a λ -redex other than a β-redex and M → M ′ . If Γ ⊢ M ′ : σ, then Γ ⊢ M : σ. Proof. (i) From Γ ⊢ M| | | [N// /x] | | | : σ we have that Γ ⊢ M[N/x] : σ using Lemma 38 multiple times, since M| | | [N// /x] | | | = M[N/x] ↓ , i.e. M[N/x] ----→ → M| | | [N// /x] | | |.

Definition 42 .

 42 The type interpretation [[-]] : Types → 2 Λ is defined by: (I1) [[p]] = S N , where p is a type atom;

  {y, z}. Since both M and N are -saturated CONT(M ) and CONT(N ) hold, hence x < y z M ∈ M and x < y z M ∈ N , i.e. x < y z M ∈ M ∩N .

•

  ρ : Λ → Λ and the semantic satisfiability relation |= connecting the type interpretation with the term valuation. Definition 46. Let ρ : var → Λ be a valuation of term variables in Λ . For M ∈ Λ , with Fv(M) = {x 1 , . . ., x n } the term valuation [[-]] ρ : Λ → Λ is defined as follows: [[M]] ρ = M| | | [ρ(x 1 )// /x 1 , . . ., ρ(x n )// /x n ] | | | providing that x = y ⇒ Fv(ρ(x)) ∩ Fv(ρ(y)) = / 0.Notation: ρ(N/x) is the valuation defined as:ρ(N/x)(y) = ρ(y) and ρ(N/x)(x) = N for x = y. Lemma 47. (i) [[x]] ρ = ρ(x); The last rule applied is (Cont), i.e., Γ, x : α, y : β ⊢ M : σ Γ, z : α ∩ β ⊢ z < x y M : σ (Cont)By the IH Γ, x : α, y :β |= M : σ. Suppose that ρ |= Γ, z : α ∩ β.This means that ρ |= Γ and ρ |= z : α ∩ β ⇔ ρ(z) ∈ [[α]] and ρ(z) ∈ [[β]].For the sake of simplicity let ρ(z) ≡ N. We define a new valuation ρ ′ such that ρ ′ = ρ(N 1 /x, N 2 /y), where N 1 and N 2 are obtained by renaming the free variables of N. Then ρ ′ |= Γ, x : α, y :β since x, y ∈ Dom(Γ), N 1 ∈ [[α]] and N 2 ∈ [[β]]. By the IH [[M]] ρ ′ = [[M]] ρ(N 1 /x,N 2 /y) ∈ [[σ]]. Using the contraction property CONT([[σ]]) and Lemma 47(v) we have that Fv(N) <Fv(N 1 ) Fv(N 2 ) [[M]] ρ(N 1 /x,N 2 /y) = [[z < x y M]] ρ ∈ [[σ]].Theorem 51 (S N for λ ∩). If Γ ⊢ M : σ, then M is strongly normalising, i.e. M ∈ S N . Proof. Suppose Γ ⊢ M : σ. By Proposition 50 Γ |= M : σ. According to Definition 48(iii), this means that (∀ρ) ρ |= Γ ⇒ ρ |= M : σ. We can choose a particular ρ 0 (x) = x for all x ∈ var. By Proposition 45(iv), [[σ]] is -saturated for each type σ, hence [[x]] ρ 0 = x ∈ [[σ]] (variable condition for n = 0). Therefore, ρ 0 |= Γ and we can conclude that [[M]] ρ 0 ∈ [[σ]]. On the other hand, M = [[M]] ρ 0 and [[σ]] ⊆ S N (Proposition 45), hence M ∈ S N .

  due to Proposition 14. Moreover, Proposition 15 allows us to give simply a meaning to simultaneous substitution.

Definition 17 (Simultaneous substitution in Λ ). Simultaneous substitution in Λ is defined as follows:

  y 1 , ..., y m ]. Then, since N 1 and N 2 are obtained from N by renaming the free variables, we have that Fv[N 1 ] = [y ′ 1 , ..., y ′ m ] and Fv[N 2 ] = [y ′′ 1 , ..., y ′′ m ]. From the assumption Γ

  y ′ m : τ m } and ∆ ′′ = {y ′′ 1 : ρ 1 , ..., y ′′ m : ρ m }. Now, by two applications of Lemma 32(v), we get that

  also strongly normalising, hence by IH it is typeable. Then M is typeable, by Proposition 39. Notice that, if M ≡ (λx.N)P → β N| | | [P// /x] | | | ≡ M ′ , then, by IH, P is typeable, since the length of the longest reduction path out of P is smaller than that of M.

  also SN, hence typeable by induction hypothesis, since the longest reduction path out of M ′ is smaller than the one out of M. This implies that N| | | [P// /x] | | |, T 1 , . . ., T n are also SN and hence typeable by sub induction. Then we build the type for M by multiple application of the rule (→ E ), as in Proposition 37. The cases M ≡ (x ⊙ N)PT 1 . . . T n and M ≡ (x < x 1x 2 N)T 1 . . . T n are analogous.

Inlining is the technique which consists in copying at compile time the text of a function instead of implementing a call to that function.

We decided to use the same notation in order to introduce less different notations.

Acknowledgements: We would like to thank anonymous referees of a previous version of this paper for their careful reading and many valuable comments, which helped us to improve the paper. We would also like to thank Dragiša Žunić for participating in the earlier stages of the work. This work is partially supported by the Serbian Ministry of Science -project ON174026 and by a bilateral project between Serbia and France within the "Pavle Savić" framework.

Remark. In Definition 43 it is not necessary to explicitly write the conditions about free variables since we work with λ -terms.

Definition 44 ( -Saturated set). A set X ⊆ Λ is called -saturated, if X ⊆ S N and X satisfies the variable, β-expansion, ω-expansion, γ-reduction, thinning and contraction properties. (iii) If M and N are -saturated, then M ∩ N is -saturated.

(iv) For all types ϕ ∈ Types, [[ϕ]] is -saturated.

Proof. (i)

• S N ⊆ S N and VAR(S N ) trivially hold.

•

• RED γ (S N ). This is trivial, since by reducing a SN term we again obtain a SN term.

• THIN(S N ). Suppose that M ∈ S N and x ∈ Fv(M). Then trivially x ⊙ M ∈ S N , since no new redexes are formed.

• CONT(S N ). Suppose that M ∈ S N , y = z, y, z ∈ Fv(M), x ∈ Fv(M) \ {y, z}. We prove that x < y z M ∈ S N by induction on the structure of M.

-

The case of → γ 3 reduction when y, z ∈ Fv(P) is analogous.

Then the only possible reduction is inside the term N which is strongly normalising as a subterm of the strongly normalising term

From here we can deduce that M ∈ S N .

This holds since by assumption M ⊆ S N and N is -saturated, i.e. VAR(N ) holds.

holds and we have that for all P ∈ N , (λx.M)NM 1 . . .

Let M ∈ M / / N . We want to prove that x < y z M ∈ M / / N for y = z, y, z ∈ Fv(M) and x ∈ Fv(M). Let P be any term in M .

We have to prove that (x < y z M) P ∈ N . Since M ∈ M / / N , we know that M P ∈ N . By assumption N is -saturated so x < y z (M P) ∈ N . Using

• M ∩ N ⊆ S N is straightforward, since M , N ⊆ S N by assumption.

• VAR(M ∩ N ). Since VAR(M ) and VAR(N ) hold, we have that ∀M 1 , . . . ,

where N = ρ(z) and N 1 , N 2 are obtained from N by renaming its free variables.

Proof.

(ii) Without loss of generality, we can assume that Fv(M) = {x 1 , . . ., x i } and Fv(N) = {x i+1 , . . . ,

On the other hand, denoting by ρ ′ = ρ(N 1 /x, N 2 /y) we obtain Proof. By induction on the derivation of Γ ⊢ M : σ.

• The last rule applied is (Ax), i.e.

x : σ ⊢ x : σ (Ax)

We have to prove x :

]. This is trivial since according to Lemma 47(i)

• The last rule applied is (→ I ), i.e.

By the IH Γ, x : α |= M : σ (*). Suppose that ρ |= Γ and we want to show that ρ |= λx.M : α → σ. We have to show that

From (*) and (**) we conclude that ρ(N/x) |= M : σ, hence we can conclude that

• The last rule applied is (→ E ), i.e.

Let ρ be any valuation. Assuming that Γ ⊢ M :


Pierre Masci
email: pierre.masci@sophia.inria.fr

Olivier Bernard
email: olivier.bernard@sophia.inria.fr

Frédéric Grognard
email: frederic.grognard@sophia.inria.fr

Continuous Selection of the Fastest Growing Species in the Chemostat

Keywords: chemostat, competition, microorganisms, control

This paper proposes closed loop controls for microorganisms in the chemostat, which make it possible to select species with fastest growth rate in chosen environmental conditions. In particular, by controlling the dilution rate and the input substrate concentration, it is possible to select a species which maximizes a criterion. In a first step a control is proposed for Monod's and Droop's models in order to regulate the total biomass concentration. We show that this causes the selection of the fastest growing species if the system has a periodic behavior. Then we propose a way of achieving periodic stresses, and of selecting the species with maximal potential growth rate. Finally, the method is simulated using Droop's model for selecting a species which can both grow fast and increase its internal substrate storage.

INTRODUCTION

The chemostat is an open bioreactor where a microorganism can grow in suboptimal conditions of substrate limitation. The chemostat model supports several ecological theories (S.R. Hansen and S.P. Hubell [1980] -R. Arditi and H. Saiah [1992] -B.J.M. [START_REF] Bohannan | Linking genetic change to community evolution: insights from studies of bacteria and bacteriophage[END_REF]) that were then extrapolated and tested in real life. Among these theories, the competition theory is one of the most famous. It states that if n competing species are introduced in a chemostat, generically (in the adequate working modes) only one species will stay in the chemostat, while the n -1 other will disappear. This principle was validated with real experiments in S.R. Hansen and S.P. Hubell [1980] where the species that "wins" the competition could be predicted; it was the one that can grow at a constant rate (equal to the dilution rate as detailed further on) with the smallest amount of limiting nutrient s * . This theoretical result could be used to select among a blend of species, the ones of interest. This idea was first introduced by S.W. [START_REF] Brown | Isolation of ethanol-tolerant mutants of yeast by continuous selection[END_REF] and then by Juan [START_REF] Jimnez | Selection of ethanoltolerant yeast hybrids in pH-regulated continuous culture[END_REF], who have made chemostat experiments for selecting ethanoltolerant mutants. By adjusting a particular stress such as an inhibitor's concentration, a substrate limitation, or the dilution rate, it can lead to the isolation of species with optimal yield. This is of particular importance since it is a rather simple way of making a particular species emerge within a population. However, in most biotechnological applications, the selection criterion based on the idea of "optimal yield" is not appropriate. A selection that would e.g. select the microorganism with the highest growth potential would be preferable, especially if one wants to identify organisms that grow in hostile conditions. More generally, the objective of this paper is to propose new selection criteria. For this, the chemostat is not run in open loop, but a control law is proposed to run the system in closed loop. We show how the competition outcome is modified and we propose new criteria that could be used for species separation.

The paper is structured as follows. In a first part we recall two classical models of microorganisms in the chemostat, and the classical competition principle. In section 2 we study a first control law that puts the chemostat into a turbidostat mode, and we show that this control causes the selection of the fastest growing species if the system has a periodic behavior. Finally we propose a control to achieve periodic substrate stresses. In section 4 we maintain a periodical substrate limitation. A simulation example illustrates the benefit of the approach and shows how three species can be separated on this principle.

SHORT REVIEW OF COMPETITION ON A SINGLE SUBSTRATE IN THE CHEMOSTAT

Basic model for microorganisms growing in the chemostat

Monod's model (1) is the basic model for describing microorganisms' growth on a single substrate in a chemostat.

     ṡ = D(s in -s) - N i=1 1 y i µ i (s)x i ẋi = (µ i (s) -D)x i (1)
where s stands for the substrate concentration in the chemostat, s in its input concentration, and x i the ith species biomass concentration. The µ i functions represent the growth rates of these species, and the y i constants are their biomass/substrate conversion yields. D is the input/output dilution rate. The system can be controlled with s in and D.

In this model the growth rate functions µ i are taken as positive monotonic increasing functions

s a < s b ⇔ µ i (s a ) < µ i (s b ) (2)
They are bounded by their supremum values µ mi : µ i (s) < µ mi and lim

s→+∞ µ i (s) = µ mi (3)

Variable yield model

Droop's model (4) is more complex but describes the internal substrate storage q of the microorganisms. It is more appropriate to describe microalgae's growth.

         ṡ = D(s in -s) - N i=1 ρ i (s)x i qi = ρ i (s) -µ i (q i )q i ẋi = (µ i (q i ) -D)x i (4)
In this model the ρ i functions represent the substrate absorption rates, while the µ i functions represent the growth rates. These functions are positive monotonic increasing functions. They are bounded by the supremum values ρ mi and μi .

For each fixed substrate concentration s, the qi equation indicates that q i goes towards Q i (s), defined as the unique solution of

µ i (Q i (s))Q i (s) = ρ i (s) (5)
Indeed, the uniqueness of Q i (s) and its attractivity are straightforward since µ i (q i )q i is increasing in q i .

Let us define the maximum internal substrate storage

Q mi = lim s→+∞ Q i (s) (6) Q mi is thus the solution of µ i (Q mi )Q mi = ρ mi .
It defines an upper-bound for q i along the solutions of (4). Indeed, if q i = Q mi , then qi = ρ i (s) -ρ mi < 0, and if q i < Q mi is verified at the initial time, then it is always verified. The fact that there is a maximum internal substrate storage Q mi for each species is biologically relevant.

Corresponding to this maximum internal substrate storage, there exists a maximum growth rate µ mi for each species

µ mi = µ i (Q mi ) = ρ mi Q mi (7)

The Competitive Exclusion Principle (CEP)

Under constant controls D and s in , for some species, there exists a substrate concentration s i for which the growth rate µ i is (or becomes) equal to the dilution rate D :

µ i (s i ) = D in Monod's model µ i (Q i (s i )) = D in Droop's model (8)
If this substrate concentration does not exist for a given species, it means that µ i (s) < D ∀s (or µ i (Q i (s)) < D ∀s in Droop's model) and the species will be washed out of the chemostat.

If µ i (s in ) (or µ i (Q i (s in )) < D)
for a particular species, that species will also be washed out of the chemostat because we will have s(t) < s in after some finite time t 0 , and then

µ i (s(t)) or µ i (Q i (s(t))) < µ i (s in ) < D for all t > t 0
The CEP stipulates that in a chemostat with N species that satisfy (8) (so that they are not guaranteed to be washed out) , single substrate growth limitation, and constant controls D and s in , all but one of the species converge to 0 : Gouzé and G. Robledo [2005]). What we aim at doing here is to find controls which change the result of the competition keeping a single species. More precisely, we want to select species of interest who maximize a criterion other than the smallest s i , by imposing a periodic behaviour to the system.

If ∃n ∈ {1, 2, ..., N -1, N } so that s n < s i ∀i = n then lim t→+∞ x i (t) = 0 ∀i = n (9)
O. [START_REF] Bernard | The effects of a controlled fluctuating nutrient environment on continuous cultures of phytoplankton monitored by a computer[END_REF] have studied the effect of periodic substrate stresses, which is a realistic ecological situation. In section 4 we have determined controls which permit to reproduce such stresses, and in section 5.2 we have shown that this causes a new selection criterion other than Criterion 1.

SELECTING THE FASTEST GROWING SPECIES

Control of the total biomass concentration

For selecting such a species in the chemostat, we need to regulate the total biomass concentration X T = N i=1 x i so that the chemostat does not become saturated with microorganisms. We achieve this by controlling D so that

ẊT = D(X T -X T ) (10)
In both models this leads us to

N i=1 µ i (.)x i -DX T = D(X T -X T ) and D = N i=1 x i X T µ i (.) (11)
When X T is close to X T , D is the weighted mean of the growth rates µ i of the microorganisms.

It is also possible to regulate K T = N i=1 k i x i with k i coefficients who can represent turbidity coefficients. This is what is approximatively done in a particular family of chemostat, the turbidostat.

The fastest species excludes all others from the chemostat

For this study the growth functions in both models will be considered only time-dependent functions µ i (t), with T i -periodic behaviors. As we shall later see such periodic behaviors can be obtained by different means. We use the following notation for the mean growth of the species :

µ meani = 1 T i Ti 0 µ i (t)dt ( 12
)
Hypothesis 2. Let us assume that ∃n ∈ [1; N ] so that µ meann > µ meani ∀i = n Theorem 3. Selection for any periodic behavior With a bounded total biomass concentration X T = N i=1 x i , species n with biggest mean growth µ meani is selected : it excludes all other species from the chemostat.

Proof

We denote

d i = ln xn xi With ẋi = (µ i -D)x i we obtain ḋi (t) = ẋn(t) xn(t) -ẋi(t) xi(t) = µ n (t) -µ i (t)
and

d i (t) = d i (0) + t 0 ḋi (τ )dτ = d i (0) + t 0 µ n (τ )dτ - t 0 µ i (τ )dτ
We then use the following notations :

p i (t) = t -t ≡ T i T i r i (t) = t ≡ T i t = p i (t)T i + r i (t) (13)
where t ≡ T i represents tmoduloT i , and p i (t) is the number of T i -periods for species i until time t. which leads us to We have shown that it is possible to select a species with fastest growth in given environmental conditions. Here we try to determine conditions which will allow us to select the species with biggest µ mi . Criterion 4. µ mi Competitiveness Criterion With a bounded total biomass concentration X T = N i=1 x i , and with s big enough so that µ i (t) ≈ µ mi ∀t, the species with fastest growth µ mi is selected : it excludes all other species from the chemostat.

t 0 ḋi (τ )dτ = p n (t) Tn 0 µ n (τ )dτ -p i (t) Ti 0 µ i (τ )dτ + R n i (t) = p n (t)   Tn 0 µ n (τ )dτ - p i (t) p n (t) Ti 0 µ i (τ )dτ   + R n i (t) = p n (t) T n µ meann - p i (t) p n (t) T i µ meani + R n i (t) with notation R n i (t) = rn(t) 0 µ n (τ )dτ - ri(t) 0 µ i (τ )

Proof and effective realization

The demonstration of Criterion 4 is the same as for Theorem 3, with µ i (t) = µ mi .

2

In order to have µ i (t) ≈ µ mi , we regulate s at a large value s 0 (so that µ i (s 0 ) or

µ i (Q i (s 0 )) ≈ µ mi ) by imposing ṡ = D(s 0 -s) (14)
which is achieved through

s in = s 0 + 1 D N i=1 ρ i (s)x i
As N i=1 ρ i (s)x i is not always measurable, we have imagined a simpler way to realize µ i (Q i (s)) ≈ µ mi : with a big constant s in and a small X T we have ṡ ≈ D(s ins) and the substrate concentration will converge close to s in , which is chosen big enough to have µ i (s in ) ≈ µ mi (µ i (Q i (s in )) ≈ µ mi in Droop's model).

ACHIEVING PERIODIC SUBSTRATE STRESSES

We propose an approach for the generation of a periodic behavior in the case of Droop's model, under control D (11). It consists in approximating an ideal T-periodic behavior of interest. In the Droop model for instance, we have reproduced a situation of periodic substrate stresses, with the following T-periodic shape for ρ i (s) :

s(t) = s M for t ≡ T ≤ τ 0 for t ≡ T > τ (15)
with s M such that ρ i (s M ) ≈ ρ mi . The ratio τ /T is the proportion of time the microorganisms are fed, and (T -τ )/T is the proportion of time during which a stress is imposed to the microorganisms. Such a shape can be approached as shown in Figure 1, with two steps : a rising phase and a falling one. The approximation is good if s(t) ≈ s M for most of the time interval [0, τ ].

Rising phase during time τ rise

We choose s in such that ṡ = λ(s M -s) :

s in = s + 1 D λ(s M -s) + N i=1 ρ i (s)x i (16)
s in = s + 1 D X T N i=1 x i X T ρ i (s) -γφ(s) (17) Since N i=1 xi X T ρ i (s) is a convex combination of the ρ i (s), we have for all s : X T N i=1 xi X T ρ i (s) ≥ X T min i ρ i (s) > X T φ(s), so that s in > 0 if X T > γ ∀t For having s in > 0 we need φ(s)γ < N i=1 xi X T ρ i (s) X T .
This can be achieved with γ < min(X T , X T (0)) under control (11).

Finally, as we will see in section 5, it is possible to estimate the falling time τ f all with ds dt = -γφ(s), and to obtain a periodic s which permits us to approach control (15). By choosing X T big enough and waiting for X T to be close to X T before starting the s in control, γ can be chosen big and s(t) ≈ 0 is reached fast. Thus, controls ( 16) and ( 17) permit us to achieve periodic behavior near (15) for s(t).

With control (15) we get approximately the following qi :

qi = ρ i -µ i (q i )q i with ρ i (t) = ρ mi for t ≡ T ≤ τ 0 for t ≡ T > τ (18)
and it is now possible to show that Theorem 5. There exists a unique periodic solution qi (t) to (18). This periodic solution is attractive for any initial condition q i (0) inside [0, Q mi ]

Proof

In the case q i (0) = 0 we have q i (τ ) > 0 because µ i (q i )q i < ρ mi , and q i (τ ) > 0 implies q i (T ) > 0 because µ i (q i )q i < µ mi q i and the decrease is slower than an exponential decrease with time constant µ mi . With q i (0) = 0 we obtain q i (T ) > q i (0).

In the case q i (0) = Q mi we have q i (τ ) = Q mi because µ i (Q mi )Q mi = ρ mi , and q i (T ) < Q mi because qi = -µ i (q i )q i < 0. With q i (0) = Q mi we obtain q i (T ) < q i (0). Thus, by continuity of q i (T ) with regard to the initial condition, there exists an initial condition q i (0) = qi (0) such that qi (T ) = qi (0) and q i is T -periodic under control (15).

We can also show that V i (t) = |q i (t) -qi (t)| is decreasing along the solutions : Vi (t) = sign(q i (t) -qi (t))( qi (t)qi (t)) < 0 because sign( qi -qi ) = sign(-µ i (q i )q i + µ i (q i )q i ) = -sign(q i -qi ). V i being a Lyapunov function converging to zero, lim t→+∞ q i (t) = qi (t). 2

Therefore, with control (15), qi (t) attracts all solutions q i (t), q i converges towards a T -periodic behavior, and so does µ i (q i (t)). We will see in section 5.2 that this periodic behavior, caused by the periodic stresses, can lead us to a new competitiveness criterion.

SIMULATIONS WITH THREE SPECIES

These simulations have been carried out on the Droop model ( 4) with control (11) so that the total biomass concentration converge toward X T .

We have used Michaelis-Menten absorption rates ρ i (s) and Droop's growth rates µ i (q i ).

ρ i (s) = ρ mi s s + K si µ i (q i ) = μi 1 - K qi q i (19)
And the following parameters for the species, whose approximate values come from I. We have used a big constant s in = 10µmol/L and a small X T = 1•10 9 •(µm) 3 /L, as was previously advised in section 3.3. We have thus obtained ṡ ≈ D(s in -s) and s converges to s in with µ i (Q i (s in )) ≈ µ mi .

Figure 2 shows the result of the simulation, where species 2 with biggest µ mi excludes all others. For these simulations we have used controls ( 16) and ( 17) to approximate ideal control ( 15), with T = 1day, X T = 400 • 10 9 (µm) 3 /L, and X T (0) = 220 • 10 9 (µm) 3 /L

For the rising phase we have used s M = 5µmol/L with s M K si so that ρ i (s M ) ≈ ρ mi , and λ = 1000 so that s rises fast. For the falling phase we have used γ = 100•10 9 (µm) 3 /L < min(X T (0), X T ), and φ(s) = ρ m φ s s+Ks φ with ρ m φ = 5 • 10 9 µmol/(µm) 3 < ρ mi and K s φ = 1µmol/L > K si so that φ(s) < ρ i (s) ∀i ∈ {1, ..., N } , ∀s. In section 4 We have obtained ṡ = -γφ(s). The fall is thus equivalent to the consumption of the substrate by a virtual species with absorption parameters ρ m φ and K s φ , and with biomass concentration γ.

We know how to predict τ f all , until s reaches a small value s 0 = 0.005µmol/L :

f all = 1 γρm φ s M -s 0 + K s φ ln s M s0
It is thus possible to choose τ rise so that τ = τ f all + τ rise , and to approach control (15). With (18) and with functions (19), after some algebraic calculus, we have demonstrated that the internal substrate storages q i converge towards T -periodic functions :

qi (t) = Q mi 1 -e -μit + qi (0)e -μit if 0 ≤ t ≡ T ≤ τ K qi 1 -e -μi(t-τ ) + qi (τ )e -μi(t-τ ) else with qi (0) = Q mi -(Q mi -K qi ) 1 -e -μi(T -τ ) 1 -e -μiT and q(τ ) = K qi + (Q mi -K qi ) 1 -e -μiτ 1 -e -μiT (20)
with lim t→+∞ q i (t) = qi (t) : the growth rate functions µ i (q i (t)) become T -periodic.

We have then calculated : represents the capacity of the species to increase its internal substrate storage.

µ meani = 1 T µ mi μi ln   1 + Q mi /K qi 1 1-e -μi τ + (Qm i /Kq i )e -μi T -1 1-e -μi T   (
Figure 3 shows that different species can be selected with different environmental condition τ , because for each species i here, there exists a τ value such that µ meani is higher than the other species' mean growth.

CONCLUSION

This work shows that it is in theory possible to select species exhibiting a desired feature in the chemostat. Moreover the selection criterion, which is the maximum growth rate under given environmental conditions, seems promising for various biotechnological applications.

The selection occurs because the total biomass concentration X T = N i=1 x i is upper bounded. It is possible to bound X T by other means than controlling D (for instance with the light). It is also most certainly possible to find new selection criteria by changing the environmental conditions with D, s in , and with other controls such as an inhibitor's concentration.

This selection method makes it possible to select quite easily a species for its study or culture. It could be used to identify species which grow in hostile conditions, to amplify and verify the presence of a species in a medium, or to select a species which is interesting for a specific biotechnological objective. This work could be extended to models describing predation or parasitism by other types of microorganisms, or

Fig. 1 .

 1 Fig. 1. Approaching ideal periodic substrate stresses (15) (dashed), with a rising and a falling phase (solid) There is no positivity problem for s in here because s M > s. Then s(t) = s M (1 -e -λt ) with s(0) = 0, and with a big λ we obtain s(t) ≈ s M for most of the time interval [0, τ rise ] Falling phase during time τ f all = τ -τ rise We choose s in such that ṡ = -γφ(s), with φ(s) < ρ i (s) ∀i ∈ {1, ..., N } , ∀s ∈ [0, s M ]

Fig. 2 .

 2 Fig. 2. Simulation of the selection of the species with biggest µ mi Lines & species : Solid -1, Dashed -2, Dotted -3 5.2 Selection under periodic substrate stresses

Fig. 3 .

 3 Fig. 3. µ meani (τ ) for the three species. The species with biggest µ meani will be selected. It is thus possible to select each of the three secies with different τ Lines & species : Solid -1, Dashed -2, Dotted -3 Finally, Figure 4 presents the simulations.

Fig. 4 .

 4 Fig. 4. Simulations of competition in the Droop model, under controls (11), (16) and (17). top : τ = 0.1T , middle : τ = 0.5T , bottom : τ = 0.9T Lines & species : Solid -1, Dashed -2, Dotted -3 agressive interactions between the species such as the production of a chemical which inhibates other species growth (see A.G. Fredrickson and G. Stephanopoulos [1981] for a presentation of factors which can mitigate the severity of the competition).

  Criterion 1. CEP's Competitiveness CriterionThe species with smallest s i , who needs less substrate than the others for reaching a growth rate µ i (s) equal to the dilution rate D, wins the competition and excludes all other species from the chemostat.

This result can be found in H.L.

[START_REF] Smith | The theory of the chemostat[END_REF]

for the Monod model with N species and for the Droop model with 2 species, and validated with several species (S.R.

Hansen and S.P. Hubell [1980]

-H. Ducobu, J. Huisman, R.R. Jonker, and L.R. Mur [1998] -J.

[START_REF] Passarge | Competition for nutrients and light: Stable coexistence, alternative stable states, or competitive exclusion?[END_REF]

).

The CEP is crucial for the understanding of natural ecosystems. That is why so many people discussed it. Some (B.T. Li , H.L.

[START_REF] De Leenheer | Competition in the chemostat : some remarks Canadian applied mathematics[END_REF]

-C.

Lobry, F. Mazenc, and A. Rapaport [2005]

-J. Hesseler, J.K. Schmidt, U. Reichl, D.

Flockerzi [2006]

-C.

Lobry and J. Harmand [2006]

) developped alternative models for which the CEP is not verified, in order to explore some coexistence cases. S.S.

Pilyugin, G.T. Reeves, and A. Narang [2004]

worked on multiple substrate limitations, and showed in these conditions that it is possible to infer the result of competition from the dynamics of single species cultures. Some works have already been done to control the competition in the chemostat, generally to enable the coexistence of several species (N.S.

Rao and E.O. Roxin [1990]

-P. de Leenheer, B.

[START_REF] De Leenheer | Competition in the chemostat : some remarks Canadian applied mathematics[END_REF]

-J.

  (0) and R n i (t) are bounded, lim t→+∞ d i (t) = +∞ because lim t→+∞ p i (t) = +∞ and µ meann > µ meani = +∞ and, as x n is upper bounded by the upper-bound on X T , then lim t→+∞ x i (t) = 0 and the proof is complete. 23.3 Selection of the species with biggest µ mi

	and with pi(t) pn(t) = t-t≡Ti t-t≡Tn	Tn Ti , since lim t→+∞	t-t≡Ti t-t≡Tn = 1 ,
	and d i Thus lim t→+∞	xn(t) xi(t)
	dτ

  Criterion 6. Periodic stresses' Competitiveness Criterion Under control (15), with τ ≈ T the species with biggest µ meani ≈ µ mi excludes all others from the chemostat; with τ T and τ1 μi•Qm i /Kq i

				the species with biggest
	T τ µ meani ≈ µ mi stat.	Qm i Kq i	excludes all others from the chemo-
	where	Qm i Kq i

21)

ACKNOWLEDGEMENTS

This work was carried out as part of the APPLE project, and financed by the French national program PROOF.