To be presented at the Workshop on Domain Theory held in honour of Dana Scott’s 70’th birthday

A lambda calculus for D_{∞}

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

1 Centro de Matemática, Facultad de Ciencias, Universidad de la República Iguá 4225 esq Mataojo, CP 11400 Montevideo, Uruguay - severi@cmat.edu.uy 2 Department of Mathematics and Computer Science, University of Leicester University Road, Leicester, LE1 7RH, UK - fdv1@mcs.le.ac.uk

Abstract. We define an extension of lambda calculus which is fully abstract for Scott’s D_{∞}-models. We do so by constructing an infinitary lambda calculus which not only has the confluence property, but also is normalising: every term has its ∞η-Böhm tree as unique normal form. The extension incorporates a strengthened form of η-reduction besides infinite terms, infinite reductions and a bottom rule allowing to replace terms without head normal form by bottom. The new η!-reduction is the key idea of this paper. It allows us to capture in a compact and natural way Barendregt’s complex ∞η-operation on Böhm trees. As a corollary we obtain a new congruence proof for Böhm tree equivalence modulo infinite η-expansion.

1 Introduction

When in November 1969 Dana Scott constructed the D_{∞} models [Sco72,Sco76], he was the first to define a denotational semantics for the lambda calculus. In the paper we ask conversely, what is the lambda calculus of those D_{∞} models? Our answer will be an extension of the lambda calculus that is fully abstract for the D_{∞} models. How should it look like? We take our cue from the well-known fact that the equality relation induced by D_{∞} can equivalently be characterised by Böhm tree equivalence modulo infinite η-expansions [Bar84],

D_{∞} ⊧ M = N ⟺ ∞ηB(M) = ∞ηB(N), for any finite terms M and N.

We want an extension of lambda calculus in which each term has its own ∞η-Böhm tree as unique normal form. This brings requirements. As Böhm trees can be infinite, the extension has to include infinite terms besides finite terms. And to make it possible that lambda terms reduce to their Böhm trees we need two more things: infinite reductions converging to some limit and ⊥-reduction to replace a term without head normal form by ⊥. So far we have followed our earlier work where we defined various infinite lambda calculi based on β-reduction and in each case their own variation of the ⊥-rule, such that these infinite calculi have respectively Böhm trees, Lévy-Longo trees and Berarducci trees as unique normal forms [KKSV95a,KKSV97,KVar,DCSVar]. However, (infinite) reduction with the usual β-, η-rules and the ⊥-rule based on head normal forms is not powerful enough to calculate ∞η-Böhm trees of lambda terms. In [SV02] we proved that infinite reduction with those three rules captures another class of Böhm trees, the η-Böhm trees [BBDCV02] which are η-normal forms of the standard Böhm trees. Barendregt tried to capture some form of infinite η-conversion in his definition of the ∞η-construction on Böhm trees (cf. pages 231-237 in [Bar84]). This construction identifies more Böhm trees then the η-normal form construction. The difference can be illustrated with help of I and Wadsworth’s J combinator, the infinite term λxz_{0}.x(λz_{1}.z_{0}(λz_{2}.z_{1}(…))). Clearly, J is the βnormal form of the finite term Y (λfxy.x(fy)), where Y is the fix-point combinator λf.(λf(xx))(λf(xx)). Both I and J are normal form wrt βη⊥-reduction. So I and J have different η-Böhm trees. Wadsworth showed that D_{∞} ⊧ I = J [Wad76] and from this one can infer that the ∞η-Böhm trees of I and J are the same [Bar84]. We propose an alternative definition of the ∞η-construction. We want to obtain the ∞η-Böhm trees as unique normal forms of β⊥-reduction and the following strong form of η-reduction:

x → →_{η^{−1}} N x ∉ F V (M)
(η!)
λx.MN → M

where → →_{η^{−1}} denotes strongly converging η-expansion. Strongly converging reduction is a key concept in infinite rewriting [KKSV95b,KKSV97]. Intuitively, an infinite reduction is strongly converging when the depth of the position of the application of the reduction rules goes to infinity along the reduction sequence. In the case of η-expansion it ensures that the term trees remain finitely branching, unlike the Nakajima trees [Nak75]. Strong converging η-expansion enjoys a few dual properties with respect to η!-reduction, like co-confluence. We demonstrate the strength of the new η!-reduction on J. Observe that J is the limit of a strongly converging η-expansion of I:

I → λxy_{0}.xy_{0} → λxy_{0}.x(λy_{1}.y_{0}y_{1}) → λxy_{0}.x(λy_{1}.y_{0}(λy_{2}.y_{1}y_{2})) → … →^{ω} J.

Next, note that J is of the form λxz_{0}.xN where N = λz_{1}.z_{0}(λz_{2}.z_{1}(…)) is a strongly converging η-expansion of the variable z_{0}. Therefore J reduces to I in a single η!-step. Of course this new definition of ∞η-Böhm tree only works provided we prove for any term the existence of a unique possible infinite normal form for βη!⊥-reduction. This is what the rest of this paper is about, where we will prove that the infinitary lambda calculus with β⊥η!-reduction is confluent and normalising. From the resulting unique normal form property we then get as immediate corollary the congruence of ∞η-Böhm trees. This is yet another technique for proving the congruence of Böhm trees (for a recent overview see [Las99]). It follows from this congruence property that ∞η-Böhm tree equivalence is equivalent to observational equivalence with respect to head normal forms. As Wadsworth has shown with help of approximants the latter is equivalent to the equivalence induced by D_{∞}. This allows us then to draw finally the desired conclusion thatour extension is fully abstract for D_{∞}. Finally we point to Curien’s interesting recent alternative [Curar] to the ∞ηconstruction. It seems unrelated to our current approach.

2 Infinite Lambda Calculus

Infinite lambda calculus houses besides the usual finite terms and finite reductions also infinite terms 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 has been produced. But the move from finite to infinite lambda calculus has to be made with care: just adding converging β-reduction destroys the confluence property. A simple counterexample is (λx.I(xx))(λx.I(xx)) which reduces with a finite reduction to Ω and with an infinite converging β-reduction to I(I(I(…))), and those latter two terms can no longer be joined even by infinite β-reductions. Both terms are in a sense computationally meaningless as both of them do not have a head normal form. To regain confluence we have to add a ⊥-rule to equate all terms without head normal form. With this addition we see that λ_{β⊥}^{∞} becomes normalising as well [KKSV97,KvOV99,KVar]. If the goal were just to obtain a confluent infinite calculus, then there are smaller sets of meaningless terms that can be equated such that confluence is ensured for converging reductions [KvOV99,KVar]. Making a choice for a particular set of meaningless terms is like making a choice for a particular semantics! We will now recall some notions and facts of infinite lambda calculus from our earlier work. We assume familiarity with basic notions and notations from [Bar84]. 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 (λxM)|_{0u} = M|_{u} (MN)|_{1u} = M|_{u} (MN)|_{2u} = N|_{u}

We will define a (sort of) length for occurrences: L(u) is the number of 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 a metric on finite lambda terms in Λ_{⊥} defined by d(M, N) = 0, if M = N and d(M, N) = 2^{−L(u)}, where u is a common occurrence of minimal length such that M|_{u} ≠ N|_{u}. Now in the spirit of Arnold and Nivat [AN80] we define the set Λ_{⊥}^{∞} as the metric completion of the set of finite lambda terms Λ_{⊥} with respect the metric d. The notion of depth is in accordance with the labelling of the Böhm trees in [Bar84]. The set Λ_{⊥}^{∞} contains all Böhm trees [KKSV97] as well as all η-Böhm trees [KKSV97,SV02] of the finite lambda terms, and more over is closed under the convergent βη⊥-reduction to be defined next. The set Λ_{⊥}^{∞} will function as the underlying set of finite and infinite lambda terms for our extensional infinitary extension λ_{β⊥η!}^{∞}. 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 [DKP91] 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 λ_{β⊥η!}^{∞}. Besides the β-reduction and η-reduction we have ⊥-reduction and two variants of η-reduction: η-expansion (η^{−1}-reduction) and η!-reduction.

M[⊥ := Ω] has no β-head normal form

(⊥)
M → ⊥

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

Previously [Ber96,KKSV95a,KKSV97,KVar] variations of λ_{β⊥}^{∞} = (Λ_{⊥}^{∞}, →_{β⊥}) have been studied. In our recent paper [SV02] we study for the first time an infinite extensional lambda calculus λ_{β⊥η}^{∞} = (Λ_{⊥}^{∞}, →_{β⊥η}). In this note we will consider the infinite extensional lambda calculus λ_{β⊥η!}^{∞} = (Λ_{⊥}^{∞}, →_{β⊥η!}). For any of these infinite lambda calculi λ_{ρ}^{∞} = (Λ_{⊥}^{∞}, → →_{ρ}) we will say that

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

– λ_{ρ}^{∞} is confluent if (Λ_{⊥}^{∞}, → →_{ρ}) satisfies the diamond property, i.e. _{ρ} ← ← ∘ → →_{ρ} ⊆ → →_{ρ} ∘ _{ρ} ← ←.

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

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

We may use following abbreviations of finite and infinite terms::

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

Without the ⊥-rule there is no chance of proving confluence. Berarducci’s counterexample is very short: Ω _{β}^{∗}← Ω_{I} → →_{β} I^{ω}. The terms Ω and I^{ω} cannot be joined. After addition of the ⊥-rule confluence is regained and both terms converge to ⊥.

Theorem 1. 1. The infinite lambda calculus λ_{β⊥}^{∞} is confluent, normalising and

ω-compressible. Cf. [KKSV97,KVar].

2. The infinite lambda calculus λ_{β⊥η}^{∞} is confluent, normalising, ω + ω-compressible and satisfies postponement: if M → →_{β⊥η} N then M → →_{β} Q_{1} → →_{⊥} Q_{2} → →_{η} N for some Q_{1}, Q_{2} ∈ Λ_{⊥}^{∞}. Cf. [SV02].

3 Some properties of λ_{η^{−1}}^{∞} and λ_{η!}^{∞}

Proof of compression of strongly converging reduction is standard [KKSV95b,KVar]:

Theorem 2. Strongly converging reduction is ω-compressible both λ_{η^{−1}}^{∞} and λ_{η!}^{∞}.

We have chosen our metric completion carefully: any η!-reduction sequence in Λ_{⊥}^{∞} is strongly convergent, as we will show next. In stark contrast, non-strongly converging η-expansion may even be non-Cauchy converging in Λ_{⊥}^{∞}, as witnessed by outermost η-expansion (in fact the apparent limit is not even in Λ_{⊥}^{∞}!):

x →_{η^{−1}} λy_{1}.xy_{1} →_{η^{−1}} λy_{2}(λy_{1}.xy_{1})y_{2} →_{η^{−1}} λy_{3}(λy_{2}(y_{1}.xy_{1})y_{2})y_{3} →_{η^{−1}} …

The relative tameness of η! can be shown with a simple counting argument. For M ∈ Λ_{⊥}^{∞} define |M|_{n} as the number of nodes at depth n. The number |M|_{n} of nodes of term M at depth n decreases if we contract an η!-redex in M at depth n. Hence:

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

Strongly converging η-expansion and η!-reduction are each others inverse:

Lemma 2. M → →_{η!} N if and only if N → →_{η^{−1}} M for any M, N in Λ_{⊥}^{∞}.

Proof. In both directions the proof is by induction on the length of the given reduction, which by compression may be assumed to be at most ω. Suppose for N and M in Λ_{⊥}^{∞} we have N → →_{η^{−1}} M. We can recognise for every occurrence of λ in M whether it descends from a symbol in N (e.g. by using underlined λ’s in the expansion rule), or whether it has been introduced by an expansion. Because N → →_{η^{−1}} M is finite or strongly converging we will find sequences of introduced λ’s of at most finite length in N, the subterm then looks like λx_{1} … x_{n}.KL_{1} … L_{n} where each L_{i} is an expansion of the corresponding x_{i}. This subterm then η! reduces in one step back to K. Clearly, there is now a depth first η!-reduction from N to M. In the other direction, suppose for N and M in Λ_{⊥}^{∞} we have M → →_{η!} N. Note that a single η!-step can be undone with a finite η-expansion, as suggested by the diagram:

\xymatrix{C[λx.P Q] \ar[r]^{∗}_{η!} & C[P] \ar@{.>}[d]^{η^{−1}} \\  & C[λx.P x] \ar@{->>}[ul]^{η^{−1}}}

We can now construct the inverse η-expansion of M → →_{η!} N, by performing the inverses of the individual steps of M → →_{η!} N in the same order. It is not hard to see that this is well defined and results in a strongly converging η-expansion. ⊓ ⊔

This lemma has as curious consequence that if we show—what we will do next—that λ_{η^{−1}}^{∞} and λ_{η!}^{∞} are confluent, we get for free that λ_{η^{−1}}^{∞} and λ_{η!}^{∞} are co-confluent!

Theorem 3. The infinitary lambda calculi λ_{η^{−1}}^{∞} and λ_{η!}^{∞} are confluent.

Proof. Confluence of λ_{η^{−1}}^{∞} is trivial. Confluence of λ_{η!}^{∞} can be shown by a simultaneous induction on the length of the two given coinitial η!-reductions. By compression we may assume that these reductions are at most of length ω, so here we don’t need transfinite induction. The proof makes use of standard tiling diagram construction [KVar]. We only check the base case which amounts of an analysis of the following cases when both given coinitial reductions have length 1. (The limit case argument follows a standard pattern.)

1. The η!-redexes are disjoint, i.e. M_{0,0} = C[λx.MN, λy.P Q].

2. The η!-redex λy.P Q is inside the operator M of the other η!-redex λx.MN, i.e. M_{0,0} = C_{1}[λx.C_{2}[λy.P Q]N]

3. The η!-redex λy.P Q is inside the argument N of the other η!-redex λx.MN, i.e. M_{0,0} = C_{1}[λx.MC_{2}[λy.P Q]]. But then both C_{2}[λy.P Q] and C_{2}[P] are ηexpansions of the same variable x.

4. The η!-redexes coincide.

The first and second cases result in the first diagram. The third and the fourth case result in respectively the second and third diagram. We indicate with a subscript that the redex contracted in M →_{ρ}^{m} N is at depth m.

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

The important thing to note is that the depth of an η!-redex in a term does not change when we contract an η!-redex elsewhere in the term. The induction now makes use of so called tiling diagrams. The most involved case being the double limit. In that case we can construct the next tiling diagram:

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

The induction hypothesis allowed us to construct all proper subtiling diagrams with top-left corner M_{0,0} and bottom-right corner M_{γ,δ} (where (γ, δ) can not be (ω, ω)) such that all rows and columns in the subdiagram are finite or strongly converging reductions. Clearly, by the fact that all subtiles are depth preserving, both the bottom row and the right-most column inherit the strong convergence property from respectively the top row and the left-most column. By the general tiling diagram theorem in [KVar] then it follows that these latter two reductions have the same limit M_{ω,ω}. In fact to apply that limit it already suffices if only one of the two inherits the strong convergence property. This will be the case in the other proofs of this paper making use of this construction. There is one thing we have glossed over: how to construct the edges of the bottom row and the right-most column. Say we look at the leftmost column of tiles: 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 (occurrences of) η!-redexes ⋃_{k≥0} ⋂_{m≥k} V_{m} gives us precisely a strongly convergent reduction M_{ω,0} → →_{η!} M_{ω,1}. In later proofs commutation proofs where the vertical reductions are β-reduction this construction is crucial, as the various V_{n} may contain even infinitely many residuals. ⊓ ⊔

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

4 Commutation properties in λ_{β⊥η!}^{∞}

Because of the various compression properties we can assume that the strongly converging reductions containing only ρ-redexes, that will occur in the hypothesis of the commutation theorems of this section, are compressed to ρ-reductions of at most length ω, for ρ any of the reduction relations in {β, ⊥, β⊥, η!, η^{−1}}.

Theorem 5. The infinitary reduction → →_{η!} commutes with → →_{β}.

Proof. The proof proceeds as in the confluence proof of η! in Theorem 3 and makes use of an inductive tiling diagram argument. Suppose M_{0,0} can do both a β-reduction and an η!-reduction at respectively depth n and m. The cases 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 Q)].

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

(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.MQ])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.NP]].

3. The β-redex disappears:

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

(b) The β and η!-redex overlap, that is M_{0,0} is of the form C[(λx.MN)P] or C[λx.(λy.M)N].

These three cases result in the following elementary tiles in which the labels on the arrows refer to the 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}; η!; m; β; n; M_{0,1}; M_{1,0}; η!; ≥m; M_{1,1}]

⊓ ⊔

Theorem 6. The infinitary reduction → →_{η^{−1}} commutes with → →_{β}.

Proof. The proof follows the standard pattern. We only show the elementary tiles. The last tile derives from the possibility that the abstraction in the β-redex gets η-expanded.

\xymatrix{M_{0,0} \ar[r]^{η^{−1}}_{m} \ar[d]_{β}^{n} & M_{0,1} \ar@{.>}[d]^{β}_{n} & M_{0,0} \ar[r]^{η^{−1}}_{m} \ar[d]_{β}^{n} & M_{0,1} \ar@{.>}[d]^{β}_{n} & M_{0,0} \ar[r]^{η^{−1}}_{m} \ar[dd]_{β}^{n} & M_{0,1} \ar@{.>}[d]^{β}_{n} \\ M_{1,0} \ar@{.>}[r]_{η^{−1}}^{m} & M_{1,1} & M_{1,0} \ar@{->>}[r]_{η^{−1}}^{≥(m−1)} & M_{1,1} &  & N \ar@{.>}[d]^{β}_{n} \\  &  &  &  & M_{1,0} \ar@{.>}[r]_{η^{−1}}^{m} & M_{1,1}}

⊓ ⊔

Lemma 3. The set of U of terms from which there is no finite β-reduction to a head normal form is both closed under strongly converging η!-reduction and strongly converging η-expansion.

Theorem 7. The infinitary reduction → →_{η!} commutes with → →_{⊥}_{out}

Proof. The restriction to ⊥_{out} is as for η, see [SV02]. The proof follows the standard pattern. The base case analysis results in the tiles, where the last needs Lemma 3:

[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}; ⊓ ⊔]

Theorem 8. The infinitary reduction → →_{η^{−1}} commutes with → →_{⊥}.

Proof. The proof follows the standard pattern. The base case analysis results in the tiles, where the first needs Lemma 3:

[figure: M_{0,0}; η^{−1}; m; ⊥; n; M_{0,1}; ⊥; n; M_{1,0}; η^{−1}; n; M_{1,1}; M_{0,0}; η^{−1}; n; ⊥; n; M_{0,1}; ⊥; n; M_{1,0}; M_{1,1}; ⊓ ⊔]

Corollary 1. The reduction → →_{η^{−1}} commutes with → →_{β⊥}.

5 Confluence and other properties of λ_{β⊥η!}^{∞}

The key to the confluence of λ_{β⊥η!}^{∞} is postponement, just like in Barendregt’s [Bar84]. We will prove that η!-reduction can be postponed in mixed β⊥η!-reductions and hence as well in mixed βη!-reductions. We start by dualizing two commutation results of the previous section: Corollary 2. The reductions → →_{η!} and → →_{η^{−1}} can be postponed over → →_{β⊥}.

Theorem 9. If M → →_{β⊥η!} N, then there exists an L such that M → →_{β⊥} L → →_{η!} N.

Proof. The proof is by 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}; η^{−1}; β⊥; M_{2,0}; M_{2,1}; η^{−1}; η^{−1}; M_{2,2}; η^{−1}; M_{ω,0}; M_{ω,1}; η^{−1}; M_{ω,2}; η^{−1}; M_{ω,ω}; η^{−1}]

Because the diagonal is strongly converging and the horizontal η^{−1}-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 η^{−1}-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 limits of the bottom row reduction and the diagonal are the same.

⊓ ⊔

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

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

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

Proof. Analogous to the proof in [SV02].

[figure: M; η!; β; (Thm 5); β⊥; N; β; M_{1}; η!; ⊥_{out}; (Thm 7); N_{1}; ⊥_{out}; nf_{β⊥}(M); η!; N_{2}; M; β⊥η!; β⊥; β⊥; (Thm 1); P; η!; β⊥; (Part 1); N; β⊥; nf_{β⊥}(M); η!; nf_{β⊥}(P); η!; nf_{β⊥}(N)]

⊓ ⊔

Combining all previous results we now can prove that λ_{β⊥η!}^{∞} is confluent, normalising and ω + ω-compressible with similar proofs as in [SV02] for the confluence λ_{β⊥η}^{∞}.

Theorem 10. The extensional infinite lambda calculus λ_{β⊥η}^{∞} is confluent, normalising and is ω + ω-compressible.

Proof. We sketch confluence:

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

⊓ ⊔

References

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

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

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

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

[Curar] P.-L. Curien. Sur l’η-expansion infinie. Comptes Rendus de l’Acadḿie des Sciences, to appear. Draft available at www.pps.jussieu.fr/~curien.

[DCSVar] M. Dezani-Ciancaglini, P. Severi, and F.J. de Vries. Infinitary lambda calculus and discrimination of Berarducci trees. Theoretical Computer Science, to appear.

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

[KKSV95a] 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.

[KKSV95b] J.R. Kennaway, J.W. Klop, R. Sleep, and F.J. de Vries. Transfinite reductions in orthogonal term rewriting systems. Information and Computation, 119(1):18–38, 1995.

[KKSV97] 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.

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

[KVar] J.R. Kennaway and F.J. de Vries. Infinitary rewriting. In J.W. Terese, editor, Term Rewriting Systems. Cambridge University Press, to appear. Draft

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

[Las99] S.B. Lassen. Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. In MFPS XV: Mathematical Foundations of Programming Semantics, Fifteenth Conference (New Orleans, LA, 1999), volume 20 of ENTCS, pages 1–29, 1999.

[Nak75] 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.

[Sco72] D.S. Scott. Continuous lattices. In Proceedings of the 1971 Dalhousie Conference on Toposes, algebraic geometry and logic, volume 274 of LNM, pages 97–136. Spinger-Verlag, 1972.

[Sco76] D.S. Scott. Data types as lattices. SIAM Journal of Computation, 5(3):522– 587, 1976.

[SV02] P. Severi and F.J. de Vries. An extensional Böhm model. In RTA’02, LNCS. Springer-Verlag, 2002. Draft available at www/mcs.le.ac.uk/~ferjan.

[Wad76] 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.