Separability of Infinite Lambda Terms

Paula Severi and Fer-Jan de Vries

Department of Mathematics and Computer Science, University of Leicester University Road, Leicester, LE1 7RH, UK - {ps56,fdv1}@mcs.le.ac.uk

Abstract. Infinite lambda calculi extend finite lambda calculus with infinite terms and transfinite reduction. In this paper we extend some classical results of finite lambda calculus to infinite terms. The first result we extend to infinite terms is Böhm Theorem which states the separability of two finite βη-normal forms. The second result we extend to infinite terms is the equivalence of the prefix relation up to infinite eta expansions and the contextual preorder that observes head normal forms. Finally we prove that the theory given by equality of ∞η-Böhm trees is the largest theory induced by the confluent and normalising infinitary lambda calculi extending the calculus of Böhm trees.

1 Introduction

Not all computations are finite. The calculation of the meaning of a linguistic expression can be infinite, whether the language is a natural language or not. Vicious circles can be a cause. In their book [3] Barwise and Moss give the following example:

The law school professor who had worked for him denounced the judge who had harassed her.

This sentence can be expressed using the formulæ:

D(P,J)

where D(x,y) means x denounces y, P means the law school professor who had worked for him and J means the judge who had harassed her. The calculations that lead to the exact references of a particular judge and professor can be performed with two rewrite rules:

P → W (J)
J → H(P)

relating to the respective clauses who had worked for him and who had harassed her. We see that the calculation of the meaning of the whole sentence now does not terminate. It may go like this:

D(P,J) → D(W (J),J) → D(W (J),H(P)) → D(W (H(P)),H(P)) →
D(W (J),H(W (J)))) → D(W (H(P)),H(W (J)))) → ...

culminating in a limit D(W (H(W (H(...)))),H(W (H(W (...))))) which does no longer seem to refer to any judge or professor.

Infinitary rewriting is the branch of rewriting that deals explicitly with infinite terms and infinite reductions. Extending a finite rewriting system into a infinite system has to be done with care when one wants to preserve a useful property like confluence. In this paper we focus on one particular theory of rewriting namely lambda calculus. Lambda calculus is confluent. Just extending finite lambda calculus with infinite lambda terms and infinite reduction destroys this confluence property. Define I = λx.x, W = λx.I(xx) and Δ = λx.xx Then the term ΔW has a one step reduction to ΔΔ and an infinite reduction to I((I(...))), namely

ΔW → _{β} W W → _{β} I(W W) → _{β} I(I(W W)) → → → _{β} I(I(I(...)))

Both ΔΔ and I(I(I(...))) reduce only to themselves, and have no common reduct. To rescue the confluence property one has to extend the lambda calculus also with an extra ⊥-rule that replaces a meaningless term by ⊥. Interestingly there are many different choices for the set of meaningless terms. The set of terms without head normal form is the largest, the set of terms without top normal form is the smallest [5]. The infinite lambda calculi that we consider here have all the same set of finite and infinite terms Λ_{⊥}^{∞} . Besides the variation that come with the choice of a set U of meaningless terms, there is another source of variation in the infinitary setting that comes with the strength of extensionality.

REDUCTION RULES  NORMAL FORMS  NF

Beta and Bottom for terms without tnf  Berarducci trees  BerT = P\overline{T N}
Beta and Bottom for terms without whnf  Lévy–Longo trees LLT = P\overline{W N}
Beta and Bottom for terms without hnf  Böhm trees  BT = P\overline{H N}
Beta, Bottom parametric on U  Parametric trees  NF = P_{U}
Beta, Bottom for terms w.o. hnf and Eta  η-Böhm trees  ηBT
Beta, Bottom for terms w.o. hnf and EtaBang ∞η-Böhm trees  ∞ηBT

Fig. 1. Infinitary Lambda Calculi

Figure 1 summarises the infinitary lambda calculi studied so far [4–6, 8, 10, 9]. An interesting aspect of infinitary lambda calculus is the possibility of capturing the notion of tree (such as Böhm and Lévy–Longo trees) as a normal form. These trees were originally defined for finite lambda terms only, but in the infinitary lambda calculus we can also consider normal forms of infinite terms. The three infinitary lambda calculi mentioned in the first three rows of Figure 1 capture the well-known cases of Böhm, Lévy–Longo and Berarducci trees [4–6]. In the fourth row, there is an uncountable class of infinitary lambda calculi with a ⊥-rule parametrised by a set U of meaningless terms [7, 8]. By changing the parameter set U of the ⊥-rule, we obtain different infinitary lambda calculi. If U is the set \overline{H N} of terms without head normal form, we capture the notion of Böhm tree. If U is the set \overline{W N} of terms without weak head normal form we obtain the Lévy–Longo trees. And if U is the set \overline{T N} of terms without top head normal form to ⊥, we recover the Berarducci trees. The infinitary lambda calculus sketched in the one but last row incorporates the η-rule [10]. This calculus captures the notion of η-Böhm tree. The last row in Figure 1 mentions the infinitary lambda calculus incorporating the η!-rule, a strengthened form of the η-rule [9], whose normal forms correspond to the ∞η-Böhm trees. In this paper we lift three classical results of finite lambda calculus to infinite lambda calculus. First we extend Böhm’s Theorem concerning separability of finite βη-normal forms, also known as finite ηBöhm trees, to possibly infinite ∞ηBöhm trees. Two terms M and N are separable if for any pair of finite terms P,Q there exists a context C such that C[M] → → _{β} P and C[N] → → _{β} Q. This statement is extended to infinite terms by considering the variation of η-reduction called η!. We prove then that two (possibly infinite) βη!-normal forms (also known as ∞ηBöhm) M and N can be separated, i.e. for any (possible infinite) pair of terms P and Q there exists a finite context C such that C[M] → → _{β} P and C[N] → → _{β} Q. The terms M,N subject to separability may be infinite. However the discriminating context remains finite and only finite β-reduction is necessary to ”separate them”. The method for finding such contexts is called the Böhm out technique [1]. The second result that we extend to infinite terms is the equivalence of the prefix relation up to infinite eta expansions and the contextual preorder that observes head normal forms. It is natural to compare terms, in particular normal forms, with help of the prefix relation ⪯. When terms are represented as trees, prefixes of a tree are obtained by pruning some of its subtrees and replacing them by ⊥. In [11] we prove that the function BT is monotone in (Λ_{⊥}^{∞} ,⪯) and that the function ∞ηBT is not so. For ∞ηBT it is the prefix relation up to infinite eta expansions denoted by ⪯_{η!} that is monotone. Another basic preorder between terms is the contextual preorder with respect to head normal forms. denoted by M ⊆_{h}N which means that for all contexts C if C[M] has a head normal form then C[N] has a head normal form. In [13] Wadsworth, generalising Böhm’s theorem, shows that the equivalence between ⊆_{h} and ⪯_{η!} on the set Λ of finite λ-terms (which is part of the Characterisation Theorem for D_{∞}). In this paper we will show the equivalence between ⊆_{h} and ⪯_{η!} on the set Λ_{⊥}^{∞} of finite and infinite lambda terms. One direction uses only properties of the reduction. The other direction extends the Böhm out technique to infinite terms. Finally we prove that the theory given by equality of ∞η-Böhm trees is the largest theory induced by a confluent and normalising infinitary lambda calculus extending the calculus of the Böhm trees. The analogous result for finite lambda calculus is that the theory H^{∗} = {(M,N) ∈ Λ | M ⊆_{h} N} is the unique Hilbert-Post complete lambda theory extending the theory H which equates the unsolvables [1].

2 Infinitary Lambda Calculus

In this section we will briefly recall some notions and facts of infinite lambda calculus from our earlier work [5, 6, 8, 10, 9]. We assume familiarity with basic notions and notations from [1]. Let Λ be the set of λ-terms and Λ_{⊥} be the set of finite λ-terms with ⊥ given by the inductive grammar:

M ::= ⊥ | x | (λxM) | (MM)

where x is a variable from some fixed set of variables V. We follow the usual conventions on syntax. Terms and variables will respectively be written with (super- and subscripted) letters M,N and x,y,z. Terms of the form (M_{1}M_{2}) and (λxM) will respectively be called applications and abstractions. A context C[ ] is a term with a hole in it, and C[M] denotes the result of filling the hole by the term M, possibly by capturing some free variables of M. If σ: V → Λ^{∞} then M^{σ} is the simultaneous substitution of the variables in M by σ. The set Λ_{⊥}^{∞} of finite and infinite λ-terms is defined by coinduction using the same grammar as for Λ_{⊥} . This set contains the three sets of Böhm, Lévy–Longo and Berarducci trees. In [6– 8], an alternative definition of the set Λ_{⊥}^{∞} is given using a metric. The coinductive and metric definitions are equivalent [2]. In this paper we consider only one set of λ-terms, namely Λ_{⊥}^{∞} , in contrast to the formulations in [6, 7] where several sets (which are all subsets of Λ_{⊥}^{∞} ) are considered. The paper [8] shows that the infinitary lambda calculi can be formulated using a common set Λ_{⊥}^{∞} , confluence and normalisation still hold since the extra terms added by the superset Λ_{⊥}^{∞} are meaningless and equated to ⊥. We define several rules we use to define various infinite lambda calculi. The β, η and η^{−1} - rules apply to finite and infinite terms as well. The extra power of the η!-rule becomes visible on infinite terms. The ⊥-rule is parametric on a set U ⊂ Λ^{∞} of meaningless terms [7, 8] where Λ^{∞} is the set of terms in Λ_{⊥}^{∞} that do not contain ⊥.

Definition 1. We define the following rewrite rules on Λ_{⊥}^{∞} :

(λx.M)N → M[x:= N] (β) \begin{matrix}M[⊥:= Ω] ∈ U M ≠ ⊥ \\ & (⊥) \\ M → ⊥ \end{matrix}

\begin{aligned}x ∉ F V (M) \\ & (η) \\ λx.Mx → M \end{aligned}  \begin{aligned}x ∉ F V (M) \\ & (η^{−1} ) \\ M → λx.Mx \end{aligned}  \begin{matrix}x → → → _{η^{−1}} N  x ∉ F V (M) \\ (η!) \\ λx.MN → M \end{matrix}

In this paper we need various rewrite relations constructed from these rules on the set Λ_{⊥}^{∞} . These are defined in the standard way, eg. → _{β⊥η!} is the smallest binary relation containing the β, ⊥ and η!-rules which is closed under contexts. Reduction sequences can be of any transfinite ordinal length α: M_{0} → M_{1} → M_{2} → ...M_{ω} → M_{ω+1} → ...M_{ω+ω} → M_{ω+ω+1} → ...M_{α}. This makes sense if the limit terms M_{ω},M_{ω+ω} ,... in such sequence are all equal to the corresponding Cauchy limits, lim_{β→λ} M_{β}, in the underlying metric space for any limit ordinal λ ≤ α. If this is the case, the reduction is called Cauchy converging. We need the stronger concept of a strongly converging reduction that in addition satisfies that the depth of the contracted redexes goes to infinity at each limit term: lim_{β→λ} d_{β} = ∞ for each limit ordinal λ ≤ α, where d_{β} is the depth in M_{β} of the contracted redex in M_{β} → M_{β+1} . Any finite reduction is, then, strongly converging. We use the following notation:

1. M → N denotes a one step reduction from M to N;

2. M → → N denotes a finite reduction from M to N;

3. M → → → N denotes a strongly converging reduction from M to N.

Variations on the reduction rules give rise to different calculi (see Figure 1). The resulting infinite lambda calculus (Λ_{⊥}^{∞} ,→ _{ρ}) we will denote by λ_{ρ}^{∞} for any ρ ∈ {β⊥,β⊥η,β⊥η!}. Since the ⊥-rule is parametric, each set U of meaningless terms gives a different infinitary lambda calculus λ_{β⊥}^{∞} . The notions of head normal form, weak head normal form and top normal form are defined as follows:

1. A head normal form (hnf) is a term of the form λx_{1}...x_{n}.yM_{1}...M_{k}.

2. A weak head normal form (whnf) is either a hnf or an abstraction λx.M.

3. A top normal form (tnf) is either a whnf or an application (MN) if there is no P such that M → → _{β} λx.P.

We define the following sets:

H N = {M ∈ Λ^{∞} | M → → _{β} N and N in head normal form}
W N = {M ∈ Λ^{∞} | M → → _{β} N and N in weak head normal form}
T N = {M ∈ Λ^{∞} | M → → _{β} N and N in top normal form}

Instances of U ⊆ Λ^{∞} are \overline{H N} , \overline{W N} and \overline{T N} the respective complements of H N , W N and T N.

Definition 2. 1. We say that a term M in λ_{ρ}^{∞} is in ρ-normal form if there is no N in λ_{ρ}^{∞}

such that M → _{ρ} N.

2. We say that λ_{ρ}^{∞} is confluent (Church-Rosser) if (Λ_{⊥}^{∞} ,→ → → _{ρ}) satisfies the diamond property, i.e. _{ρ}← ← ← ∘ → → → _{ρ} ⊆ → → → _{ρ} ∘ _{ρ}← ← ← .

3. We say that λ_{ρ}^{∞} is normalising if for all M ∈ Λ_{⊥}^{∞} there exists an N in ρ-normal form such that M → → → _{ρ} N.

Theorem 3. [6–8] Let U be a set of meaningless terms. The calculi λ_{β⊥}^{∞} with a parametric ⊥-rule on the set U are confluent, normalising and satisfy postponement of ⊥ over β.

In [8], confluence of the parametric calculi is proved for any Cauchy converging reduction, not only strongly converging ones.

Theorem 4. [10, 9] The infinite lambda calculi of ∞η-Böhm and η-Böhm trees are confluent and normalising.

We will use the following properties of η!-reduction proved in [9].

Theorem 5. [9]

1. Inverse reductions: M → → → _{η!} N if and only if N → → → _{η^{−1}} M.

2. The infinitary lambda calculus λ_{η!}^{∞} is confluent.

3. The relations → → → _{η!} and → → _{β} commute.

4. The transfinite η! and η^{−1} -reductions preserves the property of having head normal form, i.e. if M → → → _{η!} N then the following are equivalent:

(a) there exists a head normal form M′such that M → → _{β} M′,

(b) there exists a head normal form N′such that N → → _{β} N′.

3 The standard prefix relation

Each of the confluent and normalising extensions of finite lambda calculus gives rise to a normal form function that assigns to a lambda term in Λ_{⊥}^{∞} a corresponding normal form. We will denote these various functions with notation used in Figure 1.

Definition 6. Let M,N ∈ Λ_{⊥}^{∞} .

1. We say that M is a prefix of N (we write M ⪯ N) if M is obtained from N by replacing some subterms of N by ⊥.

2. M ⪯_{NF} N if NF(M) ⪯ NF(N).

Definition 7. Let M ∈ Λ_{⊥}^{∞} . We define the truncation of M at depth n, denoted as M^{n}, as the result of replacing in M all subterms at depth n by ⊥.

The following lemmas are particular cases of general lemmas proved in [11, 12] to deduce continuity of BT and LLT on the cpo (Λ_{⊥}^{∞} ,⪯).

Lemma 8. Let C[M] ∈ Λ_{⊥}^{∞} . Then, (C[M])^{n} = C^{n}[M^{k}] where k = max(0,n − d) and d is the depth of the hole in C.

Lemma 9. If M ⪯ N and M → → → _{β} M′then N → → → _{β} N′and M′⪯ N′for some N′.

Lemma 10. Let M,N ∈ Λ_{⊥}^{∞} . If M ⪯ N then M ⪯_{BT} N.

Lemma 11. Let P ∈ Λ_{⊥}^{∞} . For all n there exists i such that (BT(P))^{n} ⪯_{BT} (P)^{n+i}.

4 Prefix up to infinite eta expansions

In this section we define the relation ⪯_{η!} on β⊥-normal forms which is equivalent to the relation ^{η} ⊆^{η} on Böhm-like trees defined in [1] (up to change of representation from terms to trees).

Definition 12. Let M,N ∈ Λ_{⊥}^{∞} . Then, M ⪯_{η!} N if BT(M) → → → _{η^{−1}} P ⪯ Q_{η^{−1}} ← ← ← BT(N) for some P,Q ∈ BT(Λ_{⊥}^{∞} ).^{1}

If M ⪯_{η!} N then there exists “a canonical pair of terms” P,Q such that M → → → _{η^{−1}} P ⪯ Q_{η^{−1}} ← ← ← N. To find this pair of terms we use a bisimulation that imposes the number of abstractions and arguments to be the same. This bisimulation is used to simplify the Böhmout technique.

Definition 13. (Honest bisimulation) Let R be a binary relation on the set of β⊥- normal forms. Then R is called a honest bisimulation if whenever MRN,

– if M = λx_{1}...x_{n}.yM_{1}...M_{m}, N = λx_{1}...x_{n′}.yN_{1}...N_{m′}and n−n′= m−m′then n = n′, m = m′and M_{i}RN_{i} for all 1 ≤ i ≤ m.

The maximal honest bisimulation R is denoted by ∼.

We give some examples of bisimilar terms:

– The constant ⊥ is bisimilar to any β⊥-normal form.

– We say that two β⊥-normal forms M and N are distinguishable if M = λx_{1}...x_{n}.yM_{1}...M_{m}, N = λx_{1}...x_{n′}.y′N_{1}...N_{m′}and either the head variables y and y′ are different or n − n′≠ m − m′. Then, distinguishable terms are bisimilar.

– The terms y and λx.yz are not bisimilar but by η-expanding the variable y we get the term λx.yx which is bisimilar to λx.yz.

1 By Theorem 5, we could replace → → → _{η!} by _{η^{−1}} ← ← ← and get an equivalent definition.

Theorem 14. (Existence of bisimilar terms) Let M,N be in β⊥-normal form. Then there are P,Q such that M → → → _{η^{−1}} P ∼ Q_{η^{−1}} ← ← ← N.

Proof. We define a function bisim : Λ_{⊥}^{∞} × Λ_{⊥}^{∞} → Λ_{⊥}^{∞} × Λ_{⊥}^{∞} by coinduction such that bisim(M,N) = (P,Q) and M → → → _{η^{−1}} P ∼ Q_{η^{−1}} ← ← ← N. We have two cases:

1. If M = λx_{1}...x_{n}.yM_{1}...M_{m}, N = λx_{1}...x_{n′}.yN_{1}...N_{m′}and n−n′= m−m′= k then we

define

bisim(M,N) = (λx_{1}...x_{n}.yP_{1}...P_{m},λx_{1}...x_{n}.yQ_{1}...Q_{m})

where P_{i} and Q_{i} are obtained as follows:

(a) If n ≥ n′and m ≥ m′then we have to eta expand N until the number of abstractions and applications coincide with the ones in M. Hence, bisim(M_{i},N_{i}) = (P_{i},Q_{i}) for 1 ≤ i ≤ m′and bisim(M_{m′+j} ,x_{n′+j} ) = (P_{m′+j} ,Q_{m′+j} ) for 1 ≤ j ≤ k.

(b) If n < n′and m < m′then we have to eta expand M until the number of abstractions and applications coincide with the ones in N. Hence, bisim(M_{i},N_{i}) = (P_{i},Q_{i}) for 1 ≤ i ≤ m and bisim(x_{n+j} ,N_{m+j} ) = (P_{m+j} ,Q_{m+j} ) for 1 ≤ j ≤ −k.

2. Otherwise, bisim(M,N) = (M,N).

It is easy to see that the function bisim as a relation is an honest bisimulation and hence, P ∼ Q.

Corollary 15. Let M,N be in β⊥-normal form and (P,Q) = bisim(M,N). Then M ⪯_{η} N if and only if P ⪯ Q.

Proof. Note that if M ⪯_{η!} N and M ∼ N then M ⪯ N.

We give some examples of how to find the pair (P,Q) = bisim(M,N). Let J be a term satisfying the recursive equation Jx = λy.x(Jy) and E_{x} be the β⊥-normal form of Jx, i.e. E_{x} = λy_{1}.x(λy_{2}.y_{2}(...)). Note that x → → → _{η^{−1}} E_{x}.

\begin{matrix}M & N & P & Q \\ y & λx.yz & λx.yx & λx.yz \\ x⊥(λy.zy) & λu.xIzu & λu.x⊥(λy.zy)u & λu.xI(λy.zy)u \\ x⊥(λy.zE_{y}) & λu.xIzE_{u} & λu.x⊥(λy.zE_{y})E_{u} & λu.xI(λy.zE_{y})E_{u} \end{matrix}

5 Contextual Preorders

In this section we give two definitions for contextual preorder in the infinitary lambda calculus and prove that they are equivalent using the previous truncation lemmas. The definitions will differ in the sets of contexts over which will be quantified. In the definition of ⊆_{h} the quantification is restricted to finite contexts, in the definition of ⊆_{h}^{∞} the quantification runs over finite and infinite contexts.

Definition 16. 1. We say that M ⊆_{h} N if for all finite contexts C, if C[M] β-reduces to a head normal form then so does C[N].

2. We say that M ⊆_{h}^{∞} N if for all (finite or infinite) contexts C, if C[M] β-reduces to a head normal form then so does C[N].

Both notions of contextual preorder coincide:

Theorem 17. The following statements are equivalent for any terms M,N ∈ Λ_{⊥}^{∞} :

1. M ⊆_{h} N.

2. M ⊆_{h}^{∞} N.

Proof. (2) implies (1) trivially. We show (1) implies 2. Let C be an infinite context. We will construct a finite context (a truncation of C) that behaves like C. Observe that:

BT^{1}(C[M])⪯_{BT} (C[M])^{1+i} for some i by Lemma 11
= C^{1+i} [(M)^{k}]by Lemma 8
⪯_{BT} C^{1+i} [M] by Lemma 10

where d is the depth of the hole in C and k = max(0,n + 1 − d). If C[M] has a head normal form, so does C^{1+i} [M]. Since C^{1+i} is finite, by (1) we have that C^{1+i} [N] has a head normal form. By Lemma 10, we have that C^{1+i} [N] ⪯_{BT} C[N] and hence C[N] has a head normal form too. ⊓ ⊔

6 Separability

In this section we extend Böhm Theorem to infinite terms. We first extend the notion of separability so that it applies to infinite terms as well. Despite this extension the discriminating contexts that we will construct will be finite so that only finite β-reduction will be needed to ”fully separate them”. Böhming-out and the separability of distinguishable terms follow along the lines of [1]. However infinite terms complicate matters because it is not possible to give a bound for the number q of the permutator P_{q} used to Böhm-out the subterms of a term.

Definition 18. Let M,N ∈ Λ_{⊥}^{∞} . We say that the terms M and N are separable if for any P,Q ∈ Λ^{∞} there exists a finite context C such that C[M] → → _{β} P and C[N] → → _{β} Q.

We will use the following notation and terminology::

1. permutators are terms of the form P_{q} = λx_{1}...x_{q+1} .x_{q+1} x_{1}...x_{q};

2. selectors are terms of the form U_{i}^{q} = λx_{1}...x_{q}.x_{i}; and

3. constants are terms of the form K^{m}= λx_{1}...x_{m+1}.x_{m+1}.

The way we select (“Böhm-out”) subterms in the infinitary lambda calculus is similar to the finite case:

Theorem 19 (Böhming-out finite and infinite terms). Let M be a β⊥-normal form such that M = λx_{1}...x_{n}.yM_{1}...M_{m}. Take q ≥ m. Then there are contexts C_{i} for 1 ≤ i ≤ q and a term P such that:

1. C_{i}[M] → → _{β} M_{i}^{σ} when 1 ≤ i ≤ m,

2. C_{i}[M] → → _{β} z_{i} when m + 1 ≤ i ≤ q; where σ = [y:= P] and z_{m+1} ...z_{q}z_{q+1} are fresh variables.

Proof. Put C′[ ] = (λy.[ ]x_{1}...x_{n})Pz_{m+1} ...z_{q}z_{q+1} and C_{i}[ ] = (λz_{q+1} .C′[ ])U_{i}^{q}. Then C_{i}[M] → → _{β} M_{i}[y:= P] for 1 ≤ i ≤ m and C_{i}[M] → → _{β} z_{i} for m + 1 ≤ i ≤ q. ⊓ ⊔

Also the following lemma generalises immediately from finite to infinite lambda calculus.

Lemma 20. Distinguishable terms are separable.

Proof. Let M = λx_{1}...x_{n}.yM_{1}...M_{m}and N = λx_{1}...x_{n′}.y′N_{1}...N_{m′}. Then, y ≠ y′or n−m ≠ n′− m′. We construct a discriminating context C such that C[M] → → → _{β} P and C[N] → → → _{β} Q for any P and Q as follows:

1. Case y ≠ y′. Suppose n ≥ n′. Let k = n − n′. Then for C[ ] we chose the context (λyy′.[ ]x_{1}...x_{n})(λx_{1}...x_{m}.P)(λx_{1}...x_{m′}x_{m′+1} ...x_{m′+k}.Q).

2. Case y = y′ and n − n′ ≠ m − m′. Suppose n ≥ n′. Since n − n′ ≠ m − m′, we can suppose m > m′+ n − n′. Let k = m − (m′+ n − n′). Now we chose for C[ ] the context (λy.[ ]x_{1}...x_{n}(λy_{1}...y_{k}.P)b_{1}...b_{k−1}Q)K^{m}where y_{1}...y_{k},b_{1}...b_{k−1} are fresh variables.

⊓ ⊔

Lemma 21. Let C be a finite context in β⊥-normal form and let M,N be distinguishable terms. Then C[M] and C[N] are separable.

Proof. We proceed by induction on the depth of the context C.

1. The base case, when C[ ] = [ ], follows from Lemma 20.

2. The inductive case is when C[ ] = λx_{1}...x_{n}.yM_{1}...C′[ ]...M_{m}, Using Theorem 19, we can find a context to Böhm-out C′[M]^{σ} and C′[N]^{σ} where σ = [y:= P_{q}]. Since C is finite, we can find q big enough so the depth of C^{′σ} is equal to depth of C′and the two terms M^{σ} and N^{σ} are still distinguishable.

Theorem 22 (Böhm Theorem extended to infinite terms). If M,N are two different βη!-normal forms without ⊥ then M and N are separable.

Proof. By Theorem 14, there exist P and Q such that M → → → _{η^{−1}} P ∼ Q_{η^{−1}} ← ← ← N. Since M ≠ N and by confluence of βη!, we have that P and Q are different β⊥-normal forms. Let d be the minimal depth where P and Q differ. We truncate the common part of P and Q at depth d and obtain a finite context C (possibly containing ⊥) such that C[P_{0}] ⪯ P and C[Q_{0}] ⪯ Q. Since P and Q are bisimilar we have that P_{0} and Q_{0} are distinguishable. By Lemma 21, we have that C[P_{0}] and C[Q_{0}] are separable. By Lemma 9, we see that P and Q are also separable. Since → → → _{η!} commutes with → → _{β}, we also have that M and N are separable.

⊓ ⊔

We give some examples of separable terms and how to find the separating context:

1. The discriminating context for the terms x and z is C[ ] = (λxz.[ ])PQ.

2. Let M = y and N = λx.yz. Then, M η-expands to λx.yx which is bisimilar to λx.yz. The context C[ ] = (λy.[ ]x)U_{1}^{1} can be used to Böhm-out the variables x and z. Then, we proceed as in the first part.

3. Let M = yy(yx) and N = yy(yz). In this case we would need to substitute the first occurrence of the variable y by U_{2}^{2} and the second occurrence by U_{1}^{1}. This is of course not possible. For this, Böhm invented the trick of the permutators. Since the greatest number of arguments of the variable y is 2, we can make use of the permutator P_{2}. The context C[ ] = (λy.[ ]x)P_{2}U_{2}^{2} does not Böhm-out exactly yx and yz. What it gives is the result of substituting these terms by P_{2}, i.e. we get P_{2}x and P_{2}z. Then, C′[ ] = [ ]aU_{1}^{2} can be used to select x and z from P_{2}x and P_{2}z.

4. Consider the infinite term R_{1} defined using the following recurrence relation: R_{1} = yR_{2}R_{2}, R_{2} = yR_{3}R_{3}R_{3} and so on, where in general, R_{k+1} adds k arguments R_{k} to y. Clearly, the number of arguments that y can have in R_{1} has no bound. To find the discriminating context for the terms M = yR_{1}(yx) and N = yR_{1}(yz), we first consider the truncations M_{0} = y⊥(yx) and N_{0} = y⊥(yz). Now a bound on the number of arguments of the variable y is 2 and in this case we can, then, use the permutator P_{2} to Böhmout the second argument of the first head variable. The discriminating context is, then, exactly the same as for the third part.

7 Equivalence between ⪯_{η} and the contextual preorder ⊆_{h}

We show that the relations ⪯_{η} and ⊆_{h} are the same in the infinitary lambda calculus.

Lemma 23 (Propagation of ⊆_{h} to substitutions of subterms). Let M,N ∈ BT(Λ_{⊥}^{∞} ) such that

λx_{1}...x_{n}.yM_{1}...M_{m} and N = λx_{1}...x_{n}.yN_{1}...N_{m}. If M ⊆_{h} N then M_{i}^{σ} ⊆_{h} N_{i}^{σ} for 1 ≤ i ≤ m where σ = [y:= P_{q}].

Proof. If follows from Theorem 19. ⊓ ⊔

M^{σ} ⊆_{h} N^{σ} does not imply that M ⊆_{h} N. Take M = x, N = yxI and σ = [y:= P_{1}]. As in the previous section, we have to find the appropriate permutator P_{q} to böhm-out the subterms of a term without changing their meaning.

Lemma 24. Let M,N ∈ BT(Λ_{⊥}^{∞} ) such that M is finite and M ≡_{d} N where d is the depth of M. If M ⊆_{h} N then M ⪯ N.

Proof. We proceed by induction on the depth of M. If the depth of M is 0 then M = ⊥ ⪯ N. If the depth of M is not 0 then M ≠ ⊥. Hence, M = λx_{1}...x_{n}.yM_{1}...M_{m} and N = λx_{1}...x_{n′}.y′N_{1}...N_{m′}. By Lemma 20, y = y′ and n − n′= m − m′. Since M and N have even eta expansions, we have that n = n′and m = m′. By Lemma 23, M_{i}^{σ} ⊆_{h} N_{i}^{σ} for 1 ≤ i ≤ m and σ = [y := P_{q}]. Take q greater than the number of symbols of M. Hence the depth of M_{i} and M_{i}^{σ} are the same and by induction hypothesis, M_{i}^{σ} ⪯ N_{i}^{σ} for 1 ≤ i ≤ m. Again q is big enough so M_{i} ⪯ N_{i}. Hence M ⊆ N. ⊓ ⊔

Theorem 25. The following statements are equivalent for terms M,N in Λ_{⊥}^{∞} :

1. M ⪯_{η} N.

2. M ⊆_{h} N.

Proof. (1) ⇒ (2): Let M′⪯ N′be such that BT(M) → → → _{η^{−1}} M′and BT(N) → → → _{η^{−1}} N′. By confluence of β⊥ and the fact that → → → _{η^{−1}} preserves the property of having head normal form, if C[M] has β-head normal form, so does C[M′]. By Lemma 10, C[N′] has β-head normal form. Hence, again by confluence of β⊥ and → → → _{η!} preserves the property of having head normal form, C[M] has β-head normal form.

(2) ⇒ (1): Suppose M ⊆_{h} N. There exists M′ and N′ such that BT(M) → → → _{η^{−1}} M′ ∼ N′_{η^{−1}} ← ← ← BT(N). Since we have that M^{′n}⪯_{η!} M and N =_{η!} N′, by the previous part, we also have that M^{′n}⊆_{h} M ⊆_{h} N =_{h} N′. By Lemma 24, we have that M^{′n}⪯ N′. Hence,

BT(M) → → → _{η^{−1}} M′= ⋃ {M^{′n}| n ∈ ω} ⪯ N′_{η^{−1}} ← ← ← BT(N)

⊓ ⊔

The previous result is part of the infinitary Characterisation Theorem for D_{∞} in [11]. In particular, it says that two terms that have different ∞η-Böhm trees can be discriminated. The complication with the application of the Böhm-out technique to ∞η-Böhm trees is clear. The ∞η-Böhm trees of finite terms can be infinite. The proof in [1] deals with the problem using a relation ≡_{α} which coincides with the equality between ∞η-Böhm trees^{2}. We have solved the problem in a slightly different way using a bisimulation and properties of the truncations.

8 Theories induced by infinitary lambda calculi

We have seen that confluent and normalising infinite extensions (where normal forms can now be infinite too!) induce a normal form function NF : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} that maps a term to its unique normal form. Each normal form function gives rise to an lambda theory:

Eq(NF) = {(M,N) ∈ Λ × Λ | NF(M) = NF(N)}

Because \overline{T N} ⊂ \overline{W N} ⊂ \overline{H N} we get the following strict inclusions:

Eq(BerT) ⊂ Eq(LLT) ⊂ Eq(BT) ⊂ Eq(ηBT) ⊂ Eq(∞ηBT)

We say that Eq(NF) is consistent if it is not the set of all equations Λ × Λ.

Theorem 26. If Eq(NF) is consistent and Eq(BT) ⊆ Eq(NF) then Eq(NF) ⊆ Eq(∞ηBT).

Proof. Suppose there are two finite terms M,N ∈ Λ such that NF(M) = NF(N) and ∞ηBT(M) ≠ ∞ηBT(N). Then by Theorem 25 there exists a context C such that C[M] β-reduces to a head normal form and C[N] does not. Then it is easy to see that for any P ∈ BT(Λ_{⊥}^{∞} ) we have that P = NF(C[M]) = NF(C[N]) = ⊥. ⊓ ⊔

It is tempting to conjecture that the smallest lambda theory that is induced by a confluent and normalising extension of the finite lambda calculus is the one related to the Berarducci trees.

Conjecture 27. Eq(BerT) ⊆ Eq(NF) ⊆ Eq(∞ηBT).

The previous generalises to infinitary theories. These are defined as follows:

Eq^{∞} (NF) = {(M,N) ∈ Λ_{⊥}^{∞} × Λ_{⊥}^{∞} | NF(M) = NF(N)}

It is clear that the previous theorem generalises with help of Theorem 25: Theorem 28. If Eq^{∞} (NF) is consistent and Eq^{∞} (BT) ⊆ Eq^{∞} (NF) then Eq^{∞} (NF) ⊆ Eq^{∞} (∞ηBT). The exact relationship between finitary and infinitary theories is not clear yet.

2 The relation ≡_{α} gives a syntactic characterisation of two β⊥-normal forms with the same ∞η-Böhm tree.

References

1. H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, Revised edition, 1984.

2. M. Barr. Terminal coalgebras for endofunctors on sets. Theoretical Computer Science, 114(2):299–315, 1999.

3. J. Barwise and L. Moss. Vicious circles. CSLI Lecture Notes Number 60, CSLI Publications, Stanford, 1996.

4. A. Berarducci. Infinite λ-calculus and non-sensible models. In Logic and algebra (Pontignano, 1994), pages 339–377. Dekker, New York, 1996.

5. J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Infinite lambda calculus and Böhm models. In Rewriting Techniques and Applications, volume 914 of LNCS, pages 257–270. Springer-Verlag, 1995.

6. J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Infinitary lambda calculus. Theoretical Computer Science, 175(1):93–125, 1997.

7. J. R. Kennaway, V. van Oostrom, and F. J. de Vries. Meaningless terms in rewriting. J. Funct. Logic Programming, Article 1:35 pp, 1999.

8. J.R. Kennaway and F. J. de Vries. Infinitary rewriting. In Terese, editor, Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science, pages 668–711. Cambridge University Press, 2003.

9. P. Severi and F. J. de Vries. A Lambda Calculus for D_{∞}. Technical report, University of Leicester, 2002.

10. P. Severi and F. J. de Vries. An extensional Böhm model. In Rewriting Techniques and Applications, volume 2378 of LNCS, pages 159–173. Springer-Verlag, 2002.

11. P. Severi and F. J. de Vries. Continuity and discontinuity in lambda calculus. In Typed Lambda Calculus and Applications, volume 3461 of LNCS. Springer-Verlag, 2005.

12. P. Severi and F. J. de Vries. Order Structures for Böhm-like models. In Computer Science Logic, volume to appear of LNCS. Springer-Verlag, 2005.

13. C. P. Wadsworth. The relation between computational and denotational properties for Scott’s D_{∞} -models of the lambda-calculus. SIAM Journal on Computing, 5(3):488–521, 1976.