Order-Incompleteness and Finite Lambda Reduction Models

Peter Selinger

The final version of this article has been published in Theoretical Computer Science 309 (2003) 43–63. It differs from the present version in that it has been copy-edited and reformatted.

Abstract

Many familiar models of the untyped lambda calculus are constructed by order theoretic methods. This paper provides some basic new facts about ordered models of the lambda calculus. We show that in any partially ordered model that is complete for the theory of β- or βη-conversion, the partial order is trivial on term denotations. Equivalently, the open and closed term algebras of the untyped lambda calculus cannot be non-trivially partially ordered. Our second result is a syntactical characterization, in terms of so-called generalized Mal’cev operators, of those lambda theories which cannot be induced by any non-trivially partially ordered model. We also consider a notion of finite models for the untyped lambda calculus, or more precisely, finite models of reduction. We demonstrate how such models can be used as practical tools for giving finitary proofs of term inequalities.

1 Introduction

Perhaps the most important contribution in the area of mathematical programming semantics was the discovery, by D. Scott in the late 1960’s, that models for the untyped lambda calculus could be obtained by a combination of ordertheoretic and topological methods. A long tradition of research in domain theory ensued, and Scott’s methods have been successfully applied to many aspects of programming semantics.

On the other hand, there are results that indicate that Scott’s methods may not in general be complete: Honsell and Ronchi Della Rocca [8] have shown that there exists a lambda theory that does not arise as the theory of a reflexive model in the cartesian-closed category of complete partial orders and Scott-continuous functions. Moreover, there are desirable properties of a model that are incompatible with the presence of a partial order: for instance, Plotkin [13], answering a question of H. Friedman, has recently shown that there exists an extensional lambda algebra A which is finitely separable. A finitely separable algebra can never be non-trivially partially ordered.

In this paper we establish some basic new facts about ordered models of the untyped lambda calculus. We show that the standard open and closed term algebras are unorderable, i.e., they cannot be non-trivially partially ordered as combinatory algebras. Recall that the standard term algebras are made up from lambda terms, taken up to β- or βη-equivalence. It follows that if a partially ordered model of the untyped lambda calculus is complete for one of the theories \underline{λβ} or \underline{λβη}, then the denotations of closed terms in that model are pairwise incomparable, i.e., the term denotations form an anti-chain.

We also consider the related question of order-incompleteness: does there exist a lambda theory (possibly with constants) which does not arise as the theory of a non-trivially ordered model? Equivalently, does there exist a lambda algebra which cannot be embedded in a non-trivially ordered model? Let us call such an algebra absolutely unorderable. Plotkin conjectures in [13] that an absolutely unorderable lambda algebra exists. Here, we give an algebraic characterization, in terms of so-called Mal’cev operators, of the absolutely unorderable T-algebras in any algebraic variety T. This reduces the question of order-incompleteness for the lambda calculus to the question whether one can consistently add a family of n Mal’cev operators to the lambda calculus. The answer is still unknown in the general case, but we prove that it is inconsistent for n ⩽ 2.

The characterization of absolutely unorderable T-algebras in terms of Mal’cev operators leads to an interesting technical observation about free order-algebras and dcpo-algebras. In a given variety of order-algebras, one may consider the free order-algebra 𝔉_{ord}(P) generated by a poset P. The question arises under what conditions 𝔉_{ord}(P) is conservative over P, i.e., under what conditions the canonical map P → 𝔉_{ord}(P) is order-reflecting. An analogous question can be asked for dcpo-algebras. Here, we give a necessary and sufficient condition: we show that the answer is completely determined by whether the given variety has a family of Mal’cev operators.

In the last part of this paper, we introduce a novel technique for proving inequalities of lambda terms. At the heart of this technique is the notion of a finite lambda reduction model. It is well-known that a model of an equational theory of the lambda calculus can never be finite or even recursive [2]. Instead, we consider models of reduction, which are not subject to the same limitations on size and complexity. A model of reduction is equipped with a partial order, and it satisfies a soundness property of the form M ⟶ N ⇒ [[M]] ⩽ [[N]], where ⟶ denotes e.g. β- or βηreduction [6, 10, 12]. One can understand such models as making precise certain invariants of terms under reduction. By combining this with the Church-Rosser property, one recovers a limited form of reasoning about convertibility. Our key observation is that models of reduction, unlike models of conversion, may be finite, and that even a finite such model can carry non-trivial information. We give a practical method for constructing such models, and we give two examples in which we use finite reduction models to demonstrate the inequality of some unsolvable lambda terms.

2 Unorderability

The main result of this section is that the open and closed term algebras of the untyped lambda calculus do not admit a non-trivial partial order compatible with the model structure. We follow Barendregt’s notation for the lambda calculus [2]. Let us begin by fixing some terminology. A preorder is said to be discrete if a ⩽ b implies a = b, indiscrete if a ⩽ b holds for all a, b, and symmetric if a ⩽ b ⇒ b ⩽ a. By a trivial preorder, we mean either the discrete or indiscrete preorder. A partial order is of course trivial iff it is discrete iff it is symmetric.

Recall that a combinatory algebra ⟨X, ·, k, s⟩ consists of a set X, a binary operation ·: X × X → X, and distinguished elements k, s ∈ X satisfying kxy = x and sxyz = xz(yz). As usual, we write ab for a · b and abc for (ab)c. We say that a preorder ⩽ on a combinatory algebra (X, ·, k, s) is compatible if application is monotone in both arguments, i.e., a ⩽ a′ and b ⩽ b′ implies a · b ⩽ a′ · b′.

A combinatory algebra is called unorderable if every compatible partial order on it is trivial. It is known that such algebras exist. For example, Plotkin [13] has recently constructed a finitely separable algebra, a property which implies unorderability. Here X is said to be finitely separable if for every finite subset A ⊆ X, every function f: A → X is the restriction of some f̂ ∈ X, meaning that for all a ∈ A, f(a) = f̂· a. Finitely separable combinatory algebras do not allow non-trivial preorders, because if a < b for some a, b ∈ X, then x ⩽ y for all x, y ∈ X via some f̂ ∈ X with f̂· a = x and f̂· b = y. The present result differs from this, because our unorderable algebras, the open and closed term algebras of the untyped lambda calculus, occur “naturally”.

2.1 Lambda terms cannot be ordered

Let Λ_{C} be the set of (α-equivalence classes of) untyped lambda terms, build from a set C of constant symbols and a countable supply of variables. Let Λ_{C}^{0} be the subset of closed terms.

Definition. The open term algebra of the λβ-calculus is the combinatory algebra ⟨Λ_{C}/=_{β}, ·, K, S⟩, where · is the application operation on terms, and K and S are the terms λxy.x and λxyz.xz(yz), respectively. The closed term algebra ⟨Λ_{C}^{0}/=_{β}, ·, K, S⟩ is defined analogously, and similarly for the λβη-calculus.

Note that these term algebras are not finitely separable: e.g. the terms ω = (λx.xx)(λx.xx) and I = λx.x cannot be separated, since the first one is unsolvable [2]. Also, the term algebras allow non-trivial preorders: for instance, two terms are ordered if and only if their meanings in the standard D_{∞}-model are ordered.

Suppose now that we want to construct a partial order on, say, the open term algebra of the λβ-calculus. An obvious approach is the following: take two distinct variables u and t, and let ⊑ be the preorder generated by a single inequation u ⊑ t. It is not hard to see that for this preorder, one has M ⊑ N iff N is obtained from M up to βequivalence by replacing some, but not necessarily all occurrences of the variable u by t. More precisely, M ⊑ N iff there is a term P (not itself containing u or t) such that M =_{β} P uut and N =_{β} P utt.

It follows that t ⋢ u, and thus this preorder is non-trivial. However, the following proposition implies that ⊑ is not a partial order.

Proposition 2.1. There exists a closed term A of the untyped lambda calculus, such that Auuut =_{β} Auttt, but Auuut ≠_{βη} Auutt, for variables u ≠ t.

Proof. The idea of the proof is as follows: Via a fixpoint combinator, define a term f such that fyx =_{β} fy(fy(fyx)) for variables x, y. In other words, any three applications of fy are equivalent to a single application. Now let Auvwt = λx.fu(fv(fw(ftx))). Then clearly Auuut =_{β} Auttt. It remains to be shown that Auuut ≠_{βη} Auutt. We delay the proof of this inequality until Section 4.4.2 below, where we prove it using the notion of finite lambda reduction models. □

Note that the proposition implies that ⊑ is not a partial order. Namely, one has Auuut ⊑ Auutt ⊑ Auttt = Auuut, but since Auuut ≠ Auutt, the preorder ⊑ is not antisymmetric.

By the same reasoning, u and t cannot be related in any compatible partial order on open terms. Thus any such partial order is discrete on variables. To show this section’s main result, we need to lift this reasoning from variables u, t to arbitrary terms U, T. This is achieved by the following lemma, which states that, if s is a fresh variable, then sU and sT behave essentially like indeterminates: any equation that holds for sU and sT will hold for variables u and t. Let T be one of the theories \underline{λβ} or \underline{λβη}, and let ^{T} ⟶ be the corresponding reduction relation.

Lemma 2.2. Let U_{1}, …, U_{n} be terms that are distinct in T , and let s be a variable not free in U_{1}, …, U_{n}. Then for all terms M, N with s ∉ FV(M, N), and for variables u_{1}, …, u_{n},

M(sU_{1})(sU_{2}) … (sU_{n}) =_{T} N(sU_{1})(sU_{2}) … (sU_{n}) implies Mu_{1}u_{2} … u_{n} =_{T} Nu_{1}u_{2} … u_{n}.

Proof. Let V = {s, u_{1}, …, u_{n}} ∪ FV(U_{1}, …, U_{n}). In the following, we assume without loss of generality that the names of all bound variables are different from elements of V. Let Λ′ be the set of all lambda terms with the following property: the variable s occurs only in subterms of the form sU, where U =_{T} U_{i} for some i. For each M ∈ Λ′, let M^{∗} be the lambda term obtained from M by replacing each subterm of the form sU by u_{i} if U =_{T} U_{i}. Formally x^{∗} = x, c^{∗} = c, (λx.M)^{∗} = λx.M^{∗}, (sU)^{∗} = u_{i} if U =_{T} U_{i}, and (MN)^{∗} = M^{∗}N^{∗} if M ≠ s. Then the following hold:

(a) For all M, N ∈ Λ′ and x ∉ V, M[N/x] ∈ Λ′ and (M[N/x])^{∗} = M^{∗}[N^{∗}/x].

(b) For all M ∈ Λ′, if M ^{T} ⟶N then N ∈ Λ′ and M^{∗} ^{T} ⟶^{∗}N^{∗}.

(c) For all M, N ∈ Λ′, if M =_{T} N then M^{∗} =_{T} N^{∗}.

(a) and (b) are easily proved by induction. (c) follows from (b) by the Church-Rosser property of ^{T} ⟶. Finally, the lemma follows by observing that M′ = M(sU_{1}) … (sU_{n}) and N′ = N(sU_{1}) … (sU_{n}) are in Λ′, and M′^{∗} = Mu_{1} … u_{n} and N′^{∗} = Nu_{1} … u_{n}. □

Theorem 2.3. Let M be the open or the closed term algebra of the λβ- or λβη-calculus. Then M does not allow a non-trivial compatible partial order.

Proof. Let ⩽ be a compatible partial order on M. Let U ≠ T ∈ M, and assume, by way of contradiction, that U ⩽ T. Let A be as in Proposition 2.1, and let s be a fresh variable. Then by compatibility,

λs.A(sU)(sU)(sU)(sT) ⩽ λs.A(sU)(sU)(sT)(sT)
⩽ λs.A(sU)(sT)(sT)(sT)
= λs.A(sU)(sU)(sU)(sT),

hence, by antisymmetry,

A(sU)(sU)(sU)(sT) =_{T} A(sU)(sU)(sT)(sT)

Applying Lemma 2.2 to M = λut.Auuut and N = λut.Auutt, one gets Auuut = Auutt for variables u and t, contradicting the choice of A. Consequently, the order is trivial. □

Corollary 2.4. In any partially ordered model of the untyped lambda calculus whose theory is \underline{λβ} or \underline{λβη}, the denotations of closed terms are pairwise incomparable. □

2.2 Lambda unorderability

We have called a preorder ⩽ on a combinatory algebra A compatible if it respects the application operation. In addition, one can require that ⩽ also respects abstraction. Abstraction is a well-defined operation if A is a lambda algebra [2, 14]. Thus, we define a lambda preorder on a lambda algebra A to be a compatible preorder such that

\frac{∀x ∈ A.ax ⩽ bx}{1a ⩽ 1b} .  (1)

Here, 1 = s(k(skk)). If λ^{∗} is the derived lambda abstractor of combinatory logic [2], then 1 = λ^{∗}xy.xy and the rule (1) is equivalent to requiring that for all combinatory terms A and B, if A ⊧ A ⩽ B then A ⊧ λ^{∗}x.A ⩽ λ^{∗}x.B.

One could conjecture that if a lambda algebra is orderable, then it is also lambda orderable. The following counterexample, due to Gordon Plotkin, shows in the strongest possible sense that this is not the case.

Theorem 2.5. (Plotkin) There exists an extensional, non-trivially partially ordered lambda algebra D which does not allow a non-trivial lambda preorder.

Proof. The idea of the construction is to work in a category where the order relation on function spaces is not pointwise. We use the category CPO^{∧} of meet cpo’s and stable functions. Recall that the objects of this category are cpo’s with bounded binary meets which act continuously, and that the morphisms are stable functions, i.e., continuous functions preserving the bounded meets [3]. The usual Scott D_{∞}-construction of models of the lambda-βη-calculus goes through in this category.

Let D_{0} be the cpo with two elements ⊥ ⩽ ⊤, and define D_{n+1} to be the stable function space D_{n}^{D_{n}}. Then D_{1} has three elements B, I, T, where B is the constant ⊥ function, T is the constant ⊤ function, and I is the identity. Notice that the stable order on D_{1} is as shown:

[figure: T; I; B]

Carry out the D_{∞}-construction starting from the initial embedding-projection pair given by e(⊥) = B, e(⊤) = T, and p(f) = f(⊥). Notice that e ∘ p ⩽ id in the stable order. The limit D satisfies D ≅ D^{D}, giving rise to an extensional lambda algebra structure on D in the standard way. Clearly the partial order ⩽ on D is non-trivial and compatible. We will show that D does not allow a non-trivial lambda preorder.

Let us identify each D_{n} with the corresponding subspace of D, and let p_{n}: D → D_{n} be the canonical projection. Notice that I and T are separable in D, since they can be mapped to any pair of elements by a stable function, and any stable function is definable in D.

Now suppose that ⊑ is any lambda-preorder on D. We will show that it is trivial, i.e., it is either discrete or indiscrete. First notice that, since D is an extensional model, 1a = a for all a ∈ D and hence we can strengthen (1) to ∀x ∈ D.ax ⊑ bx implies a ⊑ b. Moreover, if f ∈ D_{n+1}, then the application f · x depends only on p_{n}(x), and thus f ⊑ g ∈ D_{n+1} iff f · x ⊑ g · x for all x ∈ D_{n}.

Suppose that ⊑ is not discrete, i.e., there are distinct elements x, y ∈ D such that x ⊑ y. Then for some n the projections x_{n} = p_{n}(x) and y_{n} = p_{n}(y) are distinct, and x_{n} ⊑ y_{n} since p_{n} is realized by some p̂_{n} ∈ D. Now one can choose elements z_{n−1}, …, z_{0} in D_{n−1}, …, D_{0} such that a = x_{n}z_{n−1} … z_{0} and b = y_{n}z_{n−1} … z_{0} are distinct elements of D_{0}, and it follows that a ⊑ b ∈ D_{0}. Hence either ⊥ ⊑ ⊤ or ⊤ ⊑ ⊥ in D_{0}. Assume without loss of generality that ⊥ ⊑ ⊤. Then I · ⊤ = T · ⊤ and I · ⊥ ⊑ T · ⊥, hence by the remark of the preceding paragraph, I ⊑ T. But since I and T are separable in D, this forces ⊑ to be the indiscrete preorder. □

Let us emphasize that the proof not only shows that the “natural order” ⩽ is not a lambda preorder, but that there is not any non-trivial lambda preorder on D.

3 Absolute unorderability

In Section 2, we have investigated models of the lambda calculus which cannot be non-trivially ordered. Of course, the existence of unorderable models does not imply that order-theoretic methods are somehow incomplete for constructing models: an unorderable model can still arise from an order-theoretic construction, for instance as a subalgebra of some orderable model.

Indeed, it is not hard to see that the open and closed term algebras, as considered in the previous section, can be embedded in an orderable model: this follows e.g. from Theorem 3.4 below. A different (and, from a model-theoretic point of view, more interesting) construction of an ordered model in which the open term algebra is embedded can be found in Di Gianantonio et al. [5].

This leads us to the related question of absolute unorderability: a model is absolutely unorderable if it cannot be embedded in an orderable one. Plotkin conjectures in [13] that an absolutely unorderable combinatory algebra exists, but the question is still open whether this is so. In this section, we present what is known: we give a syntactic characterization of the absolutely unorderable algebras in any algebraic variety T in terms of the existence of a family of Mal’cev operators. Plotkin’s conjecture is thus reduced to the question whether Mal’cev operators are consistent with the lambda calculus.

The question of absolute unorderability can also be formulated in terms of theories, rather than models. In this form, we refer to it as the order-incompleteness question: does there exist a lambda theory (possibly with constants) which does not arise as the theory of an ordered model? This question is obviously equivalent to the question of the existence of an absolutely unorderable algebra.

A property that is related to order-incompleteness, but much weaker, is the well-known topological incompleteness. Addressing the latter, Honsell and Ronchi Della Rocca [8] have shown that there is a lambda theory which is not the theory of any reflexive CPO-model. However, their theory is not order-incomplete, and the methods used in investigating topological incompleteness are quite different from those used here. We should mention that the question whether \underline{λβ} or \underline{λβη} arises as the theory of a reflexive CPO-model is still open.

3.1 A characterization of absolutely unorderable algebras

Let T be an algebraic variety (given by a signature and equations). We say that a preorder ⩽ on a T-algebra A is compatible if a_{i} ⩽ b_{i} for i = 1 … k implies f(a_{1}, …, a_{k}) ⩽ f(b_{1}, …, b_{k}), for each k-ary function symbol f in the signature of T. Notice that compatible preorders are closed under arbitrary intersections. If ⩽ is compatible, then so is the dual preorder ⩾. Every compatible preorder determines a congruence ∼_{⩽} on A, which is the intersection of ⩽ and ⩾. Also notice that ⩽ naturally defines a partial order on A/∼_{⩽}.

A T-algebra A is said to be unorderable if it does not allow a non-trivial compatible partial order. Also, A is said to be absolutely unorderable if for any embedding A → B of T-algebras, B is unorderable.

Now consider a T-algebra A. As usual, A[x_{1}, …, x_{n}] denotes the T-algebra obtained from A by freely adjoining indeterminates x_{1}, …, x_{n}. We regard A as a subset of A[x_{1}, …, x_{n}]. Let ≼ be the smallest compatible preorder on A[u, t] such that u ≼ t.

Lemma 3.1. ≼ is discrete on A, i.e., a ≼ b ⇒ a = b for a, b ∈ A.

Proof. Let ∼ be the kernel of the canonical homomorphism A[u, t] → A[x] which sends both u and t to x. Then ≼ ⊆ ∼ and ∼ is discrete on A. □

Lemma 3.2. A is absolutely unorderable if and only if t ≼ u.

Proof. For the left-to-right implication, suppose A is absolutely unorderable. Consider the natural map A → A[u, t] → A[u, t]/∼_{≼}. Lemma 3.1 implies that the composition is an embedding, hence ≼ must be discrete as a partial order on A[u, t]/∼_{≼}. Equivalently, ≼ as a preorder on A[u, t] is symmetric, and thus t ≼ u. For the converse, suppose A is not absolutely unorderable. Then there is an embedding F: A → B of T-algebras where B has a non-trivial compatible partial order ⩽. Choose U ≠ T ∈ B such that U ⩽ T, and consider the unique map G: A[u, t] → B such that u ↦ U, t ↦ T and G|_{A} = F. Define a ⩽ b in A[u, t] iff G(a) ⩽ G(b) in B. Then ⩽ is a compatible preorder on A[u, t] with u ⩽ t, hence ≼ is contained in ⩽. But t ⩽̸ u, hence t ⋠ u. □

Further, ≼ has the following explicit description: On A[u, t], define a ⊲ b if and only if there is a polynomial A(x, y, z) ∈ A[x, y, z] such that A(t, u, u) = a and A(t, t, u) = b.

Lemma 3.3. ≼ is the transitive closure of ⊲.

Proof. Let ⊲^{∗} be the transitive closure. Clearly, ⊲^{∗} is a preorder contained in ≼, and it satisfies u ⊲^{∗} t. Moreover, ⊲, and thus ⊲^{∗}, is compatible, as can be seen by considering terms of the form A(x, y, z) = f(A_{1}(x, y, z) … A_{k}(x, y, z)) for each k-ary function symbol f. Since ≼ is smallest with these properties, it follows that ≼ = ⊲^{∗}. □

Putting together Lemmas 3.2 and 3.3, we get the following characterization of absolutely unorderable algebras. We say that an equation p(u, t) = q(u, t) holds absolutely in A if it holds in A[u, t].

Theorem 3.4. Characterization of absolutely unorderable T-algebras. Let T be an algebraic variety. A Talgebra A is absolutely unorderable if and only if, for some n ⩾ 1, there exist polynomials M_{i}(x, y, z) ∈ A[x, y, z], for i = 1 … n, such that the following equations hold absolutely in A:

t = M_{1}(t, u, u)
M_{1}(t, t, u) = M_{2}(t, u, u)
M_{2}(t, t, u) = M_{3}(t, u, u)  (2)
⋮
M_{n}(t, t, u) = u

Proof. By Lemmas 3.2 and 3.3, A is absolutely unorderable if and only if there are t_{1}, …, t_{n−1} ∈ A[u, t] such that t ⊲ t_{1} ⊲ … ⊲ t_{n−1} ⊲ u. The theorem follows by definition of ⊲. □

In the case n = 1, the equations (2) have the simple form t = M(t, u, u) and M(t, t, u) = u. A ternary operator M satisfying these equations is called a Mal’cev operator, after A.I. Mal’cev, who studied such operators to characterize varieties of congruence-permutable algebras [11]. Accordingly, we call M_{1}, …, M_{n} satisfying (2) a family of generalized Mal’cev operators, and we call the equations (2) the generalized Mal’cev axioms. Hagemann and Mitschke [7] have shown that an algebraic variety has n-permutable congruences if and only if it has a family of generalized Mal’cev operators. It was proved by W. Taylor [15, 4] that algebras in a variety with n-permutable congruences are unorderable; however, the converse is a new result. Also note that Theorem 3.4 characterizes individual algebras that are absolutely unorderable, rather than varieties of unorderable algebras.

3.2 An application to order-algebras and dcpo-algebras

A compatibly partially ordered algebra over a given signature Σ is called an Σ-order-algebra. Moreover, it is called a Σ-dcpo-algebra if the order is directed complete and the algebra operations are continuous. Let I be a set of inequations s ⩽ t between terms in the language of Σ. A Σ-order-algebra satisfying these inequations is called a ΣI-order-algebra, and similarly for dcpo-algebras. For more details, see [1] or [14].

Fix Σ and I. For any poset P, there exists a free ΣI-order-algebra 𝔉_{ord}(P), with a canonical monotone map ȷ: P → 𝔉_{ord}(P). Similarly, for any dcpo D, there exists a free ΣI-dcpo-algebra 𝔉_{dcpo}(D) with a canonical continuous map ȷ: D → 𝔉_{dcpo}(D) [1].

One may ask under which circumstances the canonical map ȷ is order-reflecting, i.e., under what conditions the free order- or dcpo-algebra conservatively extends the order on the generators. The following theorem shows that the answer depends only on the presence of generalized Mal’cev operators in ΣI. Recall that a k-ary operation in Σ is simply a term t(x_{1}, …, x_{k}) in the signature Σ.

Theorem 3.5. Let Σ be a signature and I a set of inequations. Let D be a non-trivially ordered dcpo, and let P be a non-trivially ordered poset. The following are equivalent:

1. The canonical map ȷ: D → 𝔉_{dcpo}(D) from D into the free ΣI-dcpo-algebra is not order-reflecting.

2. Every ΣI-dcpo-algebra is trivially ordered.

3. The canonical map ȷ: P → 𝔉_{dcpo}(P) from P into the free ΣI-order-algebra is not order-reflecting.

4. Every ΣI-order-algebra is trivially ordered.

5. There are ternary operations M_{1}, …, M_{n} in Σ such that I entails

t ⩽ M_{1}(t, u, u)
M_{1}(t, t, u) ⩽ M_{2}(t, u, u)
M_{2}(t, t, u) ⩽ M_{3}(t, u, u)  (3)
⋮
M_{n}(t, t, u) ⩽ u

Proof. 1. ⇒ 2.: Suppose B is a non-trivially ordered ΣI-dcpo-algebra with elements a < b. We show that ȷ is order-reflecting. Let x, y ∈ D with ȷ(x) ⩽ ȷ(y). Define g: D → B by

g(z) = \{ \begin{matrix}a & if z ⩽ y \\ b & if z ⩽̸ y \end{matrix}

Then g is continuous; therefore, by the universal property of 𝔉_{dcpo}(D), there exists a unique continuous homomorphism h: 𝔉_{dcpo}(D) → B such that g = h ∘ ȷ. By monotonicity of h, we get g(x) = h(ȷ(x)) ⩽ h(ȷ(y)) = g(y) = a, hence x ⩽ y.

2. ⇒ 1.: A map ȷ: D → 𝔉_{dcpo}(D) from a non-trivially ordered set into a trivially ordered one cannot be orderreflecting.

3. ⇔ 4.: Same as 1. ⇔ 2., replacing the word “continuous” by “monotone”.

2. ⇒ 4.: Suppose there is a non-trivially ordered ΣI-order-algebra ⟨A, ⩽⟩. We consider the ideal completion of A: A subset I ⊆ A is an ideal if it is downward closed and directed. Let Idl(A) be the ideal completion of A, i.e., the set of all ideals, ordered by inclusion. Abramsky and Jung [1] prove that Idl(A) is a ΣI-dcpo-algebra. Moreover, the map A → Idl(A): x ↦ ↓x is order preserving and reflecting, and hence Idl(A) is non-trivially ordered.

4. ⇒ 5.: Let V be a countable set of variables, and let 𝔉_{ord}(V) be the free ΣI-order-algebra over discrete V. If every ΣI-order-algebra is trivially ordered, then so is 𝔉_{ord}(V), which implies that I ⊢_{ineq} s ⩽ t iff I ⊢_{ineq} t ⩽ s. We can therefore regard I as a set of equations. The claim follows by applying Theorem 3.4 to A = 𝔉_{ord}(∅).

5. ⇒ 2.: Suppose ΣI has operators satisfying (3). Then for any ΣI-dcpo-algebra B, if a ⩽ b ∈ B, then b ⩽ M_{1}(b, a, a) ⩽ M_{1}(b, b, a)⩽ … ⩽ M_{n}(b, b, a) ⩽ a, hence B is trivially ordered. □

Remark. Notice that the implication 5. ⇒ 4.shows that the inequalities (3) already imply the corresponding equalities (2).

3.3 Absolute unorderability and the lambda calculus

In the lambda calculus, a term M_{i}(x, y, z) can be expressed in curried form as M_{i}xyz. Plotkin posed the question whether an absolutely unorderable lambda algebra exists [13]. Clearly, this is the case if and only if, for some n, the equations (2) are consistent with the lambda calculus. Unfortunately, it is not known whether this is true except in the cases n = 1 and n = 2. In these cases, (2) is inconsistent with the lambda calculus, as we will now show. Notice that if the axioms are consistent for some n, then also for all m ⩾ n, by letting M_{n+1}, …, M_{m} = λxyz.z

Let Y be any fixpoint operator of combinatory logic, for instance the paradoxical fixpoint combinator Y = λF.(λz.F (zz))(λz.F (zz)). We write μx.M for Y (λx.M). The operator μ satisfies the fixpoint property:

μx.A(x) = A(μx.A(x)). (fix)

The diagonal axiom is

μx.A(x, x) = μy.μz.A(y, z). (Δ)

Lemma 3.6 (Plotkin, Simpson). Assuming the diagonal axiom, the generalized Mal’cev axioms (2) are inconsistent with the lambda calculus for all n.

Proof. Let x be arbitrary. Then

x = μz.x
= μz.M_{1}xzz  by (2)
= μy.μz.M_{1}xyz by (Δ)
= μz.M_{1}xxz  by (fix)
= μz.M_{2}xzz  by (2)
= …
= μz.M_{n−1}xxz
= μz.z  by (2).

Hence x = μz.z for all x, which is an inconsistency. □

Theorem 3.7 (Plotkin, Simpson). For n = 1, the Mal’cev axioms are inconsistent with the lambda calculus.

Proof. Suppose M is a Mal’cev operator. Let x be arbitrary and let A = μy.μz.Mxyz. Then

A =^{(fix)} μz.MxAz =^{(fix)} MxAA =^{(2)} x,

hence x = μz.MxAz = μz.Mxxz = μz.z. □

Theorem 3.8 (Plotkin, Selinger). For n = 2, the generalized Mal’cev axioms are inconsistent with the lambda calculus.

Proof. Suppose M_{1} and M_{2} are operators satisfying the generalized Mal’cev axioms (2). Define A and B by mutual recursion such that

\begin{aligned}A & = & μx.f(M_{1}xAB)(M_{1}xAB) \\ B & = & μy.μz.f(M_{2}ABy)(M_{2}ABz). \end{aligned}

Then

B = f(M_{2}ABB)(M_{2}ABB) by (fix)
= f(M_{1}AAB)(M_{1}AAB) by (2)
= A  by (fix).

So μx.fxx = μx.f(M_{1}xAA)(M_{1}xAA) = A = B = μy.μz.f(M_{2}AAy)(M_{2}AAz) = μy.μz.fyz, which is the diagonal axiom. By Lemma 3.6, this leads to an inconsistency. □

4 Finite Lambda Reduction Models

It is well-known that a model of the untyped lambda calculus, in the traditional equational sense, can never be finite or even recursive [2]. Consequently, model constructions of the lambda calculus typically involve passing to an infinite limit, yielding unwieldy models in which term denotations or equality of terms are not effectively computable.

By contrast, if one considers models of reduction, rather than of conversion, there is no such limitation on size or complexity. As we will see, it is quite possible for a model of reduction to be finite and yet interesting. Informally, by a model of conversion, we mean a model with a soundness property of the form

M ≅ N ⇒ [[M]] = [[N]],

where ≅ is e.g. β- or βη-convertibility, and [[ ]] is the semantic interpretation function. On the other hand, a model of reduction has an underlying partial order and a soundness property of the form

M ⟶ N ⇒ [[M]] ⩽ [[N]],

where ⟶ is e.g. β- or βη-reduction. Models of reduction have been considered by different authors [6, 10, 12]. We will focus here on a formulation which was given by Plotkin [12] in the spirit of the familiar syntactical lambda models [2].

4.1 Syntactical models of reduction

As before, let V be the set of variables of the lambda calculus, and let Λ be the set of untyped lambda terms up to α-equivalence. To keep the notation simple, we do not consider constant symbols in this section, although they could be easily added. For a partially ordered set P, let P^{V} be the set of all valuations, i.e., functions from V to P.

Definition. (Plotkin [12]) A syntactical model of β-reduction ⟨P, ·, [[ ]]⟩ consists of a poset P, a monotone binary operation ·: P × P → P, and an interpretation function

[[ · ]]_{·}: Λ × P^{V} → P

such that the following properties are satisfied:

1. [[x]]_{ρ} = ρ(x)

2. [[MN]]_{ρ} = [[M]]_{ρ} · [[N]]_{ρ}

3. [[λx.M]]_{ρ} · a ⩽ [[M]]_{ρ(x:=a)}, for all a ∈ P

4. ρ|_{FV(M)} = ρ′|_{FV(M)} ⇒ [[M]]_{ρ} = [[M]]_{ρ′}

5. (∀a.[[M]]_{ρ(x:=a)} ⩽ [[N]]_{ρ(x:=a)}) ⇒ [[λx.M]]_{ρ} ⩽ [[λx.N]]_{ρ}

Moreover, we say ⟨P, ·, [[ ]]⟩ is a syntactical model of βη-reduction, if it also satisfies the property

6. [[λx.Mx]]_{ρ} ⩽ [[M]]_{ρ}, if x ∉ FV(M).

The usual syntactical lambda models (of conversion) [2] arise as the special case where P is discretely ordered.

Note that properties 1.–3. do not form an inductive definition of the function [[ ]]. In general, [[ ]] is not uniquely determined by ⟨P, ·⟩.

Notice that the partial order on a model of reduction differs from the partial order on a model of conversion, as considered in the first part of this paper. The order on an ordered model of conversion is commonly understood as an information order, where a ⩽ b means that a is “less defined” than b. On the other hand, models of reduction have a reduction order, where a ⩽ b means a reduces to b. One has the following soundness properties:

Proposition 4.1 (Plotkin [12]). The following are properties of syntactical models of β-reduction:

1. Monotonicity. If ρ(x) ⩽ ρ′(x) for all x, then [[M]]_{ρ} ⩽ [[M]]_{ρ′}.

2. Substitution. [[M[N/x]]]_{ρ} = [[M]]_{ρ(x:=[[N]]_{ρ})}.

3. Soundness for reduction. If M ^{β} ⟶N, then [[M]]_{ρ} ⩽ [[N]]_{ρ}. In a syntactical model of βη-reduction: If M ^{βη} ⟶N, then [[M]]_{ρ} ⩽ [[N]]_{ρ}. □

The soundness property for reduction does not in general yield useful information about convertibility, since interconvertible terms M ≅ N may have different denotations. However, if the reduction relation satisfies the Church-Rosser property, as is the case for β- and βη-reduction, then M ≅ N implies that M ⟶ Q and N ⟶ Q for some term Q. Thus, in a model of β- or βη-reduction, we get the following, restricted form of soundness for convertibility. Recall that two elements a and b in a poset are called compatible, in symbols a ⌣ ⌢ b, if there exists c with a ⩽ c and b ⩽ c.

M ≅ N ⇒ [[M]]_{ρ} ⌣ ⌢ [[N]]_{ρ}.  (4)

This property can be useful for reasoning about non-equality of terms, particularly if the underlying poset P has many pairs of incompatible elements. For this reason, we will be especially interested in the cases where P is a flat partial order, or a tree, or more generally, a bounded complete domain. Recall that a bounded complete domain is a non-empty poset in which all bounded subsets and all directed subsets have a least upper bound. Note that any bounded complete domain has a least element.

4.2 Constructing models of β-reduction

Syntactical models of β-reduction are constructed much more easily than models of conversion. To start with a trivial example, take any pointed poset P and monotone function ·: P × P → P, and define, somewhat uningeniously, [[λx.M]]_{ρ} = ⊥. Among the possible interpretation functions for given P and ·, this choice is the minimal one.

Much more interesting is the situation in which there exists a maximal choice for [[ ]]. Note that, in light of the soundness property for convertibility (4), it is desirable for [[ ]] to be as large as possible, so as to discriminate more terms. We will now explore a sufficient condition for a maximal [[ ]] to exist, in the case where P is a bounded complete domain.

Definition. A monotone function ·: P × P → P is compatible-extensional if for all a, b ∈ P,

\frac{∀x ∈ P. a · x ⌣ ⌢ b · x}{a ⌣ ⌢ b} .

The following proposition yields a practical method for constructing models of reduction. Notice that the method applies in particular to the cases where P is a flat poset or a finite tree. In these cases, the requirement that · preserves bounded suprema in its left argument reduces to the requirement that · is left strict.

Proposition 4.2. Let P be a bounded complete domain, and let ·: P × P → P be a compatible-extensional binary operation, preserving bounded suprema in its left argument. Then there exists a maximal interpretation function [[ ]] among all possible interpretation functions making ⟨P, ·, [[ ]]⟩ into a syntactic model of β-reduction. Moreover, [[ ]] can be defined inductively as follows:

1. [[x]]_{ρ} = ρ(x)

2. [[MN]]_{ρ} = [[M]]_{ρ} · [[N]]_{ρ}

3. [[λx.M]]_{ρ} is the maximal b ∈ P such that b · a ⩽ [[M]]_{ρ(x:=a)} for all a ∈ P.

Proof. It suffices to show that a maximal b always exists in clause 3, because the claim then follows easily. So consider the set B of all c ∈ P such that c · a ⩽ [[M]]_{ρ(x:=a)} for all a ∈ P. Note that B is closed under existing suprema, because · preserves them in its left argument. Moreover, the set B is directed: if c, c′ ∈ B, then c · a ⌣ ⌢ c′ · a for all a, and thus c ⌣ ⌢ c′ by compatible-extensionality, hence c ∨ c′ exists in B. It follows that B has a least upper bound b, which is the desired maximum. □

A categorical version of this proposition, in terms of adjoints, is given in Section 4.6. The following lemma is useful for calculating the denotation of multiple lambda abstractions:

Lemma 4.3. If [[ ]] is defined as in Proposition 4.2, then for all n ⩾ 1, the denotation of an n-fold lambda abstraction [[λx_{1} … x_{n}.M]]_{ρ} is the maximal b ∈ P such that for all a_{1} … a_{n} ∈ X, b · a_{1} ⋯ a_{n} ⩽ [[M]]_{ρ(x_{1}:=a_{1})...(x_{n}:=a_{n})}.

Proof. By induction on n. □

4.3 Order-extensionality and models of βη-reduction

An extensional model of β-conversion is always a model of βη-conversion. A similar property holds for models of reduction: A monotone function ·: P × P → P is called order-extensional if

\frac{∀x ∈ P. a · x ⩽ b · x}{a ⩽ b} .

The construction in Proposition 4.2 yields a model of βη-reduction if · is order-extensional. More generally:

Lemma 4.4. If ⟨P, ·, [[ ]]⟩ is a syntactical model of β-reduction and · is order-extensional, then ⟨P, ·, [[ ]]⟩ is a model of βη-reduction.

Table 1: Multiplication table for a flat model

\begin{matrix}· & 1 & 2 & 3 & ⋯ & p − 1 & p \\ 1 & 2 & 3 & 4 & ⋯ & p & 1 \\ 2 & 3 & 3 & 4 & ⋯ & p & 1 \\ 3 & 4 & 3 & 4 & ⋯ & p & 1 \\ ⋮ & ⋮ & ⋮ & ⋮ & ... & ⋮ & ⋮ \\ p − 1 & p & 3 & 4 & ⋯ & p & 1 \\ p & 1 & 3 & 4 & ⋯ & p & 1 \end{matrix}

Proof. Suppose x ∉ FV(M). Then for all a ∈ P, [[λx.Mx]]_{ρ} · a ⩽ [[Mx]]_{ρ(x:=a)} = [[M]]_{ρ} · a, hence [[λx.Mx]]_{ρ} ⩽ [[M]]_{ρ}. □

We note that in the special case where P is a tree, order-extensionality is a consequence of compatible-extensionality and extensionality:

Lemma 4.5. If P is a tree, and if · is compatible-extensional and extensional, then it is also order-extensional.

Proof. Suppose for all x, a · x ⩽ b · x, hence a · x ⌣ ⌢ b · x, hence a ⌣ ⌢ b by compatible-extensionality. Since P is a tree, either a ⩽ b or a ⩾ b. In the first case, we are done; in the second case, a · x ⩾ b · x, and hence a · x = b · x, for all x, which implies a = b by extensionality. □

4.4 Examples: two flat models

In the following examples, we consider models where the underlying poset is flat, i.e., P = X_{⊥} for a discrete set X, and where the application operation · is strict in both arguments. We call these models flat models, and remark that the application operation on such a model is equivalently given by a partial function ·: X × X ⇀ X. If X is finite, the function · can be given by a “multiplication table”, and it is easy to read properties such as compatible-extensionality from the defining table. For instance, · is compatible-extensional if no two rows of the table are compatible, and it is order-extensional if no row is subsumed by another. In particular, if the table is everywhere defined, then both compatible-extensionality and order-extensionality coincide with (ordinary) extensionality.

4.4.1 A class of finite models to distinguish the terms Ω_{n}

Let x be a variable and define x^{1} = x and x^{n} = x^{n−1}x for n ⩾ 2. Let ω_{n} = λx.x^{n} and Ω_{n} = ω_{n}ω_{n}. None of these terms, for n ⩾ 2, have a normal form, e.g. Ω_{2} = (λx.xx)(λx.xx) reduces only to itself. The terms Ω_{n} are unsolvable; therefore, their interpretations coincide with ⊥ in the D_{∞}-model [9, 16]. We will now give a class of finite flat models that distinguishes them.

Fix an integer p ⩾ 1 and let X = {1, 2, …, p}, regarded as integers modulo p with addition and subtraction. Define ·: X × X → X by

n · m = \{ \begin{matrix}n + 1 & if m = 1 \\ m + 1 & if m ≠ 1. \end{matrix}

A “multiplication table” for this operation is shown in Table 1. Clearly, the application operation defined in this way is compatible-extensional and order-extensional. Define [[ ]] as in Proposition 4.2 to get a model of βη-reduction. For n ⩾ 2, we calculate 1^{n} = n and m^{n} = m + 1 for m ≠ 1. Hence, for all x ∈ X and n ⩾ 2,

x^{n} = (n − 1) · x
⇒  [[ω_{n}]] = [[λx.x^{n}]] = n − 1
⇒  [[Ω_{n}]] = [[ω_{n}ω_{n}]] = (n − 1) · (n − 1) = n.

Table 2: Values for ψ(c, b, a) and k · c · b · a
c  b a ψ(c, b, a) k · c · b · a
k or 0 or 1 k k  0  0
k 0  0  0
k 1  1  1
0 k  0  0
0 0  0  0
0 1  1  1
1 k  0  0
1 0  1  1
1 1  0  0

Hence, [[Ω_{n}]] ≠ ⊥ for n ⩾ 2, and we have [[Ω_{n}]] = [[Ω_{m}]] iff n = m (mod p). Thus, each pair of terms Ω_{n}, Ω_{m} is distinguished in one of these models.

Note that the syntactic invariant picked out by these models can also be formulated syntactically, approximately as follows: in a term of the form ω_{n}ω_{n}...ω_{n}, pick out the last subterm, and determine the power of x in it. In general, the invariants picked out by a finite model can be much more complex.

4.4.2 Proof of Proposition 2.1: A non-trivial 3-element model

In this section, we will apply a finite model of reduction to finish the proof of Proposition 2.1. Recall that we are showing that there exists a closed term A of the untyped lambda calculus, such that Auuut =_{β} Auttt, but Auuut ≠_{βη} Auutt, for variables u ≠ t. As outlined before, the idea is to let Auvwt = λx.fu(fv(fw(ftx))), where f is a term such that fyx =_{β} fy(fy(fyx)). Such an f can be easily constructed via a fixpoint combinator. We define f via the paradoxical fixpoint combinator, which leads to the following concrete term for f:

f = hh, where h = λzyx.zzy(zzy(zzyx)).

Clearly Auuut =_{β} Auttt. To see that Auuut ≠_{βη} Auutt for variables u and t, we will construct a 3-element flat model. Let X = {k, 0, 1}, and let · be defined by the following “multiplication table”:

\begin{matrix}· & k & 0 & 1 \\ k & 0 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 1 & 0 & 1 & 0 \end{matrix}

Then · is compatible-extensional. Define [[ ]] inductively as in Proposition 4.2. Now consider the function ψ(c, b, a) := [[zzy(zzy(zzyx))]]_{ρ(z:=c)(y:=b)(x:=a)} = ccb(ccb(ccba)). Table 2 shows the values of this function, and one observes that ψ(c, b, a) = k · c · b · a for all c, b, a ∈ X. Hence by Proposition 4.2, [[h]] = [[λzyx.zzy(zzy(zzyx))]] is defined and equal to k, and consequently [[f]] = [[hh]] = kk = 0. If ρ(u) = ρ(x) = 0 and ρ(t) = 1, then

[[fu(fu(fu(ftx)))]]_{ρ} = 1
[[fu(fu(ft(ftx)))]]_{ρ} = 0.

By soundness for convertibility (4), it follows that fu(fu(fu(ftx))) ≠_{βη} fu(fu(ft(ftx))). Thus Auuut ≠_{βη} Auutt, which finishes the proof of Proposition 2.1.

4.5 Completeness

Given a syntactical model of β- or βη-reduction ⟨P, ·, [[ ]]⟩, one can define its lift ⟨P_{⊥}, ·′, [[ ]]′⟩ as follows by extending · strictly, and by defining [[M]]′_{ρ} = [[M]]_{ρ} if ρ(x) ≠ ⊥ for all x ∈ FV(M), and [[M]]′_{ρ} = ⊥ otherwise. It is easily checked that this is again a model of β-, respectively, βη-reduction. As a trivial consequence, one has the following completeness theorem for convertibility in models of reduction:

Proposition 4.6. Completeness: If M ≠_{β} N, then there exists a flat reduction model and ρ for which [[M]]_{ρ} ⌣̸ ⌢ [[N]]_{ρ}. If M ≠_{βη} N, then the model can be chosen to be compatible-extensional.

Proof. Take a model of conversion such that [[M]]_{ρ} ≠ [[N]]_{ρ} for some ρ, e.g. a term model. Then its lift is a flat model with [[M]]′_{ρ} ⌣̸ ⌢ [[N]]′_{ρ}. □

Of course this completeness property is not very interesting. A much more interesting question is how close one can come to a finite completeness theorem for models of reduction. Can every inequality M ≠_{β} N be demonstrated in a finite model of reduction? The answer to this question is no, since such a finite completeness theorem would yield a decision procedure for convertibility of lambda terms, which is known to be an undecidable problem. However, it would be interesting to identify subclasses of terms for which a finite completeness property holds, or to describe the class of equations that hold in all finite models of reduction, in all flat models, etc.

4.6 Categorical models of reduction

In this section, we investigate the relationship between syntactic and categorical models of reduction. By an orderenriched cartesian-closed category, we mean a cartesian-closed category (ccc) where each hom-set (A, B) is equipped with a partial order, such that composition is monotone, and such that the natural isomorphisms (A, B) × (A, C) ≅ (A, B × C) and (A × B, C) ≅ (A, C^{B}) are order-isomorphisms.

Definition. A categorical model of β-reduction ⟨D, e, p⟩ is given by an object D in an order-enriched ccc, together with a pair of morphisms e: D → D^{D} and p: D^{D} → D, such that e ∘ p ⩽ id_{D^{D}}, in diagrams:

\xymatrix{D^{D} \ar[d]_{p} \ar[dr]^{id}_{⩽} \\ D \ar[r]_{e} & D^{D}.}

If moreover p ∘ e ⩽ id_{D}, then ⟨D, e, p⟩ is a categorical model of βη-reduction.

Categorical models of reduction have been studied by various authors, e.g. by Girard [6] for the case of qualitative domains, or by Jacobs et al. [10], where they are called models of expansion. For a detailed discussion of these and other references, see Plotkin [12]. One can interpret each lambda term M with free variables in x_{1}, …, x_{n} as a morphism [[M]]_{x_{1},...,x_{n}}: D^{n} → D in the standard way by induction on M. Here e is used in the interpretation of application, and p in the interpretation of abstraction. One gets the following soundness property:

Proposition 4.7. Soundness for reduction. In a categorical model of β-reduction, if M ^{β} ⟶N, then [[M]]x̄ ⩽ [[N]]x̄. In a categorical model of βη-reduction, if M ^{βη} ⟶N, then [[M]]x̄ ⩽ [[N]]x̄. □

We say that an object D in an order-enriched ccc is order-well-pointed if for all f, g: D → E, whenever f ∘ x ⩽ g ∘ x for all x: 1 → D, then f ⩽ g. Notice that this implies that D is well-pointed. But in addition, it implies that the hom-set (D, E) is ordered pointwise, which is not a consequence of well-pointedness, as can be seen in any ccc of stable functions [3].

Proposition 4.8. Suppose ⟨D, e, p⟩ is a categorical model of β-reduction and D is order-well-pointed. Then a syntactical model of β-reduction ⟨P, ·, [[ ]]⟩ is obtained by setting P = |D| = (1, D), a · b = e(a)(b), and by defining [[ ]] inductively:

\begin{aligned}[[x]]_{ρ} & = & ρ(x), \\ [[MN]]_{ρ} & = & e([[M]]_{ρ})([[N]]_{ρ}), \\ [[λx.M]]_{ρ} & = & p(λa.[[M]]_{ρ(x:=a)}). \end{aligned}

Moreover, if p ∘ e ⩽ id_{D}, then ⟨P, ·, [[ ]]⟩ is a syntactical model of βη-reduction.

Proof. The only interesting part is to show that λa.[[M]]_{ρ(x:=a)}, an abuse of notation, denotes a well-defined morphism. This is best seen by observing that for any M,

[[M]]_{ρ} = 1 ⟶^{⟨ρ(x_{1}),...,ρ(x_{n})⟩} D^{n} ⟶^{[[M]]_{x_{1},...,xn}} D.

□

In Section 4.2, we considered the situation where [[ ]] can be chosen maximally with respect to given ⟨P, ·⟩. In the categorical setting, this corresponds to the situation where p is right adjoint to e. The following is the analogue of Proposition 4.2 in categorical language:

Proposition 4.9. In the category of posets, let P be a bounded complete domain, and let e: P → P^{P} preserve bounded suprema. Define a · b = e(a)(b). Then e has a right adjoint in the category of posets if and only if · is compatible-extensional. □

Proof. For one direction, suppose e has a right adjoint p: P^{P} → P. Suppose a, b ∈ P such that a · x ⌣ ⌢ b · x for all x ∈ P. Define f(x) = (a · x) ∨ (b · x) for every x ∈ P. The function f: P → P is monotone, and e(a), e(b) ⩽ f, hence a, b ⩽ p(f), and thus a ⌣ ⌢ b. Therefore, · is compatible-extensional. Conversely, suppose · is compatibleextensional. For any f ∈ P^{P}, consider the set P_{f} = {x ∈ P | e(x) ⩽ f}. Since e is strict, P_{f} is non-empty. Consider any a, b ∈ P_{f}. Because e(a) ⌣ ⌢ e(b), we have a · x ⌣ ⌢ b · x for all x, hence a ⌣ ⌢ b by strong extensionality. Let c = a ∨ b. Because e preserves existing suprema, c ∈ P_{f}. Hence, P_{f} is directed, and we can define p(f) = [figure]P_{f}. Clearly, the function p thus defined is monotone, and x ⩽ p(f) iff x ∈ P_{f} iff e(x) ⩽ f. Therefore e ⊣ p. □

Note that the right adjoint p: P^{P} → P need not in general be continuous. For this reason, the proposition refers to the category of posets, and not to the category of bounded complete domains.

4.7 Models of reduction and D_{∞}-models

Consider a categorical model of reduction ⟨D, e, p⟩ in the category CPO, such that p∘e = id_{D}. For instance, any finite model of βη-reduction of the kind discussed in Section 4.2 is of this form. Then e and p form an embedding-projection pair, and one can use them as the basis for carrying out Scott’s D_{∞}-construction. It is natural to ask how the resulting D_{∞}-model is related to the original model of reduction.

As usual, construct the D_{∞} model as the bilimit of the sequence D_{0} = D and D_{n+1} = D_{n}^{D_{n}}, connected by embedding-projection pairs e_{n}, p_{n}. Let ι_{n}: D_{n} → D_{∞} and π_{n}: D_{∞} → D_{n} be the limiting morphisms.

Note that each ⟨D_{n}, e_{n}, p_{n}⟩ is a categorical model of reduction, and ⟨D_{∞}, e_{∞}, p_{∞}⟩ is a categorical model of conversion. Let [[ ]]^{n} and [[ ]]^{∞} be the respective interpretation functions. They are related as follows. For a valuation ρ: V → D_{∞}, let ρ_{n} = π_{n} ∘ ρ. Then for all lambda terms M,

[[M]]_{ρ}^{∞} = [figure: n⩾0] ι_{n}[[M]]_{ρ_{n}}^{n}.

In particular, it follows that ι_{n}[[M]]_{ρ_{n}}^{n} ⩽ [[M]]_{ρ}^{∞} for every M, and by applying π_{n} to both sides, [[M]]_{ρ_{n}}^{n} ⩽ π_{n}[[M]]_{ρ}^{∞}. Equality does not in general hold. The following proposition further relates these models:

Proposition 4.10. If M and N are lambda terms such that [[M]]_{ρ}^{∞} ⌣ ⌢ [[N]]_{ρ}^{∞}, then for all n, [[M]]_{ρ_{n}}^{n} ⌣ ⌢ [[N]]_{ρ_{n}}^{n}. The converse holds if D_{∞} is bounded complete (this is the case, for instance, if D was bounded complete).

Proof. Suppose [[M]]_{ρ}^{∞} ⌣ ⌢ [[N]]_{ρ}^{∞}. Let c ∈ D_{∞} such that [[M]]_{ρ}^{∞}, [[N]]_{ρ}^{∞} ⩽ c. Then [[M]]_{ρ_{n}}^{n} ⩽ π_{n}[[M]]_{ρ}^{∞} ⩽ π_{n}c, and similarly for [[N]]_{ρ_{n}}^{n}. For the converse, assume D_{∞} is bounded complete. Assume that for all n ⩾ 0, [[M]]_{ρ_{n}}^{n} ⌣ ⌢ [[N]]_{ρ_{n}}^{n}. Then ι_{n}[[M]]_{ρ_{n}}^{n} ⌣ ⌢ ι_{n}[[N]]_{ρ_{n}}^{n} for all n. Let c_{n} = ι_{n}[[M]]_{ρ_{n}}^{n} ∨ ι_{n}[[N]]_{ρ_{n}}^{n} in D_{∞}. Then (c_{n})_{n⩾0} is an increasing sequence and [[M]]_{ρ}^{∞} = [figure]_{n} ι_{n}[[M]]_{ρ_{n}}^{n} ⩽ [figure]_{n} c_{n}, and similarly [[N]]_{ρ}^{∞} ⩽ [figure]_{n} c_{n}, hence [[M]]_{ρ}^{∞} ⌣ ⌢ [[N]]_{ρ}^{∞}. □

As a consequence, any two terms that can be distinguished in a finite model of βη-reduction, of the kind discussed in Section 4.2, can also be distinguished in a D_{∞}-model over a finite base domain. In particular, the terms Ω_{n} can be distinguished in such a D_{∞} model, as can the terms Auuut and Auutt of Proposition 2.1. This is perhaps surprising, since such unsolvable terms are identified with ⊥ in the “standard” D_{∞} model constructed from a two-element domain.

Acknowledgments

I would like to thank Gordon Plotkin for introducing me to the problem of partial orders on term models, and for many stimulating discussions. Thanks to Furio Honsell, Simona Ronchi, and Alex Simpson for helpful discussions, and to Martina Fischer for pointing me to the application to dcpo-algebras. Thanks to the anonymous referees for their valuable comments.

References

[1] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, 1994.

[2] H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North-Holland, 2nd edition, 1984.

[3] G. Berry. Stable models of typed λ-calculi. In Proceedings of the 5th International Colloquium on Automata, Languages and Programming, Springer LNCS 62, pages 72–89, 1978.

[4] S. Bulman-Fleming and W. Taylor. Union-indecomposable varieties. Colloquium Mathematicum, 35:189–199, 1976.

[5] P. Di Gianantonio, F. Honsell, S. Liani, and G. D. Plotkin. Countable non-determinism and uncountable limits. In Proceedings of CONCUR ’94, Springer LNCS 836, 1994. See also: Uncountable limits and the Lambda Calculus, Nordic Journal of Computing 2, 1995.

[6] J.-Y. Girard. The system F of variable types, fifteen years later. Theoretical Computer Science, 45:159–192, 1986.

[7] J. Hagemann and A. Mitschke. On n-permutable congruences. Algebra Universalis, 3:8–12, 1973.

[8] F. Honsell and S. Ronchi Della Rocca. An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences, 45(1), 1992.

[9] M. Hyland. A syntactic characterization of the equality in some models for the lambda calculus. J. London Math. Soc., 12:361–370, 1976.

[10] B. Jacobs, I. Margaria, and M. Zacchi. Filter models with polymorphic types. Theoretical Computer Science, 95:143–158, 1992.

[11] A. I. Mal’cev. K obščeǐ teorii algebraičeskih sistem. Mat. Sb. N. S. 35 (77), pages 3–20, 1954.

[12] G. D. Plotkin. A semantics for static type inference. Information and Computation, 109:256–299, 1994.

[13] G. D. Plotkin. On a question of H. Friedman. Information and Computation, 126(1):74–77, 1996.

[14] P. Selinger. Functionality, Polymorphism, and Concurrency: A Mathematical Investigation of Programming Paradigms. PhD thesis, University of Pennsylvania, 1997.

[15] W. Taylor. Structures incompatible with varieties, Abstract 74T-A224. Notices of the American Mathematical Society, 21:A-529, 1974.

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