Order-Incompleteness and Finite Lambda Models Extended Abstract

Peter Selinger^{∗} Department of Mathematics University of Pennsylvania

209 S. 33rd Street Philadelphia, PA 19104-6395

selinger@math.upenn.edu

Abstract

Many familiar models of the type-free 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 type-free 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 �nite models for the type-free lambda calculus. We introduce partial syntactical lambda models, which are derived from Plotkin’s syntactical models of reduction, and we investigate how these models can be used as practical tools for giving �nitary proofs of term inequalities. We give a 3-element model as an example.

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 typefree lambda calculus could be obtained by a combination of order-theoretic 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.

In this paper we establish some basic new facts about ordered models of the type-free 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. We also give a syntactic characterization, in terms of Mal’cev operators, of those combinatory algebras which are absolutely unorderable in the sense that they cannot be embedded in any orderable algebra.

In the second part of the paper (Section 4), we develop a notion of �nite models for the type-free lambda calculus. It has long been known that a model of the lambda calculus in the traditional sense can never be �nite or even recursive [1]. We circumvent this problem by introducing partial syntactical lambda models, which differ from the usual syntactical lambda models [1] in that their operations are only partially de�ned, hence giving denotations only to a subset of lambda terms. Such models can be �nite, and consequently term denotations are effectively computable. We give an example of a non-trivial 3-element model.

Let us brie�y present the main issues discussed in this paper.

Order-Incompleteness. Many familiar models of the typefree lambda calculus, like Scott’s D_{∞} and P ω, are constructed by order theoretic methods. It is a natural question to ask whether the class of such ordered models is complete with respect to the lambda calculus. More precisely, every model de�nes, via the interpretation function, a lambda theory, by which we mean a congruence relation on closed lambda terms with or without constants, closed under the β-rule. By \underline{λβ} we denote the minimal theory, i.e.the theory of β-conversion. By \underline{λβη}, we denote the theory of βηconversion. We consider the following two completeness questions:

(i) Is there a non-trivially partially ordered model whose theory is \underline{λβ} (or \underline{λβη})?

(ii) Does every lambda theory arise as the theory of a non-trivially partially ordered model?

∗This research was supported by a graduate fellowship from the Institute for Research in Cognitive Science and by a dissertation fellowship from the School of Arts and Sciences at the University of Pennsylvania.

Although these questions are of similar nature, (i) is easy, while (ii) is hard. Question (i) asks for a partially ordered model which is complete for β- or βη-conversion. Recall that neither D_{∞} nor P ω are complete in this sense, since in these models the meanings of unsolvable terms are equated [6, 13, 1]. In Corollary 8 below, we construct partially ordered models that are β- and βη-complete. Question (i) becomes more dif�cult, and more interesting, when it is specialized to smaller classes of models. Di Gianantonio, Honsell and Plotkin [2] give a positive answer with respect to models that satisfy a certain weak ω_{1}-continuity condition. It is an open problem whether (i) still holds when specialized to the class of topological models, i.e.models which arise as re�exive objects in a cartesian closed category of complete partial orders and Scott-continuous functions. This is the long-standing topological completeness problem, see [5].

We will show in Section 2 that all models that satisfy condition (i) share an interesting property: the denotations of lambda terms necessarily form a discrete subset, i.e. denotations are pairwise incomparable. This is a consequence of our Theorem 3: the standard open and closed term algebras of the type-free lambda calculus cannot be non-trivially partially ordered as combinatory algebras.

Question (ii) asks for the existence of order-incomplete lambda theories. We call a theory order-incomplete if it does not arise as the theory of a non-trivially partially ordered model. In Section 3, we give a syntactical characterization of such theories: the order-incomplete lambda theories are exactly those theories that have a family of so-called generalized Mal’cevoperators. Mal’cev operators are known from universal algebra [8, 12, 4], and they arise here because of their ability to interfere with orders.

For the smaller class of topological models, (ii) is known to be false: Honsell and Ronchi Della Rocca [5] give a lambda theory that is not induced by any topological model.

Finite Lambda Models. Our notion of �nite models for the type-free lambda calculus is derived from a notion of models of reduction. Models of reduction have been considered by different authors [3, 7, 9], and we will focus here on a formulation which is given by Plotkin [9] in the spirit of the familiar syntactical lambda models [1]. Informally, by a model of convertibility for a lambda calculus, we mean a model with a soundness property of the form

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

where ≅ is e.g. β- or βη-convertibility, and [[ ]] is a ‘meaning’ function of lambda terms. On the other hand, a model of reduction has a soundness property of the form

M ⟶ N ⇒ [[M]] ≤ [[N]],

where ⟶ is e.g. β- or βη-reduction, and ≤ is some order on meanings of terms.

It is known that models of convertibility for the type-free lambda calculus are never �nite or even recursive [1]. By contrast, models of reduction can quite possibly be �nite, and we shall see that they are easy to construct � but they do not in general yield any information about convertibility of terms. Our notion of partial models combines features of both.

The key observation that leads to the de�nition of partial models is that in certain models of reduction, a restricted form of reasoning about convertibility is possible. Speci�- cally, this is the case if the underlying order is �at, i.e.of the form X_{⊥}, where X is a set. A partial model can therefore be understood as a �at model of reduction. After giving the relevant de�nitions in 4.1 and 4.2, we investigate methods of de�ning such models in practice. Such a method is given in 4.3, and an example is worked out in 4.4 of how a 3element partial model can be used to establish a non-trivial term inequality.

2 Lambda terms cannot be ordered

The main result of this section is that the open and closed term algebras of the type-free lambda calculus do not allow a non-trivial partial order. It is understood that by an ordered model we mean one where the order is compatible with the model structure. Since we formulate the results in terms of combinatory algebras, this simply means that application is a monotone operation. We follow Barendregt’s notation for the lambda calculus [1].

De�nition An applicative structure (X, ·) is a set X with a binary operation. A combinatory algebra (X, ·, k, s) is an applicative structure with distinguished k, s ∈ X satisfying kxy = x and sxyz = xz(yz). Recall that every combinatory algebra is combinatory complete, i.e., for any polynomial expression p(x_{1}, …, x_{n}) there is an element f ∈ X with fx_{1} … x_{n} = p(x_{1}, …, x_{n}).

We say that a preorder ≤ on an applicative structure (X, ·) is compatible if a ≤ b implies f · a ≤ f · b for all f, a, b ∈ X. Note that by combinatory completeness, this implies p(a) ≤ p(b) for any polynomial expression p(x); in particular, for a compatible preorder, application is monotone in both arguments.

A preorder is said to be discrete if a ≤ b implies a = b, indiscrete if a ≤ b holds for all a, b, and trivial if it is either descrete or indiscrete. By convention, we will refer to preorders that merely satisfy a ≤ b ⇒ b ≤ a as symmetric. A symmetric partial order is, of course, discrete and hence trivial.

A combinatory algebra is called unorderable if the only compatible partial orders on it are the trivial ones. Such algebras have been previously known to exist. For example, Plotkin [10] has recently exhibited a �nitely separable algebra, a property which implies unorderability. Here (X, ·) is said to be �nitely separable if for every �nite 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, for 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 type-free lambda calculus, occur �naturally�.

De�nition Let �_{C} be the set of (α-equivalence classes of) untyped lambda terms, built from constants in C and some countable supply V of variables. Similarly, �_{C}^{0} is the set of closed terms. For �_{∅} we simply write �.

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 de�ned analogously, and similarly for the λβη-calculus.

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

We start with a lemma, to be proved in 4.4 below:

Lemma 1 There is a closed term A of the type-free lambda calculus with Auuut =_{β} Auttt, but Auuut ≠_{βη} Auutt ≠_{βη} Auttt for variables u ≠ t. □

The lemma is relevant to orders because of the following observation: if ≤ is any compatible partial order on open terms and u ≠ t are variables, then u ≰ t. For suppose u ≤ t, then Auuut ≤ Auutt ≤ Auttt = Auuut, hence Auuut = Auutt by antisymmetry, which contradicts Lemma 1.

This shows that any compatible partial order on the open term algebra is trivial on variables. To show that it is trivial on arbitrary terms u, t, we need the following technical fact: If u, t are terms and s is a fresh variable, then any inequality which holds for variables u and t will also hold for su and st. In this sense, we can say that su and st behave like generic arguments. This is summarized in Lemma 2. Here =_{β(η)} denotes either =_{β} or =_{βη}.

Lemma 2 Let u_{1}, …, u_{n} be terms such that u_{i} ≠_{β(η)} u_{j} for i ≠ j. If s is a variable not free in u_{1}, …, u_{n}, then su_{1}, su_{2}, …, su_{n} behave like generic arguments, i.e.for all

terms M, N with s ∉ FV(M, N),
M(su_{1})(su_{2}) … (su_{n}) =_{β(η)} N(su_{1})(su_{2}) … (su_{n})

implies Mx_{1}x_{2} … x_{n} =_{β(η)} Nx_{1}x_{2} … x_{n}.

Proof Idea: An easy syntactic proof is possible by observing that the subterms of the form (su) never disappear under βηreductions. A more semantic proof can be given if one uses Plotkin’s separability result [10] to embed the open term algebra in a separable algebra. There, one can choose s to map u_{1}, …, u_{n} to x_{1}, …, x_{n}, respectively. □

Theorem 3 Let M be the open or the closed term algebra of the λβ- or λβη-calculus. Then M does not allow a nontrivial compatible partial order. Proof: Equality in M is denoted by =_{β(η)}. Take a compatible partial order ≤. Let u, t be terms with u ≤ t. Let A be as in Lemma 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) =_{β(η)} A(su)(su)(st)(st)

Applying Lemma 2 to M = λut.Auuut and N = λut.Auutt, one gets u =_{β(η)} t. Consequently, the order is trivial. □

Corollary 4 In any partially ordered model of the type-free lambda calculus which is complete for one of the theories \underline{λβ} or \underline{λβη}, the denotations of terms are discretely ordered.

□

3 A characterization of absolutely unorderable algebras

We have shown that the combinatory algebra of open lambda terms cannot be non-trivially ordered. Nevertheless, it follows from Di Gianantonio, Honsell and Plotkin [2] that it can be embedded in an orderable algebra. It is an interesting question whether there is a combinatory algebra which is absolutely unorderable in the sense that it cannot even be embedded in an orderable one. Plotkin conjectures in [10] that the answer is yes.

The problem of absolute unorderability is closely related to the completeness question (ii) in the introduction. Clearly, the lambda theories that cannot be realized in a non-trivially partially ordered model are those whose term algebra is absolutely unorderable.

We will now characterize absolutely unorderable algebras as those algebras that have a family of generalized Mal’cevoperators. Such operators are known from the study of Mal’cev varieties in universal algebra. They are relevant here because of the way they interfere with orders.

3.1 Absolutely unorderable algebras and generalized Mal’cev operators

A combinatory algebra A is absolutely unorderable if there is no embedding of combinatory algebras A → B such that B allows a non-trivial compatible partial order. The following theorem characterizes such algebras. As usual, A[u, t] denotes the combinatory algebra obtained by freely adjoining indeterminates u, t to A.

Theorem 5 The following are equivalent:

1. A is absolutely unorderable.

2. For every compatible preorder ≤ on A[u, t], if u ≤ t then t ≤ u.

3. For some n ≥ 1, there exist elements M_{1}, …, M_{n} ∈ A, called generalized Mal’cev operators, such that, for indeterminates u, t,

t = M_{1}tuu
M_{1}ttu = M_{2}tuu
M_{2}ttu = M_{3}tuu  (Malcev_{n})
⋮
M_{n}ttu = u □

Remark: We say an equation p(u, t) = q(u, t) holds for indeterminates u, t if it holds in A[u, t]. This is a stronger condition than being satis�ed in A, which is usually denoted by A ⊧ p(u, t) = q(u, t), and which means that the equation holds for all u, t ∈ A. If A is extensional, or more generally if A is a lambda model [1], the two concepts coincide.

In the case n = 1, the equations (Malcev_{1}) have the simple form t = Mtuu and Mttu = u. This is the usual Mal’cev operator known from universal algebra. Generalized Mal’cev operators for n ≥ 1 have been used by Hagemann and Mitschke [4] to characterize n-permutable classes of universal algebras.

It is worth noting that Theorem 5 holds not just for combinatory algebras, but in fact in any equational variety. Specifically:

Theorem 6 Let A be an algebra in an equational variety of algebras. Then A is absolutely unorderable if and only if, for some n ≥ 1, there are M_{1}(x, y, z), …, M_{n}(x, y, z) ∈ A[x, y, z], such that the equations (Malcev_{n}) are satis�ed in A[u, t]. □

3.2 Generalized Mal’cev operators and theories

We call a lambda theory order-incomplete if it does not arise as the theory of any non-trivially partially ordered lambda algebra, i.e. if no ordered model is complete for it. In the introduction, we were asking in question (ii) whether an order-incomplete theory exists. Applying Theorem 5, and using the duality between models and theories, we can now also characterize order-incomplete theories in terms of generalized Mal’cev operators. Lambda algebras are de�ned in [1].

Theorem 7 For a lambda theory T , the following are equivalent:

1. T is order-incomplete.

2. The closed term algebra �_{C}^{0}/T is absolutely unorderable.

3. The open term algebra �_{C}/T is absolutely unorderable.

4. T has a family of generalized Mal’cev operators, i.e. there are closed terms M_{1}, …, M_{n} ∈ �_{C}^{0} such that T ⊢ t = M_{1}tuu etc. for variables u, t.

5. There is no interpretation of T in any non-symmetri-cally preordered lambda algebra. □

Note that if T_{2} is an extension of an order-incomplete theory T_{1}, then by 4., T_{2} is also order-incomplete. Also note that because of 5., an order-incomplete theory does not have any (not necessarily complete) non-trivially ordered models. In particular, neither \underline{λβ} nor \underline{λβη} are order-incomplete theories. Thus we can positively answer question (i) from the introduction:

Corollary 8 Both \underline{λβ} and \underline{λβη} arise as the theory of a nontrivially partially ordered model. □

3.3 Mal’cev operators and consistency

At the beginning of this section, we asked whether an absolutely unorderable combinatory algebra exists. In light of Theorem 5, this is the case if and only if, for some n, the equations (Malcev_{n}) are consistent with combinatory logic. Unfortunately, this is not known, except in the cases n = 1 and n = 2.

Let Y be any �xpoint operator of combinatory logic, and write μx.M for Y (λx.M). The operator μ satis�es the �xpoint property:

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

The diagonal axiom is

μy.μx.A(x, y) = μx.A(x, x). (�)

Theorem 9 (Plotkin, A. Simpson) Assuming the diagonal axiom, (Malcev_{n}) is inconsistent with combinatory logic for all n. Proof: Let x be arbitrary. Let A = μz.M_{1}xzz. Then A = μz.x = x. Also,

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

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

Theorem 10 (Plotkin, Simpson) (Malcev_{1}) is inconsistent with combinatory logic. Proof: Suppose M is a Mal’cev operator. Let x be arbitrary and let A = μy.μz.Mxyz. Then

A =^{(�x)} μz.MxAz =^{(�x)} MxAA =^{(Malcev_{1})} x,

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

Theorem 11 (Plotkin, Selinger) (Malcev_{2}) is inconsistent with combinatory logic. Proof: Suppose M_{1} and M_{2} are operators satisfying (Malcev_{2}). De�ne 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 (�x)
= f(M_{1}AAB)(M_{1}AAB) by (Malcev_{2})
= A.  by (�x)

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 Theorem 9, this leads to an inconsistency. □

4 Finite models for the lambda calculus

4.1 Models of reduction

De�nition 12 An ordered applicative structure (P, ·) is a poset P with a monotone binary operation ·: P × P → P. Let P^{V} be the set of all valuations, i.e.functions from variables to P. A syntactical model of β-reduction (P, ·, [[ ]]) [9] is an ordered applicative structure together with a meaning function

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

such that the following hold:

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

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

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

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 satis�es the additional property

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

Note that if P is a discrete partial order, we obtain the usual syntactical lambda models (of convertibility) [1].

Also note that 1.�3. do not form an inductive de�nition; rather they state properties of a function [[ ]] which is given a priori. In particular, 3. does not uniquely determine the meaning of an abstraction.

Unlike in ordered models of convertibility, where the order relation is to be understood as ‘information order’, here we are dealing with a reduction order: a ≤ b intuitively means a reduces to b. More precisely, the following properties hold:

Proposition 13 (Plotkin [9]) The following are properties of 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 model of βη-reduction: If M ^{βη} ⟶N, then [[M]]_{ρ} ≤ [[N]]_{ρ}. □

De�nition 14 A categorical model of β-reduction (P, p, e) is given by an object P in an order-enriched cartesian closed category, together with a pair of morphisms p: P → P^{P} and e: P^{P} → P, such that p∘e ≤ id_{P^{P}}. If moreover e∘p ≤ id_{P}, then (P, p, e) is a categorical model of βη-reduction.

Such categorical models of reduction have been studied by various authors, e.g. by Girard [3] for the case of qualitative domains, or by Jacobs et al. [7], where they are called models of expansion. For a detailed discussion of these and other sources, see Plotkin [9].

There is an evident way of de�ning a syntactical model of β-reduction (P, ·, [[ ]]) from a concrete categorical model of β-reduction, by letting a · b := p(a)(b) and [[λx.M]]_{ρ} := e(λa.[[M]]_{ρ(x:=a)}). Similarly for βη. This is completely analogous to Scott’s familiar rendition of a model of convertibility as a re�exive object in a cartesian closed category [11].

Constructing models of reduction is much easier than the corresponding task of �nding models of convertibility. Indeed, for a given p: P → P^{P}, there are a few obvious choices for e: a minimal choice is always possible if P has a least element ⊥. In this case, let e be the constant ⊥ function, which amounts to declaring [[λx.M]]_{ρ} to be always unde�ned. On the other hand, if p has a right adjoint e, then e is maximal with p ∘ e ≤ id. In this case, [[λx.M]]_{ρ} is the maximal b ∈ P such that for all a ∈ P, b · a ≤ [[M]]_{ρ(x:=a)}.

4.2 Partial Models

We have already noted that the soundness property for models of reduction does not in general yield any information about convertibility. The best statement one can make is that, if the reduction under consideration is con�uent (Church-Rosser), then [[M]]_{ρ} and [[N]]_{ρ} must be compatible, i.e.

M ≅ N ⇒ ∃c ∈ P.[[M]]_{ρ} ≤ c and [[N]]_{ρ} ≤ c.

For this reason we will be especially interested in partial orders P that have lots of incompatible pairs. An important special case arises with (P, ·, [[ ]]) where P = X_{⊥} is a �at order, and where ·: P × P → P is strict in each argument. In this case, it is convenient to consider ⊥ as the unde�ned element, and ·, [[ ]] as partial functions. This gives rise to the following de�nition.

De�nition 15 A partial applicative structure (X, ·) is a set X with a partial binary operation ·: X × X ⇀ X. Let Val(X) be the set of partial valuations V ⇀ X. A partial syntactical lambda model (X, ·, [[ ]]), or partial model for short, is given by a partial applicative structure together with a partial map

[[ · ]]_{·}: �_{X} × Val(X) ⇀ X,

such that properties 1.�5. in De�nition 12 hold, where = is replaced by Kleene equality and ≤ by directed equality. Moreover, if property 6. holds, (X, ·, [[ ]]) is a partial βηmodel.

Kleene equality is de�ned as follows: A = B if and only if A and B are either both unde�ned or both de�ned and equal. Directed equality, which we often denote by A [figure] B, means that if A is de�ned, then so is B and they are equal.

The idea of using partiality in models for the lambda calculus is not new. In fact, Kleene’s ��rst model�, which consists of G� odel numbers of partial recursive functions and their application, is partial. Partial models in our sense, however, need not even be partial combinatory algebras. In particular, here we do not even assume that the meanings of the combinators S and K are necessarily de�ned.

In any particular partial syntactical lambda model, the class of terms which denote in it is not given a priori, but derived. The following soundness properties ensure that this class is closed under reduction. Note that for partial models, we have two notions of soundness: the one for reduction like before, and now, as a trivial consequence, one for convertibility.

Proposition 16 The following are properties of partial models:

1. Soundness for reduction. If M ^{β} ⟶N, then [[M]]_{ρ} [figure] [[N]]_{ρ}.

2. Soundness for convertibility. If M =_{β} N, and if [[M]]_{ρ} and [[N]]_{ρ} are both de�ned, then [[M]]_{ρ} = [[N]]_{ρ}.

3. In a partial βη-model, the respective properties hold for =_{βη}. □

4.3 Methods of construction

For a given partial model, the semantic interpretation function [[ ]] is given a priori, satisfying certain properties. For all practical purposes, one desires to be able to de�ne [[ ]] inductively. This is in general not possible. It turns out, however, that if (X, ·) is strongly extensional, then [[ ]] can be de�ned inductively in a maximal way:

De�nition 17 A partial applicative structure (X, ·) is weakly extensional if for all elements a, b ∈ X, whenever ∀x ∈ X.ax [figure] bx then a = b. It is strongly extensional if for all elements a, b ∈ X, whenever (∀x ∈ X.ax and bx de�ned ⇒ ax = bx), then a = b.

Note that strong extensionality implies weak extensionality, and that in the total case, both coincide with extensionality. For a given partial applicative structure (X, ·), let P = X_{⊥} be the corresponding �at order, and de�ne p: P → P^{P} by p(a)(b) = a · b. The following proposition relates weak extensionality to the η-rule, and strong extensionality to the existence of a right adjoint to p:

Proposition 18 If (X, ·) is weakly extensional and |X| ≥ 2, then every partial model (X, ·, [[ ]]) is a partial βη-model. If (X, ·) is strongly extensional, then p: P → P^{P} has a right adjoint. □

Hence, if we start with a strongly extensional applicative structure (X, ·), it is possible to de�ne [[ ]] inductively, using the adjointness p ⊣ e like in the discussion following De�nition 14. The resulting de�nition of [[ ]] is maximal, and it is summarized in the following corollary:

Corollary 19 If (X, ·) is a strongly extensional applicative structure, then the following de�nes a partial βη-model:

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

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

3. [[λx.M]]_{ρ} is de�ned iff there exists b ∈ X with b · a [figure] [[M]]_{ρ(x:=a)} for all a ∈ X. By strong extensionality, such an element b is necessarily unique. De�ne [[λx.M]]_{ρ} = b.

Moreover, if [[ ]] is de�ned in this way, then for all n ≥ 1 and b ∈ X, one has b = [[λx_{1} … x_{n}.P]]_{ρ} if and only if for all a_{1} … a_{n} ∈ X, b · a_{1} ⋯ a_{n} [figure] [[P]]_{ρ(x_{1}:=a_{1})...(x_{n}:=a_{n})}. In particular, if such b exists, it is unique; otherwise [[λx_{1} … x_{n}.P]]_{ρ} is unde�ned. Proof: The last claim follows by induction on n. □

4.4 Example: A 3-element partial model

We demonstrate the methods of the previous subsection by supplying a proof of Lemma 1 above. The proof illustrates how a simple partial model can be ‘put to action’.

Lemma There is a closed term A of the type-free lambda calculus with Auuut =_{β} Auttt, but Auuut ≠_{βη} Auutt ≠_{βη} Auttt for variables u ≠ t. Proof: De�ne terms

h = λzyx.zzy(zzy(zzyx))
f = hh
A = λuvwt.λx.fu(fv(fw(ftx))).

Then for all x, y:

fyx ⟶^{β} fy(fy(fyx)),

hence for all u, t:

λx.fu(ftx) ⟶^{β} λx.fu(fu(fu(ftx))) = Auuut
λx.fu(ftx) ⟶^{β} λx.fu(ft(ft(ftx))) = Auttt.

To see that Auuut ≠_{βη} Auutt for variables u and t, we will construct a partial model with as little as 3 elements. Let X = {k, 0, 1}, and let · be de�ned 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 (X, ·) is a (strongly) extensional applicative structure. De�ne [[ ]] inductively as in Corollary 19. Although (X, ·) is total, [[ ]] will be partial.

Consider the partial functions ϕ(c, b, a) := k · c · b · a and ψ(c, b, a) := [[zzy(zzy(zzyx))]]_{ρ(z:=c)(y:=b)(x:=a)} = ccb(ccb(ccba)). Rather tediously, the values of these functions are calculated in this table:

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 by Corollary 19, [[h]] = [[λzyx.zzy(zzy(zzyx))]] is de�ned 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, fu(fu(fu(ftx))) ≠_{βη} fu(fu(ft(ftx))) ⇒ Auuut ≠_{βη} Auutt. □

4.5 Towards partial completeness theorems

For partial models, the following completeness theorem holds trivially, since the models can be chosen to be total.

Proposition 20 Completeness: If M ≠_{β} M′, then there is a partial model and ρ for which [[M]]_{ρ}, [[M′]]_{ρ} are de�ned and [[M]]_{ρ} ≠ [[M′]]_{ρ}. If M ≠_{βη} M′, then the model can be chosen to be strongly extensional. □

Of course much more interesting questions can be asked, e.g.how close one can come to a �nite completeness theorem for partial models? In other words: can every inequality M ≠_{β} M′ be demonstrated in a �nite partial model? The answer is obviously no, since this would yield a decision procedure for convertibility of lambda terms. It remains open to identify interesting strict subclasses of terms for which a �nite completeness property holds.

Further Research

In the introduction, we mentioned the topological completeness problem: does there exist a topological model which is complete for β-conversion. This is a long-standing open problem, see e.g.[5]. Here, by a topological model we mean a model which arises as a re�exive object in a cartesian closed category of complete partial orders and Scottcontinuous functions. Our results imply that if such a model is complete, then the term denotations in it must be discretely ordered. It remains to be seen whether this result can shed some light on the topological completeness problem.

We have also made partial progress with respect to another incompleteness question, namely order-incomplete-ness: Does every lambda theory arise as the theory of a non-trivially partially ordered model? We have characterized order-incomplete lambda theories, or equivalently, absolutely unorderable algebras, syntactically via the presence of generalized Mal’cev operators. The question remains whether, for some n ≥ 1, such operators are consistent with the lambda calculus, and hence, whether an orderincomplete theory exists. So far, answers are only known for the cases n = 1 and n = 2.

There are many open questions regarding our partial syntactical lambda models. These models seem to resist many of the usual constructions, e.g. it is unclear whether they form an interesting category or how to de�ne substructures etc. The soundness properties in Proposition 16 lack an important feature: they do not embody reasoning from additional hypotheses. While this can be easily �xed in the case of soundness for reduction, it is a non-trivial problem in the case of soundness for convertibility, since the latter involves the Church-Rosser property in a crucial way.

Further, it is an interesting question how close one can get, using partial models, to a �nite completeness theorem for the lambda calculus. With the prospects for such a theorem limited by undecidability considerations, it might nevertheless be possible to identify suitable and interesting classes of terms for which a �nite model property holds. In particular, what is the theory of �nite partial models, i.e. which equations hold in all �nite partial models?

Conclusion

This paper provides some basic new facts about ordered models of the type-free lambda calculus. While most known models are ordered, we show that the familiar term algebras are not; they do not allow a partial order. A consequence, with a possible application to the topological completeness problem, is that in an ordered model which is complete for β- or βη-conversion, the term denotations must necessarily form a discrete subset.

We also investigate the problem of order-incomplete-ness: Can every model of the lambda calculus be embedded in an orderable one, or equivalently, does every lambda theory arise as the theory of a non-trivially partially ordered model? Towards an answer to this question, we show that a theory, or a model, is order-incomplete if and only if it has a family of generalized Mal’cev operators. Such operators are known from universal algebra, where they are used to characterize permutabilities of congruence relations. In our context, Mal’cev operators are relevant because of their ability to interfere with partial orders. It remains open whether such operators are consistent with the lambda calculus.

We introduce a new notion of �nite models for the lambda calculus, called partial syntactic lambda models. Partial models can be a convenient tool for reasoning about lambda terms. They can be regarded as a special case of the more natural class of Plotkin’s syntactical models of reduction. Unlike in traditional models of the lambda calculus, which are never recursive, term denotations can be easily and effectively calculated in �nite models.

Acknowledgments

Thanks to Gordon Plotkin for introducing me to the problem of partial orders on term models, and to Furio Honsell for pointing out the connection with incompleteness theorems. Thanks to Dana Scott, Phil Scott, Peter Freyd and Martin Hyland for discussions, to Andre Scedrov for his supervision, and to the Isaac Newton Institute at Cambridge University for hosting all of the above at various times during the Semantics of Computation Program in Fall 1995.

References

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

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

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

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

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

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

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

[8] A. I. Mal’cev. K ob�s� ce�� teorii algebrai� ceskih sistem. Mat. Sb. N. S. 35 (77), pages 3�20, 1954.

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

[10] G. D. Plotkin. On a question of H. Friedman. Unpublished, 1995.

[11] D. S. Scott. Relating theories of the λ-calculus. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 403�450. Academic Press, London, New York, 1980.

[12] J. D. H. Smith. Mal’cev Varieties, volume 554 of Lecture Notes in Mathematics. Springer Verlag, 1976.

[13] C. Wadsworth. The relation between computational and denotational properties for Scott’s D_{∞}-models of the lambdacalculus. SIAM J. Comput., 5:488�521, 1976.