Continuity and Discontinuity in Lambda Calculus

Paula Severi and Fer-Jan de Vries

Department of Mathematics and Computer Science, University of Leicester University Road, Leicester, LE1 7RH, UK

Abstract. This paper studies continuity of the normal form and the context operators as functions in the infinitary lambda calculus. We consider the Scott topology on the cpo of the finite and infinite terms with the prefix relation. We prove that the only continuous parametric trees are Böhm and Lévy–Longo trees. We also prove a general statement: if the normal form function is continuous then so is the model induced by the normal form; as well as the converse for parametric trees. This allows us to deduce that the only continuous models induced by the parametric trees are the ones of Böhm and Lévy–Longo trees. As a first application, we prove that there is an injective embedding from the infinitary lambda calculus of the ∞η-Böhm trees in D_{∞}. As a second application, we study the relation between the Scott topology on the prefix relation and the tree topologies. This allows us to prove that the only parametric tree topologies in which all context operators are continuous and the approximation property holds are the ones of Böhm and Lévy–Longo. As a third application, we give an explicit characterisation of the open sets of the Böhm and Lévy–Longo tree topologies.

1 Introduction

The study of the infinitary lambda calculi has focused on confluence and normalisation [4, 9–12, 16, 15] and sequentiality [5]. In this paper we will look at another property of these calculi, namely continuity. Our starting point are lambda calculi that extend finite lambda calculus with infinite terms and transfinite reduction. The β and η reduction rules apply to infinite terms in much the same way as they apply to finite terms. However, characteristic for these calculi is that they contain a ⊥-rule that maps a certain set U of meaningless terms to ⊥. Without such an addition the extension of finite lambda calculus with infinite terms and reductions immediately would result in loss of confluence [9]. All infinite calculi that we consider have the same set of finite and infinite terms Λ_{⊥}^{∞}. The variation comes from the choice of the set U and the strength of extensionality. Figure 1 summarises the infinitary lambda calculi studied so far [4, 9, 10, 12, 16, 15]. 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, 9, 10]. In the fourth row, there is an uncountable class of infinitary lambda calculi with a ⊥-rule parametrised by a set U of meaningless terms [11, 12]. By changing the parameter set U of the ⊥-rule,

REDUCTION RULES  NORMAL FORMS NF

Beta and Bottom for terms without tnf  Berarducci trees  BeT = T\overline{T}
Beta and Bottom for terms without whnf  Lévy–Longo trees  LT = T\overline{W}
Beta and Bottom for terms without hnf  Böhm trees  BT = T\overline{H}
Beta, Bottom parametric on U  Parametric trees  T_{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

we obtain different infinitary lambda calculi. If U is the set of terms without head normal form, we capture the notion of Böhm tree. If U is the set of terms without weak head normal form we obtain the Lévy–Longo trees. And if U is the set 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 [16]. 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 [15]. The normal forms in this calculus capture the notion of ∞η-Böhm trees. When the infinite extensions are confluent and normalising (normal forms can now be infinite too!) they induce a function NF : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} mapping a term to its unique normal form. The normal form functions NF induce models of the finite lambda calculus: just interpret a term M by its normal form NF(M) and application M · N of two terms M and N by NF(MN). It is natural to compare terms, in particular normal forms, by 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 ⊥. Whereas application in the model of Böhm trees is well-known to be continuous with respect to the Scott topology induced by the prefix relation, it is perhaps less well-known that in case of the model of Berarducci trees, the normal form function BeT : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} and the application operator are not even monotone [8]. For the models induced by NF, it makes sense to study continuity of all context operators and this includes not only the application operator but also the abstraction. In this paper we will make a systematic study of continuity of the following two functions and the relation between them:

– the normal form functions NF with respect to the Scott topology on (Λ_{⊥}^{∞}, ⪯) and – the context operators λλM ∈ NF(Λ_{⊥}^{∞}).NF(C[M]) : NF(Λ_{⊥}^{∞}) → NF(Λ_{⊥}^{∞}) in the

models induced by NF.

We first prove that the only continuous parametric tree functions are the ones that correspond to Böhm and Lévy–Longo trees. We also show that the η and ∞η-Böhm tree functions are not continuous. We also study the relation between continuity of NF and continuity of the context operators in the models induced by NF. We prove that if NF is continuous then so is the model induced by NF; as well as the converse when NF is a parametric tree. This allows us to deduce that the only continuous models induced by the parametric trees are the ones of Böhm and Lévy–Longo trees. As a first application of our results on continuity, we show that there is an injective embedding from the infinitary lambda calculus of ∞η-Böhm trees in Scott’s models D_{∞}. We use the fact that the model induced by BT is continuous to prove that the interpretation on D_{∞} extended to infinite terms is homomorphic with the abstraction and the application. As a second application, we study the relation between the Scott topology on the prefix relation and the tree topologies. We prove that the only parametric tree topologies that make all context operators continuous and in which the approximation property holds are the ones of Böhm and Lévy–Longo. Continuity of the finite context operators λλM ∈ Λ.C[M] : Λ → Λ in the Böhm and Lévy–Longo tree topologies is proved in [2, 14] using the labelled reduction. We show that it can also be deduced from confluence via the infinitary lambda calculus As a third application, we define the notion of NF-topology and prove that the BTtopology and the LT-topology coincide with the old notions of Böhm and Lévy–Longo tree topologies.

2 Infinite Lambda Calculus

We will now briefly recall some notions and facts of infinite lambda calculus from our earlier work [9, 10, 12, 16, 15]. We assume familiarity with basic notions and notations from [2]. 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. 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 [10–12], an alternative definition of the set Λ_{⊥}^{∞} is given using a metric. The coinductive and metric definitions are equivalent [3]. In this paper we consider only one set of λ-terms, namely Λ_{⊥}^{∞}, in contrast to the formulations in [10, 11] where several sets (which are all subsets of Λ_{⊥}^{∞}) are considered. The paper [12] 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 ⊥.

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 [7] 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 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 reduced redex in M_{β} → M_{β+1}. Note that any finite reduction is 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.

We define several rules used to define different infinite lambda calculi. The β, η and η^{−1}-rules are extensions of the rules for finite lambda calculus to infinite terms. The η!-rule does not appear in the finite lambda calculus. The ⊥-rule is parametric on a set U ⊂ Λ^{∞} of meaningless terms [11, 12] where Λ^{∞} is the set of terms in Λ_{⊥}^{∞} that do not contain ⊥. 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 = {M ∈ Λ^{∞} | M → →_{β} N and N in head normal form}
W = {M ∈ Λ^{∞} | M → →_{β} N and N in weak head normal form}
T = {M ∈ Λ^{∞} | M → →_{β} N and N in top normal form}

Instances of U ⊆ Λ^{∞} are \overline{H}, \overline{W} and \overline{T} the respective complements of H, W and T . Since the ⊥-rule is parametric, each set U of meaningless terms gives a different infinitary lambda calculus λ_{β⊥}^{∞}.

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

(λx.M)N → M[x := N] (β)  \begin{matrix}M[⊥ := Ω] ∈ U \\ & (⊥) \\ 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{aligned}x → → →_{η^{−1}} N  x ∉ F V (M) \\ & (η!) \\ λx.MN → M \end{aligned}

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. Variations on the reduction rules will give rise to different calculi (see Figure 1). The resulting infinite lambda calculus (Λ_{⊥}^{∞}, →_{ρ}) we will denote by λ_{ρ}^{∞} for any ρ ∈ {β⊥, β⊥η, β⊥η!}.

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.

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

Theorem 3. [10–12] The calculi λ_{β⊥}^{∞} with a parametric ⊥-rule on the set U are confluent, normalising, ω-compressible and satisfy postponement of ⊥ over β.

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

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

Assumption. In the rest of the paper whenever we refer to the function NF : Λ_{⊥}^{∞} → Λ_{⊥}^{∞}, we are assuming that the infinitary lambda calculus in question is confluent and normalising and that NF is the function that maps a term to its unique normal form.

3 Equality induced by the normal form

The theory given by NF is the set Eq(NF) = {(M, N) ∈ Λ_{⊥}^{∞}×Λ_{⊥}^{∞} | NF(M) = NF(N)}. Figure 1 shows an order between the calculi. On the first row we see the smallest theory of λ-terms given by the equality of Berarducci trees and in the last row we see the largest theory given by equality of ∞η-Böhm trees. Hence,

Eq(BeT) ⊂ Eq(LT) ⊂ Eq(BT) ⊂ Eq(ηBT) ⊂ Eq(∞ηBT)

Note that T ⊃ W ⊃ H and \overline{T} ⊂ \overline{W} ⊂ \overline{H}.

Lemma 5. Let U be a set of meaningless terms satisfying the axioms of [11, 12]. If the theory Eq(T_{U}) is consistent then \overline{T} ⊆ U ⊆ \overline{H}.

Proof. By the axioms of meaningless terms [11, 12], we know that \overline{T} ⊆ U. Suppose now towards a contradiction that there exists M ∈ U such that M ∉ \overline{H}. Then M has a head normal form. Suppose M = λx_{1} … x_{n}.yP_{1} … P_{k}. Once more applying the axioms of meaningless terms, we have that (Mx_{1} … x_{n})[y := λy_{1} … y_{k}.P] → →_{β} P ∈ U for any P ∈ Λ_{⊥}^{∞}. It follows that all terms P ∈ Λ_{⊥}^{∞} have the same normal form and hence the theory is not consistent.

As a consequence of the previous lemma, any consistent theory of parametric trees lays between the theories of Berarducci and Böhm trees:

Eq(BeT) ⊆ Eq(T_{U}) ⊆ Eq(BT)

Theorem 6. The class of parametric trees is uncountable.

Proof. For each subset X of the set of finite closed β-normal forms, we define a set U_{X} as follows:

U_{X} = \{M ∈ Λ^{∞} | M → →_{β} RP_{1} … P_{n}, n ∈ ω, R ∈ \overline{T} and P_{1}, …, P_{n} ∈ X\}

It is possible to prove that the set U_{X} satisfies the axioms of [11, 12].

4 Truncation and preorders

In this section we define the notion of truncation and some preorders used in this paper. In the next section we will use truncations instead of approximants to prove continuity.

Definition 7. Let M ∈ Λ_{⊥}^{∞}.

1. 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 ⊥.

2. The truncation of the normal form of M at depth n is denoted by NF^{n}(M).

The following lemma is proved by induction on the depth of the hole in the context.

Lemma 8. Let C[M] ∈ Λ_{⊥}^{∞} and d the depth of the hole in C. If n > d then (C[M])^{n} = C^{n}[M^{n−d}]. Otherwise C[M]^{n} = C^{n} is a term without a hole in it.

Definition 9. Let M, N ∈ Λ_{⊥}^{∞}. 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 ⊥

The pair (Λ_{⊥}^{∞}, ⪯) is an algebraic cpo. The compact elements are the finite λ-terms. In particular, truncations of terms are compact. We denote the supremum of a directed subset X of (Λ_{⊥}^{∞}, ⪯) by ⋃ X. In the particular case of Böhm trees, the pair (BT(Λ_{⊥}^{∞}), ⪯) is isomorphic to (B, ⊆) where B is the set of Böhm–like trees and ⊆ is the prefix relation on trees [2].

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

1. We say that M ⪯_{fin} N if M is the result of replacing a finite number of subterms of N by ⊥.

2. Let NF : Λ_{⊥}^{∞} → Λ_{⊥}^{∞}. Then, M ⪯_{NF} N if NF(M) ⪯ NF(N).

3. M ⪯_{η^{−1}} N if BT(M) → → →_{η^{−1}} P ⪯ Q _{η^{−1}}← ← ← BT(N) for P, Q in β⊥-normal form.

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

5. 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].

The relation ⪯_{NF} is a preorder, i.e. it is reflexive and transitive. It is also a partial order if restricted to the set of normal forms, i.e. it is antisymmetric.

Definition 11. We say that NF quasi-preserves ⪯_{fin} if NF(M) ⪯ NF(N) for all M ⪯_{fin} N.

5 Continuity of the normal form function NF

We will now consider the Scott topology on the cpo (Λ_{⊥}^{∞}, ⪯) and study continuity of the normal form function NF : Λ_{⊥}^{∞} → Λ_{⊥}^{∞}. We prove that the only parametric trees satisfying continuity are BT and LT.

We give some counterexamples against continuity of the normal form function:

Counterexample 12. The map NF : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is not continuous in (Λ_{⊥}^{∞}, ⪯) in the following cases:

1. Case NF = BeT. We show that BeT is not monotone in (Λ_{⊥}^{∞}, ⪯). Take M = ⊥y, N = (λx.⊥)y. Then M ⪯ N but NF(M) ⪯̸ NF(N).

2. Case NF = {ηBT, ∞ηBT}. We show that ηBT and ∞ηBT are not monotone. Take M = λx.y⊥ and N = λx.yx. Then M ⪯ N but NF(M) ⪯̸ NF(N).

3. Case NF = T\overline{O} and \overline{O} = \overline{W} ∪ \{M ∈ Λ^{∞} | M → →_{β} λx_{1} … x_{n}.N and N ∈ \overline{W}\}. Then T\overline{O} is monotone but it is not continuous. The infinite sequence of abstractions O = λx_{1}x_{2} … is in normal form but the truncations O^{n} = λx_{1} … x_{n}.⊥ reduce to ⊥ for all n. Hence ⋃_{n∈ω} O^{n} = O = NF(O) ≠ ⋃_{n∈ω} NF(O^{n}) = ⊥.

Definition 13. We say that the truncations are NF-increasing if there exists m such that M →_{ρ} N implies M^{n+m} ⪰_{NF} N^{n} for all n.

Lemma 14. Let λ_{ρ}^{∞} be ω-compressible. If the truncations are NF-increasing then for all n there exists l such that NF^{n}(P) ⪯_{NF} P^{n+l}.

Proof. By confluence, normalisation and ω-compression for λ_{ρ}^{∞}, there exists a strongly convergent reduction sequence of length ω from P to NF(P):

P = P_{0} →_{ρ} P_{1} →_{ρ} P_{2} … NF(P)

Since this reduction sequence is strongly convergent, there exists P_{i} such that NF^{n}(P) = (P_{i})^{n}. Since the truncations are NF-increasing, we construct the following (finite) chain from P^{n+l} to NF^{n}(P):

P^{n+im} = (P_{0})^{n+im} ⪰_{NF} (P_{1})^{n+(i−1)m} … ⪰_{NF} (P_{i−1})^{n+m} ⪰_{NF} (P_{i})^{n} = NF^{n}(P)

Taking l = im we have that NF^{n}(P) ⪯_{NF} P^{n+l}.

Lemma 15. Let P, Q ∈ Λ_{⊥}^{∞}. Then, P^{n}[x := Q^{n}] ⪰ (P [x := Q])^{n}.

This is proved by induction on the number of symbols of P^{n}.

Lemma 16. If T_{U} quasi-preserves ⪯_{fin} then the truncations are T_{U}-increasing.

Proof. Suppose M →_{⊥} ⊥. We have that M^{n} ⪰_{T_{U}} ⊥. Suppose M = C[(λx.P)Q] →_{β} C[P [x := Q]] = N. Let d be the position of the hole in C[ ] and k = n − d > 0.

(C[(λx.P)Q])^{n+2} = C^{n+2}[(λx.P^{k})Q^{k+1}] by Lemma 8
→_{β} C^{n+2}[P^{k}[x := Q^{k+1}]
⪰ C^{n}[P^{k}[x := Q^{k}]]
⪰ C^{n}[(P [x := Q])^{k}] by Lemma 15
= (C[P [x := Q]])^{n}  by Lemma 8

Since β⊥ is confluent (Theorem 4) and T_{U} quasi-preserves ⪯_{fin},

(C[(λx.P)Q])^{n+2} ⪰_{T_{U}} (C[P [x := Q]])^{n}

Definition 17. Let σ be a function from positions of ⊥’s to Λ_{⊥}^{∞}. We define M^{σ} as the result of replacing ⊥’s in M by the corresponding terms given by σ.

Lemma 18. Let M, N ∈ Λ_{⊥}^{∞}. Then, M ⪯ N if and only if M^{σ} = N for some σ.

Lemma 19. Let σ be a function from positions of ⊥’s to Λ_{⊥}^{∞}. If M → → →_{β} N then there exists σ′ such that M^{σ} → → →_{β} N^{σ′}.

This is proved by induction on the length of the reduction sequence from M to N.

Theorem 20. BT and LT are monotone in (Λ_{⊥}^{∞}, ⪯).

Proof. Let M, N ∈ Λ_{⊥}^{∞} such that M ⪯ N. We prove that BT(M) ⪯ BT(N). By normalisation of β⊥ and postponement of ⊥ over β (Theorem 4 and Theorem 3), we have that there exists P such that M → → →_{β} P → → →_{⊥} BT(M). By Lemma 19 we have that N = M^{σ} → → →_{β} P^{σ′}. We prove that for all n, BT^{n}(P) ⪯ BT^{n}(P^{σ′}) by induction on n. Suppose n = h + 1. We have three cases:

1. Case P = ⊥. Then BT^{n}(P) = ⊥ ⪯ BT^{n}(P^{σ′}).

2. Case P = λx_{1} … x_{n}.y Q_{1} … Q_{k}.

Then BT^{n}(P) = λx_{1} … x_{n}.y BT^{h_{1}}(Q_{1}) … BT^{h_{k}}(Q_{k}). It follows by induction hypothesis that BT^{h_{i}}(Q_{i}) ⪯ BT^{h_{i}}(Q_{i}^{σ_{h_{i}}}). Hence P^{n} ⪯_{BT} (P^{σ′})^{n}.

3. Case P = λx_{1} … x_{n}.(λy.R)SQ_{1} … Q_{k}. Since P → → →_{⊥} BT(M), P cannot have head normal form. Hence BT^{n}(P) = ⊥ ⪯ BT^{n}(P^{σ′}).

This proof can be easily adapted to Lévy–Longo trees with some minor adjustments.

Corollary 21. The functions BT and LT are continuous in (Λ_{⊥}^{∞}, ⪯).

Proof. By Theorem 20, we have that ⋃_{n∈ω} BT(M^{n}) ⪯ BT(M). The truncations are BT-increasing by Theorem 20 and Lemma 16. The calculus of Böhm trees is ω-compressible by Theorem 3. Hence, we have that:

BT(M) = ⋃_{n∈ω} BT^{n}(M)
= ⋃_{n∈ω} BT(BT^{n}(M)) because BT^{n}(M) is in normal form
⪯ ⋃_{n∈ω} BT(M^{n})  by Lemma 14

The same proof works for LT.

We prove that the only parametric tree functions T_{U} : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} satisfying continuity are the Böhm tree function and the Lévy–Longo tree function.

Theorem 22. If T_{U} : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is continuous then T_{U} = BT or T_{U} = LT.

Proof. By Lemma 5, we have that \overline{T} ⊆ U ⊆ \overline{H}. We prove that U = \overline{H} or U = \overline{W}. Suppose that M ∈ \overline{W} − \overline{T} . We can also suppose that M ∈ BeT(Λ_{⊥}^{∞}) because \overline{T} ⊆ U and T_{U}(BeT(M)) = T_{U}(M) by confluence of β⊥. We have two cases:

1. Let M = ⊥P_{k} … P_{1} and N = (λx_{1} … x_{k}.⊥)P_{k} … P_{1}. Since T_{U} is monotone and M ⪯ N, we have that T_{U}(M) ⪯ T_{U}(N) = ⊥. Hence M ∈ U.

2. Let M = (((… P_{3})P_{2})P_{1}). Then, T_{U}(M) = ⋃_{n∈ω} T_{U}(M^{n}) = ⊥. Hence M ∈ U.

Hence, we have that \overline{W} − \overline{T} ⊆ U and also \overline{W} ⊆ U. Suppose now that \overline{W} ⊂ U ⊆ \overline{H}. Then there exists M ∈ U such that M ∈ \overline{H} − \overline{W}. We prove that \overline{H} − \overline{W} ⊆ U and hence U = \overline{H}. We can suppose that the terms in \overline{H} − \overline{W} are in LT(Λ_{⊥}^{∞}) and then they are either of the form λx_{1} … λx_{k}.⊥ or λx_{1}x_{2}x_{3} . . .. We have two cases:

1. Let M = λx_{1} … λx_{k}.⊥ for some k.

T_{U}(λx.⊥) = T_{U}(Mx_{1} … x_{k−1}) because Mx_{1} … x_{k−1} → →_{β} λx.⊥
= T_{U}(⊥x_{1} … x_{k−1}) because M ∈ U
= ⊥  because \overline{W} ⊆ U

Then, we also have that T_{U}(λx_{1} … x_{n}.⊥) = ⊥ for all n. Since T_{U} is continuous, we also have that T_{U}(λx_{1}x_{2} …) = ⊥.

2. Let M = λx_{1}x_{2} . . .. Then ⊥ = T_{U}(M) ⪰ T_{U}(M^{n}) = λx_{1} … x_{n}.⊥ for all n.

6 Models induced by NF

In this section we define the model induced by NF and give a notion of continuity for these models.

Definition 23. The model induced by NF, denoted by M(NF), is the applicative structure (NF(Λ_{⊥}^{∞}), . , [[ ]]) defined as follows:

1. M.N = NF(MN) for all M, N ∈ NF(Λ_{⊥}^{∞}),

2. [[M]]_{σ} = NF(M^{σ}) for all M ∈ Λ and where M^{σ} is the simultaneous substitution of all free variables of M by σ.

By Theorem 6, the class of models induced by the parametric trees is uncountable. It is easy to prove that M(NF) is indeed a λ-model of the finite lambda calculus using confluence and normalisation (see Definition 5.3.2 in [2]). We consider the prefix relation ⪯ on NF(Λ_{⊥}^{∞}). For NF ∈ {BT, LT, BeT, ∞ηBT, ηBT}, the pair (NF(Λ_{⊥}^{∞}), ⪯) is a cpo. We can deduce that the set of normal forms is closed under directed suprema by showing first that a redex in a term should also be present in some finite prefix. In general, the pair (NF(Λ_{⊥}^{∞}), ⪯) may not be a cpo:

Counterexample 24. We show an example of a pair (T_{U}(Λ_{⊥}^{∞}), ⪯) which is not a cpo. Let I = λx.x and K = λxy.x. We consider the infinite term K^{∞} = ((… K)K)I). The set K = \overline{T} ∪ \{M ∈ Λ^{∞} | M → →_{β} K^{∞}\} satisfies the axioms of [11, 12] and, then, T_{K} : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is a parametric tree function. The term K^{∞} is a redex but none of its prefixes contain any redex. The pair (T_{K}(Λ_{⊥}^{∞}), ⪯) is not a cpo because the set X = {T_{K}^{n}(K^{∞}) | n ∈ ω} ⊂ T_{K}(Λ_{⊥}^{∞}) but K^{∞} = ⋃ X ∉ T_{K}(Λ_{⊥}^{∞}).

For the models induced by NF, it makes sense to define a notion of continuity that considers all context operators and not only the application. In particular, we can consider the abstraction operator as a function in the model, i.e. abs(M) = NF(λx.M) for M ∈ NF(Λ_{⊥}^{∞}).

Definition 25. Let C[ ] be a context in Λ_{⊥}^{∞}. The context operator C[ ] restricted to NF is the function λλM∈NF(Λ_{⊥}^{∞}).NF(C[M]) : NF(Λ_{⊥}^{∞}) → NF(Λ_{⊥}^{∞}).

Definition 26. M(NF) is continuous if the following holds:

1. (NF(Λ_{⊥}^{∞}), ⪯) is a cpo,

2. the context operators C[ ] restricted to NF are continuous in the Scott topology on the cpo (NF(Λ_{⊥}^{∞}), ⪯) for all context C[ ] ∈ Λ_{⊥}^{∞}.

3. the approximation property holds: NF(M) = ⋃_{n∈ω} NF(NF^{n}(M)) for M ∈ Λ_{⊥}^{∞}.

Counterexample 27. We give examples against continuity of M(NF):

1. Case NF = BeT. The application is not monotone, though the abstraction is continuous. Take M = ⊥, N = λx.⊥ and P = y. Then M ⪯ N but M ·P ⪯̸ N ·P. The approximation property holds since BeT^{n}(M) is in normal form for all n.

2. Case NF = {ηBT, ∞ηBT}. Neither the abstraction nor the application operators are monotone:

(a) Take M = y⊥ and N = yx. Then M ⪯ N but abs(M) ⪯̸ abs(N).

(b) Take M = λzx.zx⊥, N = λzx.zxx and P = λx.y. Then M ⪯ N but M · P ⪯̸ N · P.

Note that in this case the approximation property does not hold.

3. Case NF = T\overline{O} and \overline{O} = \overline{W} ∪ \{M ∈ Λ^{∞} | M → →_{β} λx_{1} … x_{n}.N and N ∈ \overline{W}\}. The abstraction and the application are not continuous:

(a) Take O = λx_{1}x_{2} . . .. Then O = abs(O) ≠ ⋃_{n∈ω} abs(O^{n}) = λx.⊥.

(b) Take fix = λf.f(f(…)) and K = λxy.x. Then O = fix·K ≠ ⋃_{n∈ω} fix^{n} ·K = ⊥. Note that in this case the approximation property does not hold.

We recall a notion of continuous λ-model defined by Welch to deduce that all fixed point operators are equal in the model [2]. For models induced by NF, this result can be deduced instead from confluence and normalisation since the normal form of a fixed point operator is λf.f(f(…)).

Definition 28. An applicative continuous λ-model is a structure (X, ·, ⊑) such that:

1. (X, ⊑) is a cpo,

2. the operation · is continuous in the Scott topology on the cpo (X, ⊑) and

3. the approximation property holds for Böhm trees on finite λ-terms: [[M]] = ⊔{[[BT^{n}(M)]] | n ∈ ω}, for all M ∈ Λ.

According to Definition 28, the model induced by BT is the only one from Figure 1 which is applicative continuous. None of the remaining trees satisfy the third clause. By replacing BT by the general form NF, we got the third clause in Definition 26.

7 Continuity of the context operators

In this section we study continuity of M(NF) in relation to continuity of NF. We prove that if NF is continuous in (Λ_{⊥}^{∞}, ⪯) then so is M(NF); and the converse for NF = T_{U}. This allows us to deduce that the only continuous models induced by the parametric trees are M(BT) and M(LT).

Theorem 29. If NF is continuous in (Λ_{⊥}^{∞}, ⪯) then

1. (NF(Λ_{⊥}^{∞}), ⪯) is an algebraic cpo.

2. The Scott topology on (NF(Λ_{⊥}^{∞}), ⪯) is the subset topology and the quotient topology by NF. In other words, it is initial for the inclusion and final for NF.

3. If f : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is continuous in (Λ_{⊥}^{∞}, ⪯) then NF ∘ f_{↾NF(Λ_{⊥}^{∞})} is continuous in (NF(Λ_{⊥}^{∞}), ⪯).

Proof. 1. This follows from Proposition 1.2.21 in [2]. Because NF(Λ_{⊥}^{∞}) is a retract of Λ_{⊥}^{∞}, the set NF(Λ_{⊥}^{∞}) of normal forms is closed under directed suprema. It is also easy to see that it is algebraic. The compact elements in (NF(Λ_{⊥}^{∞}), ⪯) are the finite normal forms.

2. See Proposition 5.0.11 in [17].

3. Let f be continuous in (Λ_{⊥}^{∞}, ⪯). Since NF : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is continuous, then so is the inclusion inc : NF(Λ_{⊥}^{∞}) → Λ_{⊥}^{∞}. Then, NF ∘ f_{↾NF(Λ_{⊥}^{∞})} = NF ∘ f ∘ inc is composition of continuous functions.

Theorem 30. If NF is continuous in (Λ_{⊥}^{∞}, ⪯) then so is M(NF).

Proof. The first clause in Definition 26 is Theorem 29 part 1. For the second clause, since C[⋃ X] = ⋃ C[X], we have that λλM ∈ Λ_{⊥}^{∞}.C[M] : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is continuous in (Λ_{⊥}^{∞}, ⪯) and, then, we apply Theorem 29 part 3. For the third clause, we have that X = {NF^{n}(M) | n ∈ ω} is a directed set and NF(M) = NF(NF(M)) = ⋃_{n∈ω}{NF(NF^{n}(M)) | n ∈ ω}.

The converse holds for the parametric trees:

Theorem 31. If M(T_{U}) is continuous then so is T_{U} : Λ_{⊥}^{∞} → Λ_{⊥}^{∞}.

Proof. It is enough to prove that T_{U} quasi-preserves ⪯_{fin}. In that case, T_{U}(M^{n}) ⪯ T_{U}(M), by Lemma 16 the truncations are T_{U}-increasing and then we have that:

T_{U}(M) = ⋃_{n∈ω} T_{U}(T_{U}^{n}(M))
⪯ ⋃_{n∈ω} T_{U}(M^{n}) by Lemma 14

We now prove that T_{U} quasi-preserves ⪯_{fin}. Let P ⪯_{fin} Q. We do induction on the number n of subterms that are replaced by ⊥ in Q. The case n = 1 is P = C[⊥] and Q = C[M]. Since all context operators are monotone, T_{U}(C[⊥]) ⪯ T_{U}(C[M]) = T_{U}(C[NF(M)]). The case n > 0 is similar.

Theorem 32. M(BT) and M(LT) are the only continuous models induced by parametric trees.

Proof. By Corollary 21, Theorem 22 and Theorem 31.

8 An embedding from ∞ηBT(Λ_{⊥}^{∞}) in D_{∞}

In this section we use the fact that M(BT) is continuous to prove that the interpretation on D_{∞} extended to infinite terms is homomorphic with the application and the abstraction. We can, then, show that there is an injective embedding from the infinitary lambda calculus of ∞η-Böhm trees in D_{∞}. Using the Approximation Theorem [19] we extend the interpretation to infinite terms as follows: [[M]] = ⊔{[[BT^{n}(M)]] | n ∈ ω} for an infinite term M.

Lemma 33. Let M, N ∈ Λ_{⊥}^{∞}.

1. If BT(M) ⪯ BT(N) then D_{∞} ⊧ M ⊑ N.

2. If BT(M) → → →_{η^{−1}} BT(N) then D_{∞} ⊧ M = N.

The first part is proved using the Characterisation Theorem on finite terms. For the second part, we have to re-do some work and prove a similar statement to Proposition 19.1.13 in [2] for infinite β⊥-normal forms.

Lemma 34. [[C[M]]] = ⊔{[[C[BT^{n}(M)]]] | n ∈ ω}

Proof. By Theorem 32, we have that λλM ∈BT(Λ_{⊥}^{∞}).BT(C[M]) is continuous. Hence,

1. C[BT^{n}(M)] ⪯_{BT} C[M] by monotonicity.

2. for all n there exists k such that BT^{n}(C[M]) ⪯_{BT} C[BT^{k}(M)] because the truncations are compact in (BT(Λ_{⊥}^{∞}), ⪯).

By Lemma 33, [[C[BT^{n}(M)]]] ⊑ [[C[M]]] and [[BT^{n}(C[M])]] ⊑ [[C[BT^{k}(M)]]].

The following lemma is a triviality in the finite lambda calculus but for the infinite case we need to prove it and use continuity.

Lemma 35. Let M, N ∈ Λ_{⊥}^{∞}.

1. [[(MN)]] = [[M]].[[N]].

2. [[(λx.M)]] = λ^{G}d ∈ D_{∞}.[[M]]_{ρ(x:=d)}.

Proof. Using Lemma 34.

Lemma 36. If D_{∞} ⊧ M ⊑ N then D_{∞} ⊧ C[M] ⊑ C[N].

Proof. This is proved by induction on the position of the hole in C using Lemma 35.

Lemma 37. Let M ∈ Λ_{⊥}^{∞}. Then [[M]] = ⊥ iff M has no head normal form.

Proof. Using the Characterisation Theorem on finite terms.

Theorem 38 (Characterisation Theorem extended to infinite terms). The following statements are equivalent for terms M, N in Λ_{⊥}^{∞}:

1. M ⪯_{η^{−1}} N.

2. D_{∞} ⊧ M ⊑ N.

3. M ⊆_{h} N.

4. M ⊆_{h_{f}} N.

Proof. (1 ⇒ 2) follows from Theorem 33. We prove (2 ⇒ 3). By Lemma 36, D_{∞} ⊧ C[M] ⊑ C[N]. Hence, by Lemma 37, if C[M] has head normal form, so does C[N]. (3 ⇒ 4) is trivial. (4 ⇒ 1) follows by applying the Böhm-out technique to ⪯_{η^{−1}} and it is rather long, though the use of commutation properties of the reductions helps to make it shorter than the proof found in [2] for the finite lambda calculus.

Remark 39. As a consequence of Theorem 38, the interpretation function [[ ]] is an injective embedding from ∞ηBT(Λ_{⊥}^{∞}) to D_{∞}. The following example shows that it is not surjective, i.e. D_{∞} contains more elements than ∞ηBT(Λ_{⊥}^{∞}). We define M_{0} = y⊥ and M_{n} = λx_{1} … x_{n}.y(x_{1}x_{2} … x_{n}⊥)x_{1}x_{2} … x_{n}. Clearly X = {M_{n} | n ∈ ω} is directed in (Λ_{⊥}^{∞}, ⪯_{η^{−1}}) and so is [[X]] = {[[M_{n}]] | n ∈ ω} in D_{∞} by the Characterisation Theorem. The supremum of [[X]] exists in D_{∞} but not in Λ_{⊥}^{∞}.

9 Tree topologies

In this section we study the relation between the Scott topology on the prefix relation and the tree topologies. This allows us to deduce that the only parametric tree topologies that make all context operators continuous and in which the approximation property holds are the ones of Böhm and Lévy–Longo. We also give an alternative proof of continuity of the context operator with respect to the Böhm and Lévy–Longo tree topologies on the set of finite lambda terms via the infinitary lambda calculus [2, 14]. The (Böhm) tree topology is defined in [2] as the initial topology for BT_{↾Λ} : Λ → BT(Λ_{⊥}^{∞}) where BT(Λ_{⊥}^{∞}) is considered with the Scott topology on the prefix relation. By just replacing BT by NF, we get the following two notions of tree topologies:

Definition 40. Suppose that (NF(Λ_{⊥}^{∞}), ⪯) is a cpo. We consider the Scott topology on (NF(Λ_{⊥}^{∞}), ⪯).

1. The tree topology on Λ_{⊥}^{∞} is the initial topology for NF : Λ_{⊥}^{∞} → NF(Λ_{⊥}^{∞}).

2. The tree topology on Λ is the initial topology for NF_{↾Λ} : Λ → NF(Λ_{⊥}^{∞}).

Remark 41. 1. The open sets in the tree topology on Λ_{⊥}^{∞} are of the form NF^{−1}(O)

with O open in NF(Λ_{⊥}^{∞}). They are closed under =_{NF}.

2. The tree topology on Λ is the subspace topology of the tree topology on Λ_{⊥}^{∞}.

In the following lemma, the function NF might not be continuous in (Λ_{⊥}^{∞}, ⪯).

Lemma 42. Suppose (NF(Λ_{⊥}^{∞}), ⪯)) is a cpo.

1. The inclusion inc : NF(Λ_{⊥}^{∞}) → Λ_{⊥}^{∞} is a continuous function from the Scott topology on (NF(Λ_{⊥}^{∞}), ⪯) to the tree topology on Λ_{⊥}^{∞}.

2. Let f : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} be a function such that NF ∘ f = NF ∘ f ∘ NF

(a) The function f is continuous in the tree topology on Λ_{⊥}^{∞} if and only if NF ∘ f_{↾NF(Λ_{⊥}^{∞})} : NF(Λ_{⊥}^{∞}) → NF(Λ_{⊥}^{∞}) is continuous in the Scott topology on (NF(Λ_{⊥}^{∞}), ⪯)).

(b) Suppose f_{↾Λ} : Λ → Λ. If f : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is continuous in the tree topology on Λ_{⊥}^{∞} then f_{↾Λ} : Λ → Λ is continuous in the tree topology on Λ.

Proof. 1. An open set in the tree topology on Λ_{⊥}^{∞} is of the form NF^{−1}(O) with O open in (NF(Λ_{⊥}^{∞}), ⪯)). Then, inc^{−1}(NF^{−1}(O)) = {M ∈ NF(Λ_{⊥}^{∞}) | M ∈ NF^{−1}(O)} = {M ∈ NF(Λ_{⊥}^{∞}) | NF(M) ∈ O} = O because NF(M) = M for all M ∈ NF(Λ_{⊥}^{∞}).

2. (a) (⇒). Let f be continuous in the tree topology on Λ_{⊥}^{∞}. Then, NF ∘ f_{↾NF(Λ_{⊥}^{∞})} = NF ∘ f ∘ inc is composition of continuous functions. (⇐). Let NF ∘ f_{↾NF(Λ_{⊥}^{∞})} be continuous. Then NF ∘ f_{↾NF(Λ_{⊥}^{∞})} ∘ NF : Λ_{⊥}^{∞} → NF(Λ_{⊥}^{∞}) is a continuous function from the tree topology to (NF(Λ_{⊥}^{∞}), ⪯)). We know that NF ∘ f_{↾NF(Λ_{⊥}^{∞})} ∘ NF = NF ∘ f ∘ NF = NF ∘ f. By Proposition 5.0.2 [17], we have that f is continuous in the tree topology on Λ_{⊥}^{∞}.

(b) Any open set in the tree topology on Λ is of the form NF^{−1}(O) ∩ Λ. Then f_{↾Λ}^{−1}(NF^{−1}(O) ∩ Λ) = f^{−1}(NF^{−1}(O)) ∩ Λ is open in the tree topology on Λ.

Theorem 43.

1. The Böhm and Lévy–Longo tree topologies are the only parametric tree topologies on the set Λ_{⊥}^{∞} that satisfies the following two conditions:

(a) continuity of all context operators λλM ∈ Λ_{⊥}^{∞}.C[M] : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} and

(b) the approximation property, i.e. NF(M) = ⋃_{n∈ω} NF(NF^{n}(M)) for M ∈ Λ_{⊥}^{∞}.

2. The finite context operators λλM ∈ Λ.C[M] : Λ → Λ are continuous in the Böhm and Lévy–Longo tree topologies on Λ.

Proof. They follow from Lemma 42 and Theorem 32.

Continuity of the finite context operators with respect to the Böhm tree topology on Λ is proved in [2] and with respect to the Lévy–Longo tree topology on Λ is proved in [14] along the lines of [2]. The proof in [2] uses the notion of approximants (approximants are finite β⊥-normal forms) and essentially the following proposition (called syntactic continuity in [1]): For all finite β⊥-normal form P such that P ⪯_{BT} C[M] there exists N in finite β⊥-normal form such that N ⪯_{BT} M and C[N] ⪯_{BT} N. This proposition has been proved using a variety of methods by Wadsworth [18], Lévy [13] and Welch [20]. Our proof (Theorem 43 part 2) uses the continuity of NF and properties of initial and final topologies.

10 The NF-topology

We will now give an explicit characterisation of the open sets in the Böhm and Lévy–Longo tree topologies.

Definition 44. A subset O of Λ_{⊥}^{∞} is an open set in the NF-topology provided

1. O is open in the Scott topology of (Λ_{⊥}^{∞}, ⪯) and

2. O is closed under =_{NF}.

It is easy to see that the NF-topology makes the normal form NF and the context operators continuous.

Lemma 45. Suppose that NF : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is continuous in (Λ_{⊥}^{∞}, ⪯). Then the tree topology is exactly the set of open sets of (Λ_{⊥}^{∞}, ⪯) closed under =_{NF}.

Proof. Since the tree topology is initial for NF, the open sets of the tree topology are open in (Λ_{⊥}^{∞}, ⪯). They are also closed under =_{NF}. Let O be an open set in (Λ_{⊥}^{∞}, ⪯) closed under =_{NF}. Then, O = NF^{−1}(NF(O)). Since the Scott topology on (NF(Λ_{⊥}^{∞}), ⪯) is final for NF, NF(O) is open in NF(Λ_{⊥}^{∞}) and hence O = NF^{−1}(NF(O)) is open in the tree topology.

Corollary 46. The BT-topology and LT-topology coincide with the Böhm and Lévy– Longo tree topologies respectively.

Proof. This follows from Corollary 21 and Lemma 45.

Unfortunately, the BeT-topology coincides with the LT-topology. In general, the T_{U}-topology is either the BT-topology or the LT-topology.

Acknowledgements. We thank Vincent van Oostrom and the referees for their useful comments, Mariangiola Dezani-Ciancaglini for her knowledge and inspiration, Simona Ronchi della Rocca for telling us the solution of a key exercise in [2] and Alexander Kurz for interesting discussions on coinduction.

References

1. R. M. Amadio and P.-L. Curien. Domains and Lambda-Calculi. Cambridge University Press, Cambridge, 1998.

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

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

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

5. I. Bethke, J.W. Klop, and R. de Vrijer. Descendants and origins in term rewriting. Information and Computation, 159:59–124, 2000.

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. N. Dershowitz, S. Kaplan, and D. Plaisted. Rewrite, rewrite, rewrite, rewrite, rewrite,…. Theoretical Computer Science, 83(1):71–96, 21 June 1991.

8. M. Dezani-Ciancaglini, P. Severi, and F.J. de Vries. Infinitary lambda calculus and discrimination of Berarducci trees. Theoretical Computer Science, 298(2):275–302, 2003.

9. J.R. Kennaway, J.W. Klop, M. 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.

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

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

12. 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.

13. J.-J. Lévy. An algebraic interpretation of the λβK-calculus, and an application of a labelled λ-calculus. Theoretical Computer Science, 2(1):97–114, 1976.

14. C.-H. L. Ong. The lazy lambda calculus:an investigation into the foundations of functional programming. PhD thesis, University of Cambridge, 1992.

15. P. Severi and F.J. de Vries. A lambda calculus for D_{∞}. Technical report, University of Leicester, 2002.

16. 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.

17. M. Smyth. Topology. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1, pages 641–762. Oxford University Press, Oxford, 1993.

18. C. P. Wadsworth. Semantics and Pragmatics of the Lambda-calculus. PhD thesis, Oxford University, 1971.

19. C. P. Wadsworth. Approximate reduction and lambda calculus models. SIAM Journal on Computing, 7(3):337–356, 1978.

20. P. Welch. Continuous semantics and inside out reductions. In C. Böhm, editor, Lambda Calculus and Computer Science Theory, volume 37 of LNCS, pages 122–146. Springer-Verlag, 1975.