Order Structures on Böhm-like Models

Paula Severi and Fer-Jan de Vries

Department of Computer Science, University of Leicester, UK

Abstract. We are interested in the question whether the models induced by the infinitary lambda calculus are orderable, that is whether they have a partial order with a least element making the context operators monotone. The first natural candidate is the prefix relation: a prefix of a term is obtained by replacing some subterms by ⊥. We prove that six models induced by the infinitary lambda calculus (which includes Böhm and Lévy-Longo trees) are orderable by the prefix relation. The following two orders we consider are the compositions of the prefix relation with either transfinite η-reduction or transfinite η-expansion. We prove that these orders make the context operators of the η-Böhm trees and the ∞η-Böhm trees monotone. The model of Berarducci trees is not monotone with respect to the prefix relation. However, somewhat unexpectedly, we found that the Berarducci trees are orderable by a new order related to the prefix relation in which subterms are not replaced by ⊥ but by a lambda term O called the ogre which devours all its inputs. The proof of this uses simulation and coinduction. Finally, we show that there are 2^{c} unorderable models induced by the infinitary lambda calculus where c is the cardinality of the continuum.

1 Introduction

In this paper we give order structure to some models induced by the infinitary lambda calculi. 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 [8]. 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 [3, 8, 9, 7, 13, 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 [3, 8,

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

Fig. 1. Infinitary Lambda Calculi

9]. In the fourth row, there is an uncountable class of infinitary lambda calculi with a ⊥-rule parametrised by a set U of meaningless terms [10, 7]. By changing the parameter set U of the ⊥-rule, 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 [13]. 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. In this paper we give some new examples of parametric 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 (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).

Figure 2 summarizes the results proved in this paper. The first order we consider is the prefix relation ⪯. This is a natural order on terms. If 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 BerT : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} and the application operator are not even monotone [6] and it is not clear how to define a domaintheoretic model whose local structure is represented by Berarducci trees, though some attempts have been made via types and filter models [4]. We prove that P_{U} : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} preserves ⪯ provided U is quasi-regular and ⊥P is equal to ⊥. This generalizes the proof of monotonicity of BT and LLT given in [14]. We, then, conclude that the prefix relation makes the context operators of six models monotone including the models of Böhm and Lévy-Longo trees.

We also define two orders for the extensional models and prove that they make the context operators monotone. The partial order ⪯_{η} on the set of η-Böhm trees is the composition of the prefix relation with transfinite η-reduction and it corresponds to the order on D_{∞}^{∗} [5]. The partial order ⪯_{η!} on the set of ∞η-Böhm trees is the composition of the prefix relation with transfinite η!- reduction and it corresponds to the order on Scott’s model D_{∞}.

The next step is to find an order for Berarducci trees. We prove that the least element of an arbitrary orderable model induced by NF should be either ⊥ or a term O called the ogre which eats all its inputs. In case the least element is ⊥ then ⊥P should reduce to ⊥ for all P ∈ Λ_{⊥}^{∞}. Hence, ⊥ cannot be the least element of an order on Berarducci trees and the only possible candidate is O. The term O is the solution to the recursive equation O = λx.O and it can be obtained by applying any fixed point operator to the combinator K = λxy.x. In the lambda model induced by Böhm trees, the ogre is interpreted as bottom. But there are many other lambda models such as the ones induced by Lévy-Longo and Berarducci trees that give a different interpretation to ogre. In these models, O is identified with the infinite sequence of abstractions λx_{1}.λx_{2}.λx_{3} . . .. We consider an order called ⊴ on terms related to the prefix relation in which subterms are not replaced by ⊥ but by the term O. We prove that the parametric trees P_{U} : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} preserve ⊴ provided U is quasi-regular and O ∈ P_{U}(Λ_{⊥}^{∞}) using simulations and coinduction. We, then, conclude that ⊴ makes the context operators monotone of five models including the model of Berarducci trees. We can see in Figure 2 that the relations ⪯ and ⊴ make the context operators of some models simultaneously monotone.

Finally, we show that there are 2^{c} unorderable models induced by the infinitary lambda calculus where c is the cardinality of the continuum. In [12] Salibra proves that there is a continuum of unorderable λ-models by considering the equation ΩMM = Ω. This idea does not work for infinitary lambda calculus because this equation interpreted as a reduction rule is not left linear and adding it to the infinitary lambda calculus of Berarducci trees would destroy confluence, as can be seen with help of a variant of Klop’s counterexample in [11]. In our case, the trick consists in equating ⊥P sometimes to ⊥ and sometimes not. We consider the set B^{0} of closed Böhm trees without ⊥ which has cardinality c and construct infinitary lambda calculi whose normal form functions U_{X} are indexed on X ⊆ B^{0} by stating that ⊥P reduces to ⊥ if P ∈ X.

2 Infinite Lambda Calculi

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

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

where x is a variable from some fixed set of variables V. We follow the usual conventions on syntax. Terms and variables will respectively be written with (super- and subscripted) letters M, N and x, y, z. Terms of the form (M_{1}M_{2}) and (λxM) will respectively be called applications and abstractions. A context C[ ] is a term with a hole in it, and C[M] denotes the result of filling the hole

Normal forms Prefix Ogre order Prefix up to η Prefix up to η! Orderable
NF  ⪯  ⊴  ⪯_{η}  ⪯_{η!}  models
∞ηBT  −  −  −  +  +
ηBT  −  −  +  −  +
BT = P\overline{HN}  +  −  −  −  +
P_{\overline{HN} −O}  +  +  −  −  +
P_{HA∪O}  +  −  −  −  +
P_{HA}  +  +  −  −  +
LLT = P\overline{WN}  +  +  −  −  +
P_{SA}  +  +  −  −  +
U_{X}  −  −  −  −  −
BerT = P\overline{T N}  −  +  −  −  +

Fig. 2. Orderability of the models induced by NF

by the term M, possibly by capturing some free variables of M. If σ : V → Λ^{∞} then M^{σ} is the simultaneous substitution of the variables in M by σ.

The set Λ_{⊥}^{∞} of finite and infinite λ-terms is defined by coinduction using the same grammar as for Λ_{⊥}. This set contains the three sets of Böhm, Lévy–Longo and Berarducci trees. In [9, 10, 7], an alternative definition of the set Λ_{⊥}^{∞} is given using a metric. The coinductive and metric definitions are equivalent [2]. In this paper we consider only one set of λ-terms, namely Λ_{⊥}^{∞}, in contrast to the formulations in [9, 10] where several sets (which are all subsets of Λ_{⊥}^{∞}) are considered. The paper [7] shows that the infinitary lambda calculi can be formulated using a common set Λ_{⊥}^{∞}, confluence and normalisation still hold since the extra terms added by the superset Λ_{⊥}^{∞} are meaningless and equated to ⊥.

We define several rules 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 [10, 7] where Λ^{∞} is the set of terms in Λ_{⊥}^{∞} that do not contain ⊥ (see Section 4).

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

\begin{matrix}(λx.M)N → M[x := N] (β) & \begin{aligned}M[⊥ := Ω] ∈ U M ≠ ⊥ \\ & (⊥) \\ M → ⊥ \end{aligned} \\ \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} \end{matrix}

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

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

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

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

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

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

no N in λ_{ρ}^{∞} such that M →_{ρ} N.

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

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

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

In [7] confluence of the parametric calculi is proved for Cauchy converging reduction as well as for strongly converging reduction.

Theorem 4. [13, 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 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. We denote by M =_{NF} N if NF(M) = NF(N).

3 Basic forms

In this section we introduce new forms of terms analogous to the notions of head, weak head and top normal forms and define certain specific subsets of Λ^{∞} (terms of Λ_{⊥}^{∞} without ⊥) containing the respective forms.

Definition 5. Let M ∈ Λ_{⊥}^{∞}. We define that

1. M is a head normal form (hnf) if M = λx_{1} … x_{n}.yP_{1} … P_{k}.

2. M is a weak head normal form (whnf) if M is a hnf or M = λx.N.

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

4. M is a rootactive form (with respect to β) if for all M → → →_{β} N there exists a redex (λx.P)Q such that N → → →_{β} (λx.P)Q.

5. M is a head bottom form (hbf) if M = λx_{1} … x_{n}.⊥P_{1} … P_{k}.

6. M is a head active form (haf) if M = λx_{1} … x_{n}.RP_{1} … P_{k} and R is rootactive.

7. M is a strong active form (saf) if M = RP_{1} … P_{k} and R is rootactive.

8. M is a strong active form relative to X (X-saf) if M = RP_{1} … P_{k} and R is rootactive and P_{1}, …, P_{k} ∈ X.

9. M is an infinite left spine form (ilsf) if M = λx_{1} … x_{n}.((… P_{2})P_{1}.

10. M is a strong infinite left spine form (silsf) if M = ((… P_{2})P_{1}.

11. M is a basic form if it is either a head normal form, a head bottom form, a head active form, an infinite left spine or the ogre.

We now define some subsets of Λ^{∞} for the previous defined forms.

Definition 6. We define the following subsets of Λ^{∞}:

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

By \overline{HN}, \overline{WN} and \overline{T N} we denote their respective complements.

Definition 7. 1. The basic sets are the following subsets of Λ^{∞}:

HA = {M ∈ Λ^{∞} | M → →_{β} N and N is head active}
IL = {M ∈ Λ^{∞} | M → → →_{β} N and N is an infinite left spine form}
O = {M ∈ Λ^{∞} | M → → →_{β} O}

2. The strongly basic sets are the following subsets of Λ^{∞}:

R = \{M ∈ Λ^{∞} | M is rootactive\} = \overline{T N}
SA = {M ∈ Λ^{∞} | M → →_{β} N and N is strong active }
SIL = {M ∈ Λ^{∞} | M → → →_{β} N and N is a strong infinite left spine form }

3. Finally we define a family of subsets of Λ^{∞} depending on some X ⊆ Λ^{∞}:

SA_{X} = {M ∈ Λ^{∞} | M → → →_{β} N and N is a strong active form relative to X}

Note that R[⊥ := Ω] ∈ R iff R is ⊥ or R is rootactive with respect to β.

Definition 8. The skeleton of a term M ∈ Λ_{⊥}^{∞} is defined by coinduction:

skel(M) = y  if M → →_{β} y
skel(M) = ⊥  if M → →_{β} ⊥
skel(M) = λx.skel(N)  if M → →_{β} λx.N
skel(M) = skel(N) skel(P) if M → →_{β} NP and N ↛ →_{β} λx.Q for any Q
skel(M) = M  if M does not have a top normal form

The skeleton of a term is essentially the Berarducci tree of a term but instead of replacing rootactive terms by ⊥, we leave rootactive terms untouched.

Lemma 9. Let M ∈ Λ_{⊥}^{∞}. Then M → → →_{β} skel(M) and skel(M) is a basic form.

4 Axioms of meaningless terms

In this section we recall the axioms of meaningless terms [10, 7] and give new examples of parametric infinite lambda calculi. Let U ⊆ Λ^{∞} be an arbitrary set. The axioms of meaningless terms on the set U are:

1. Closure under β-reduction. If M ∈ U and M → → →_{β} N then N ∈ U.

2. Overlap. If λx.M ∈ U then (λx.M)N ∈ U.

3. Closure under substitution. If M ∈ U then M^{σ} ∈ U.

4. Rootactiveness. R ⊆ U.

5. Indiscernibility. Let M ↔^{U} N denote that if N is obtained from M by replacing some (possibly infinitely many) subterms in U by other terms in U. Then, M ∈ U iff N ∈ U.

Definition 10. A set U ⊆ Λ^{∞} of meaningless terms is a set that satisfies the five axioms of meaningless terms.

Hence, the parametric infinitary lambda calculi are the calculi λ_{β⊥}^{∞} with a parametric ⊥-rule on a set U satisfying the axioms of meaningless terms given above. The normal form of these calculi is denoted by P_{U}. If U = Λ^{∞} then M =_{P_{U}} ⊥ for all M ∈ Λ_{⊥}^{∞} and P_{U} induces the trivial theory. Since indiscernibility is not easy to prove, we will reduce it to some property which is easier to prove. For this, we need the following properties on a set U ⊆ Λ^{∞}:

1. Closure under β-expansion. If N ∈ U and M → → →_{β} N then M ∈ U.

2. Indiscernibility on skeletons. Let P be a skeleton such that P ⪯_{U} M and P ⪯_{U} N. Then, M ∈ U iff N ∈ U.

Definition 11. A set U of strongly meaningless terms is a set that satisfies: closure under β-reduction, overlap, closure under substitution, rootactiveness, closure under β-expansion and indiscernibility on skeletons.

Theorem 12. [10, 7] \overline{HN}, \overline{WN} and \overline{T N} = R are sets of meaningless terms.

Definition 13. Let U ⊆ Λ^{∞}, M, N ∈ Λ_{⊥}^{∞}. Then, M ⪯_{U} N if M is obtained from N by replacing some subterms of N which belong to U by ⊥.

Lemma 14. Let U be closed under substitution. If M ⪯_{U} N and M → → →_{β} M′ then N → → →_{β} N′ and M′ ⪯_{U} N′ for some N′.

Proof. This is proved by induction on the length of the reduction sequence. ⊓ ⊔

The following lemma may not hold for terms that are not rootactive. For instance, take (λx.Ω) ∈ U, M = ⊥P and N = (λx.Ω)P. Then M ⪯_{U} N and N →_{β} N′ = Ω but there is no M′ such that M → →_{β} M′ ⪯_{U} N′.

Lemma 15. Let U be closed under substitution and M rootactive. If M ⪯_{U} N and N → →_{β} N′ then there exists M′ such that M → →_{β} M′ and M′ ⪯_{U} N′.

Proof. We do only one step of β-reduction. Since M is rootactive, we then have that M = (λx.M_{0})M_{1} … M_{k}. But then N = (λx.N_{0})N_{1} … N_{k} and M_{i} ⪯_{U} N_{i}. We contract the β-redex in the head position in N and in M. Since U is closed under substitution, M_{0}[x := M_{1}]M_{2} … M_{k} ⪯_{U} N_{0}[x := N_{1}]N_{2} … N_{k}. ⊓ ⊔

Lemma 16. Let U be closed under substitution. If M ⪯_{U} N and M rootactive then N is rootactive.

Proof. Suppose now that N is not rootactive, then there exists a top normal form N′ such that N → →_{β} N′ by contracting only head redexes. Then, by Lemma 15 there exists M′ such that M → →_{β} M′ and M′ ⪯_{U} N′. If N′ is a top normal form then so is M′. ⊓ ⊔

Theorem 17. If U ⊂ Λ^{∞} is a set of strongly meaningless terms then it is also a set of meaningless terms.

Proof. Both definitions have the first four axioms in common. We prove indiscernibility. Let M ↔^{U} N. Then there exists P such that P ⪯_{U} M and P ⪯_{U} N. By Lemma 9 and Lemma 14, we have that skel(P) ⪯_{U} M′ and skel(P) ⪯_{U} N′ for some M′, N′ such that M → → →_{β} M′ and N → → →_{β} N′. By indiscernibility on skeletons M′ ∈ U iff N′ ∈ U. Since U is closed under β-reduction and β-expansion, we have that M ∈ U iff N ∈ U. ⊓ ⊔

Theorem 18. The following sets are sets of strongly meaningless terms:

1. HA, SA, HA ∪ IL and HA ∪ O

2. SA_{X} if X is a subset of closed terms in BerT(Λ_{⊥}^{∞}) without ⊥.

Proof. The first five axioms are not difficult to prove. We prove indiscernibility on skeletons for SA_{X}. Suppose P is a skeleton and P ⪯_{SA_{X}} M, N.

1. If P is either a head normal form, the ogre or an infinite left spine so are M and N. Hence, M, N ∉ SA_{X}.

2. If P = λx_{1} … x_{n}.RP_{1} … P_{k} is a head active form. By Lemma 16, M and N are also head active forms. Then M = λx_{1} … x_{n}.R′M_{1} … M_{k}, N = λx_{1} … x_{n}.R′′N_{1} … N_{k}. and P_{i} ⪯_{SA_{X}} M_{i}, N_{i} for 1 ≤ i ≤ k. If M ∈ SA_{X} then n = 0 and M_{i} = BerT(M_{i}) ∈ X ⊆ Λ^{∞}. Since M_{i} = BerT(M_{i}), we have that M_{i} does not contain subterms in SA_{X} and hence P_{i} = M_{i}. Then, P_{i} does not contain ⊥ and also P_{i} = N_{i}. Clearly, N_{i} ∈ X and N ∈ SA_{X}.

3. Suppose P = λx_{1} … x_{n}.⊥P_{1} … P_{k} is a head bottom form. The bottom in the head of P has to be replaced by some term in SA_{X} to get M and N. Then, we proceed as in the previous part to prove that P_{i} = M_{i} = N_{i} ∈ X.

⊓ ⊔

5 Regular and quasi-regular sets

In this section we define and give examples of regular and quasi-regular sets of meaningless terms. Figure 3 summarizes and shows all these sets. ordered by inclusion. We use the notation U → U if U ⊃ U′.

\xymatrix{ &  & HA ∪ IL ∪ O = \overline{HN} \ar@{-->}[dl] \ar@{-->}[dr] \\  & HA ∪ IL = \overline{HN} − O \ar@{-->}[dl] \ar@{-->}[dr] &  & HA ∪ O \ar[dl] \\ SA ∪ SIL = \overline{WN} \ar@{-->}[dr] &  & HA \ar[dl] \\  & SA \ar[d] \\  & _{SA_{X}} \ar[d] \\  & R = \overline{T N}}

Fig. 3. Sets of meaningless terms ordered by inclusion

Definition 19. Let U ⊆ Λ^{∞} be a set of meaningless terms.

1. U is regular if for all basic sets X, if X ∩ U ≠ ∅ then X ⊆ U.

2. U is quasi-regular if for all strongly basic sets X, if X ∩ U ≠ ∅ then X ⊆ U.

If a set is regular then it is quasi-regular. The sets SA_{X} are neither regular nor quasi-regular provided X ≠ ∅ and X ≠ Λ^{∞}.

Theorem 20. Let U be a set of meaningless terms.

1. If λx.M ∈ U then M ∈ U.

2. If λx.M ∈ U then HA ⊆ U. In particular, if O ∈ U then HA ⊂ U.

3. If SIL ⊆ U then SA ⊆ U.

4. If IL ⊆ U then HA ⊆ U.

5. If a head normal form is in U then U = Λ^{∞}.

Proof. We only prove the first three parts. The rest are similar.

1. By the overlap and closure under β-reduction axioms, (λx.M)x →_{β} M ∈ U.

2. By the overlap axiom, (λx.M)Q ∈ U for all Q ∈ Λ^{∞}. By indiscernibility we have that RQ ∈ U for R ∈ R and also RQ_{1} … Q_{k} ∈ U for all Q_{i} ∈ Λ^{∞}. By the previous part and indiscernibility, λx.R ∈ U and hence λx_{1} … x_{n}.RQ_{1} … Q_{k} ∈ U.

3. Let (^{ω}Q) = ((…)Q)Q). We have that (^{ω}Q) = (^{ω}Q)Q ∈ U By indiscernibility, RQ ∈ U for any R ∈ R and also RQ_{1} … Q_{k} ∈ U for all Q_{i} ∈ Λ^{∞}. ⊓ ⊔

Corollary 21. The regular sets are: HA ∪ IL ∪ O = \overline{HN}, HA ∪ IL = \overline{HN} − O, HA ∪ O and HA. The quasi-regular sets are the regular ones and the sets SA ∪ SIL = \overline{WN}, SA and R = \overline{T N}.

6 Explicit definition of the normal forms

Figure 4 shows the difference between the normal forms of the different parametric infinitary lambda calculi considered in this paper.

In the figure we make the abbreviations: λx.M = λx_{1} … x_{n}.M and MP = MP_{1} … P_{k}. For simplicity we assume that P_{i} ∈ P_{U}(Λ_{⊥}^{∞}) for all i. The case of head bottom forms is not shown in the table but it is as the case of head active forms where ⊥ plays the role of the rootactive term R. The cases U = \overline{HN} , \overline{WN} and \overline{T N} correspond to the cases of Böhm, Lévy-Longo and Berarducci trees respectively.

Set U Head normal form Ogre Head active form Inf left spine form
P_{U}(λx.yP)  P_{U}(O)  P_{U}(λx.RP)  P_{U}(λx.((… P_{2})P_{1}))
\overline{HN}  λx.yP  ⊥  ⊥  ⊥
\overline{HN} − O  λx.yP  O  ⊥  ⊥
HA ∪ O  λx.yP  ⊥  ⊥  λx.((… P_{2})P_{1})
HA  λx.yP  O  ⊥  λx.((… P_{2})P_{1})
\overline{WN}  λx.yP  O  λx.⊥  λx.⊥
SA  λx.yP  O  λx.⊥  λx.((… P_{2})P_{1})

SA^{X}

λx.yP O \{ \begin{matrix}λx.⊥ & if P ∈ X \\ λx.⊥P & otherwise \end{matrix} λx.((… P_{2})P_{1})

\overline{T N}  λx.yP  O  λx.⊥P  λx.((… P_{2})P_{1})

Fig. 4. Definition of P_{U}(M) when M is a skeleton

7 Models induced by NF

There are many ways of making models of lambda calculus, i.e. λ-models. In this paper we will emphasise yet another method where the lambda calculus itself does the job. The idea is simple: any confluent and normalising extension of lambda calculus gives rise to a model: namely the set of normal forms. Taking the normal form of the application of two normal forms then is the application for this semantics.

Definition 22. 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 ∈ Λ.

It is easy to prove that M(NF) is a λ-model using confluence and normalization (see Definition 5.2.7, Definition 5.3.1 and Theorem 5.3.6 in [1]).

Definition 23. A partial order ⊑ on a set A is a relation on A that reflexive, transitive and antisymmetric. If the partial order ⊑ on A has a least element we say that ⊑ is a pointed poset on A.

We consider partial orders on the set Λ_{⊥}^{∞} or NF(Λ_{⊥}^{∞}). If M is the least element of a pointed poset ⊑ on NF(Λ_{⊥}^{∞}) then, obviously, M is in normal form. Domain Theory usually follows the convention of denoting the least element by ⊥. In our case, ⊥ is a special constant in the syntax which equates the undefined or meaningless terms but we will see that it is not necessarily the least element. In some cases, the least element could be the ogre O (if O ∈ NF(Λ_{⊥}^{∞})).

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

For the models induced by NF, it makes sense to define a notion of monotonicity that considers all context operators and not only the application.

Definition 25. The partial order ⊑ makes the context operators of M(NF) monotone if the following hold:

1. (NF(Λ_{⊥}^{∞}), ⊑) is a pointed poset and

2. the context operators C[ ] restricted to NF are monotone in (NF(Λ_{⊥}^{∞}), ⊑) for all context C[ ] ∈ Λ_{⊥}^{∞}.

Definition 26. We say that M(NF) is orderable (by ⊑) if there exists a partial order ⊑ on NF(Λ_{⊥}^{∞}) that makes the context operators monotone. We say that M(NF) is unorderable if it is not orderable.

8 The prefix relation

Definition 27. 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 prefix relation ⪯ is a pointed poset on NF(Λ_{⊥}^{∞}) with ⊥ as least element.

Lemma 28. If M ⪯ N then there exists N′ such that P_{U}(M) ⪯ N′ and N → → →_{β} N′.

Proof. Using Lemma 9 and by taking U = Λ^{∞} in Lemma 14, we have that skel(M) ⪯ N′ for some N′ such that N → → →_{β} N′. Hence P_{U}(M) ⪯ skel(M) ⪯ N′.

⊓ ⊔

The following theorem is a generalization of the proof of monotonicity of BT and LLT given in [14]. It is possible to give an alternative proof of this theorem using a simulation similar to Theorem 42.

Theorem 29. Let U be quasi-regular and SA ⊆ U. Then, P_{U} : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is monotone in (Λ_{⊥}^{∞}, ⪯).

Proof. Let M, N ∈ Λ_{⊥}^{∞} such that M ⪯ N. We prove that P = P_{U}(M) ⪯ P_{U}(N). By Lemma 28 we have that P ⪯ Q and N → → →_{β} Q for some Q. It is enough to prove that P^{n} ⪯ P_{U}(Q) (where P^{n} denotes the truncation of P at depth n). Then, P = ⋃_{n∈ω} P^{n} ⪯ P_{U}(Q). We prove P^{n} ⪯ P_{U}(Q) fo all n by induction.

1. P = λx_{1} … x_{n}.yP_{1} … P_{m}. Then Q = λx_{1} … x_{n}.yQ_{1} … Q_{m} and for all i, P_{i} ⪯ Q_{i}. Hence, P_{U}(Q) = λx_{1} … x_{n}.yP_{U}(Q_{1}) … P_{U}(Q_{m}). By induction hypothesis, (P_{i})^{h} ⪯ P_{U}(Q_{i}) for all h < n. It is easy to see that P^{n} ⪯ P_{U}(Q).

2. P = O. Then P = Q = O.

3. P = λx_{1} … x_{n}.⊥P_{1} … P_{m}. Then, Q = λx_{1} … x_{n}.Q_{0}. Since SA ⊆ U, we have that m = 0. If n > 0 then by Theorem 20 no abstraction belongs to U and hence P_{U}(Q) = λx_{1} … x_{n}.P_{U}(Q_{0}).

4. P = λx_{1} … x_{n}.((…)P_{2})P_{1}. Then, Q = λx_{1} … x_{n}.((…)Q_{2})Q_{1}. Suppose towards a contradiction that Q ∈ U. Then ((…)Q_{2})Q_{1} ∈ U by Theorem 20. Since U is quasi-regular, all infinite left spine should belong to U and contradicts the fact that P is an infinite left spine in β⊥-normal form. Hence, P_{U}(Q) = λx_{1} … x_{n}.((…)P_{U}(Q_{2}))P_{U}(Q_{1}). By induction hypothesis, (P_{U}(P_{i}))^{h} ⪯ P_{U}(Q_{i}) for all h < n. It is easy to see that (P)^{n} ⪯ P_{U}(Q). ⊓ ⊔

The next corollary is deduced from Corollary 21 and the previous theorem.

Corollary 30. The functions NF ∈ \{BT, P_{\overline{HN} −O}, P_{HA∪O}, P_{HA}, LLT, P_{SA}\} are monotone in (Λ_{⊥}^{∞}, ⪯).

Theorem 31. If NF : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is monotone in (Λ_{⊥}^{∞}, ⪯) then the prefix relation ⪯ makes the context operators of M(NF) monotone.

Proof. If M ⪯ N then C[M] ⪯ C[N]. Since P_{U} is monotone, we have that P_{U}(C[M]) ⪯ P_{U}(C[N]). ⊓ ⊔

Corollary 32. The prefix relation ⪯ makes the context operators of M(NF) monotone for NF ∈ \{BT, P_{\overline{HN} −O}, P_{HA∪O}, P_{HA}, LLT, P_{SA}\}.

Corollary 33. The models induced by BT, P_{\overline{HN} −O}, P_{HA∪O}, P_{HA}, LLT and P_{SA} are all orderable.

We show some examples in which the prefix relation does not make all the context operators monotone:

1. The prefix relation ⪯ does not make the application monotone of M(BerT), though it makes the abstraction monotone. Take M = ⊥, N = λx.⊥ and P = y. Then M ⪯ N but M · P ⪯̸ N · P.

2. The prefix relation ⪯ does not make either the abstraction or the application of M(ηBT) and M(∞ηBT) monotone.

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

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

9 Orders for extensionality

We define two partial orders for which the context operators of the extensional models will be monotone.

Definition 34. 1. Let M, N ∈ ηBT(Λ_{⊥}^{∞}). Then, M ⪯_{η} N if M _{η} ← ← ← P ⪯

Q → → →_{η} N for some P, Q ∈ BT(Λ_{⊥}^{∞}).

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

Lemma 35. [13, 15] Let M, N ∈ Λ_{⊥}^{∞}. If M → → →_{η} N, then BT(M) → → →_{η} BT(N). And if M → → →_{η!} N, then BT(M) → → →_{η!} BT(N).

Theorem 36. 1. ⪯_{η} makes the context operators of M(ηBT) monotone.

2. ⪯_{η!} makes the context operators of M(∞ηBT) monotone.

Proof. We only prove (1). The proof of (2) is similar. Suppose that M ⪯_{η} N. Then BT(M) → → →_{η} P ⪯ Q _{η}← ← ← BT(N). By Lemma 35 and monotonicity of BT (Corollary 30), BT(C[M]) → → →_{η} BT(C[P]) ⪯ BT(C[Q]) _{η}← ← ← BT(C[N]). ⊓ ⊔

Corollary 37. The models induced by ηBT and ∞ηBT are orderable.

10 Ogre as least element

In order to make the application of Berarducci trees monotone, the ogre should be the least element and not ⊥. This is a consequence of the following theorem:

Theorem 38. If ⊑ makes the application of M(NF) monotone then we have that:

1. either ⊥ is the least element of ⊑ and ⊥P →_{⊥} ⊥ for all P ∈ Λ_{⊥}^{∞} or

2. O is the least element of ⊑.

Proof. Suppose that M ∈ NF(Λ_{⊥}^{∞}) is the least element. Then M ⊑ λx.M and we choose x ∉ fv(M). If application is monotone then M · P ⊑ (λx.M) · P =_{NF} M and hence MP =_{NF} M for all P for all P ∈ NF(Λ_{⊥}^{∞}). Now either M = ⊥ in which case ⊥P →_{⊥} ⊥ for all P ∈ Λ_{⊥}^{∞}. Or M ≠ ⊥ and then Mx = M for all x. Hence M is the solution of the recursive equation M = λx.M and so M = O. ⊓ ⊔

We define a partial order making the model of Berarducci trees monotone:

Definition 39. Let O ∈ NF(Λ_{⊥}^{∞}). We define ⊴ on NF(Λ_{⊥}^{∞}) as follows: M ⊴ N if M is obtained from N by replacing some subterms of N by O.

It is easy to see that ⊴ is partial order and that O is the least element.

Definition 40. An ogre simulation is a relation S on Λ_{⊥}^{∞} such that MSN implies:

1. If M = λx_{1} … x_{n}.y then N = λx_{1} … x_{n}.y.

2. If M = λx_{1} … x_{n}.⊥ then N = λx_{1} … x_{n}.⊥.

3. If M = λx_{1} … x_{n}.P Q then N = λx_{1} … x_{n}.P′Q′, P SP′ and QSQ′.

The relation ⊴ is the maximal ogre simulation.

Lemma 41. Let M ⊴ N.

1. If M → → →_{β} M′ then there exists N′ such that M′ ⊴ N′ and N → → →_{β} N′.

2. If N → → →_{β} N′ then there exists M′ such that M′ ⊴ N′ and M → → →_{β} M′.

3. If M is rootactive then N is rootactive.

Proof. The first two parts are proved by induction on the length of the reduction sequence. The last part uses the second one. ⊓ ⊔

Theorem 42. Let O ∈ P_{U}(Λ_{⊥}^{∞}). If U is quasi-regular then P_{U} : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is monotone in (Λ_{⊥}^{∞}, ⊴).

Proof. Let M, N ∈ Λ_{⊥}^{∞} such that M ⊴ N. We prove that P_{U}(M) ⊴ P_{U}(N). Let U = skel(M). By Lemma 41 we have that U ⊴ V and N → → →_{β} V for some V. We define S as the set of pairs (P_{U}(P), P_{U}(Q)) such that P and Q are subterms of respectively U and V at the same position p and they are not subterms of rootactive terms. Note that if U ⊴ V then P ⊴ Q. We prove that S is an ogre simulation. Suppose (P, Q) ∈ S. Then,

1. P = λx_{1} … x_{n}.yP_{1} … P_{m}. Then Q = λx_{1} … x_{n}.yQ_{1} … Q_{m} and for all i, P_{i} ⊴ Q_{i}. Hence, P_{U}(P) = λx_{1} … x_{n}.yP_{U}(P_{1}) … P_{U}(P_{m}) and P_{U}(Q) = λx_{1} … x_{n}.yP_{U}(Q_{1}) … P_{U}(Q_{m}). By definition of S, (P_{U}(P_{i}), P_{U}(Q_{i})) ∈ S.

2. P = O. Then P_{U}(P) = O.

3. P = λx_{1} … x_{n}.RP_{1} … P_{m}. Then, Q = λx_{1} … x_{n}.Q_{0}Q_{1} … Q_{m}, also R ⊴ Q_{0} and P_{i} ⊴ Q_{i} for 1 ≤ i ≤ m. By Lemma 41, if R is rootactive so is Q_{0}. Hence, P_{U}(P) = λx_{1} … x_{n}.⊥P_{U}(P_{1}) … P_{U}(P_{m}) and P_{U}(Q) = λx_{1} … x_{n}.⊥P_{U}(Q_{1}) … P_{U}(Q_{m}). By definition of S, we have that (P_{U}(P_{i}), P_{U}(Q_{i})) ∈ S.

4. P = λx_{1} … x_{n}.⊥P_{1} … P_{m}. Similar to the previous case.

5. P = λx_{1} … x_{n}.((…)P_{2})P_{1}. Then Q = λx_{1} … x_{n}.((…)Q_{2})Q_{1}. We have two cases:

(a) If P_{U}(P) = λx_{1} … x_{n}.⊥ then P_{U}(Q) = λx_{1} … x_{n}.⊥ by Theorem 20 and the fact that U is quasi-regular.

(b) P_{U}(P) = λx_{1} … x_{n}.((…)P_{U}(P_{2}))P_{U}(P_{1}). By Theorem 20 and since U is quasi-regular, we have that P_{U}(Q) = λx_{1} … x_{n}.((…)P_{U}(Q_{2}))P_{U}(Q_{1}). By definition of S, (P_{U}(P_{i}), P_{U}(Q_{i})) ∈ S. ⊓ ⊔

The next corollary is deduced from Corollary 21 and the previous theorem.

Corollary 43. BerT, P_{SA}, LLT, P_{HA} and P_{\overline{HN} −O} are monotone in (Λ_{⊥}^{∞}, ⊴).

Theorem 44. If NF : Λ_{⊥}^{∞} → Λ_{⊥}^{∞} is monotone in (Λ_{⊥}^{∞}, ⊴) then ⊴ makes the context operators of M(NF) monotone.

Proof. If M ⊴ N then C[M] ⊴ C[N]. Since P_{U} is monotone, we have that P_{U}(C[M]) ⊴ P_{U}(C[N]). ⊓ ⊔

Corollary 45. ⊴ makes the context operators monotone of the models induced by BerT, P_{SA}, LLT, P_{HA} and P_{\overline{HN} −O}.

Corollary 46. The model induced by BerT is orderable.

The order ⊴ does not make the context operators of the models induced by P_{SA_{X}} monotone if X ≠ ∅ and X ≠ Λ^{∞}. For instance, if X = {I} then ⊥O ⋬ ⊥ =_{P_{SA_{X}}} ⊥I.

11 Unorderable models

In this section we construct 2^{c} unorderable models induced by the infinitary lambda calculus where c is the cardinality of the continuum. We consider the set B^{0} of closed terms in BT(Λ_{⊥}^{∞}) without ⊥ which has the cardinality c of the continuum. For each subset X of B^{0}, we construct an infinitary lambda calculus as follows. By Theorem 18, SA_{(X∪O)} is a set of meaningless terms and P_{SA_{(X∪O)}} is a parametric tree which we abbreviate as U_{X}.

Theorem 47. Let X ⊆ B^{0} be non-empty. The models induced by the parametric trees U_{X} are unorderable.

Proof. Suppose there exists a partial order ⊑ that makes the context operators of M(U_{X}) monotone. By Theorem 38, we have that O is the least element of ⊑. Since X is non-empty, there exists M ∈ X and M = λx_{1} … x_{n}.x_{i}M_{1} … M_{k}. Take N = λx_{1} … x_{n}.x_{i}O … O. On one hand, both head bottom forms ⊥O and ⊥M reduce to ⊥. On the other hand, the head bottom form ⊥N does not reduce to ⊥. We have that N ∉ X ∪O because the terms in X ⊆ B^{0} are Böhm trees that have a head normal form at any depth. Hence, ⊥O =_{U_{X}} ⊥ ⊑ ⊥N ⊑ ⊥ =_{U_{X}} ⊥M.

⊓ ⊔ Corollary 48. There are 2^{c} unorderable models induced by the infinitary lambda calculus where c is the cardinality of the continuum.

Acknowledgements. We thank Mariangiola Dezani-Ciancaglini and Alexander Kurz for helpful comments and discussions.

References

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

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

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

4. A. Berarducci and M. Dezani-Ciancaglini. Infinite λ-calculus and types. Theoretical Computer Science, 212(1-2):29–75, 1999. Gentzen (Rome, 1996).

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

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

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

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

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

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

11. J. W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical centre tracts. Mathematisch Centrum, 1980.

12. A. Salibra. Topological incompleteness and order incompleteness of the lambda calculus. ACM Transactions on Computational Logic, 4(3):379–401, 2003. (Special Issue LICS 2001).

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

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

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