To appear in the Proceedings of the 13th International Conference on Rewriting, Techniques and Applications, RTA’02

An Extensional Böhm Model

Paula Severi^{1}^{⋆} and Fer-Jan de Vries^{2}

1 Departimento di Informatica, Università di Torino. Corso Svizzera 185, 10149 Torino, Italy - severi@di.unito.it

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

Abstract. We show the existence of an infinitary confluent and normalising extension of the finite extensional lambda calculus with beta and eta. Besides infinite beta reductions also infinite eta reductions are possible in this extension, and terms without head normal form can be reduced to bottom. As corollaries we obtain a simple, syntax based construction of an extensional Böhm model of the finite lambda calculus; and a simple, syntax based proof that two lambda terms have the same semantics in this model if and only if they have the same eta-Böhm tree if and only if they are observationally equivalent wrt to beta normal forms. The confluence proof reduces confluence of beta, bottom and eta via infinitary commutation and postponement arguments to confluence of beta and bottom and confluence of eta. We give counterexamples against confluence of similar extensions based on the identification of the terms without weak head normal form and the terms without top normal form (rootactive terms) respectively.

1 Introduction

In this paper we present a confluent infinitary extension λ_{β⊥η}^{h∞} of the extensional lambda calculus λ_{βη}. In earlier work confluent infinitary extensions of the lambda calculus λ_{β} without the eta rule have been studied. Typically, confluence of such infinitary extensions cannot be obtained unless we add a form of bottom rule that identifies computationally insignificant terms with some added symbol ⊥. Different choices of computationally insignificant terms may lead to different confluent and normalising extensions. The main three choices, the set of terms without head normal form, the set of terms without weak head normal form and the set of terms without top normal form (rootactive terms) result in three different confluent and normalising calculi in which the normal forms are respectively known as Böhm trees, Lévy-Longo trees and Berarducci trees. In contrast, here for extensional lambda calculus we have no choice: only identification of all terms without head normal form with ⊥ results in the confluent, normalising calculus λ_{β⊥η}^{h∞}. The normal forms of this calculus are known as eta-Böhm trees [2]. As corollaries of confluence and normalisation we obtain a simple,

⋆ Partially supported by IST-2001-322222 MIKADO; IST-2001-33477 DART.

syntax based, construction of an extensional Böhm model �_{η} of the finite lambda calculus; plus a new and simple syntax based proof that two lambda terms have the same semantics in this model if and only if they have the same eta-Böhm tree if and only if they are observationally equivalent wrt to beta normal forms. Hence this extensional Böhm model �_{η} equates more terms than Barendregt’s Böhm model � in [3]). It induces the same equality relation as Park’s model D_{∞}^{∗} of [16, 6, 17]. The eta rule has not been considered before in infinitary lambda calculus mainly because of a counterexample [12, 11] showing that arbitrary transfinite βηreductions can not be compressed into reductions of at most ω length, as in the case without eta, since infinite β-reduction can create an eta redex.^{1} The confluence proof in [12] heavily depended on compression. The recent approach of [11] uses transfinite induction and postponement of ⊥-reduction over β-reduction. In this paper we will follow the postponement proof technique. Roughly speaking we will show that any transfinite mixed β⊥η-reduction factors into a β⊥- reduction followed by an η-reduction. Confluence of β⊥η-reduction then follows from confluence of β⊥-reduction, commutation of β-reduction and ⊥-reduction with η-reduction, and confluence of η-reduction. The commutation of η-reduction and ⊥-reduction requires care: in general only outermost (or maximal [3]) ⊥- reduction commutes with η-reduction, which can be easily overlooked, already in finite lambda calculus. The calculus λ_{β⊥η}^{h∞} is normalising: given a term one first reduces it via a leftmost outermost β⊥-reduction to its Böhm tree, and then via a leftmost outermost ηreduction to its eta-Böhm tree. This two step process cannot really be improved upon. We will show that at most ω+ω steps are needed to compute the eta-Böhm tree of a lambda term. Using the notation of the counterexample in the footnote against ω-compression, the term z(λx.Ex)(λx.Ex)(λx.Ex) … is an example of a term that needs at least ω+ω steps to reduce to its eta-Böhm tree zy^{ω}y^{ω}y^{ω} . . .. This contrasts with the three infinitary extensions of λ_{β}, where the reduction to normal form needs at most ω steps.

2 Infinite Lambda Calculus

Infinite lambda calculus houses besides the usual finite terms and reductions also infinite terms and infinite, converging reduction. It incorporates in a natural way the open-ended view on computation that, as the computation of a program proceeds, more and more information is read from the input, and more and more of the output is produced. We will now recall some notions and facts of infinite lambda calculus presented in [12, 11]. We assume familiarity with basic notions and notations from [3].

1 Consider a term E with the property that Ex →_{β}^{∗} y(Ex) (e.g. the term E = Ω_{λzw.y(zw)} in the notation of Definition 1) and the term y^{ω} = y(y(y(…))). Then λx.Ex →_{β}^{∗} λx.(y(Ex))x →_{β}^{∗} λx.y(y(Ex))x → →_{β}^{ω} λx.y^{ω}x →_{η} y^{ω}. This example is related to the example of 10.1.22 in [3].

Let Λ_{⊥} be the set of finite λ-terms given by the inductive grammar:

M ::= ⊥ | x | MM | λx.M

Let u be any finite sequence of 0, 1 and 2’s. The subterm M|_{u} of a term M ∈ Λ_{⊥} at occurrence u (if there is one) is defined by induction as usual:

M|_{⟨⟩} = M (λx.M)|_{0u} = M|_{u} (MN)|_{1u} = M|_{u} (MN)|_{2u} = N|_{u}

We will define three length related measures for occurrences: length_{h}(u) is the number of 2’s in u, length_{w}(u) is the number of 0’s and 2’s in u and finally length_{t}(u) is the number of 0’s, 1’s and 2’s in u. The depth at which a subterm N in M occurs can now be measured by the length of the occurrence u of N in M. This leads to three different metrics d_{x} on Λ_{⊥} for x ∈ {h, w, t}: x-metric d_{x}(M, N) = 0, if M = N and d_{x}(M, N) = 2^{−length_{x}(u)}, where u is a common occurrence of minimal length such that M|_{u} ≠ N|_{u}. Now in the spirit of Arnold and Nivat [1] we define the sets Λ_{⊥}^{h∞}, Λ_{⊥}^{w∞} and Λ_{⊥}^{t∞} as the metric completions of the set of finite lambda terms Λ_{⊥} over the respective metrics d_{h}, d_{w} and d_{t}. The indices h, w and t stand for head normal form, weak head normal form and top normal form respectively. It may be illustrative to draw pictures and to think of terms as trees: draw the edges corresponding to the counted occurrences vertically and all other edges horizontally. Then trees in the three metric completions don’t have infinite horizontal branches. In case of Λ_{⊥}^{h∞} this implies, when paths of branches are coded by sequences of 0, 1 and 2’s, that its trees are characterised by the fact that their branches don’t have infinite “tails” consisting of 0 and 1’s only.

Definition 1. Some abbreviations for useful finite and infinite λ-terms:

\begin{aligned}I & = & λx.x & K_{∞} & = & λx.λx. … & Ω & = & (λx.xx)λx.xx \\ 1 & = & λxy.xy & M^{ω} & = & M(M(M …)) & Ω_{M} & = & (λx.M(xx))λx.M(xx) \\ K & = & λxy.x & ^{ω}M & = & ((… M)M)M & Ω_{η} & = & λx_{0}.(λx_{1}.(…)x_{1})x_{0} \end{aligned}

The inclusions Λ_{⊥}^{h∞} ⊂ Λ_{⊥}^{w∞} ⊂ Λ_{⊥}^{t∞} are strict. For instance, x^{ω} ∈ Λ_{⊥}^{h∞}, K_{∞} ∈ Λ_{⊥}^{w∞} − Λ_{⊥}^{h∞} and ^{ω}x ∈ Λ_{⊥}^{t∞} − Λ_{⊥}^{w∞}. As shown in [12, 11] the sets Λ_{⊥}^{h∞}, Λ_{⊥}^{w∞} and Λ_{⊥}^{t∞} are the three minimal infinitary extensions of the finite lambda calculus λ_{β} containing respectively the Böhm trees, Lévy-Longo trees and the Berarducci trees and each closed under its respective notion of convergent reduction to be defined next. The set Λ_{⊥}^{h∞} will function as the underlying set of finite and infinite lambda terms for our extensional infinitary extension λ_{β⊥η}^{h∞}. Many notions of finite lambda calculus apply and/or extend more or less straightforwardly to the infinitary setting. The main idea which goes back to Dershowitz e.a. in [8] is that 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 M_{0} →_{α} M_{α} is called Cauchy converging. We need the stronger concept of a strongly converging reduction that in addition satisfies that the depth of the reduced redexes goes to infinity at each limit term: lim_{β→λ} d_{β} = ∞ for each limit ordinal λ ≤ α, where d_{β} is the depth in M_{β} of the reduced redex in M_{β} → M_{β+1}. We will denote strongly converging reduction by → →. Any finite reduction M_{0} →^{∗} M_{n} is strongly converging. Finally we have to introduce the basic reduction relations of λ_{β⊥η}^{h∞}. Besides the familiar beta and eta rules it contains one of the bottom rules ⊥_{h} (or ⊥ for short). We define three bottom rules ⊥_{x} where x ∈ {h, w, t} as follows:

M → ⊥, provided M[⊥ := Ω] ∈ U_{x} (⊥_{x})

We usually omit the subscript x and we write ⊥ instead of ⊥_{x}. Outermost bottom reduction, denoted as →_{⊥_{out}}, is the restriction of bottom reduction to outermost redexes. The sets U_{x} are sets of ⊥-free finite and infinite lambda terms and defined as follows:

1. The (for this paper most important) set U_{h} is the set of ⊥-free terms in Λ_{⊥}^{h∞} that don’t have (a finite β-reduction to) a head normal form, where a term is a head normal form if it is of the form λx_{1} … λx_{n}.yM_{1} … M_{m}.

2. The set U_{w} is the set of ⊥-free terms in Λ_{⊥}^{w∞} that don’t have (a finite βreduction to) a weak head normal form, where a term is a weak head normal form if it is either a term of the form yM_{1} … M_{n} or an abstraction λx.M.

3. The set U_{t} is the set of ⊥-free terms in Λ_{⊥}^{t∞} that don’t have (a finite βreduction to) a top normal form (rootstable form), where a term is a top normal form, if it is either an abstraction λx.M, or, an application MN where M cannot β-reduces (in a finite number of steps) to an abstraction.

Some examples: The term Ω does not have a top normal form and therefore belongs to all three sets. The term Ωx is a top normal form but has no (weak) head normal form. The term λx.Ω is a weak head normal form, but has no head normal form. Hence all inclusions in U_{h} ⊃ U_{w} ⊃ U_{t} are strict. The extensional infinite lambda calculus that is the main object of study in this paper is the calculus λ_{β⊥η}^{h∞} = (Λ_{⊥}^{h∞}, →_{β⊥η}). We will also briefly mention λ_{β⊥η}^{x∞} = (Λ_{x}^{∞}, →_{β⊥η}) for x ∈ {w, t}. For any of these infinite lambda calculi λ_{ρ}^{x∞} we say that

– a term M in λ_{ρ}^{x∞} is in ρ-normal form if there is no N in λ_{ρ}^{x∞} such that M →_{ρ} N.

– λ_{ρ}^{x∞} is infinitary confluent (or just confluent for short) if (Λ_{x}^{∞}, → →_{ρ}) satisfies the diamond property, i.e. _{ρ} ← ← ∘ → →_{ρ} ⊆ → →_{ρ} ∘ _{ρ} ← ←.

– λ_{ρ}^{x∞} is (weakly) normalising if for all M ∈ Λ_{x}^{∞} there exists an N in ρ-normal form such that M → →_{ρ} N.

– Let α be an ordinal. We say that λ_{ρ}^{x∞} is α-compressible if for all M, N such that M → →_{ρ} N there exists a reduction from M to N of length at most α.

Without the bottom rule there is no chance of proving confluence. Berarducci’s counterexample [5] is very short: Ω _{β}^{∗}← Ω_{I} → →_{β} I^{ω}. Crucial properties of those three infinite lambda calculi λ_{β⊥}^{h∞}, λ_{β⊥}^{w∞} and λ_{β⊥}^{t∞} are:

Theorem 1. Confluence, normalisation and compression of β⊥ [12, 11]. The infinite lambda calculi λ_{β⊥}^{h∞}, λ_{β⊥}^{w∞} and λ_{β⊥}^{t∞} are confluent, normalising and ω-compressible.

Theorem 2. Postponement of β over ⊥ [11]. If M → →_{β⊥} N then there exists Q such that M → →_{β} Q → →_{⊥} N.

3 Two non-confluent extensional infinite lambda calculi

Before we give the proof of confluence of λ_{β⊥η}^{h∞} we will show that the two related extensional infinite lambda calculi λ_{β⊥η}^{w∞} and λ_{β⊥η}^{t∞} are not confluent. In fact what we note is that already the finite calculi λ_{β⊥η}^{w} and λ_{β⊥η}^{t} are not confluent for finite reductions. For this we use the term Ω_{η} ∈ Λ_{⊥}^{w∞} ⊂ Λ_{⊥}^{t∞}. Similar to Ω which β-reduces to itself in only one step, this term η-reduces to itself in only one step. The body of the outermost abstraction in Ω_{η} has no weak (top) normal form. The span ⊥ _{⊥}← Ω_{I} _{η}← Ω_{1} → →_{β} Ω_{η} →_{⊥} λx.⊥ can only be joined if λx.⊥ →_{⊥} ⊥, which does not hold for the ⊥_{w}-rule and the ⊥_{t}-rule. Hence this is a counterexample of confluence of both λ_{β⊥η}^{w∞} and λ_{β⊥η}^{t∞}. Remark also that there is a critical pair between the eta rule and each bottom rule: λx.⊥ _{⊥}← λx.⊥x →_{η} ⊥. The reverse step follows from the fact that the term ⊥x[⊥ := Ω] := Ωx has no weak head normal form. This pair can be completed only if λx.⊥ →_{⊥} ⊥ which is true for the ⊥_{h}-rule, but not for the ⊥_{w}-rule. This gives an alternative counterexample against confluence of λ_{β⊥η}^{w∞}.

4 The confluent extensional infinite lambda calculus λ_{β⊥η}^{h∞}

In this section we will prove the confluence and normalisation of λ_{β⊥η}^{h∞}. Thereto we will first prove some useful properties of the infinitary eta calculus λ_{η}^{h∞}, secondly the commutation of eta and beta and the commutation of eta and outermost bottom, and thirdly postponement of eta over beta and bottom.

4.1 The infinitary eta calculus λ_{η}^{h∞}

The set Λ_{⊥}^{h∞} has the very pleasant property that any Cauchy-converging ηreduction sequence in Λ_{⊥}^{h∞} is h-strongly convergent. This property is not shared by the other two infinitary extensions Λ_{⊥}^{w∞} and Λ_{⊥}^{t∞}. For instance there exists a Cauchy-converging and non-h-strongly converging η-reduction sequence from the term Ω_{η} ∈ Λ_{⊥}^{w∞} ⊂ Λ_{⊥}^{t∞}.

Definition 2. For M ∈ Λ_{⊥}^{h∞} define |M|_{n} as the number of nodes at h-depth n.

The number |M|_{n} of nodes of term M at h-depth n decreases if and only if we contract an η-redex in M at h-depth n. Hence:

Lemma 1. Any Cauchy-converging η-reduction starting from a term in Λ_{⊥}^{h∞} is h-strongly convergent.

Proof. Suppose by contradiction that we have some transfinite Cauchyconverging η-reduction sequence M_{0} →_{η} M_{1} →_{η} …, that reduces infinitely often at h-depth n. Then infinitely many of the inequalities in the next sequence are strict: |M_{0}|_{n} ≥ |M_{1}|_{n} ≥ |M_{2}|_{n} ≥ … But infinite strictly decreasing sequences of natural numbers don’t exist. Hence the limit of the h-depth of the contracted redexes in this sequence goes to infinity at each limit ordinal ≤ α. Therefore any η-reduction sequence starting from a term in Λ_{⊥}^{h∞} is h-strongly converging. ⊓ ⊔

Lemma 2. The infinitary lambda calculus λ_{η}^{h∞} is ω-compressible.

Proof. Let M → →_{η} N a reduction sequence of length γ. We will prove that there exists a sequence from M to N of length at most ω. The proof proceeds by transfinite induction on γ. The argument of the limit case is standard, see [11]. If γ is a successor ordinal, it is sufficient to prove that a sequence of length ω +1 can be compressed into one of length ω. Without loss of generality, we may suppose that we have a strongly η-reduction sequence of length ω + 1 from M_{0} to M_{ω} as in:

[figure: M_{0}; ∗; η; λx.M_{k}x; η; η; λx.M_{k+1}x; η; η; λx.M_{k+2}x; η; λx.M_{ω}x; η; M_{k}; η; M_{k+1}; η; M_{k+2}; M_{ω}]

Then working to the right onwards from λx.M_{k}x the dotted squares can be all constructed. This results in a reduction of length ω starting at M_{0} and after k + 1 steps continuing as M_{k} →_{η} M_{k+1} →_{η} . . .. The limit of this converging reduction is clearly M_{ω}. ⊓ ⊔

In the following lemma, as well as later for other reduction relations, we indicate with a superscript that the redex contracted in M →_{η}^{m} N is at depth m.

Lemma 3. Let M_{0} be a term in Λ_{⊥}^{h∞}. If M_{0} →_{η}^{m} M_{1} and M_{0} →_{η}^{n} M_{2} then one of the following two cases holds:

[figure: M_{0}; η; m; η; n; M_{1}; η; n; M_{2}; η; m; M_{3}; M_{0}; η; n; η; n; M_{1}; M_{2}; M_{3}]

Proof. Note that the h-depth of an η-redex in a term does not change when we contract an η-redex elsewhere in the term. ⊓ ⊔ Theorem 3. The infinitary lambda calculus λ_{η}^{h∞} is confluent.

Proof. Let two coinitial η-reductions be given. By compression (Lemma 2) we may assume that their length is at most ω. By simultaneous induction on their length we show that for any two coinitial η-reductions can be joined with a so called tiling diagram construction [11] in which all horizontal and vertical reductions are strongly converging. Suppose we have two η-reductions of length ω: M_{0,0} → →_{η} M_{0,ω} and M_{0,0} → →_{η} M_{ω,0}. We will not present the whole induction, but comment on the main cases.

The successor-successor case of the induction is in fact the previous lemma.

The successor-limit case: this follows if we can construct the following tiling diagram in which the notation M →_{η}^{=} N expresses that in the reduction from M to N in which at most one reduction step has been performed: at h-depth m.

[figure: M_{0,0}; η; n_{0}; η; m_{0}; M_{0,1}; η; n_{1}; η; m_{0}/=; M_{0,2}; η; m_{0}/=; M_{0,ω}; η; m_{0}/=; M_{1,0}; η; n_{0}/=; M_{1,1}; η; n_{1}/0; M_{1,2}; M_{1,ω}]

By induction hypothesis this diagram can be constructed but for the right most edge. The bottom reduction inherits the (strong) convergence property from the top reduction. As we are dealing with η-reduction it is easy to see that there is at most one residual of the redex contracted in M_{0,0} →_{η} M_{1,0} in M_{0,ω}. Contraction of this set of residuals gives the reduction of the rightmost edge: it will be at most one step.

The limit-limit case: Using the induction hypothesis we can construct diagrams for pair of coinitial sequences of respective lengths (n, m) where either n < ω and m ≤ ω, or m < ω and n ≤ ω. By the general tiling diagram theorem in [11] or in this particular instance simply the uniform nature of the strong convergence of all vertical and horizontal reductions it follows that their limits have to be

[figure: M_{0,0}; η; n_{0}; η; m_{0}; M_{0,1}; η; n_{1}; η; m_{0}/=; M_{0,2}; η; m_{0}/=; M_{0,ω}; η; m_{0}/=; M_{1,0}; η; n_{0}/=; η; m_{1}; M_{1,1}; η; n_{1}/0; η; m_{1}/=; M_{1,2}; η; m_{1}/=; M_{1,ω}; η; m_{1}/=; M_{2,0}; η; n_{0}/=; M_{2,1}; η; n_{1}/=; M_{2,2}; M_{2,ω}; M_{ω,0}; η; n_{0}/=; M_{ω,1}; η; n_{1}/=; M_{ω,2}; M_{ω,ω}]

the same: M_{ω,ω}. ⊓ ⊔

Theorem 4. The infinitary lambda calculus λ_{η}^{h∞} is normalising.

Proof. Let M_{0} be given. We construct a reduction M_{0} →_{η} M_{1} →_{η} M_{2} … recursively: suppose we have M_{n} then we construct M_{n+1} by contracting the leftmost η-redex of smallest h-depth. This gives us a possibly infinite reduction which by Lemma 1 can only be strongly converging. Its last term is an η-normal form.

This is trivial in case of a finite reduction; in case of an infinite reduction, there is a standard reductio ad absurdum argument: Suppose there is a η-redex in the limit term, then this η-redex was already present at some finite stage in the reduction and apparently not reduced in the remaining reduction. But the reduction strategy is such that no redex can get overlooked. Contradiction. ⊓ ⊔

4.2 Commutation

In this section we prove that the reductions → →_{η} commutes with both → →_{β} and → →_{⊥}. As each of these reduction relations on its own is ω-compressible we can assume that the length of the reductions is at most ω.

Theorem 5. [Commutation of → →_{β} and → →_{η}] If M_{0,0} → →_{β} M_{0,γ} and M_{0,0} → →_{η} M_{δ,0} then there exists M_{δ,γ} such that M_{0,γ} → →_{η} M_{δ,γ} and M_{δ,0} → →_{β} M_{δ,γ}.

Proof. A double induction on the length of the two sequences, respectively γ and δ. The critical cases in this proof are: (1, 1), (1, ω), (ω, 1) and (ω, ω).

(γ, δ) = (1, 1): This case is a careful analysis of cases based on the relative positions of the β-redex and the η-redex. Suppose M_{0} can do both a β-reduction and an η-reduction at respectively h-depth n and m. The possible situations are:

1. The redexes do not interfere with each other:

(a) The redexes are not nested, i.e. M_{0,0} = C[(λx.M)N, (λy.P y)].

(b) The β-redex is inside the η-redex, that is M_{0,0} is of the form C_{1}[λx.C_{2}[(λy.M)N]x].

(c) The η-redex is inside the body of the abstraction, that is M_{0,0} is of the

form C_{1}[(λx.C_{2}[λy.My])N].

2. The η-redex is inside the argument of the application, that is M_{0,0} is of the form C_{1}[(λx.M)C_{2}[λy.Ny]].

3. The β-redex and η-redex overlap, that is M_{0,0} is either C[(λx.Mx)N] or C[λx.(λy.M)x].

These possibilities result in three different diagrams (the labels on the arrows refer to the h-depth of the contracted redex):

[figure: M_{0,0}; η; m; β; n; M_{0,1}; β; n; M_{1,0}; η; n; M_{1,1}; M_{0,0}; η; m; β; n; M_{0,1}; β; n; M_{1,0}; η; ≥m−1; M_{1,1}; M_{0,0}; η; n; β; n; M_{0,1}; M_{1,0}; M_{1,1}]

It is important to note that the depth of the eventual residual of β-redex remains the same after contraction of the η-redex.

(γ, δ) = (1, ω): This case is simple. The construction of the commutation diagram comes down to an infinite horizontal chain of base case diagrams. Either the β gets cancelled against one of the η-steps or not. This implies that from a certain point onwards the vertical edges are equalities or not.

(γ, δ) = (ω, 1): This case is somewhat involved. Using the previous case we construct for any natural number n the horizontal reduction M_{n,0} → →_{η} M_{n,1}. This way we get the vertical reduction on the right M_{1,0} →_{β} M_{1,1} →_{β} M_{1,2} →_{β} … which is strongly converging because its reduction steps take place at the same depth as the corresponding steps on the left. Hence it has a limit, say M_{ω,1}. In fact each horizontal η-reduction is the complete development of a set V_{n} of (occurrences of) η-redexes in M_{n,0}. The missing η-reduction at the bottom can now be filled in: complete development of the set of

\xymatrix{M_{0,0} \ar[r]_{η} \ar[d]^{β} & M_{0,1} \ar[d]^{β}_{=} \\ M_{1,0} \ar@{->>}[r]_{η} \ar[d]^{β}_{=} & M_{1,1} \ar@{->>}[d]^{β}_{=} \\ M_{ω,0} \ar@{->>}[r]^{η} & M_{ω,1}}

(occurrences of) η-redexes ⋃_{k≥0} ⋂_{m≥k} V_{m} gives us precisely a strongly convergent reduction M_{ω,0} → →_{η} M_{ω,1}.

(γ, δ) = (ω, ω): Repeated application of the previous two cases allows us to construct the tiling diagram. The vertical β-reductions are all strongly converging in a uniform way: at most some β-steps can get cancelled, but the h-depth of the remaining β-residuals remains unaltered. The horizontal η-reduction sequences cannot be else than strongly converging by Lemma 1. Using the tiling diagram theorem of [12] or the uniform (nature of the) strong

[figure: M_{0,0}; η; β; M_{0,1}; η; β; =; M_{0,2}; β; =; M_{0,ω}; β; =; M_{1,0}; η; β; M_{1,1}; η; β; =; M_{1,2}; β; =; M_{1,ω}; β; =; M_{2,0}; η; M_{2,1}; η; M_{2,2}; M_{2,ω}; M_{ω,0}; η; M_{ω,1}; η; M_{ω,2}; M_{ω,ω}]

convergence of all vertical reductions we get that the bottom reduction and the rightmost reduction both end in the same limit term. ⊓ ⊔

Commutation of → →_{η} with → →_{⊥} does not hold as it is shown by the counterexample Ω _{η} ← λx.Ωx →_{⊥} λx.⊥. However, if we restrict ourselves to leftmost outermost ⊥ reduction we can prove commutation of → →_{η} with → →_{⊥}. First a lemma saying that ⊥-redexes are preserved under η-reduction.

Lemma 4. Let M ∈ Λ_{⊥}^{h∞} be a ⊥-free term and M → →_{η} N.

1. If M is a β-head normal form then so is N.

2. If N is a β-head normal form then M has a β-head normal form.

3. M ∈ U_{h} if and only if N ∈ U_{h}.

Proof. 1. Standard inductive argument on the length of the η-reduction.

2. Without loss of generality we may assume that an η-reduction ending in a β-head normal form is finite. By induction on the length n of this reduction we will show that there is a reduction of linear β-redexes from the initial term to a β-hnf, where a β-redex (λx.P)Q is linear if the bound variable x occurs free in P at most once.

The base case, when n = 0, is trivial. Induction step: suppose M →_{η} P →_{η}^{n} N and N is a β-hnf. By induction hypothesis there exists P′ in β-head normal form such that P →_{β}^{∗} P′ by contraction of linear β-redexes. By Lemma 5 (its proof does not depend on this result nor the next theorem) we can postpone the η-step from M to P over the linear β-reduction to P′, so that we get M →_{β}^{∗} M′ →_{η}^{=} P′, where the β-reduction contracts linear β-redexes. An easy case analysis shows that either M′ is in β-head normal form or reduces to one by contracting a linear β-redex.

3. Suppose that N β-reduces to a head normal form. Then M β-reduces to a head normal form by postponement of η-reduction over β-reduction (Lemma 5) and the previous part. The converse is proved similarly using commutation instead of postponement. ⊓ ⊔

Theorem 6. Commutation of → →_{η} with → →_{⊥}_{out}. If M_{0,0}→ →_{⊥}_{out}M_{0,γ} and M_{0,0} → →_{η} M_{δ,0} then there exists M_{δ,γ} such that M_{0,γ} → →_{η} M_{δ,γ} and M_{δ,0}→ →_{⊥}_{out}M_{δ,γ}.

Proof. The induction proof proceeds as the previous proof of Theorem 5. We skip all cases but:

(γ, δ) = (1, 1): A careful analysis of cases based on the relative positions of the ⊥_{out}-redex (denoted by U below) and the η-redex leads to two basic situations:

– The ⊥-redex is inside the η-redex: M_{0,0} ≡ C_{1}[λx.C_{2}[U]x].

– The η-redex is inside the ⊥-redex: M_{0,0} ≡ C_{1}[C_{2}[λx.Mx]] ≡ C_{1}[U].

These two cases result in the following two diagrams:

[figure: M_{0}; η; m; ⊥_{out}; n; M_{1}; ⊥_{out}; n; M_{2}; η; m; M_{3}; M_{0}; η; m; ⊥_{out}; n; M_{1}; ⊥_{out}; n; M_{2}; M_{2}]

Note that the h-depth of the ⊥_{out}-redex and its eventual residual after contraction of the η-redex is the same. The last case follows from Lemma 4. ⊓ ⊔

4.3 Postponement

We will prove that η-reduction can be postponed in mixed β⊥η-reductions and hence as as well in mixed βη-reductions. We first need two preparatory lemmas.

Lemma 5. Let γ, δ ≤ ω. If M_{0,0} → →_{η} M_{0,γ} → →_{β} M_{δ,γ}, then there exists an M_{δ,0} such that M_{0,0} → →_{β} M_{δ,0} → →_{η} M_{δ,γ}. If M_{0,γ} → →_{β} M_{δ,γ} is finite, then M_{0,0} → →_{β} M_{δ,0} will be finite as well.

Note: in (λx.(λy.M)x)N →_{η} (λy.M)N →_{β} M[x := N] the resulting reduction after postponement of η-reduction requires two β-reduction steps.

Proof. The proof is again a double induction on the length of the two reductions. In the proof we try to reconstruct a tiling diagram for:

\xymatrix{M_{0,0} \ar@{->>}[r]_{η} \ar@{->>}[d]^{β} & M_{0,γ} \ar@{->>}[d]^{β} \\ M_{δ,0} \ar@{->>}[r]_{η} & M_{δ,γ}}

The proof by induction is an interesting variation on the proof of commutation of β and η. We skip all cases but one:

(γ, δ) = (1, ω): Suppose the contracted redex in the final β-reduction M_{0,ω} →_{β} M_{1,ω} has h-depth n. Then because M_{0,0} → →_{η} M_{0,ω} is strongly converging, there is a k such that for i ≥ k the depth of all remaining η-redexes in M_{0,k} → →_{η} M_{0,ω} is at least n.

[figure: M_{0,0}; ∗; n; β; η; ∗; (ind hyp); M_{0,k}; η; >n; β; n; M_{0,ω}; β; n; M_{1,0}; η; M_{1,k}; η; M_{1,ω}]

Hence all M_{0,i} for i ≥ k contain a β-redex at the same position as the one redex contracted in M_{0,ω}. Let M_{1,i} be the result of contracting that β-redex in M_{0,i}. Since the η-reduction at M_{0,i} takes place at depth lower than n, we get case 1 (a and c) and case 2 of the proof of Theorem 5 and hence M_{1,i} → →_{η} M_{1,i+1}. By Lemma 1 this reduction sequence is strong converging and its limit coincides with M_{1,ω}. An appeal to Theorem 5 completes the proof of this case. ⊓ ⊔

The next lemma is proved in a similar way.

Lemma 6. If M_{0,0} → →_{η} M_{0,γ} → →_{⊥} M_{δ,γ}, then there exists an M_{δ,0} such that M_{0,0} → →_{⊥} M_{δ,0} → →_{η} M_{δ,γ}. If M_{0,γ} → →_{⊥} M_{δ,γ} is finite, then M_{0,0} → →_{⊥} M_{δ,0} will be finite as well.

Proof. The proof is a double induction. We only do the case (δ, γ) = (1, 1), and skip the rest. By case analysis and using Lemma 4 we obtain the following two diagrams:

[figure: M_{0,0}; η; m; ⊥; n; M_{0,1}; ⊥; n; M_{1,0}; η; m; M_{1,1}; M_{0,0}; η; m; ⊥; n; M_{0,1}; ⊥; n; M_{1,0}; M_{1,1}]

⊓ ⊔

Combining the previous two lemmas with Theorem 2 we get:

Corollary 1. If M_{0,0} → →_{η} M_{0,γ} → →_{β⊥} M_{δ,γ}, then there exists an M_{δ,0} such that M_{0,0} → →_{β⊥} M_{δ,0} → →_{η} M_{δ,γ}. If M_{0,γ} → →_{β⊥} M_{δ,γ} is finite, then M_{0,0} → →_{β⊥} M_{δ,0} will be finite as well.

Theorem 7. Postponement of → →_{η} over → →_{β⊥}. If M → →_{β⊥η} N, then there exists an L such that M → →_{β⊥} L → →_{η} N.

Proof. The proof is by (a genuine!) transfinite induction on the number of subsequences of the form M_{1} → →_{η} M_{2} → →_{β} M_{3} in M → →_{β⊥η} N. The base case is trivial, the successor case follows directly from Corollary 1. We only show the limit case for the limit ω. The proof for arbitrary limits is similar. Consider:

M ≡ M_{1,0} → →_{η} M_{1,1} → →_{β⊥} M_{2,1} → →_{η} M_{2,2} → →_{β⊥} M_{3,2} . . . . . . M_{ω,ω} ≡ N

Using the induction hypothesis we construct the next diagram row by row.

[figure: M_{1,0}; η; β⊥; M_{1,1}; β⊥; M_{2,0}; η; M_{2,1}; η; M_{2,2}; M_{ω,0}; η; M_{ω,1}; η; M_{ω,2}; η; M_{ω,ω}]

Because the diagonal is strongly converging and the horizontal η-reductions don’t change the depth of the vertical β⊥-reductions, all vertical reductions are strongly convergent as well and have limits. By induction hypothesis they are connected by η-reduction steps. By Lemma 1 the combined reduction at the bottom row is strongly converging. By the uniform nature of the strong convergence of all vertical reductions the limit of reductions at the bottom row and the diagonal are the same. ⊓ ⊔

Corollary 2. Let M, N ∈ Λ_{⊥}^{h∞}.

1. If M → →_{η} N, then nf_{β⊥}(M) → →_{η} nf_{β⊥}(N).

2. If M → →_{β⊥η} N, then nf_{β⊥}(M) → →_{η} nf_{β⊥}(N).

Proof.

To prove the first item we postpone ⊥ over β (Theorem 2). Next because the ⊥-reduction ends in a β⊥-normal form we can remove all non-outermost ⊥-steps. Then we can construct the diagram on the left using the two commutation theorems. The term N_{2} is in β⊥-normal form, and hence by the unique β⊥-normal form

[figure: M; η; β; (Thm. 5); β⊥; N; β; M_{1}; η; ⊥_{out}; (Thm. 6); N_{1}; ⊥_{out}; nf_{β⊥}(M); η; N_{2}]

property (Theorem 1) we get N_{2} = nf_{β⊥}(N).

For the proof of second item we build the diagram below using postponement of η-reduction over β⊥-reduction (Theorem 7) and the previous part.

[figure: M; β⊥η; β⊥; β⊥; (Thm. 1); P; η; β⊥; (Part 1); N; β⊥; nf_{β⊥}(M); η; nf_{β⊥}(P); η; nf_{β⊥}(N)]

⊓ ⊔

4.4 Confluence and normalisation

Finally we prove that λ_{β⊥η}^{h∞} is confluent, normalising and ω + ω-compressible.

Theorem 8. Confluence of β⊥η. The extensional infinite lambda calculus λ_{β⊥η}^{h∞} is confluent.

Proof.  [figure: M_{0}; β⊥η; β⊥η; β⊥; M_{1}; β⊥; (Cor 2); nf_{β⊥}(M_{0}); η; η; (Thm 3); M_{2}; β⊥; (Cor 2); nf_{β⊥}(M_{1}); η; nf_{β⊥}(M_{2}); η; M_{3}]

⊓ ⊔

Our proof technique using postponement has the flavour of the confluence proof for finite λ_{βη} of Curry and Feys [7], and may therefore seem to be related to the confluence proof of the finite λ_{β⊥η} of 15.2.15(ii) in [3]. The latter proof makes use of η-normal forms, whereas we use the auxiliary notion of β⊥-normal forms. Note, however, that η-normal forms don’t work, as can be seen by applying the proof technique of [3] to the coinitial reductions Ω _{η}← λx.Ωx →_{⊥} λx.⊥. In its compact form our proof does not restrict to a confluence proof for λ_{β⊥η}. But it is not hard to distill from the previous proofs a proof for the finite setting that make use of ⊥-normal forms instead of β⊥-normal forms. It may be of interest to see whether other proofs of finitary confluence for finite λ_{β⊥η} can be generalised to the infinitary setting. For instance: the older proof of Barendregt, Bergstra, Klop and Volken [4] and the more recent proof by van Oostrom [15].

Theorem 9. Normalisation and compression of β⊥η. The extensional infinite lambda calculus λ_{β⊥η}^{h∞} is normalising and is ω + ω-compressible.

Proof. By theorems 1, 3 and 2, the calculi λ_{β⊥}^{h∞} and λ_{η}^{h∞} are confluent, normalising and ω-compressible. The β⊥η-normal form of a term can be obtained by first computing the β⊥-normal form and then the η-normal form. To prove thatλ_{β⊥η}^{h∞} is ω +ω-compressible we use postponement of eta over beta and bottom. Finally recall the last nine lines of the introduction. ⊓ ⊔

5 Eta-Böhm trees and the extensional Böhm model

As a corollary of the confluence and normalisation results we see that each term in λ_{β⊥η}^{h∞} has a unique β⊥η-normal form, its eta-Böhm tree. Hence we can construct an extensional Böhm model �_{η} for both λ_{βη} and λ_{β⊥η}^{h∞} almost for free. In the notation of [3] we define the triple �_{η}= (�_{η}, ·, [[ ]]) as follows:

1. �_{η} is the set of β⊥η-normal forms of terms in Λ_{⊥}^{h∞}.

2. M · N = nf_{β⊥η}(MN) for all M, N in �_{η}.

3. [[M]]ρ = nf_{β⊥η}(M^{ρ}) where M in �_{η}and M^{ρ} is the simultaneous substitution of all free variables of M for ρ(x).

The unique normal form property of λ_{β⊥η}^{h∞} implies well-definedness of this definition. The ease of this construction contrasts with the usual construction based on elaborate continuity arguments in [3] of the standard Böhm model for λ_{β}. An informal definition of eta-Böhm trees can be found in [2]. It is also possible to give a corecursive definition. In early approaches to eta-Böhm trees sets of finite β⊥η-approximants have been used, see for example [10, 6].

Theorem 10. The following statements are equivalent for terms in λ_{β⊥η}^{h∞}:

1. M, N have the same eta-Böhm tree.

2. M and N are observationally equivalent wrt finite βη-normal forms [13], i.e. C[M] has a finite βη-normal form if and only if C[N] has a finite βη-normal form for all C.

3. M, N have the same interpretation in Park’s model D_{∞}^{∗} [16, 6, 17] for the extensional lambda calculus.

(1 ⇔ 2) has been proved by Hyland in [10] and (2 ⇔ 3) has been proved in [6]. Note that the direction (1 ⇒ 2) is in fact a corollary of the unique normal form property of λ_{β⊥η}^{h∞}, see [9] for an argument in a similar situation where approximants can not be used.

6 Future research

We are currently working on another infinitary extension of λ_{βη} that has the infinite-eta-Böhm trees as its normal forms. How to build an extension that captures the Nakajima trees [14, 18, 3] is still a challenge.

Acknowledgements

The first author thanks the Department of Mathematics and Computer Science of Leicester University for their hospitality. Both authors are grateful to Mariangiola Dezani-Ciancaglini and Vincent van Oostrom for discussions and Mario Severi for providing computer facilities during the preparation of this document.

References

1. A. Arnold and M. Nivat. The metric space of infinite trees. algebraic and topological properties. Fundamenta Informaticae, 4:445–476, 1980.

2. S. van Bakel, F. Barbanera, M. Dezani-Ciancaglini, and F.J. de Vries. Intersection types for λ-trees. TCS, 272(1-2):3–40, 2002.

3. H. P. Barendregt. The Lambda Calculus Its Syntax and Semantics. North-Holland Publishing Co., Amsterdam, Revised edition, 1984.

4. H. P. Barendregt, J. Bergstra, J. W. Klop, and H. Volken. Degrees, reductions and representability in the lambda calculus. Technical report, Department of Mathematics, Utrecht University, 1976.

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

6. M. Coppo, M. Dezani-Ciancaglini, and M. Zacchi. Type theories, normal forms, and D_{∞}-lambda-models. Information and Computation, 72(2):85–116, 1987.

7. H.B. Curry and R. Feys. Combinatory Logic, volume I. North-Holland Publishing Co., Amsterdam, 1958.

8. N. Dershowitz, S. Kaplan, and D.A. Plaisted. Rewrite, rewrite, rewrite, rewrite, rewrite, …. Theoretical Computer Science, 83(1):71–96, 1991.

9. M. Dezani-Ciancaglini, P. Severi, and F.J. de Vries. Infinitary lambda calculus and discrimination of Berarducci trees. TCS, 200X. Draft available on

www/mcs.le.ac.uk/~ferjan.

10. J. M. E. Hyland. A survey of some useful partial order relations on terms of the lambda calculus. In C. Böhm, editor, Lambda Calculus and Computer Science Theory, volume 37 of LNCS, pages 83–93. Springer-Verlag, 1975.

11. J.R. Kennaway and F.J. de Vries. Infinitary rewriting. In TeReSe, editor, Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 200X. Draft available on www/mcs.le.ac.uk/~ferjan.

12. J.R. Kennaway, J. W. Klop, R. Sleep, and F.J. de Vries. Infinitary lambda calculus. TCS, 175(1):93–125, 1997.

13. J. H. Morris Jr. Lambda calculus models of programming languages. PhD thesis, M.I.T., 1968.

14. R. Nakajima. Infinite normal forms for the λ-calculus. In C. Böhm, editor, Lambda calculus and Computer Science Theory, volume 37 of LNCS, pages 62–82. Springer-Verlag, 1975.

15. V. van Oostrom. Developing developments. TCS, 175(1):159–181, 1997.

16. D. Park. The Y-combinator in Scott’s lambda-calculus models (revised version). Technical report, Department of Computer Science, University of Warwick, 1976.

Copy available at www.dcs.qmul.ac.uk/~ae/papers/others/ycslcm/.

17. G.D. Plotkin. Set-theoretical and other elementary models of the λ-calculus. TCS, 121:351–409, 1993.

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