Karim Nour
email: karim.nour@univ-savoie.frkhelifa.saber@gmail.com

Khelifa Saber

Some properties of the λµ ∧∨ -calculus

Keywords: A, ∆ Γ v : B, ∆ Γ u, v : A ∧ B, ∆

In this paper, we present the λµ ∧∨ -calculus which at the typed level corresponds to the full classical propositional natural deduction system. Church-Rosser property of this system is proved using the standardization and the finiteness developments theorem. We define also the leftmost reduction and prove that it is a winning strategy.

Introduction

The λµ ∧∨ -calculus is an extension of the λµ-calculus associated by the Curry-Howard correspondence to the full classical natural deduction system, it was introduced by P. De Groote [START_REF] Groote | Strong Normalization of Classical Natural Deduction with Disjunction[END_REF]. In the λµ ∧∨ -calculus as in any other abstract reduction system, termination, confluence and standardization appear among the principal properties. The question of termination, of course for the typed λµ ∧∨ -calculus, was studied by many authors [START_REF] David | A short proof of the Strong Normalization of Classical Natural Deduction with Disjunction[END_REF], [START_REF] Groote | Strong Normalization of Classical Natural Deduction with Disjunction[END_REF], [START_REF] Matthes | Non-strictly positive fixed point for classical natural deduction[END_REF] and [START_REF] Nour | A semantical proof of strong normalization theorem for full propositional classical natural deduction[END_REF], however the proof of strong normalization in [START_REF] Groote | Strong Normalization of Classical Natural Deduction with Disjunction[END_REF] based on the CPS-transaltion did not work, correction for this proof was given in [START_REF] Ikeda | Strong normalization proofs by CPS-translations[END_REF].

Confluence is a very important property, it guarantees the uniqueness of the normal form (if it exists) independently of the strategy of reduction, i.e, if we are allowed to write terms which necessarily do not finish under reduction, one expects at least that the possible result is independent of the strategy of reduction. There are different methods to prove the confluence property: parallel reduction, complete development, finiteness developments and standardization... For a strongly normalizable term rewriting system, one needs only to check the local confluence which suffices when combinated with Newman lemma.

Standardization is classical and a very convenient tool, the issue is the order in which the reduction steps are performed. In a standard reduction, this is done from left to right. According to the standardization theorem, any sequence of reductions can be transformed into a standard one. We find in current literature various equivalent definitions of this notion. In our work, we adopt the one given by R. David and W. Py [START_REF] David | Une preuve simple de résultats classiques en λ-calcul[END_REF] and [START_REF] Py | Confluence en λµ-calcul[END_REF], it is very convenient and has the advantage that we do not need to formalize the notion of residus "descendant" of a redex.

The presence of the permutative reduction of the form "((t [x.u, y.v]) ε) reduces to (t [x.(u ε), y.(v ε)])" has certain consequences not only on the termination of the system, but also on the standardization and the confluence, since the resulting rewriting system is not orthogonal. Therefore the treatment of these two notions is not trivial at all. Intuitively standard reduction contract redexes from external to internal and from left to right. However there is more freedom in the presence of permutative reductions, a permutative redex of the form ((µa.t [x.u, y.v]) [r.p, s.q]) ε may permute to (µa.t [x.(u [r.p, s.q]), y.(v [r.p, s.q])]) ε and to (µa.t [x.u, y.v]) [r.(p ε), s.(q ε)] and both possiblities as well as the embedded µredex should be treated equivalently. We can not favour one over the other and consider for example, the classical one as external or the leftmost one. That would be also the same thing for the two permutatives redexes.

In this work we use a definition "à la David" which captures this intuitive notion of standardization, when restricted to the λ-calculus (resp the λµ-calculus) corresponds exactly to the one given in [START_REF] David | Une preuve simple de résultats classiques en λ-calcul[END_REF] (resp [START_REF] Py | Confluence en λµ-calcul[END_REF]). As an application of this definition, we prove that leftmost reduction in a sense which we determinate later is a gaining strategy.

The finiteness developments theorem says that: if we mark a set R of redex occurences in a given term t and reduce only the marked redex occurences and redex occurences which descend from marked redex occurences, the reduction process always terminates. If we reduce every marked redex occurence, then the order in which such reductions are performed does not matter, R uniquely determines a term u to which t is reduced under any complete reduction of marked redex occurences. In addition, if we mark another set R of redex occurences in t and follow this set through a complete R-reduction, the redex occurences from R may be transformed by substitution or copied. However, it does not matter in what way we perform a complete R-reduction, the set of redex occurences in u which descend from R is again uniquely determined. This theorem has important consequences like the confluence property. The proof for this theorem is difficult and required a standardization theorem, this is what we establish in the major part of this work.

This paper is presented as follows. Section 2 is an introduction to the typed λµ ∧∨ -calculus. Section 3, contains some useful technical results, in order to well define, head and leftmost reduction. In Section 4, we define the standard reductions and prove the standardization theorem. In Section 5, we introduce a marked version of λµ ∧∨ -calculus, to keep traces of the residu of redexes and prove the finiteness developments theorem. We close this section by the main theorem of this paper, i.e, the confluence property.

Notations and definitions

Definition 2.1 We use notations inspired by the paper [START_REF] Andou | Church-Rosser property of simple reduction for full first-order classical natural deduction[END_REF].

1. Types are formulas of propositional logic built from an infinite set of propositional variables and the constant ⊥, using the connectors →, ∧ and ∨.

2. Let X and A be two disjoint infinite alphabets for distinguishing the λ-variables and µ-variables respectively. We code deductions by using a set of terms T which extends the λ-terms and is given by the following grammars:

T := X | λX .T | (T E) | T , T | ω 1 T | ω 2 T | µA.T | (A T ) E := T | π 1 | π 2 | [X .T , X .T ]
An element of the set E is said to be an E-term. An E-term in the form (T E) or (A T ) is called an application.

Γ t : A; ∆, a : A Γ (a t) : ⊥; ∆, a : A ⊥ i Γ t : ⊥; ∆, a : A Γ µa.t : A; ∆ µ 4.
The cut-elimination procedure corresponds to the reduction rules given below.

They are those we need to obtain the subformula property.

(a) Logical reduction rules:

• (λx.u v) β u[x := v] • ( t 1 , t 2 π i ) πi t i • (ω i t [x 1 .u 1 , x 2 .u 2 ]) D u i [x i := t]
(b) Permutative reduction rule:

• ((t [x 1 .u 1 , x 2 .u 2 ]) ε) δ (t [x 1 .(u 1 ε), x 2 .(u 2 ε)])
(c) Classical reduction rule:

• (µa.t ε) µ µa.t[a := * ε]
where t[a := * ε] is obtained from t by replacing inductively each subterm in the form (a v) by (a (v ε)).

5.

Let ε and ε be E-terms. The notation ε ε means that ε reduces to ε by using one step of the reduction rules given above. Similarly, ε * ε means that ε reduces to ε by using some steps of the reduction rules given above. The length of the sequence reductions ε * ε is the number of the one step reduction.

6. Let ε and ε be E-terms and r a redex of ε. The notation ε r ε means that ε reduces to ε by reducing the redex r.

7. An E-term ε is said to be normal iff it has no redexes.

3 Characterization of the λµ ∧∨ -terms

In this section we develop some results already present in [START_REF] David | A short proof of the Strong Normalization of Classical Natural Deduction with Disjunction[END_REF]. The presence of the critical pairs for the standardization, and the fact that a λµ ∧∨ -term can have more than one head, unlike the λ-calculus or the λµ-calculus, need such results before defining the notion of standardization, head or leftmost reductions.

Definition 3.1 1. A term t is said to be simple if it is a variable or an application.

2. Let H = { * 1 , ..., * n , ...} be an infinite set of holes. The set of general contexts C is given by the following grammar: 1. The length of ε is defined by lg(ε) = n.

C := H | λx.C | C, C | ω 1 C | ω 2 C
2. The sequence is said to be nice iff ε n is the only E-term which can be in the form [x.u, y.v].

3. The sequence ε is said to be normal iff each ε i is normal.

4. We write ε ε iff ε = ε 1 ...ε i ...ε n , and ε = ε 1 ...ε i ...ε n where ε i ε i for 1 ≤ i ≤ n. Lemma 3.2 (and definition) Let t be a simple term.

1. The term t can be uniquely written as one of the figures below.

2. A head of t (denoted as hd(t)) is a set of subterms of t, it is defined by the figures below.

3. In the cases (1), ( 2), (3), ( 4) and (5) (resp. ( 6)) the sequence ε (resp. εε) can be empty. In the cases (5) and (6) if εε is not nice, then εε = r [y.u, z.v]ε i s.

t hd (t) 0 x x 1 (a u) ε a 2 ((λx.u ε) ε) (λx.u ε) 3 (( u 1 , u 2 ε) ε) ( u 1 , u 2 ε) 4 ((ω i u ε) ε) (ω i u ε) (µa.u ε) or 5 ((µa.u ε) ε) any permutative redex in the form ((µa.u r[y.v, z.w]) ε i ) x, if the sequence εε is nice, 6 ((x ε) ε)
else, any permutative redex in the form ((x r[y.u, z.v]) ε i ) Proof By induction on the simple term t. We have either t is a variable, either t = (a u) or t = (u ε). Therefore we will examine the form of u.

-If u is not a simple term, then u = λx.v, u = u 1 , u 2 , u = ω i v or u = µa.v.
All these forms give us that t is respectively in the case (2), ( 3), ( 4) or [START_REF] David | Une preuve simple de résultats classiques en λ-calcul[END_REF].

-If u is a simple term, then induction hypothesis concludes.

The uniqueness is clear.

Remark 3.1 1.
Observe that simple terms of the form ((x ε) ε) and ((µa.u ε) ε) can have more than one head. hd(t) is a non-deterministic function to subterms of t.

2. Terms of the form (λx.u ε), ( u 1 , u 2 ε) and (ω i v ε) are not always redexes, for example (λx.u π i ), (ω i v u), ( u, v [x, p.y, q]), ... and obviously they can not be typed. Therefore hd(t) in the cases (2), ( 3) and (4) is not always a redex. This is why, in the rest our proofs such cases are not considered, not because these terms are not typed but because there is no redex to reduce (if there are, they are in the subterms, and inductions hypotheses allowed to conclude).

The lemma 3.2 allows the λµ ∧∨ -term to be characterized in the following corollary, this characterization is useful for the standardization theorem section. Corollary 3.1 Any term can be written in the one of the following forms (a v) ε or (t ε), where t = x, λx.u, u 1 , u 2 , ω i u or µa.u and ε is a finite sequence of E-terms possibly empty. Proof Direct consequence of the lemma 3.2.

Standardization theorem

The standardization theorem is a useful result stating that if t * t , then there is a sequence of reductions from t to t "standard" in the sense that contractions are made from left to right, possibly with some jumps in between.

Intuitively the standard reduction contracts redexes from the external to the internal and from left to right. For λ-calculus, a standard reduction from the term (λx.u v)ε 1 ...ε n either starts by reducing the head redex (λx.u v), else this one will never be converted after performing u, v or the arguments ε i , i.e, from external to internal. An other characteristic, standard reduction from the term ((x u) v) has to reduce firstly in u and then in v, in this given order from left to right, this last notion is not captured by our definition given bellow since we consider that reduction in u and v are independent of each other.

One of the main consequences of standardization is that normal forms, if existing, can be reached by leftmost sequence reduction.This will be a simple consequence since standard reduction is defined such a way that leftmost reduction is just a particular standard one (definition of leftmost reduction is presented in next section).

The following definition of a standard sequence of reductions is somehow a generalization of those given by R. David and W. Py in [START_REF] David | Une preuve simple de résultats classiques en λ-calcul[END_REF] and [START_REF] Py | Confluence en λµ-calcul[END_REF], in the sense that if we restrict our definition to the λ or the λµ-calculus, it captures exactly their definitions .

Definition 4.1

1. Let w = r[x.p, y.q]εs where r and s are possibly empty. We define a new reduction relation by: w r[x.(p ε), y.(q ε)]s. As usual * denotes the reflexive and transitive closure of .

2. Let ε, ε be two E-terms such that ε ε 1 ... ε n = ε . We denote κ(ε * ε ) =
(n, c) where c stands for the complexity of ε (n is the length of the reduction ε * ε ). We say that this sequence reduction is standard and we write ε * st ε iff it is obtained as follows. This definition is given by induction on the ordered lexicographic pair (n, c). We use simultaneously the following abreviations:

ε = ε 1 ...ε n * st ε = ε 1 ...ε n means that ε i * st ε i for each 1 ≤ i ≤ n. (C λ ) If ε = (λx.u ε), then ε = (λx.u ε ) with u * st u and ε * st ε . (C µ ) If ε = (µa.u ε), then ε = (µa.u ε ) with u * st u and ε * st ε . (C π ) If ε = ( u 1 , u 2 ε), then (ε = u 1 , u 2 ε ) with u i * st u i and ε * st ε . (C ω ) If ε = (ω i u ε), then ε = (ω i u ε ) with u * st u and ε * st ε . (V λ ) If ε = (x ε), then ε = (x ε ) with ε * st ε . (V µ ) If ε = (a u), then ε = (a u ) with u * st u . • If ε = (t ε), where t is a simple term in the form (λx.u v) (resp. ( u 1 , u 2 π i ), (µa.u ), (ω i u [x 1 .v 1 , x 2 .v 2 ]
), x, a ), we denote by r its possible reductom

u[x := v] (resp. u i , µa.u[a := * ], v i [x i := u]). (⇒) Either ε (r ε) * st ε , ( δ ) Either ε (t ε ) * st ε with ε ε . ( µ ) Either ε (µa.u ε ) * st ε with ε ε , and this only if t = (µa.u ). ( ω ) Or ε (ω i u ε ) * st ε with [x 1 .v 1 , x 2 .v 2 ]ε ε , and this only if t = (ω i u [x 1 .v 1 , x 2 .v 2 ]). • If ε = π i , then ε = π i . • If ε = [x 1 .u 1 , x 2 .u 2 ], then ε = [x 1 .u 1 , x 2 .u 2 ] with u i * st u i . Remark 4.1
1. In the rules C λ , ..., C ω the sequence ε is possibly empty and this corresponds to the cases where ε is not a simple term.

2. Given a λµ ∧∨ -term of the form (t ε) standard reduction strategies can start with various permutations using the rule δ ( µ , ω according to the form of t) until either we obtain a nice sequence and then reducing the possible head redex by the rule ⇒ or start performing subterms of the arguments using the rules V λ , V µ or the rules C λ , ..., C ω .

Lemma 4.1 Assume that ε * st ε . 1. If v * st v , then ε[x := v] * st ε [x := v ]. 2. If * st , then ε[a := * ] * st ε [a := * ].
Proof Only the second assertion will be treated. By induction on κ(ε * st ε ). We give just the case where the substitution intervenes.

4.2 If ε * st ε ε , then ε * st ε . Proof By induction on κ(ε * st ε ) = (n, c
). We examine how ε * st ε following the different forms of ε.

-The cases where ε is not a simple term are direct consequences of the induction hypothesis (decreasing of c).

-If ε is a simple term, we will examine some cases, the others are similar or more simpler.

(C λ ) Let ε = (λx.u ε) * st (λx.u ε ) = ε ε , with u *
st u and ε * st ε (here of course ε is not empty since ε is simple). We distinguish three cases:

-If ε = (λx.u ε ) (resp. (λx.u ε )), where u u (resp. ε ε ), then the induction hypothesis concludes. -If ε = (u [x := v ] ε 2 ...ε n ), then ε = vε 2 ...ε n where v * st v , ε i * st ε i and ε = v ε 2 ...ε n . Therefore, by the lemma 4.1, u[x := v] * st u [x := v ], thus (u[x := v] ε 2 ...ε n ) * st (u [x := v ] ε 2 ...ε n ). Finally, by the rule (⇒), we have ε (u[x := v] ε 2 ...ε n ) * st (u [x := v ] ε 2 ...ε n ) is a standard sequence of reductions. -The last case is ε = (λx.u ε ) where ε ε . Therefore ε = ε 1 ...[y.p, z.q]ε i ...ε n * st ε 1 ...[y.p , z.q ]ε i ...ε n and then ε = ε 1 ...[y.(p ε i ), z.(q ε i )]...ε n . We have [y.(p ε i ), z.(q ε i )] * st [y.(p ε i ), z.(q ε i )], hence the rule ( δ ) allows to conclude: ε (λx.u ε 1 ...[y.(p ε i ), z.(q ε i )]...ε n ) * st (λx.u ε 1 ...[y.(p ε i ), z.(q ε i )]...ε n ) = ε .
(C µ ) , (C π ) and (C ω ) are similar to the previous case.

(V λ ) Let ε = (x ε), then ε = (x ε) * st ε = (x ε ) (x ε ) = ε , and -Either ε = ε 1 ...ε i ...ε n * st ε 1 ...ε i ...ε n = ε ε 1 ...ε i ...ε n = ε , hence, by induction hypothesis, ε i * st ε i . Therefore, we have ε * st ε and ε = (x ε) * st (x ε ) = ε . -Or ε = ε 1 ...[y.p, z.q]ε i ...ε n * st ε 1 ...[y.p , z.q ]ε i ...ε n = ε ε 1 ...[y.(p ε i ), z.(q ε i )]...ε n = ε . We have [y.(p ε i ), z.(q ε i )] * st [y.(p ε i ), z.(q ε i )], therefore, by the rule ( δ ), (x ε) (x ε 1 ...[y.(p ε i ), z.(q ε i )]...ε n ) * st (x ε 1 ...[y.(p ε i ), z.(q ε i )]...ε n ) = (x ε ) is a standard sequence of re- ductions.
(V µ ) is a direct consequence of the induction hypothesis (decreasing of c).

(⇒) ,( δ ), ( µ ) and ( ω ) are direct consequences of the application of the induction hypothesis (decreasing of n).

Remark 4.2

1. In [START_REF] Joachimski | Standardization and Confluence for a Lambda Calculus with a Generalized Applications[END_REF], F. Joachimski and R. Matthes presented the ΛJ-calculus which is an extension of the λ-calculus by a generalized application that gives rise to permutative reductions, the resulting rewriting system is not orthogonal (this is also the case of the λµ ∧∨ -calculus). The definition of the standardization established here produced exactly the same treatment of the logical and the classical reductions ( β , πi , D and µ ) like that of β-reduction in [START_REF] Joachimski | Standardization and Confluence for a Lambda Calculus with a Generalized Applications[END_REF], this means that to avoid difficulties relative to µ-reduction, we need to treat it similarly as β-reduction. The ΛJ-calculus has served us as a model for studying our λµ ∧∨ -calculus. In fact, concerning the standardization, the restriction of the λµ ∧∨ -calculus to the λµ-one can serve as a model for the study of the rewriting system with permutative and structural reductions, as well as the ΛJ-calculus serves as a minimal model for the study of term rewriting systems with permutation.

2. In the definition 4.1, we can be "more restrictive", by this we mean that, we have a strong standardization theorem when replacing the rules δ and ω by:

( λ ) ε = ((λx.u v) ε) ((λx.u v) ε ) * st ((λx.u v ) ε ) = ε with u * st u , v * st v and ε ε * ε * st ε . ( π ) ε = (( u 1 , u 2 π i ) ε) (( u 1 , u 2 π i ) ε ) * st (( u 1 , u 2 π i ) ε ) = ε with u i * st u i and ε ε * ε * st ε . ( D ) ε = ((ω i u [x 1 .v 1 , x 2 .v 2 ]) ε) ((ω i u ε ) * st (ω i u ε ) = ε with u * st u and [x 1 .v 1 , x 2 .v 2 ]ε ε * ε * st ε .
This can be explained by the fact that:

• For the rules λ and π , there are no interactions between v, π i and ε via permutative reductions.

• For the rule D , even there are interactions between [x 1 .v 1 , x 2 .v 2 ] and ε via permutative reductions, after a D -reduction we will always get

(v i ε)[x i := u] = (v i [x i := u] ε) since x i is not free in ε.
Contrary to the case ε = ((µa.u [x.p, y.q]) [r.k, s.l] ) in which there are more complications. Suppose that we give the priority to the classical redex, i.e, if it is not converted in the beginning then it will be never performed, thus the lemma 4. st q (it depends on p and q). To resolve this problem we have to consider the rule µ .

3. In the rest of this paper, we consider only typed terms, although the results that we prove here (normalisation of the leftmost reduction and the finiteness developments theorem) do not use neither the strong normalization theorem (hard to prove in this context) nor the confluence property (which is here a consequence the finiteness developements theorem). Untyped terms will not be considered for reasons of ease of reading. Note that techniques that we develop here allow to prove our results for all the calculus, but this requires modifications of some definitions (the head of a term, the head normal form, ...) and the treatment of more cases in proofs.

Head and leftmost reductions

In the λ-calculus, the leftmost reduction of a term consists in reducing its lefmost redex. Despite its laziness, this reduction has the advantage that is a winning strategy. By this, we means that: if a term t is normalizable, then leftmost reduction of t always reaches its normal form. In the λµ ∧∨ -calculus, a term can have more than one head, the thing which prevents us from defining the leftmost reduction in the sameway as in λ-calculus. Therefore, we start this section by introducing the notion of head reduction (which is also different from the one of the λ-calculus). This allows, first, to define the leftmost reduction as an iteration of head reduction. Then, to prove that a sequence of leftmost reductions is a standard one. Finally, to prove that the definition of the leftmost reduction which we give, provides a gaining strategy too. 2. A simple head normal form is a simple term in the form (x ε) where ε is a nice sequence, or in the form (a u), the elements of the sequence ε (resp u) are called the arguments of the head variable x (resp a). The sequence ε is a nice one, and these are the only cases where we cannot reduce in the head, because there is no head since the arguments of the sequence cannot interacte between them via permutative reductions. A head normal form is a term in the form C[t 1 , ..., t n ] where all the t i are simple head normal forms.

Remark 5.1 Observe that there is no unicity of "the" head normal form. Take the simple term t = ((x [y.u, z.v]) [r.p, s.q]ε), then t * hd (x [y.((u [r.p, s.q]) ε), z.((v [r.p, s.q]) ε)]) = t 1 , t * hd (x [y.(u [r.(p ε), s.(q ε)]), z.(v [r.(p ε), s.(q ε)])]) = t 2 , and both of t 1 and t 2 are head normal froms. Definition 5.2 A leftmost reduction of a term t consists to apply a head reduction on t until its head normal form C[t 1 , ..., t n ] (if it exists) and reiterate it on the arguments of t i . We denote t * L t if t is reduced to t by a leftmost reduction. When an argument of a head variable is an E-term in the form [x.u, y.v], the reduction consists simply to reduce in u and v. If t * L t , then we denote κ(t * L t ) = (n, c) where n stands for the length of the reduction t * L t and c the complexity of t.

The following theorem says that every sequence of leftmost reductions is a standard one. -The cases where t is not a simple term are direct consequences of the induction hypothesis. For example, if t = λx.u, then t = λx.u where u * L u . Therefore, by induction hypothesis (decreasing of the complexity c), u * L u is a standard sequence reductions, thus λx.u * L λx.u is a standard one too.

-The cases where t is a simple term: • The other cases are similar to the previous. This theorem gives another way to define a leftmost reduction similarly to the definition of the standard reduction. The following definition (theorem) can be easily proven to be "equivalent" to the one given above.

• If t = (µa.u ε) ε,
Theorem 5.2 (definition) Let ε, ε be two E-terms (resp. ε and ε two finite sequences of E-terms) such that ε * ε (resp. ε * ε ). We say that ε * l ε (resp. ε * l ε ) iff it is obtained as follows. This definition is given by induction on the ordered lexicographic pair κ(ε * ε ) = (n, c) (resp. κ(ε * ε ) = (n, c)) where n is the length of the reduction ε * ε (resp. ε * ε ) and c stands for the complexity of ε (resp. ε).

1. ε * l ε • If ε = λx.u, then ε = λx.u with u * l u . • If ε = µa.u, then ε = µa.u with u * l u . • If ε = u, v , then ε = u , v with u * l u and v * l v . • If ε = ω i u, then ε = ω i u with u * l u . • If ε = (a u), then ε = (a u ) with u * l u . • If ε = (x ε), then ε = (x ε ) with ε * l ε . • If ε = ((λx.u v) ε), then ε l (u[x := v] ε) * l ε . • If ε = ((µa.u ) ε), then -Either ε (µa.u[a := * ] ε) * l ε . -Or ε ((µa.u θ) s) * l ε with θ. • If ε = (( u 1 , u 2 π i ) ε), then ε (u i ε) * l ε , • If ε = ((ω i u [x 1 .v 1 , x 2 .v 2 ]) ε), then ε (v i [x i := u] ε) * l ε . • If ε = π i , then ε = π i . • If ε = [x 1 .u 1 , x 2 .u 2 ], then ε = [x 1 .u 1 , x 2 .u 2 ] with u i * l u i . 2. ε * l ε • If ε is not nice, then ε s * l ε . • Else ε = ε 1 ...ε n , then ε = ε 1 ...ε n with ε i * l ε i for each 1 ≤ i ≤ n.
We have * l and * L are the same reduction.

Finiteness of developments

In the λ-calculus, the finiteness developments theorem stipulates that: for a given term t and a subset R of redexes of t, if we reduce only redexes which belong to R or their residus, then any sequence of reductions terminates. Based on this theorem and the local confluence of β-reduction, R. David [START_REF] David | Une preuve simple de résultats classiques en λ-calcul[END_REF] gave a short proof of the confluence theorem of β-reduction. The notion of residus of redex is enough clear in λ-calculus, roughly speaking a residu of redex is a redex which is not created, thus if at the beginning in the term t we mark each redex which belongs to R, then we can reduce only these marked redexes. Of course when such redex is copied or transformed by some substitutions, we consider that the new redex is not a created one since it keeps its mark. The same idea will be developed in the next paragraph. First, let us take an example to illustrate this.

Example 6.1 Let t = ((µa.u [y.p, z.q]) ε) and R = {t, (µa.u [y.p, z.q])}, then t (µa.u [y.(p ε), z.(q ε)]) = t 1 and t (µa.u[a := * [y.p, z.q]] ε) = t 2 . Observe that if we want to obtain a commun redectum from t 1 and t 2 , we have to reduce some redexes in t 1 and t 2 . Implicitely these redexes are the residus of redexes in R, they must not be seen as created redexes. The same term t but where the redexes in R are marked gives t = ((μa.u y.p, z.q ) ε). t (μa.u y.(p ε), z.(q ε) ) μa.u[a := * y.(p ε), z.(q ε) ] t (μa.u[a := * y.p, z.q ] ε) μa.u[a := * y.p, z.q ε] * μa.u[a := * y.(p ε), z.(q ε) ]

We mark the commutative (resp classical) redex t (resp. (µa.u [y.p, z.q])) in this way: [, ] (resp. µ ) become , (resp. μ). The commun redecum is the term (without

marks) µa.u[a := * [y.(p ε), z.(q ε)]].
Therefore for the purpose of this section, we introduce a marked version of the λµ ∧∨ -calculus. 1. We extend the syntax of the λµ ∧∨ -calculus by adding new symbols λ, μ, < . , . >, Ω i and . , . . These symbols are called marks. The sets T and E of marked terms are defined by the following grammars:

The marked terms

T := T | ( λX .T T) | (< T, T > π i ) | (Ω i T [X .T, X .T]) | (Ω i T X .T, X .T ) | (T E) | μa.T E := E | T | X .T, X .T 2.
The reduction rule of E consists in the union of the following reduction rules. The meaning of these new reductions is to capture the definition of the finiteness developments, where we reduce only redexes at the beginning or only their residus (which will be exactly the marked redexes).

• ( λx.t u) β t[x := u] • (< t 1 , t 2 > π i ) πi t i • (Ω i t [x 1 .u 1 , x 2 .u 2 ]) D u i [x i := t] • (Ω i t x 1 .u 1 , x 2 .u 2 ) Ω u i [x i := t] • ((Ω i t x 1 .u 1 , x 2 .u 2 ) ε) ∆ (Ω i t x 1 .(u 1 ε), x 2 .(u 2 ε) ) • ((t x 1 .u 1 , x 2 .u 2 ) ε) δ (t x 1 .(u 1 ε), x 2 .(u 2 ε) ) • (μa.t ε) µ μa.t[a := * ε]
We denote by * the reflexive and transitive closure of .

3. Let t ∈ T and r a redex of t, we define r the marked redex obtained by making r as follows:

• If r = (λx.u v), then r = ( λx.u v) • If r = ( t 1 , t 2 π i ), then r = (< t 1 , t 2 > π i ) • If r = (ω i u [x 1 .u 1 , x 2 .u 2 ]), then r = (Ω i u [x 1 .u 1 , x 2 .u 2 ]) • If r = ((u [x 1 .u 1 , x 2 .u 2 ]) ε), then r = ((u x 1 .u 1 , x 2 .u 2 ) ε) • If r = (µa.t ε), then r = (μa.t ε)
We denote red(t) the set of all redexes of t. Let R be a subset of red(t), we define tR the marked term obtained from t by marking each redex of t which belongs to R. We said that tR is the R-corresponding marked term to t.

4. Let ε ∈ E, we define the E-term ε by induction on ε:

• If ε ∈ E, then ε = ε • If ε = ( λx.u v), then ε = (λx.ǔ v) • If ε = (< t 1 , t 2 > π i ), then ε = ( ť1 , ť2 π i ) • If ε = (Ω i t [x.u, y.v]) or (Ω i t x.u, y.v ), then ε = (ω i ť [x.ǔ, y.v]) • If ε = (t ), then ε = ( ť ˇ ) • If ε = μa.u, then ε = µa.ǔ • If ε = x.u, y.v , then ε = [x.ǔ, y.v]
The operationˇquite simply consists in projecting any marked term in the set E, i.e, to consider any marked term as any other term without marks.

Example 6.2 Let t = ((µa.u [x.p, y.q]) ε), R = {(µa.u [x.p, y.q])}, S = {t}, K ⊆ red(p), L ⊆ red(u) ∪ red(ε) and T = {(µa.u [x.p, y.q]), t}, then tR = ((μa.u [x.p, y.q]) ε), tS = ((µa.u x.p, y.q ) ε), tK = ((µa.u [x.p K , y.q]) ε), tL = ((µa.û L [x.p, y.q]) εL ) and tT = ((μa.u x.p, y.q ) ε).

Remark 6.1 1. Let t be a term and R ⊆ red(t). It is clear that ťR = t.

2.

When there is only one given set R of redexes of a given term t, we use the abusive notation t to denote the R-corresponding marked term to t.

ť (t = ť0 R ť1 R ť2 ... R ť ).
2. The term t is said to be R-strongly normalizable iff there are no infinite Rdevelopments of t, i.e, all the R-developments are finite.

Remark 6.2 If t is a term and R a set of some redexes of t, then note that R and reduction are the same, any infinite sequence of reductions starting from t corresponds to an infinite sequence of * R reductions starting from t. Thus one can be able to identify them, this fact will be implicitly used in the next paragraph, where R and are confused. 1. A semi-permutative redex of ε is any initial segment in the form r[x.p, y.q]ε i , where (2 ≤ i ≤ m) and r is possibly empty.

2. A set of redexes of ε is the union of sets of redexes of each ε i and any possible semi-permutative redex of ε.

Lemma 6.3 Let t be a term, ū = u 1 ...u n a finite sequence of terms and ε = ε 1 ...ε m a finite sequence of E-terms. Let also σ = [(x i := u i ) 1≤i≤n ; (a j := * ε j ) 1≤j≤m ] and R be a set of redexes of t, ū and ε. If t, ū and ε are R-strongly normalizable, then tσ is R-strongly normalizable.

Proof First, let t = (u ε) as in the corollary 3.1. We prove this by induction on the ordered lexicographic pair (lg(ε), c) where lg(ε) is the number of E-terms of ε and c denotes the complexity of t. For the simplicity and the clearness of the proof, we prefer to avoid using marked terms.

1. The cases where t is not simple are direct consequences of induction hypothesis (decreasing of c).

2. The case t = (x i ¯ ): tσ = (u i ¯ σ), by induction hypothesis (u i and ¯ σ) are R-strongly normalizable, we have to examine two cases according to ¯ :

(a) If ¯ is a nice sequence: since we can not reduce the possible created redex (u i ¯ σ) and for the previous reasons, tσ is R-strongly normalizable. (b) If ¯ is not a nice sequence: = 1 ... j-2 [x.p, y.q] j ... k , let's denote ¯ σ by ¯ = 1 ... j-2 [x.p , y.q ] j ... k . Suppose that there exists a sequence of infinite R-reductions, starting from tσ as follows: (u

i 1 ... j-2 )[x.p , y.q ] j ... k * R (u i 1 ... j-2 )[x.p , y.q ] j ... k R (u i 1 ... j-2 )[x.(p j ), y.(q j )]... k = t * R .
... By the standardization theorem, tσ * st t , and this standard reductions is in the form:

(u i 1 ... j-2 )[x.p , y.q ] j ... k R (u i 1 ... j-2 )[x.(p j ), y.(q j )]... k (u i 1 ... j-2 )[x.(p j ), y.(q j )]... k = t * R .
...This means that (u i 1 ... j-2 )[x.(p j ), y.(q j )]... k * R , since we can not reduce the possible created redexes (p j ) and (q j ), thus we have a contradiction with induction hypothesis (decreasing of lg(¯ ) from k to k -1).

3. The case t = (µa.u ) ¯ , let's denote uσ, σ and ¯ by respectively by u , and ¯ , which are by induction hypothesis R-strongly normalizable. Therefore, if a sequence of infinite R-reductions exists, it will be in one of the two following forms: (b) Or ¯ is not a nice sequence, and we conclude as in the case 2.b of head variable x.

Theorem 6.1 Let t be a term and R ⊆ red(t), then t is R-strongly normalizable.

Proof

The proof is similar to the one of the previous lemma. Let t = (u ε) as in the corollary 3.1. We prove this by induction on the ordered lexicographic pair (lg(ε), c) where c denotes the complexity of t.

1. The cases where t is not simple are direct consequences of induction hypothesis (decreasing of c).

The case

t = (x ε) (a) If ε = ε 1 .
..ε m is nice, then, by induction hypothesis, each ε i is R-strongly normalizable. Therefore t too.

(b) Else t = (x ε 1 ...ε j-2 )[y.p, z.q]ε j ...ε m . Suppose that there exists a sequence of infinite R-reductions starting from t, then, by induction hypothesis, none of ε i contains infinite R-reduction. Therefore t = (x ε 1 ...ε j-2 )[y.p, z.q]ε j ...ε m * R (x ε 1 ...ε j-2 )[y.p , z.q ]ε j ...ε m R (x ε 1 ...ε j-2 )[y.(p ε j ), z.(q ε j )]...ε m = t j * R .... By the standardization theorem t * st t j , this standard reduction is in the form

t = (x ε 1 ...ε j-2 )[y.p, z.q]ε j ...ε m R (x ε 1 ...ε j-2 )[y.(p ε j ), z.(q ε j )]...ε m * R (x ε 1 ...ε j-2 )[y.(p ε j ), z.(q ε j )]...ε m . This means that (x ε 1 ...ε j-2 )[y.(p ε j ), z.(q ε j )]...ε m * R .
.., since we can not reduce the possible created redexes (p ε j ) or (q ε j ), this gives a contradiction with the induction hypothesis (decreasing of lg(ε), from m to m -1). In this proof we only mark the redexes which will be reduced.

-t = (x ε 1 )ε 2 ... r.u, s.v y.p, z.q ε j ...ε m , t 1 = (x ε 1 )ε 2 ... r.(u y.p, z.q ), s.(v y.p, z.q ) ε j ...ε m and t 2 = (x ε 1 )ε 2 ... r.u, s.v y.(p ε j ), z.(q ε j ) ...ε m . Therefore check that t 3 = (x ε 1 )ε 2 ... r.(u y.(p ε j ), z.(q ε j ) ), s.(v y.(p ε j ), z.(q ε j ) ) ...ε m is the commun marked redectum obtained of course by R-reductions.

-t = ((µa.u [x.r, y.s]) εε).

- 2. This is a direct consequence of (1), theorem 6.1 and Newman lemma. Proof This is a direct consequence of lemma 6.4 and theorem 6.2.

One of the consequences of the standardization theorem is that the normal form if it exists, it can be reached by the leftmost reduction. Theorem 6.4 If t is the normal form of t, then t * l t . Proof Since t * t , then there exists a standard reduction from t to t , i.e, t * st t . We process by induction on κ(t * st t ) = (n, c). The cases where t is not a simple term are direct consequences of induction hypothesis (decreasing of c). Let us examine the two following cases:

Proof ( 1 )

 1 By induction on C. (2) By induction on t. (3) By induction on C. Definition 3.2 Let ε = ε 1 ...ε n a sequence of E-terms.

  If ε = (a u), then ε = (a u ) where u * st u , thus, ε[a := * ] = (a (u[a := * ] )) and ε [a := * ] = (a (u [a := * ] )). By induction hypothesis, we have u[a := * ] * st u [a := * ], then, by definition, (a (u[a := * ] )) * st (a (u [a := * ] )).

Theorem 4 . 1 (

 41 Standardization theorem) If ε * ε , then ε * st ε .Proof By induction on the length of the reduction ε * ε it suffices to prove the following lemma.

Lemma

  2 does not hold for this sequence of reductions: ε ((µa.u [x.p, y.q]) [r.(k ), s.(l )]) (µa.u [x.(p [r.(k ), s.(l )]), y.(q [r.(k ), s.(l )])]) * st (µa.u [x.p , y.q ]) = ε µa.u[a := * [x.p , y.q ]]] = ε , where (p [r.(k ), s.(l )]) * st p and (q [r.(k ), s.(l )]) * st q , for the simple reason which is: we do not know how these two standard sequence reductions are made (p [r.(k ), s.(l )]) * st p and (q [r.(k ), s.(l )]) *

Theorem 5 . 1

 51 If t * L t , then this sequence of reductions is a standard one. Proof By induction on κ(t * L t ).

Definition 6. 1

 1

Lemma 6 . 2

 62 Let ε, ε , , be E-terms and R a set of redexes of ε and such that ε* R ε . If * R , then, ε[a := * ] * R ε [a := * ].Proof By induction on ε. Definition 6.3 Let ε = ε 1 ...ε m be a finite sequence of E-terms.

  (a) Either (µa.u ) ¯ * R (µa.u ) ¯ R (µa.u [a := * ] ¯ ) = t * R ..., by the standardization theorem, tσ * st t in following sequence: (µa.u ) ¯ R (µa.u [a := * ] ¯ ) * R (µa.u [a := * ] ¯ ) = t * R ... hence (µa.u [a := * ] ¯ ) * R ... and this gives a contradiction with the induction hypothesis (decreasing of lg(¯ ) from k to k -1).

3 .

 3 The case t = (µa.u ε)ε, this gives by induction hypothesis and the standardization theorem two possibilities to the form of the sequence of the R-infinite reductions:(a) t = (µa.u ε) ε 1 ...ε m R (µa.u[a := * ε] ε 1 ) ε 2 ...ε m * R (µa.u [a := * ε ] ε 1 ) ε 2 ...ε m * R .... This means that (µa.u[a := * ε] ε 1 ) ε 2 ...ε m * R .... By the lemma 6.3, u[a := * ε] is R-strongly normalizable,therefore this gives a condradiction with the induction hypothesis (decreasing of lg(ε), from m to m -1).(b) t = (µa.u ε) ε 1 ...[x.p, y.q]ε j ...ε m R (µa.u ε) ε 1 ...[x.(p ε j ), y.(q ε j )]...ε m * R (µa.u ε ) ε 1 ...[x.(p ε j ), y.(q ε j )]...ε m * R .... This means that (µa.u ε) ε 1 ...[x.(p ε j ), y.(q ε j )]...ε m * R .... By a similar argument as the previous, this gives a contradiction.

Theorem

  If t 1 = ((µa.u [x.r, y.s]) εε) and t 2 = (µa.u [a := * [x.r, y.s]] εε), then, by the lemma 6.2, we take t 3 = (µa.u [a := * [x.r, y.s]] εε). -If t 1 = ((µa.u [x.r, y.s]) εε) and t 2 = ((µa.u [x.(r ε), y.(s ε)]) ε), then we take t 3 = ((µa.u [x.(r ε), y.(s ε)]) ε). -If t 1 = (µa.u[a := * [x.r, y.s]] εε) and t 2 = ((µa.u [x.(r ε), y.(s ε)]) ε), then, both of the commutative and the classical redexes are marked redexes in t = ((μa.u x.r, y.s ) εε), hence t1 = (μa.u[a := * x.r, y.s ] εε) R (μa.u[a := * x.r, y.s ε] ε) R (μa.u[a := * x.(r ε), y.(s ε) ]ε) = t 3 , and t 2 = ((μa.u x.(r ε), y.(s ε) ) ε) R (μa.u[a := * x.(r ε), y.(s ε) ] ε) = t 3 . It is obvious that ť3 = (µa.u[a := * [x.(r ε), y.(s ε)]]ε) is the commun redectum.

Lemma

  |µa.C We consider only general contexts with different holes, i.e, if * i1 , ..., * in are the holes of a general context C, then, * ip = * iq for each p = q. If C is a context with holes * 1 , ..., * n and t 1 , ..., t n are terms, then C[t 1 , ..., t n ] is the term obtained by replacing each * i by t i . The free variables of t i can be captured in the term C[t 1 , ..., t n ]. Let t 1 , ..., t n , t 1 , ..., t m be simple terms and C, C two contexts. If C[t 1 , ..., t n ] = C [t 1 , ..., t m ], then C = C . 2. Each term t can be uniquely written as C[t 1 , ..., t n ], where C is a context and t 1 , ..., t n are simple terms. 3. Let t = C[t 1 , ..., t i , ..., t n ] be a term and r a redex of t i . If t r t , then t i

	3. Let C be a general context with holes * i1 , ..., * in and f a bijection from N to N,
	then, the general context f (C) is the context C with the holes * f (i1) , ..., * f (in) ,
	i.e, f (C) is the general context C just with a different enumeration of its
	holes. Let C, C be two general contexts. We said that C is equivalent to C
	and denote this by C C , if there exists a bijection f from N to N such that
	C = f (C). Thus, if C	C, then C and C have the same number of holes.
	4. A context is an equivalent class for the previous equivalent relation. Then we
	can always suppose that the n holes of a context are * 1 , ..., * n in this given
	order.
	5. Lemma 3.1	1. r
	C i [t i 1 , ..., t i m ] and t = C [t 1 , ..., t i-1 , t i 1 , ..., t i m , t i+1 , ..., t n ] where C = C[ * i :=
	C i ].

  Definition 5.1 1. Let C[t 1 , ..., t n ] as in (2) of the lemma 3.1. A one step head reduction of a simple term t consists in reducing a head redex if any. We denote t hd t if t is reduced to t by a head reduction. A one step head reduction of a term C[t 1 , ..., t n ] corresponds to a one step head reduction of one of the simple terms t i (1 ≤ i ≤ n). We denote by * hd the reflexive and transitive closure of hd .

  then either t hd (µa.u[a := * ε] ε) * L t or t hd ((µa.u ) r) * L t where εε r. Therefore, by induction hypothesis (decreasing of the length lg), (µa.u[a := * ε] ε) * L t and ((µa.u ) r) * L t are two standard sequence reductions, thus, by definition, both of t hd (µa.u[a := * ε] ε) * L t and t hd ((µa.u ) r) * L t are standard sequence reductions too.

  3. Observe that terms in the forms λx.t, < t 1 , t 2 > and Ω i t are not elements of E. Marks can only occur as marks of redexes except in terms of the form μa.t and the form (t x.u, y.v ). It follows that a -normal form never contains any marks except μ or . , . .The following lemma shows that the set of marked terms is closed under substitutions and reductions. Let t be a term and R a subset of red(t). It is denoted by t * t if it finishes with the marked term t . We denote it also by t *

	6.2 Finiteness developments theorem
	Definition 6.2 1. A sequence of reductions t = t 0	t 1	t 2	... is called R-development of t.
		R
	4. It is also clear that any term is a -normal marked term (since	consists
	only in reducing marked redexes).
	Lemma 6.1	1. If t, u, ∈ E, then t[x := u], t[a := * ] ∈ E.
	2. If t ∈ E and t * t , then t ∈ E.
	3. If t, ε, ∈ E, t	t , ε	ε and	*	, then ε[x := t] * ε[x := t ] and
	ε[a := * ] * ε[a := * ].
	Proof Easy.

  6.2 (Confluence of R ) Let t, t 1 , t 2 be terms and R ⊆ red(t). 1. If t R t 1 and t R t 2 , then there exists t 3 such that t 1 * R t 3 and t 2 * R t 3 . 2. If t * R t 1 and t * R t 2 , then there exists t 3 such that t 1 * R t 3 and t 1 * R t 3 . Proof 1. By induction on the complexity of t. Let us check the following cases, the other cases are simple consequences of the induction hypothesis.

  6.4 If t * t , then t = t 0 * red(t0) t 1 * red(t1) t 2 * red(t2) ... * red(tn) t n+1 = t . Proof Easy. Remark 6.3 It is easy to see that if u * red(u) v * red(u) w, then v * red(v) w. Now the main result of this paper can be easily established. Theorem 6.3 (Confluence of ) Let t, t 1 , t 2 be terms such that t * t 1 and t * t 2 , then there exists t 3 such that t 1 * t 3 and t 1 * t 3 .

The meaning of the new constructors is given by the typing rules below where Γ (resp ∆) is a context, i.e, a set of declarations of the form x : A (resp a : A) where x is a λ-variable (resp a is a µ-variable) and A is a formula.Γ, x : Ax : A ; ∆ ax Γ, x : A t : B; ∆ Γ λx.t : A → B; ∆ → i Γ u : A → B; ∆ Γ v : A; ∆ Γ (u v) : B; ∆ → e

e Γ t : A; ∆ Γ ω 1 t : A ∨ B; ∆ ∨ 1 i Γ t : B; ∆ Γ ω 2 t : A ∨ B; ∆ ∨ 2 i Γ t : A ∨ B; ∆ Γ, x : A u : C; ∆ Γ, y : B v : C; ∆ Γ (t [x.u, y.v]) : C; ∆ ∨ e

Acknowledgments: We wish to think R. Matthes and the anonymous rapporteur for the many exchanges and the rich discussions.

-t = (x ε) -If ε = ε 1 ...ε n is nice, then t = (x ε ) where ε = ε 1 ...ε n and each ε i * ε i normal. Therefore the induction hypothesis concludes.

-Else t = ((x r[y.p.z.q])ε i k) and the standard reduction is in the form

Therefore by induction hypothesis (decreasing of n), we have that ((x r)[y.(p ε i ).z.(q ε i )]) k) * l t . Thus t = ((x r)[y.p.z.q]ε i k) l ((x r)[y.(p ε i ).z.(q ε i )]) k) * l t . -t = ((µa.u ε) ε), then the standard reduction from t to the normal form t is in the following forms:


René David
email: david@univ-savoie.fr

Karim Nour
email: nour@univ-savoie.fr

About the range property for H

) has shown that the range property fails for H. We give here some conditions on a closed term that imply that its range has an infinite cardinality.

Introduction 1.Our motivations

Let T be a λ-theory. The range property for T states that if λx.F is a closed λ-term, then its range (considering λx.F as a map from M to M where M is the algebra of closed λ-terms modulo the equality defined by T ) has cardinality either 1 or Card(M). It has been proved by Barendregt in [START_REF] Barendregt | Constructive proofs of the range property in Lambda Calculus[END_REF] that the range property holds for all recursively enumerable theories. For the theory H equating all unsolvable terms, the validity of the range property has been an open problem for a long time. Very recently A. Polonsky has shown (see [START_REF] Polonsky | The range property fails for H[END_REF]) that it fails.

In an old attempt to prove the range property for H, Barendregt (see [START_REF] Barendregt | Towards the range property for the lambda theory H[END_REF]) suggested a possible way to get the result. The idea was, roughly, as follows. First observe that, if the range of a term is not a singleton, it will reduce to a term of the form λx.F [x]. Assuming that, for some A, F [x := A] = H F [x := Ω], he proposed another term A (the term J ν • A of Conjecture 3.2 in [START_REF] Barendregt | Towards the range property for the lambda theory H[END_REF]) having a free variable ν that could never be erased or used in a reduction of F [x := A ]. He claimed that, by the properties of the variable ν, the terms F [x := A n ] should be different where A n = A [ν := c n ] and c n is, for example, the Church numeral for n. It has been rather quickly understood by various researchers that the term proposed in [START_REF] Barendregt | Towards the range property for the lambda theory H[END_REF] actually had not the desired property and, of course, Polonsky's result shows this method could not work. Moreover, even if the term A had the desired property it is, actually, not true that the terms F [x := A n ] would be different: see section 1.3 below.

Our results

Even though the failure of the range property for H is now known, we believe that having conditions which imply that the range of a term is infinite is, "by itself" interesting. We also think that the idea proposed by Barendregt remains interesting and, in this paper, we consider the following problem.

Say that F has the Barendregt's persistence property if for each A such that F [x := A] = H F [x := Ω] we can find a term A that has a free variable ν that could never be erased or applied in a reduction of F [x := A ] (see definition 3.7).

We give here some conditions on terms that imply the Barendregt's persistence property. Our main result is Theorem 3.2. It can be stated as follows. Let F be a term having a unique free variable x and A be a closed term such that F [x := A] = H F [x := Ω]. We introduce a sequence (F k ) k∈N of reducts of F that can simulate (see Lemma 3.4) all the reductions of F . By considering, for each k, the different occurrences of x in F k we introduce a tree T and a special branch in it (see Theorem 3.1). Denoting by x (k) the corresponding occurrence of x in F k , Theorem 3.2 states that :

(1) If, for k ∈ N, the number of arguments of x (k) in F k is bounded, F has the Barendregt's persistence property.

(2) Otherwise and assuming the branch in T is recursive there are two cases.

(2.a) If some of the arguments of x (k) in F k come in head position infinitely often during the head reduction of F [x := A], then F has the Barendregt's persistence property.

(2.b) Otherwise, it is possible that F does not have the Barendregt's persistence property.

In case [START_REF] Barendregt | The Lambda Calculus, Its Syntax and Semantics[END_REF] we give two arguments. The first one is quite easy and uses this very particular situation. It gives a term A where ν cannot be erased but we have not shown that it is never applied (it is not applied only in the branch defined in section 3). The second one (which is more complicated) is a complete proof that F has the Barendregt's persistence property. It can also be seen as an introduction to the more elaborate case 2.(a). For case 2.(b) we give examples of terms F for which there is no term having this property.

A final remark

Note that, actually, even if a term A having the Barendregt's persistence property can be found this would not give an infinite range for λx.F . This is due to the fact that the property of A does not imply that

F [x = A n ] = H F [x = A m ] for n = m where A k = A [ν = c k ]
and c k is the Church integer for k. This is an old result of Plotkin (see [START_REF] Plotkin | The λ-calculus is ω-incomplete[END_REF]). Thus, having an infinite range will need another assumption. We will also consider this other assumption and thus give simple criteria that imply that the range of λx.F is infinite.

The paper is organized as follows. Section 2 gives the necessary definitions. Section 3 considers the possible situations for F and states our main result. Section 4 and 5 give the proof in the cases where we actually can find an A . Section 6 gives some complements.

Preliminaries

Notation 2.1

1. We denote by Λ • the set of closed λ-terms. 3. #(t) is the code of t i.e. an integer coding the way t is built.

4. We denote by the β-reduction, by Ω the Ω-reduction (i.e. t Ω Ω if t is unsolvable), by h the head β-reduction and by βΩ the union of and Ω .

5. If R is a notion of reduction, we denote by R * its reflexive and transitive closure.

6. Let x be a free variable of a term t. We denote by x ∈ βΩ(t) the fact that x does occur in any t such that t * βΩ t . 7. As usual (u t 1 t 2 ... t n ) denotes (...((u t 1 ) t 2 ) ... t n ). (u n v) will denote (u (u ... (u v)...)) and (v u ∼n ) will denote (v u ... u) with n occurrences of u.

Notation 2.2

1. Unknown sequences (possibly empty) of abstractions or terms will be denoted with an arrow. For example λ -→ z or -→ w . However, to improve readability, capital letters will also be used to denote sequences. The notable exceptions are F, A, J taken from Barendregt's paper or standard notations for terms as I, K, Ω. When the meaning is not clear from the context, we will explicitly say something as " the sequence λ -→ z of abstractions".

2. For example, to mean that a term t can be written as some abstractions followed by the application of the variable x to some terms, we will say that

t = λ - → z .(x - → w ) or t = λZ.(x W ).
3. If R, S are sequences of terms of the same length, R * S means that each term of the sequence R reduces to the corresponding term of the sequence S.

(λx.F ) = {[F [x := u]] H / u ∈ Λ • }.
3. A closed term λx.F has the range property for H if the set (λx.F ) is either infinite or has a unique element.

Theorem 2.2 There is a term λx.F ∈ Λ • that has not the range property for H.

Proof See [START_REF] Polonsky | The range property fails for H[END_REF].

Definition 2.2 Let U, V be finite sequences of terms.

1. We denote by U :: V the list obtained by putting U in front of V .

U

V means that some initial subsequence of V is obtained from U by substitutions and reductions.

Lemma 2.2

1. U V iff there is a substitution σ such that σ(U ) reduces to an initial segment of V . for some -→ w . The only problem in making this definition precise is that, during the reduction of C to λ -→ x .([] -→ w ) the potentially free variables of u may be substituted and we have to deal with that. The notations and tools developed in, for example, [START_REF] David | Computing with Böhm trees[END_REF], [START_REF] David | Nour Storage operators and directed lambda-calculus[END_REF] allows to do that precisely. Since this is intuitively quite clear and we do not need any technical result on this definition, we will not go further.

3 The different cases ¿From now on, we thus fix terms F and A. We assume that:

• F is not normalizable and has a unique free variable denoted as x such that x ∈ βΩ(F ). In the rest of the paper we will write t

[A] instead of t[x := A]. • F [A] F [Ω] Notation 3.1 1.
The different occurrences of a free variable x in a term will be denoted as x [i] for various indexes i.

2. Let t be a term and x [i] be an occurrence of the (free) variable x in t. We denote by Arg(x [i] , t) (this is called the scope of x [i] in [START_REF] Barendregt | The Lambda Calculus, Its Syntax and Semantics[END_REF]) the maximal list of arguments of

x [i] in t i.e the list V such that ([] V ) is the applicative context of x [i] in t.
Since Arg(x [i] , t) may contain variables that are bounded in t and since a term is defined modulo α-equivalence, this notion is not, strictly speaking, well defined. This is not problematic and we do not try to give a more formal definition.

Lemma 3.1 Assume u * v and x [i] (resp. x [j] ) is an occurrence of x in u (resp. v) such that x [j] is a residue of x [i] . Then Arg(x [i] , u) Arg(x [j] , v).

Proof

Since the relation is transitive it is enough to show the result when u v. This is easily done by considering the position of the reduced redex. Definition 3.1 Let x [i] be an occurrence of x in some term t. We say that x [i] is pure in t if there is no other occurrence x [j] of x in t such that x [i] occurs in one of the elements of the list Arg(x [j] , t).

For example, let t = (x (x y)). It can be written as (x [START_REF] Barendregt | The Lambda Calculus, Its Syntax and Semantics[END_REF] (x [START_REF] Barendregt | Constructive proofs of the range property in Lambda Calculus[END_REF] y)) where the occurrence x [START_REF] Barendregt | The Lambda Calculus, Its Syntax and Semantics[END_REF] is pure but x [START_REF] Barendregt | Constructive proofs of the range property in Lambda Calculus[END_REF] is not pure and Arg(x [START_REF] Barendregt | The Lambda Calculus, Its Syntax and Semantics[END_REF] , t) = (x [2] y).

Note that, if x [START_REF] Barendregt | The Lambda Calculus, Its Syntax and Semantics[END_REF] , ..., x [n] are all the pure occurrences of x in t, there is a context

C with holes [] 1 , ..., [] n such that t = C[[] i = (x [i] Arg(x [i] , t)) : i = 1...n]
and x does not occur in C. Lemma 3.2 Let t, t be some terms such that t reduces to t . Assume that

x [i ] is a residue in t of x [i] in t and x [i ] is pure in t . Then x [i] is pure in t. Proof Immediate.
The next technical result is akin to Barendregt's lemma discussed by de Vrijer in Barendregt's festschrift (see [START_REF] De Vrijer | Barendregts lemma[END_REF]). It has a curious history discussed there. First proved by van Dalen in [START_REF] Van Daalen | The Language Theory of Automath[END_REF], it appears as an exercise in Barendregt's book at the end of chapter 14. Its truth may look strange. Note that the reductions coming from the term B are done in the holes of the reduct G of F . Lemma 3.3 Let B be a closed term. Assume F [B] * t. Then there is a G such that

• F * G = D[[] i = w i : i ∈ I] where D is a context with holes [] i (indexed by the set I of all the pure occurrences x [i] of x in G) and w i = (x [i] Arg(x [i] , G)). • t = D[[] i = w i : i ∈ I] where w i [B] * w i . Proof By induction on lg(F [B] * t), cxty(F ) where lg(F [B] * t) is the length of a standard reduction of F [B]
to t and cxty(F ) is the complexity of F , i.e the number of symbols in F .

-If F = λy.F , then t = λy.t where

F [B] * t . Since lg(F [B] * t) = lg(F [B] * t )
and cxty(F ) < cxty(F ), we conclude by applying the induction hypothesis on the reduction F [B] * t .

-

If F = (y F 1 ...F n ), then t = (y t 1 ...t n ) where F i [B] * t i . Since lg(F i [B] * t i ) ≤ lg(F [B] * t)
and cxty(F i ) < cxty(F ), we conclude by applying the induction hypothesis on the reductions

F i [B] * t i . -If F = (λy.U V F 1 ...F n )
where the head redex is not reduced during the reduction

F [B] * t, then t = (λyu v f 1 ...f n ) where U [B] * u, V [B] * v and F i [B] * f i . Since lg(U [B] * u) ≤ lg(F [B] * t), lg(V [B] * v) ≤ lg(F [B] * t) , lg(F i [B] * f i ) ≤ lg(F [B] * t), cxty(U ) < cxty(F ), cxty(V ) < cxty(F ) and cxty(F i ) < cxty(F ),

we conclude by applying the induction hypothesis on the reductions U

[B] * u, V [B] * v, F i [B] * f i .
-If F = (λy.U V -→ F ) and the first step of the standard reduction reduces the head redex, then

F [B] = (U [y := V ] - → F )[B] * t. Let F = (U [y := V ] - → F ). Since lg(F [B] * t) < lg(F [B] * t)
, we conclude by applying the induction hypothesis on the reduction F [B] * t.

-If F = (x -→ F ), then G = F and D is the term made of a single context [] and w = F .

The next lemma concerns the reduction of F under a recursive cofinal strategy. The canonical one is the Gross-Knuth strategy, where one takes, at each step, the full development of the previous one.

Lemma 3.4 There is a sequence (F k ) k∈N such that 1. F 0 = F and, for each k, F k * F k+1 . 2. If F * G, then G * F k for some k. 3. The function k → #(F k ) is recursive. Proof
By Theorem 2.1, choose F k+1 as a common reduct of F k and all the reducts of F in less than k steps. Definition 3.2 Let x [i] be an occurrence of x in some F k . We say that x [i] is good in F k if it satisfies the following properties:

• x [i] is pure in F k . • u[A] is solvable for every sub-term u of F k such that x [i] occurs in u.

Note that this implies that (x

[i] Arg(x [i] , F k ))[A] is solvable.
Observe that every pure occurrence of x in F k+1 is a residue of a pure occurrence of x in F k . This allows the following definition.

Definition 3.3

1. Let T be the following tree. The level k in T is the set of pure occurrences of x in F k . An occurrence

x [i] of x in F k+1 is the son of an occurrence x [j] of x in F k if x [i] is a residue of x [j] . 2. A branch in T is good if, for each k, the occurrence x [k] of x in F k chosen by the branch is good in F k .
Theorem 3.1 There is an infinite branch in T that is good. Proof By Konig's Lemma it is enough to show: (1) for each k, there is an occurrence of x in F k that is good and (2) if the son of an occurrence

x [i] of x is good then so is x [i] .
(1) Assume first that there is no good occurrences of x in F k . This means that, for all pure occurrences

x [i] of x in F k , either (x [i] Arg(x [i] , F k ))[A] is unsolvable or this occurrence appears inside a sub-term u of F k such that u[A] is unsolvable. But, if (x [i] Arg(x [i] , F k ))[A] is unsolvable then so is (x [i] Arg(x [i] , F k ))[Ω] and, if u[A] is unsolvable, then so is u[Ω] (proof :

consider the head reduction of u[A]

; either A comes in head position or not ; in both cases the result is clear). This implies that

F [A] F [Ω].
(2) follows immediately from the fact that a residue of an unsolvable term also is unsolvable and that, if

(x U )[A] is unsolvable and U V then so is (x V )[A]. Example Let G be a λ-term such that G * λuλv.(v (G (x u) v)) and F = (G I). If we take λv.(v k (G (x (x ...(x I))) v)) for F k , what is the good occurrence of x in F k which appears in a good branch in T ? It is none of those in (x (x ...(x I))...), it is the one in G !
From now on, we fix an infinite branch in T that is good Notation 3.2 We denote by x (k) the occurrence of x in F k chosen by the branch. Let U k = Arg(x (k) , F k ). Lemma 3.5 There is a sequence (σ k ) k∈N of substitutions and there are sequences (S k ) k∈N , (R k ) k∈N of finite sequences of terms such that, for each k, R k is obtained from σ k (U k ) by some reductions and U k+1 = R k :: S k . Proof This follows immediately from Lemma 3.1.

Definition 3.4

We define the sequence V k by : V 0 = U 0 and

V k+1 = σ k (V k ) :: S k . Lemma 3.6 1. For each k, V k * U k . 2. For each k > k, there is a substitution σ k k such that σ k k (S k ) is a sub- sequence of V k . Proof
This follows immediately from Lemma 3.5.

If k = k + 1, σ k k = id. Otherwise σ k k = σ k -1 • σ k -2 • ... • σ k+1 Definition 3.5
We define, by induction on k, the sequence ρ k of reductions and the terms t k as follows.

1. ρ 0 is the head reduction of (A V 0 [A]) to its head normal form.

2. t k = λ - → z k . (y k -→ w k ) is the result of ρ k .
3. ρ k+1 is the head reduction of (σ k (t k ) S k [A]) to its head normal form.

Lemma 3.7 The term t k is the head normal form of (A V k [A]). Proof Easy.

Notation and comments

1. Denote by ρ the infinite sequence of reductions ρ 0 , ρ 1 , ..., ρ k , .... Note that it is not the reduction of one unique term. ρ 0 computes the head normal form t 0 of (A V 0 [A]). The role of σ 0 is to substitute in the result the substitution that changes U 0 into the first part of U 1 . Note that, by Lemma 3.5, this first part may also have been reduced but here we forget this reduction. Then we use ρ 1 to get the head normal form t 1 of (σ 0 (t 0 ) S 1 [A]) and keep going like that.

2. Note that, by Lemma 3.6 and 3. (a) Say that ν is never applied in a reduct of t if no reduct t of t contains a sub-term of the form (ν u).

(b) Say that ν is persisting in t if ν ∈ βΩ(t) and ν is never applied in any reduct of t.

2. We say that the term F has the Barendregt's persistence property if we can find a term A that has a free variable ν that is persisting in F [A ].

Comment and example

1. The condition "ν is never applied" in the previous definition implies that, letting

A n = A [ν = c n ], a reduct of F [A n ] is, essentially, a reduct of F [A ].
2. Here is an example. Let G be a λ-term such that G * λuλv.(v (G (u I) v)) and F = (G x). We can take λz.(z k (G (x

I ∼k ) z)) for F k . It follows easily that F [I] F [Ω]. We have U k = I ∼k , S k = I, t k = I and σ k = id.
Let J be a λ-term such that J * λuλvλy.(v (J u y)) and I = (J ν I).

If F [I ] * t, then, by Lemma 3.3, t * λz.(z n (G I z)) for some n where I is a reduct of (I I ∼n ). It is easily checked that ν is persisting in

F [I ]. Since no c n occurs as a sub-term of a reduct of F [I ], it is not difficult to show that, if n = m, then F [I n ] F [I m ] where I n = I [ν := c n ] and thus (λx.F ) is infinite. Theorem 3.2
1. Assume first that the length of the U k are bounded. Then, F has the Barendregt's persistence property.

2. Assume next that the length of the U k are not bounded and the branch we have chosen in T is recursive.

(a) If the set of those k such that S k comes in head position during ρ is infinite, then F has the Barendregt's persistence property.

(b) Otherwise it is possible that F does not have the Barendregt's persistence property. Proof 1. It follows immediately from Lemma 3.1 that there are l, k 0 > 0 such that for all k ≥ k 0 , lg(U k ) = l. The fact that F has the Barendregt's persistence property is proved in section 4.

(a)

The fact that F has the Barendregt's persistence property is proved in section 5.

(b) There are actually two cases and the reasons why we cannot find a term A are quite different.

i. For all k there is k > k such that y k ∈ dom(σ k ). The fact that the head variable of t k may change infinitely often does not allow to use the technic of sections 4 or 5. A. Polonsky has given a term F that corresponds to this situation and such that a variable ν can never be persisting in a term A of the form λx 1 ...x n .(x i w 1 ... w m ). See example 1 below. ii. For some k 1 , y k ∈ dom(σ k ) for all k ≥ k 1 . Since there are infinitely many k ≥ k 1 such that S k is non empty this implies that, after some steps, t k does not begin by λ. Thus, there is k 2 and y, such that, for all k ≥ k 2 , t k = (y -→ w k ). Using the technic of sections 4 or 5 allows to put a term J in front of some (fixed) element of the sequence -→ w k but this is not enough to keep ν. We adapt the example of A. Polonsky to give a term F that corresponds to this situation and such that a variable ν can never be persisting in a term A of the form λx 1 ...λx n .(A w 1 ... w n ) where w j λy 1 ...λy rj .(x j w j 1 ...w j rj ). See example 2 below. Comments 1. For case 1. we will give two proofs. The first one is quite simple. The second one is much more elaborate and even though it, actually, does not work for all the possible situations, we give it because it is an introduction to the more complex section 5. In the first proof, we simply use the fact that the length of the U k are bounded to find a term A that has nothing to do with A. In the second proof and in section 5, the term A that we give has the Bargendregt's property and behaves like A (using the idea of [START_REF] Barendregt | Towards the range property for the lambda theory H[END_REF]) in the sense that it looks like an infinite η-expansion of A.

2. When we say, in case 2.(b) of the theorem, that it is possible that F does not have the Barendregt's persistence property we are a bit cheating. We only show (except in example 1) that there is no A with a persisting ν satisfying an extra condition. This condition is that A looks like A i.e. the first levels of the Böhm tree of A must be, up-to some η-equivalence, the same as the ones of A.

3. It is known that there are recursive (by this we mean that we can compute their levels) and infinite trees such that each level is finite and that have no recursive infinite branch. We have not tried to transform such a tree in a lambda term such that the corresponding T has no branch that is good and recursive but we guess this is possible. We have

F * λyλz.(z n (G λvλw.(w m (H (K n v) (x y (K n v) ∼m ) w)) z)) and it is clear that F [I] F [Ω]. Let I λxλx 1 .
..λx r .(x w 1 ...w r ) where, for 1 ≤ j ≤ r, w j λy 1 ...λy rj (x j w j 1 ...w j rj ). For n ≥ max 1≤j≤r (r j ),

F [I ] λyλz.(z n (G λvλw.(w m (H (K n v) (y w 1 ...w r ) w)) z))
for some w j where ν does not occur and thus ν is not persisting in F [I ].

Note, however, that ν is persisting in F [I ] where I = λz.(z ν).

4 Case 1 of Theorem 3.2

We assume in this section that we are in case 1. of Theorem 3.2.

A simple argument

Let A = λx 1 ...λx l λz.(z ν) where l is a bound for the length of the U k . We show that ν ∈ βΩ(F [A ]). It is easy to show that ν is never applied in the terms (A U k [A ]) but the fact that ν is never applied in a reduct of F [A ] is not so clear. Since, because of the next section, we do not need this point we have not tried to check.

If

F [A ] * H * Ω G. By Lemma 3.3, F * F = D[[] i = w i : i ∈ I], w i = (x (i) Arg(x (i) , F )) and H = D[[] i = w i : i ∈ I] where w i [A ] * w i .
Let k be such that F F k . Let i 0 ∈ I be such that the occurrence of x (k) in F k chosen by the good branch is a residue of the occurrence of x [i0] in F . By Lemma 3.1, the length of Arg(x [i0] , F ) is bounded by l and thus w i0 = λx q ...x l λz.(z ν) for some q ≤ l.

It remains to show that the sub-term λz.(z ν) of w i0 cannot be erased in the Ω-reduction from H to G. Assume it is not the case. Then, there is a sub-term

D of D containing the hole [] i0 such that D [[] i = w i : i ∈ I] is unsolvable. D [[] i = w i ]
is solvable (since, otherwise, the occurrence x [k] will be in an unsolvable sub-term of F k and this contradicts the fact that x [k] is good). Since the reduction D

[[] i = w i ] * D [[] i = w i ]
only is inside the w i , since the first term is solvable and the second one is not, then, by the Church-Rosser property, the head variable of the head normal form of D

[[] i = w i ] is an occurrence of x. By Lemma 3.2, x [i0] is pure in F . x [i0] is not the head variable of the head normal form of D [[] i = w i ]
(since, otherwise, by the Church-Rosser property, D [[] i = w i ] would be solvable). Contradiction.

The proof

There are actually different situations.

Either, for some k

1 ≥ k 0 , y k ∈ - → z k for any k ≥ k 1 . Since for k ≥ k 1 , S k is
empty and the head variable of t k is not substituted, there is -

→ z and z ∈ - → z , such that, for k ≥ k 1 , t k = λ - → z . (z -→ w k ).
2. Or y k ∈ -→ z k for all k ≥ k 0 and (a) Either the situation is unstable (i.e. the set of those k such that

y k ∈ dom(σ k ) is infinite). (b) Or, there is - → z , y ∈ - → z and k 1 ≥ k 0 , such that, for k ≥ k 1 , t k = λ - → z . (y -→ w k ).
We assume that we are in situation 1. or 2.(b) which may be synthesized by: there exists k 0 and some fixed variable y (that may be in -→ z or not), such that, for all k ≥ k 0 , t k = λ -→ z . (y -→ w k ) for some -→ w k . We fix p ≥ lg( -→ z ) + l + 2 where l is a bound for the length of the U k . Let A = (J ν A) where J is a new constant with the following reduction rule (J ν u) λy 1 ...λy p .(u (J ν y 1 )...(J ν y p ))

We will prove that ν is persisting in

F [A ].
The term A is not a pure λ-term since the constant J occurs in it. We could, of course, replace this constant by a λ-term J that has the same behavior, e.g. (Y λkλy 1 ...λy p .(u (k ν y 1 )...(k ν y p ))) where Y is the Turing fixed point operator. But such a term introduces some problems in Lemma 4.4 because J and (J ν) contain redexes and can be reduced. With such a term J , though intuitively true, this lemma (as it is stated) does not remain correct.

Making this lemma correct (with J instead of a constant) will require the treatment of redexes inside J and (J ν). The reader should be convinced that this can be done but, since it would need tedious definitions, we will not do it.

Note that, in situation 2.(a), we cannot do the kind of proof given below. Here is an example. Let G be a λ-term such that G * λuλv.(v (G λy.(u (K y)) v)) and F = (G x). We can take λz.(z k (G λy.(x (K k y)) z) for F k . We thus have

U k = (K k y), t k = λz 1 ...λz k . y and σ k = [y := (K y)]. It is clear that F [I] F [Ω]. But F [I ] * λz.(z k (G I z)) for any I λyλy 1 ...λy k . (y w 1 ...w k )
where ν is possibly free in the w i . Thus ν is not persisting in F [I ].

Some preliminary definitions and results

When, in a term t, we replace some sub-term u by (J ν u) to get t , the reducts u (resp. u ), of t (resp. of t ) are very similar. The goal of this section is to make this a bit precise. Definition 4.1

1. We define, for terms u, the sets E u of terms by the following grammar:

E u = u |(J ν e u ) |λ - → y .(e u - → e y )
2. Let t, t be some terms. We denote by t t if there is a context C with one hole such that t = C[u] and t = C[u ] where u ∈ E u .

Notations and comments

1. Note that, in the previous definition as well as in the sequel, e u always denotes a term in E u and, for a sequence -→ y of variables , -→ e y always denote a sequence of terms -→ v (of the same length as -→ y ) such that for each variable y in -→ y , the corresponding term in -→ v is a member of E y . Also note that, in the previous definition, for a term λ -→ y .(e u -→ e y ) to be in E u , we assume that the variables in -→ y do not occur in e u .

2. t t means that t is obtained from t by replacing some sub-term u of t by (J ν u) or by reducing redexes introduced by J i.e. the one coming from its reduction rule (J ν u) λy 1 ...λy p .(u (J ν y 1 )...(J ν y p )) and those whose λ's are among λy 1 ...λy p .

Lemma 4.1 1. If t ∈ E z and t ∈ E u then t[z := t ] ∈ E u 2. If a a and b b , then a[x := b] * a [x := b ] 3. If u * u and if v is an Ω-redex in u , then v * v for some Ω-redex v in u.
4. If t ∈ E u then t * λ -→ y (u -→ e y ) for some -→ e y .

Proof 1, 2 and 3 are immediate. 4 is proved by induction on the number of rules used to show t ∈ E u . For the second point, we do the proof for one step of reduction u v and we use the first point and Lemma 4.1.

Lemma 4.3 1. If -→ λx.(x - → c ) * u, then u * -→ λx -→ λy.(x - → c - → e y ) for some - → c * - → c and some - → e y . 2. If u * -→ λx.(x - → c ) and u * u , then u * -→ λx -→ λy.(x - → c - → e y ) for some - → c * - → c and some - → e y .
Proof 1. We do the proof on an example. It is clear that this is quite general. Assume

λx 1 λx 2 (x c 1 c 2 ) * u, then u ∈ E λx1u1 , u 1 ∈ E λx2u2 , u 2 ∈ E (v1 c 2 ) , v 1 ∈ E (v2 c 1 ) , v 2 ∈ E x , c 1 * c 1 and c 2 * c 2 .
The β-reduction is done starting from inside and the propagation is done by using Lemma 4.1.

It is a consequence of the first point and Lemma 4.2.

The next lemma means that, when a redex appears in some u where u * u , it can either come from the corresponding redex in u, or has been created by the transformation of an application in u that was not already a redex or comes from the replacement of some sub-term u by, essentially, (J ν u). • or R = (J ν a ), u = C[a] for some context C and some term a such that C * C and a * a .

2. Assume u * u and u * v . Then v * v for some v such that u * v. Proof For the first point, there are two cases. Either the redex R is the residue of a redex in u or it has been created by the operations from the grammar E.

For the second point, it is enough to prove the result for one step of reduction u v . Use the first point. Definition 4.2 Let t be a solvable term. We say that:

1. ν occurs nicely in t if the only occurrences of ν are in a sub-term of the form (J ν).

2. ν occurs correctly in t if it occurs nicely in t and the head normal form of t looks like -→ λx.(x -→ c -→ e y ) for some final subsequence -→ y of -→ x of length at least 1 such that ν does occur in -→ e y .

Lemma 4.5 Let t be a solvable term. Assume that ν occurs nicely (resp. correctly) in t. Then ν occurs nicely (resp. correctly) in every reduct of t.

Proof By the properties of J.

Lemma 4.6 The variable ν is never applied in a reduct of

F [A ].
Proof The variable ν occurs nicely in F [A ], then, by Lemma 4.5, it occurs nicely in every reduct of

F [A ], thus ν is never applied in a reduct of F [A ]. 4.2.2 End of the proof Proposition 4.1 For k ≥ k 0 , ν occurs correctly in (A V k [A]). Proof (A V k [A]) * (A (J ν V k [A]
)) (note that this last term may be misunderstood : it actually means (A (J ν a 1 ) ...

(J ν a q )) where V k [A] is the sequence a 1 ...a q ) and (A V k [A]) * h λ - → z .(y -→ w k ). Thus, by Lemma 4.3, (A (J ν V k [A])) * -→ λz -→ λx.(y -→ w k - → e x )
for some -→

w k * -→ w k and - → e x . But (A V k [A]) * λ - → y (A (J ν V k [A]) ----→ (J ν y)) and thus (A V k [A]) * λ - → y .(λ - → z λ - → x . (y -→ w k -→ w x ) ----→ (J ν y)). Using then p-l ≥ lg( - → z )+2 and distinguishing y ∈ - → z or y ∈ - → z it follows easily that (A V k [A]) * λ - → y 1 (y 2 -→ w k --→ w y3 ) where - → y 3 is a final subsequence of - → y 1 , -→ e y3 ∈ --→ E y3 and lg( - → y 3 ) ≥ 1.
The fact that ν occurs nicely is clear.

Proposition 4.2 Assume that there is a sequence (j k ) k∈N of integers such that, for each k, ν occurs correctly in

(A U j k [A]). Then ν is persisting in F [A ]. Proof Let t 1 be a reduct of F [A ]
. By Lemma 4.6, it is enough to show that ν does occur in t 1 . By Lemma 2.1, let t 2 be such that

F [A ] * t 2 * Ω t 1 . By Lemma 3.3, F * G = D[[] i = w i : i ∈ I] where w i = (x [i] Arg(x [i] , G)) and t 2 = D[[] i = w i : i ∈ I] where w i is a β-reduct of w i [A ].
By Lemma 3.4, G * F j k for some k. Let x [j] be the occurence of x in G which has x (j k ) as residue in F j k . By Lemma 3.1, there is a substitution σ and a sequence V of terms such that U j k = W :: V and σ(M j ) reduces to W where M j = Arg(x [j] , G). By Lemma 4.4, let w j be such that (A Arg(x [j] , G)[A]) reduces to w j and w j * w j . Since (A σ(M j )[A]) reduces both to σ(w j ) and to (A W [A]), let s be a common reduct of (σ(w j )

V [A]) and (A W [A] V [A]). Since ν occurs correctly in (A W [A] V [A]
), it occurs correctly (by Lemma 4.5) in s. But (σ(w j ) V [A]) reduces to s and ν does not occur in σ neither in V [A], then ν occurs in w j . Thus it occurs in w j and thus in t 2 .

Since an Ω-reduction of w j cannot erase ν (otherwise, by Church-Rosser, ν will not occur in a reduct of s) and w j * w j , then, by Lemma 4.1(item 3), an Ωreduction of w j cannot erase all its ν. The same proof as the one in section 4.1 shows that ν cannot be totally erased by the Ω-reduction from t 2 to t 1 and thus it occurs in t 1 . 5 Case 2(a) of Theorem 3.2

Here is an example of this situation. Let F = (G x) where G is a λ-term such that G * λuλv.(v (G (u K K) v)). We can take λz.(z k (G (x K ∼2k ) z) for F k . Thus

U k = K ∼2k , S k = K ∼2 , t k = K and σ k = id. F [K] F [Ω]. We are in situation 2.(a) of Theorem 3.2 because (σ k (t k ) S k [K]) = (K K ∼2 ) * K.

The idea of the construction

The desired A looks like the one for the previous case. It will be ( J c 0 ν A) for some other term J that behaves mainly as J but has to be a bit more clever. The difference with the previous one is the following. For the J of section 4.2, (J ν u) reduces to a term where the J that occurs in the arguments of u is the same. Here J has to be parameterized by some integers. This is the role of its first argument. We will define a term J and will denote ( J c n ) by J n i.e. intuitively, the J at "step" n. Here (J n ν u) will reduce to a term where J n+1 and not J n occurs in the arguments of u. See Definition 5.2 and Lemma 5.1 below.

The reason is the following. In section 4.2, after some steps, the head variable of (A V k [A]) does not change anymore and the variable ν can no more disappear. Here, to be able to ensure that ν does not disappear, J must occur in head position infinitely often and, for that, it has to be able to introduce more and more λ's.

The λ's that are introduced by J n (i.e. λy 1 ...λy hn of Lemma 5.1) are used for two things. First they ensure that a J will be added to the next S k , say S kn , coming in head position. Secondly, they ensure that ν occurs correctly in (A V jn [A]) where j n is large enough to let S kn come in head position. This is the idea but there is one difficulty. If S kn comes in head position during the head reduction of (A V jn [A]), it will also come in head position during the reduction of (A V jn [A]) but (see Lemma 4.3) some λ's are put in front (the -→ λy of Lemma 5.3). If we could compute their number it will not be problematic but, actually, this is not possible. For the following reason: these λ's come from the J k that came in head positions in previous steps but, when we are trying to put a J in front of S kn it is possible that J p has already appeared in head position for some p > n.

We thus proceed as follows. J 0 introduces enough λ's to put J 1 in front of S k0 (the first S k that comes in head position during ρ) and to ensure that ν will occur correctly in (A V j0 [A]). Then we look at the first term of V j0 that comes in head position during ρ. This term, say a 0 , has J 1 in front of it in the head reduction of (A V j0 [A]). This is the term (a 0 may be a term in S k0 but it may be some other term) that will allow to define the number of λ s that J 1 introduces. It introduces enough λ s to put J 2 in front of S k1 , the next S k coming in head position, and to ensure that ν occurs correctly in the reduction of (A V j1 [A]). Note that k 1 has to be large enough to avoid the λ's that occur at the beginning of the term where a 0 occurs in head position. We keep going in this way to define the J n . It is clear (this could be formally proved by using standard fixed point theorems) that the function h (see definitions 5.1 and 5.2 below) that computes the parameter c n at step n is recursive. A formalization of this is given in Definition 5.1 below.

There is a final, though not essential, difficulty to make this precise. The definition of J needs to know the function h. But to compute h we need some approximation of J. More precisely to compute h(n) we need to know the behavior of J where only the values of h(p) for p < n will be used. To do that, we introduce fake J n (they are denoted as Jn below). They are as J n but the term J n+1 (which is not yet known since h(n + 1) is not yet known) is replaced by some fresh constant γ. Note that, using the standard fixed point theorem, we could avoid these fake Jn but then, Definition 5.1 below should be more complicated because the constant γ would be replaced by a term computed from a code of J and we should explain how this is computed ... Finally note that it is at this point that we use the fact that the branch in T is recursive.

Back to the example

With the example given before, we can take for J a λ-term such that J * λuλvλy 1 λy 2 .(v ( J u y 1 ) ( J u y 2 )) and for K the term ( J ν K).

Then K * K = λy 1 λy 2 λz 1 λz 2 .(y 1 ( J u z 1 ) ( J u z 2 )). Since, if F [K ] * t, then t * λz.(z k (G K z)). It follows that ν is persisting in F [K ].
Note that here the function h is constant. Given any recursive function h it will not be difficult to build terms F, A such that the corresponding function h is precisely h . Definition 5.1 For each i, let l i be the number of λ's at the head of t i .

The definition of J needs some new objects. Let γ be a new constant. We define, by induction, the integers j n , h n , the terms Jn , a jn and the sequence of terms B jn .

In this definition a term (or a sequence of terms) marked with is a term in relation with the corresponding unmarked term.

• (Step 0 ) Let j 0 be the least integer j such that some S k comes in head position during ρ j (the head reduction of (A Since, for some i, d i [A] comes in head position during the head reduction of (A V j0 [A]), then, for some i , (γ ν d i [A]) comes in head position during the head reduction of (( J0 ν A) V j0 [A]) and thus (( J0 ν A) V j0 [A]) * λX j0 ((γ ν a j0 ) B j0 ) for some a j0 , some sequence X j0 of variables and some sequence B j0 of terms.

V j [A])), k 0 = lg(V j0 ), h 0 = max(l 0 , k 0 ). Let V j0 = d 1 ...
• (Step 1 ) Let j 1 be the least integer j > j 0 such that some S k comes in head position during ρ j for k large enough (lg(X j0 ) < lg(S j0 :: ...

:: S k-1 ) is needed). Then (( J0 ν A) V j1 [A]) = (( J0 ν A) V j0 [A] S j0 ...S k ...S j1-1 ) * ((γ ν a j0 ) B j0 ) T 0 . Let h 1 = l j0 + lg(B j0 :: T 0 ) + 1 and J0 = J1 [γ := λnλxλx 1 ...λx h1 (x (γ n x 1 ) ... (γ n x h1 ))]. Then (( J1 ν A) V j1 [A]) * λX j1 ((γ ν a j1 ) B j1
) for some term a j1 and some sequence B j1 of terms.

• (Step n+1 ) Assume the integers j n , h n and the term Jn are already defined. Let j n+1 be the least integer j > j n such that some S k comes in head position during ρ j for k large enough (lg(X jn ) < lg(S j1 :: ... :: S k-1 ) is needed). Then (( Jn ν A) V jn+1

Comment

Note that, since the branch in T is recursive, it follows, by standard arguments, that the function h defined by h(i) = h i is computable. Definition 5.2

• Let H be a λ-term that represents the function h. • For each n ∈ N, we denote ( J c n ) by J n .

Lemma 5.1 For each n ∈ N, (J n ν u) * λy 1 ...λy hn .(u (J n+1 ν y 1 )...(J n+1 ν y hn )).

Proof Easy. As in the previous section, we consider J n as constants with the reduction rules of the previous Lemma. Let A = (J 0 ν A). We prove that ν is persisting in F [A ]. Proof This follows from Lemma 5.2 Definition 5.4 Let t be a solvable term. We say that:

1. ν occurs nicely in t if the only occurrences of ν are in a sub-term of the form (J n ν).

2. ν occurs correctly in t if it occurs nicely in t and the head normal form of t looks like -→ λx.(x -→ c -→ e y ) for some final subsequence -→ y of -→ x of length at least 1 such that ν does occur in -→ e y .

The intuitive meaning of Lemma 5.4 below is "for each n ∈ N, t jn * (a jn B jn ) and (A V jn [A]) * λX jn .(J n+1 ν a jn B jn )".

Strictly speaking, this is not true, because the a jn and B jn are not the "real" ones i.e. the ones that occur in the reduction with the real J. For two reasons:

• The first one is easily corrected: in a jn and B jn the constant γ must be replaced by J n+1

• The second one is more subtle. In the correct lemma, and the J n should be the "real" ones. But the a jn are defined using Jp which are only fake J p . Stating the correct lemma will need complicated, and useless, definitions. We will not do it and thus we state the lemma in the way it should be, intuitively, understood. 2. Is it true that, if F [A ] is a universal generator then so is F [A]. Note that, somehow, the A we have constructed is a kind of η-infinite expansion of A.

If these two propositions were true, we could replace the assumption of Proposition 6.1 by the (more elegant) fact that F [A] is not a universal generator. The terminology "Scope lemma" is borrowed to A. Polonsky. In his paper he stated an hypothesis (denoted as the scope Lemma) which corresponds to the previous property. Proposition 6.2 Assume F, A satisfy the scope lemma. Then the range of λx.F is infinite. Proof Immediate.

2 .

 2 We denote by c k the Church integer for k and by Suc a closed term for the successor function. As usual we denote by I (resp. K, Ω) the term λx.x (resp. λxλy.x, (δ δ) where δ = λx.(x x)).

2 .Notation 2 . 3

 223 The relation is transitive. Proof Easy. We will have to use the following notion. A sub-term u of a term v comes in head position during the head reduction of v. This means the following: v can be written as C[u] where C is some context with exactly one hole. During the head reduction of C the hole comes in head position i.e C reduces to λ -→ x .([] -→ w )

Example 1 . 2 .

 12 This example is due to A. Polonsky. Let G, H be λ-terms such that G * λyλz.(z G λu.(y (K u)) z) and H * λuλvλw.(w (H u (v u) w)). Let F = (G λy.(H y x)). We have F * λz.(z n (G λyλw.(w m (H (K n y) (x (K n y) ∼m ) w)) z)). Thus, if B λy 1 ...λy r .(y i w 1 ...w l ) where ν is possibly free in the w j , F [B] λz.(z l (G λyλw.(w r (H (K l y) y w)) z)) and ν is not persisting in F [B] (since it can be erased). This means that for all closed term A such that F [A] F [Ω], and for all solvable term A , ν is not persisting in F [A ]. Example This example is an adaptation of the previous one. Let G, H be λ-terms such that G * λyλz.(z (G λu.(y (K u)) z)) and H * λuλvλw.(w (H u (v u) w)). Let F = λy.(G λv.(H v (x y))).

Lemma 4.2 1 .

 1 Assume u = C[(λx.a b)] for some context C and let u * u . Then u = C [(a b )] for some context C and some terms a , b such that C * C , a ∈ E λx.a , a * a and b * b . 2. Assume u * u and u * v. Then, v * v for some v such that u * v . Proof The first point is immediate because the operations that are done to go from u to u are either in C (to get C ) or in b (to get b ) or in a (to get a ) or in λx.a . It is enough to check that locals and globals operations on a commute.

Lemma 4.4 1 .

 1 Assume u = C [R ] for some context C and some redex R and let u * u . Then : • either R = (λx.a b ), u = C[(λx.a b)] for some context C and some terms a, b such that C * C , a * a and b * b . • or R = (a b ), u = C[(a b)] for some context C and some terms a, b such that C * C , a = λ -→ y .(a -→ e y ), a * a and b * b .

Corollary 4 . 1 ν

 41 is persisting in F [A ].ProofBy Proposition 4.1, for k ≥ k 0 , ν occurs correctly in (A V k [A]). By Lemma 4.5, ν occurs correctly in (A U k [A]) and we conclude by Proposition 4.2.

  d k0 and J0 = λnλxλx 1 ...λx h0 (x (γ n x 1 ) ... (γ n x h0 )). Then (( J0 ν A) V j0 [A]) * λy 1 ...y r0 (A (γ ν d 1 [A]) ... (γ ν d k0 [A]) (γ ν y 1 ) ... (γ ν y r0 )).

  [A]) = (( Jn ν A) V j1 [A] S jn ...S k ...S jn+1-1 ) * ((γ ν a jn ) B jn ) T n .Let h n+1 = l jn +lg(B jn :: T n )+1 and Jn+1 = Jn [γ := λpλxλx 1 ...λx hn+1 (x (γ p x 1 ) ...(γ p x hn+1 ))]. Then (( Jn+1 ν A) V jn+1 [A]) * λX jn+1 ((γ ν a jn+1 ) B jn+1) for some term a jn+1 and some sequence B jn+1 of terms.

•

  Let T = λaλbλc.(a (b (z (suc k) n c))), D = λkλnλx.(H k T I x) and J = (Y λz.D) where Y is the Turing fixed point operator.

2 . 4 . 5 . 3

 2453 Assume u * u and u * v . Then, v * v for some v such that u * v. Proof Same proof as Lemmas 4.2 and 4.Lemma If u * -→ λx.(x -→ c ) and u * u , then u * -→ λx -

Lemma 5 . 4

 54 For each n ∈ N, t jn * (a jn [γ := J n+1 ] B jn [γ := J n+1 ]) and (A V jn [A]) * λX jn .(J n+1 ν a jn [γ := J n+1 ] B jn [γ := J n+1 ]).Proof By induction on n.

Definition 6 . 1

 61 Let A n = A [ν = c n ].Say that F, A satisfy the Scope lemma if, for every n, m, the fact thatF [A n ] F [A m ] implies that, for some k, (x U k )[x := A n ] (x U k )[x := A m ].

  βΩ t 3 for some t 3 . Proof See, for example,[START_REF] Barendregt | The Lambda Calculus, Its Syntax and Semantics[END_REF]. If t * t 1 and t * t 2 , then t 1

	Lemma 2.1 βΩ v, then u Theorem 2.1 1. If u *

* w * Ω v for some w. 2. * βΩ satisfies the Church-Rosser property : if t * βΩ t 1 and t * βΩ t 2 , then t 1 * βΩ t 3 and t 2 * * t 3 and t 2 * t 3 for some t 3 . Moreover #(t 3 ) can be computed from #(t 1 ), #(t 2 ) and a code for the reductions t * t 1 , t * t 2 . Proof See [1]. Definition 2.1 1. We denote by the equality modulo * βΩ i.e. u v iff there is w such that u * βΩ w and v * βΩ w and we denote by [t] H the class of t modulo . 2. For λx.F ∈ Λ • , the range of λx.F in H is the set

  ∈ βΩ(F ) and F is normalizable, then the range of t is trivially infinite since then the set {[F [x := λx 1 ...λx n c k ]] H / k ∈ N} is infinite where n is the size of the normal form of F .3. More generally, if t has a finite Bohm tree then it satisfies the range property.

	Let t = λx.F [x] be a closed term. First observe that
	1. If x ∈ βΩ(F ), then the range of t is a singleton.
	2. If x

  7, t k is some head normal form for (A U k [A]) but it is not the canonical one i.e. the one obtained by reducing, at each step, the head redex. Say that S k comes in head position during ρ if, for some k > k, an element of the list σ k k (S

	Definition 3.6

k )[A] comes in head position during the head reduction of (A V k [A]). Definition 3.7

1. Let t be a term with a free variable ν.

  Definition 5.[START_REF] Barendregt | Towards the range property for the lambda theory H[END_REF] 1. We define, for terms u, the sets E u of terms by the following grammar:E u = u |(J n ν e u ) |λ -→ y .(e u -→ e y )2. Let t, t be some terms. We denote by t t if there is a context C with one hole such that t = C[u] and t = C[u ] where u ∈ E u . Lemma 5.21. Assume u * u and u * v. Then, v * v for some v such that u * v .

Say that a term u is a weak generator if for every closed λ-term t one of its reducts occurs as a sub-term of a reduct of u. A universal generator is, trivially, a weak generator. Is the converse true ?

Acknowledgement. We wish to thank Andrew Polonsky for helpful discussions and also the anonymous referees for their remarks and suggestions.

Proposition 5.1 For each n ∈ N, ν occurs correctly in (A V jn [A]).

Proof

We have (A V jn [A]) * λX jn .(J n+1 ν a jn [γ := J n+1 ] B jn [γ := J n+1 ]) = λX jn .((λz 1 ...λz hn+1 .( a jn [γ := J n+1 ] (J n+2 ν z 1 ) ... (J n+2 ν z hn+1 )) B jn [γ := J n+1 ]). Since h n+1 = l jn +lg(B jn T n )+1, then, by Lemma 5.4, (A V jn [A]) * λX jn λZ.(t jn e Z ) where t jn * t jn , e Z * Z and lg(Z) > l jn . Therefore, by Lemma 5.3, ν occurs correctly in (A V jn [A]). Lemma 5.5 Let t be a solvable term. Assume that ν occurs correctly in t. Then ν occurs (and it occurs correctly) in every reduct of t.

Proof

This follows immediately from the fact that if (J n ν y) * u, then ν ∈ βΩ(u). Lemma 5.6 Let k be an integer such that ν occurs correctly in

Proof This follows immediately from Lemmas 5.3 and 5.5.

The other assumption

As we already said the fact that ν is persisting in F [A ] does not imply that, letting

To ensure that the range of λx.F is infinite, we need another assumption on F .

Let λx.F be a closed term and A be such that

. In propositions 6.1 and 6.2 below we assume that F has the Barendregt's persistence property. Let A be the corresponding term. We also assume that A has been obtained by the way developed in section 4.2 or in section 5. Note that, in these cases, ν is never applied in a reduct of F [A ]. Proposition 6.1 Assume there is a sequence (t n ) n∈N of distinct closed and normal terms such that, for every n, t n never occurs as a sub-term of some t such that F [A ] * βΩ t . Then, the range of λx.F is infinite.

for some n = m and let u be a common reduct. Since ν is never applied in a reduct of F [A ], there are reducts a n and a m of

Remark

Say that u is a universal generator if, for every closed λ-term t, there is a reduct of u where t occurs as a sub-term. Before Plotkin gave his counterexample, Barendregt had proved that the omega-rule is valid when t, t are not universal generators. Our hypothesis on the existence of the sequence (t n ) n∈N may look similar. Assuming that F [A ] is not a universal generator, there is a term t that never occurs as a sub-term of a reduct of F [A ]. Letting t 0 = t and t n+1 = λx.t n , the reducts of F [A ] never contain one of these terms. Also, they are not equal, because otherwise t is Ω. This is however not enough to show that the F [ν := t n ] are distinct because we need that no reduct of F [A ] contains a reduct of one of the t n (this is why, in our hypothesis, we have assumed that the t n are normal). This raises two questions :