Chapter 8

Logical Relations

8.1 Introduction to Logical Relations

Logical relations are an important tool in the study of typed lambda calculus. Essentially, a logical relation R is a collection {R^{σ} | σ a type} of typed relations with the relation R^{σ → τ} for type σ → τ determined from the relations R^{σ} and R^{τ} in a way that guarantees closure under application and lambda abstraction. The relation R^{σ × τ} for type σ × τ is determined from the relations R^{σ} and R^{τ} in a way that guarantees closure under pairing and projection, and similarly for sums (disjoint unions) and other types. Since logical relations are very general, some important algebraic concepts like homomorphisms and congruence relations lead to special classes of logical relations. However, logical relations lack many familiar properties of their algebraic analogs. For example, the composition of two logical relations may not be a logical relation, even in the special cases where both logical relations seem to act as homomorphisms or congruence relations. Logical relations are also closely related to partial equivalence relation models (Section 5.6).

The main topics in this chapter are:

• Definition of logical relation over typed applicative structure and the “basic lemma.” For λ^{→}, this lemma says that logical relations are closed under application and lambda abstraction. In particular, if R is a logical relation between models A and B, and M is a closed term, then R relates the meaning of M in A to the meaning of M in B.

• Completeness and reduction properties of typed lambda calculus and PCF using logical relations over the typed applicative structure of terms.

• Logical partial functions and partial equivalence relations, which are roughly similar to homomorphisms and congruence relations over algebraic structures. These are used to prove completeness of the equational axioms for particular models.

• Representation independence using logical relations. Intuitively, representation independence states that implementors of a programming language have some freedom in the way they implement data types. For example, in implementing a language based on λ^{→} with type constant bool , it does not matter whether true is represented by 1 and false by 0, or viceversa, as long as operations like conditional behave properly.

• Special types of logical relations, such as those appropriate to domain-theoretic (cpo) models.

Logical relations for typed lambda calculus were developed by Howard, Tait, Friedman, Statman, Plotkin, and others. The main historical references are [How73, Tai67, Fri75, Plo73, Plo80] and the three papers by Statman [Sta82, Sta85b, Sta85a]. Many of the results presented in this chapter are proved in [Sta85b], using a slightly different framework, although our definition of relation over applicative structures that are not Henkin models is different from his. The uniform treatment of relations over models and terms, and the revised definition of “admissible,” are based on [Mit86c].

There are many interesting properties of logical relations that we do not have sufficient space to go into. Among other things, logical relations have applications to strictness analysis [BHA86, Abr90], full abstraction [Mul87], and realizability semantics of constructive logics [Mit86a, MO86].

8.2 Logical Relations Over Applicative Structures

8.2.1 Definition of Logical Relation

We will formulate the basic definitions using λ^{×,→} applicative structures. Since the set of terms, as well as any model, forms a typed applicative structure, we will be able to use logical relations to prove syntactic as well as semantic results about typed lambda calculus.

Let A = ⟨{A^{σ}}, {Proj_{1}^{σ,τ} , Proj_{2}^{σ,τ} , App_{A}^{σ,τ} }, Const_{A}⟩ and B = ⟨{B^{σ}}, {Proj_{1}^{σ,τ} , Proj_{2}^{σ,τ} , App_{B}^{σ,τ} }, Const_{B}⟩ be λ^{×,→} applicative structures for some signature Σ. A logical relation R = {R^{σ}} over A and B is a family of relations indexed by the type expressions over Σ such that

• R^{σ} ⊆ A^{σ} × B^{σ} for each type σ,

• R^{σ × τ} (p, q) iff R^{σ}(Proj_{1}p, Proj_{1}q) and R^{τ} (Proj_{2}p, Proj_{2}q),

• R^{σ → τ} (f, g) iff ∀x ∈ A^{σ}. ∀y ∈ B^{σ}. R^{σ}(x, y) ⊃ R^{τ} (App_{A} f x, App_{B} g y),

• R^{σ}(Const_{A}(c), Const_{B}(c)) for every typed constant c: σ of Σ.

For λ^{→}, we drop the condition on R^{σ × τ}, and for extensions of λ^{×,→}, there is an additional condition for each type form. The central property for λ^{→} is that two functions, f and g, are logically related iff they map related arguments to related results. Given R^{σ} and R^{τ}, this determines R^{σ → τ} uniquely, and similarly for σ × τ, and other types. We will often write R(x, y) for R^{σ}(x, y) when σ is either clear from context or irrelevant. We also write R ⊆ A × B to indicate that R is a relation over A and B.

Some trivial examples of logical relations are the identity and “true everywhere” relations.

If A is extensional, then the identity relation I = {I^{σ}} ⊆ A × A with I^{σ}(x, y) iff x = y ∈ A^{σ} is logical.

For any applicative structures A and B of the same signature, the relation R ⊆ A × B that relates every element of A^{σ} to every element of B^{σ} is logical.

When the signature Σ has no term constants, logical relations may be constructed by choosing arbitrary R^{b} ⊆ A^{b} × B^{b} for each type constant b and extending to higher types inductively. For signatures with term constants, it is sometimes more difficult to construct logical relations. However, if all constants have base type (i.e., if c: σ is a constant of the signature, then σ is a type constant), we may construct logical relations by choosing a relation for each type constant that respects the interpretation of all term constants. It is also relatively easy to accommodate first-order function constants (see Exercise 8.2.2). For higher-order constants such as fix_{nat → nat}: ((nat → nat) →(nat → nat)) → nat → nat , however, we must construct relations in a special way. For fix specifically, this is discussed in Section 8.6.2.

Binary logical relations illustrate the general properties of logical relations well and will be sufficient for most of our purposes. However, it is worth noting that the definition above generalizes easily to k-ary logical relations R over applicative structures A_{1}, …, A_{k}, including the case k = 1. All of the results of this chapter generalize easily to relations of arbitrary arity; only the notation becomes more complicated. The reason is that logical relations of any arity may be viewed as unary logical relations. The reader may enjoy formulating the definition of logical predicate (unary logical relation) and proving that a logical relation R ⊆ A × B is just a logical predicate over the straightforwardly-defined product applicative structure A × B (see Exercise 8.2.1).

Exercise 8.2.1 Let A and B be λ^{→} applicative structures. Write out a definition for the product structure

A × B = ⟨{A^{σ} × B^{σ}}, {App^{σ,τ} }, Const⟩,

with application defined component-wise. Show that a typed relation R is a binary logical relation over A and B iff R is a logical predicate (unary logical relation) over A × B.

Exercise 8.2.2 Let Σ be a λ^{→} signature with type constant nat and term constants 0, 1: nat and +, ∗: nat → nat → nat . Describe the smallest logical relation R ⊆ A × A over any Σ applicative structure A.

Exercise 8.2.3 Let A be the full classical λ^{→} hierarchy for some signature Σ without term constants. For each type constant b of Σ, let π^{b} be some permutation on A^{b}. Let R ⊆ A × A be the logical relation determined by

R^{b}(a, b) iff π^{b}a = b.

Show that for every type τ, the relation R^{τ} is the graph of a permutation π^{τ} on A^{τ}, and that

π^{σ → τ} f = π^{τ} ∘ f ∘ (π^{σ})^{−1}.

A logical relation with this property is called a hereditary permutation.

Exercise 8.2.4 Let A be a λ^{→} typed applicative structure for some signature Σ without term constants and define the predicate R ⊆ A by

R^{σ} = \{ \begin{matrix}A^{σ} & if ∃ closed M: σ, \\ ∅ & otherwise. \end{matrix}

Use Lemma 4.3.14 to prove that R is a logical relation iff Σ has only one type constant. This shows that in proving properties of logical relations, it is not sufficient to consider only the special case with one type constant.

8.2.2 The Basic Lemma

The Basic Lemma establishes that the meaning of a term in one model is always logically related to its meaning in any other model. On the face of it, the Basic Lemma only seems to apply to models, since the meaning of a term is not necessarily defined in an arbitrary applicative structure. However, with a little extra work, we can also state a version of the lemma which will be useful in proving properties of applicative structures that are not models. We will take this up after stating the Basic Lemma for models. For simplicity, we restrict our attention to λ^{→}.

An auxiliary definition will make the lemma easier to write down. A logical relation R ⊆ A × B may be regarded as a relation on environments for A and B, as follows. We say that environments η_{a} for A and η_{b} for B, satisfying Γ, are related by R, and write R^{Γ}(η_{a}, η_{b}), if

R^{σ}(η_{a}(x), η_{b}(x))

for every x: σ ∈ Γ.

Lemma 8.2.5 (Basic Lemma, for models) Let R ⊆ A × B be a logical relation and let η_{a} and η_{b} be environments for models A and B with η_{a}, η_{b} ⊧ Γ and R^{Γ}(η_{a}, η_{b}). Then

R(A[[Γ ▷ M : σ]]η_{a}, B[[Γ ▷ M : σ]]η_{b})

for every typed term Γ ▷ M : σ.

Proof We use induction on terms. Constants are straightforward, since we assume that any logical relation respects constants. For a variable Γ ▷ x : σ, it is easy to see that R(A[[Γ ▷ x : σ]]η_{a}, B[[Γ ▷ x : σ]]η_{b}), since we have assumed R(η_{a}(x), η_{b}(x)) for every variable x in Γ. For an application Γ▷MN : τ, we assume inductively that R^{σ → τ} (A[[Γ▷M : σ → τ]]η_{a}, B[[Γ▷M : σ → τ]]η_{b}) and R^{σ}(A[[Γ ▷ N : σ]]η_{a}, B[[Γ ▷ N : σ]]η_{b}). By the definition of logical relation, we have

R^{τ} (App A[[Γ ▷ M : σ → τ]]η_{a} A[[Γ ▷ N : σ]]η_{a}, App B[[Γ ▷ M : σ → τ]]η_{b} B[[Γ ▷ N : σ]]η_{b}),

which implies that A[[Γ ▷ MN : τ]]η_{a} and B[[Γ ▷ MN : τ]]η_{a} are related.

For an abstraction Γ ▷ λx: σ.M : σ → τ, we want to show that

R(A[[Γ ▷ λx: σ.M : σ → τ]]η_{a}, B[[Γ ▷ λx: σ.M : σ → τ]]η_{b})

whenever η_{a} and η_{b} are related. If η_{a} and η_{b} are related, then whenever R^{σ}(a, b), the modified environments η_{a}[x ↦ a] and η_{b}[x ↦ b] are related. Therefore, by the inductive hypothesis, we have

∀a, b. R^{σ}(a, b) ⊃ R(A[[Γ, x: σ ▷ M : τ]]η_{a}[x ↦ a], B[[Γ, x: σ ▷ M : τ]]η_{b}[x ↦ b]).

But, since A[[Γ, x: σ ▷ M : τ]]η_{a}[x ↦ a] = App (A[[Γ ▷ λx: σ.M : σ → τ]]η_{a}) a, and similarly for B, it follows from the definition of logical relation that A[[Γ ▷ λx: σ.M : σ → τ]]η_{a} and B[[Γ ▷ λx: σ.M : σ → τ]]η_{b} are related.

The Basic Lemma may be generalized to applicative structures that are not models by including some hypotheses about the way terms are interpreted. If A is an applicative structure, a partial mapping A[[ ]] from terms and environments to A is an acceptable meaning function if

A[[Γ ▷ M : σ]]η ∈ A^{σ} whenever η ⊧ Γ

and the following conditions are satisfied:

A[[Γ ▷ x : σ]]η  = η(x)
A[[Γ ▷ c : σ]]η  = Const(c)
A[[Γ ▷ MN : τ]]η  = App A[[Γ ▷ M : σ → τ]]η A[[Γ ▷ N : σ]]η
A[[Γ ▷ λx: σ.M : σ → τ]]η = A[[Γ ▷ λy: σ.[y/x]M : σ → τ]]η
A[[Γ ▷ M : σ]]η_{1}  = A[[Γ ▷ M : σ]]η_{2} whenever η_{1}(x) = η_{2}(x) all x ∈ F V (M)
A[[Γ, x: σ ▷ M : τ]]η  = A[[Γ ▷ M : τ]]η for x not in Γ

Two important examples of acceptable meaning functions are meaning functions for models and substitution on applicative structures of terms. These and other examples appear following the next definition. The last three conditions of the definition above are not strictly necessary for the Basic Lemma. However, they are natural properties that hold of all the examples we consider.

In addition to acceptable meaning functions, we will need some assumptions about the behavior of a logical relation on lambda abstractions. A logical relation over models is necessarily closed under lambda abstraction, as a consequence of the way that lambda abstraction and application interact. However, in an arbitrary applicative structure, abstraction and application may not be “inverses,” and so we need an additional assumption to prove the Basic Lemma.

If R ⊆ A × B and A[[ ]], B[[ ]] are acceptable meaning functions, we say R is admissible for A[[ ]] and B[[ ]] if, for all related environments η_{a}, η_{b} ⊧ Γ and terms Γ, x: σ ▷ M : τ and Γ, x: σ ▷ N : τ,

∀a, b. R^{σ}(a, b) ⊃ R^{τ} (A[[Γ, x: σ ▷ M : τ]]η_{a}[x ↦ a], B[[Γ, x: σ ▷ N : τ]]η_{b}[x ↦ b])

implies

∀a, b. R^{σ}(a, b) ⊃ R^{τ} (App (A[[Γ ▷ λx: σ.M : σ → τ]]η_{a}) a, App (B[[Γ ▷ λx: σ.N : σ → τ]]η_{b}) b).

The definitions of acceptable meaning function and admissible logical relation are technical and motivated primarily by their use in applications of the Basic Lemma. To give some intuition, several examples are listed below.

Example 8.2.6 If A is a model, then the ordinary meaning function A[[ ]] is acceptable. It is clear that if A and B are models, then any logical R ⊆ A × B is admissible, since then

A[[Γ, x: σ ▷ M : τ]]η_{a}[x ↦ a] = App (A[[Γ ▷ λx: σ.M : σ → τ]]η_{a}) a,

and similarly for Γ, x: σ ▷ N : τ.

Example 8.2.7 Let T be an applicative structure of terms M such that Γ ▷ M : σ for some Γ ⊆ H, as in Example 4.5.1. An environment η for T is a mapping from variables to terms, which we may regard as a substitution. Let us write ηM for the result of substituting terms for free variables in M, and define a meaning function on T by

T [[Γ ▷ M : σ]]η = ηM.

It is a straightforward but worthwhile exercise to verify that T [[ ]] is an acceptable meaning function. We will see in Section 8.3.1 that every lambda theory E gives us an admissible logical relation R_{E} ⊆ T × T . In short, R_{E} relates any pair of terms that are provably equal from E. The reason why R_{E} is admissible is that we can prove Γ ▷ λx: σ. M = λx: σ. N : σ → τ immediately from Γ, x: σ ▷ M = N : τ.

Example 8.2.8 If A is a typed combinatory algebra, then A is an applicative structure with an acceptable meaning function. The standard acceptable meaning function for A is obtained by translation into combinators. More specifically, as described in Section 4.5.7, we may translate a typed term Γ ▷ M : σ into a combinatory term Γ ▷ cl(M) : σ that contains constants K and S of various types but does not involve lambda abstraction. Since any such combinatory term has a meaning in A, we can take the meaning of Γ ▷ cl(M) : σ as the meaning of Γ ▷ M : σ. It is easy to verify that this is an acceptable meaning function. However, recall that since a combinatory algebra need not be extensional, β -equivalent terms may have different meanings. It is shown in Exercise 8.2.16 that every logical relation over combinatory algebras is admissible.

Example 8.2.9 A special case of Example 8.2.8 that deserves to be singled out is that from any partial combinatory algebra D, as defined in Section 5.6.2, we may construct a typed combinatory algebra A_{D}. In this structure, the interpretation of each typed term will be an element of the untyped partial combinatory algebra. We shall see in Sections 8.2.4 and 8.2.5 that the symmetric and transitive logical relations over A_{D} correspond exactly to partial equivalence relation models over D.

Using acceptable meaning functions and admissible relations, we have the following general form of the Basic Lemma.

Lemma 8.2.10 (Basic Lemma, general version) Let A and B be applicative structures with acceptable meaning functions A[[ ]] and B[[ ]] and let R ⊆ A × B be an admissible logical relation. Suppose η_{a} and η_{b} are related environments satisfying the type assignment Γ. Then

R(A[[Γ ▷ M : σ]]η_{a}, B[[Γ ▷ M : σ]]η_{b})

for every typed term Γ ▷ M : σ.

The proof is similar to the proof of the Basic Lemma for models, since the acceptability of A[[ ]] and B[[ ]], and the admissibility of R, are just what we need to carry out the proof. We will go through the proof to see how this works. Proof We use induction on terms. For a constant c, we assume R(Const_{A}(c), Const_{B}(c)) as part of the definition of logical relation, so the lemma follows from the definition of acceptable meaning function. For a variable Γ▷x : σ, we have R(η_{a}(x), η_{b}(x)) by assumption. Since A[[ ]] is acceptable, A[[Γ ▷ x : σ]]η_{a} = η_{a}(x), and similarly for B[[ ]]. Therefore R(A[[Γ ▷ x : σ]]η_{a}, B[[Γ ▷ x : σ]]η_{b}).

For an application Γ▷MN : τ, we assume inductively that R^{σ → τ} (A[[Γ▷M : σ → τ]]η_{a}, B[[Γ▷M : σ → τ]]η_{b}) and R^{σ}(A[[Γ ▷ N : σ]]η_{a}, B[[Γ ▷ N : σ]]η_{b}). Since R is logical, it follows that

R^{τ} (App A[[Γ ▷ M : σ → τ]]η_{a} A[[Γ ▷ N : σ]]η_{a}, App B[[Γ ▷ M : σ → τ]]η_{b} B[[Γ ▷ N : σ]]η_{b}).

Since the meaning functions are acceptable, it follows that A[[Γ ▷ MN : τ]]η_{a} and B[[Γ ▷ MN : τ]]η_{a} are related.

For an abstraction Γ ▷ λx: σ.M : σ → τ, we want to show that

R(A[[Γ ▷ λx: σ.M : σ → τ]]η_{a}, B[[Γ ▷ λx: σ.M : σ → τ]]η_{b})

for related environments η_{a} and η_{b}. If η_{a} and η_{b} are related, then whenever R^{σ}(a, b), the modified environments η_{a}[x ↦ a] and η_{b}[x ↦ b] are related. By the inductive hypothesis, we have

∀a, b. R^{σ}(a, b) ⊃ R(A[[Γ, x: σ ▷ M : τ]]η_{a}[x ↦ a], B[[Γ, x: σ ▷ M : τ]]η_{b}[x ↦ b]).

Since R is admissible, it follows that

∀a, b. R^{σ}(a, b) ⊃ R^{τ} (App (A[[Γ ▷ λx: σ.M : σ → τ]]η_{a}) a, App (B[[Γ ▷ λx: σ.M : σ → τ]]η_{b}) b).

But by definition of logical relation, this implies that A[[Γ ▷ λx: σ.M : σ → τ]]η_{a} and B[[Γ ▷ λx: σ.M : σ → τ]]η_{b} are related.

The following lemma is useful for establishing that logical relations over term applicative structures are admissible. For simplicity, we state the lemma for logical predicates only.

Lemma 8.2.11 Let T be an applicative structure of terms with meaning function defined by substitution, as in Example 8.2.7. Let P ⊆ T be a logical predicate. If

∀N ∈ P^{σ}. P^{b}(([N/x]M)N_{1} … N_{k}) implies ∀N ∈ P^{σ}. P^{b}((λx: σ.M)NN_{1} … N_{k})

for any type constant b, term λx: σ.M in T^{σ → τ_{1} →... → τ_{k} → b} and terms N_{1} ∈ T^{τ_{1}}, …, N_{k} ∈ T^{τ_{k}}, then P is admissible.

This lemma may be extended to λ^{×,→} using elimination contexts in place of sequences of applications, as described in Section 8.3.4. Proof For a term applicative structure T , the definition of admissible simplifies to

∀N ∈ P^{σ}.P^{τ} ([L_{1}, …, L_{ℓ}, N/x_{1}, …, x_{ℓ}, x]M) implies ∀N ∈ P^{σ}.P^{τ} (([L_{1}, …, L_{ℓ}/x_{1}, …, x_{ℓ}]λx: σ.M)N)

Since x is a bound variable in the statement of the lemma, we are free to choose x so as not to appear in any of the L_{i}. Therefore, it suffices to show that

∀N ∈ P^{σ}.P^{τ} ([N/x]M) implies ∀N ∈ P^{σ}.P^{τ} ((λx: σ.M)N)

for arbitrary M,x and τ. Since this follows immediately from condition

(∗) ∀N ∈ P^{σ}.P^{τ} (([N/x]M)N_{1} … N_{k}) implies ∀N ∈ P^{σ}.P^{τ} ((λx: σ.M)NN_{1} … N_{k}),

it suffices to show (∗) by induction on τ. The base case is easy, since this is the hypothesis of the lemma.

For the inductive step, we assume (∗) for types τ_{1} and τ_{2} and assume

∀N ∈ P^{σ}.P^{τ_{1} → τ_{2}}(([N/x]M)N_{1} … N_{k}).

We must show that [N/x]M may be replaced by (λx: σ.M)N. Let Q ∈ P^{τ_{1}} . By assumption and the fact that P is logical, we have

∀N ∈ P^{σ}.P^{τ_{2}}(([N/x]M)N_{1} … N_{k}Q)

By the inductive hypothesis, is follows that

∀N ∈ P^{σ}.P^{τ_{2}}((λx: σ.M)NN_{1} … N_{k}Q).

Since this holds for all Q ∈ P^{τ_{1}} , we may conclude that

∀N ∈ P^{σ}.P^{τ_{1} → τ_{2}}((λx: σ.M)NN_{1} … N_{k}).

This completes the inductive step and the proof of the lemma.

Our definition of “admissible” is similar to the definition given in [Sta85b], but slightly weaker. Using our definition we may prove strong normalization directly by a construction that does not seem possible in Statman’s framework [Sta85b, Example 4].

Exercise 8.2.12 Let A be a Henkin model. We say that a ∈ A^{σ} is lambda definable from a_{1} ∈ A^{σ_{1}}, …, a_{k} ∈ A^{σ_{k}} if there is a term {x_{1}: σ_{1}, …, x_{k}: σ_{k}} ▷ M : σ such that a = [[M]]η in the environment η with η(x_{i}) = a_{i}. Use the Basic Lemma (for models) to show that if R ⊆ A × A is a logical relation, a ∈ A^{σ} is lambda definable from a_{1} ∈ A^{σ_{1}}, …, a_{k} ∈ A^{σ_{k}}, and R^{σ_{i}}(a_{i}, a_{i}) for each i, then R^{σ}(a, a).

Exercise 8.2.13 Complete Example 8.2.7 by showing that T [[Γ ▷ M : σ]]η = ηM is an acceptable meaning function for T .

Exercise 8.2.14 Let A be a lambda model for some signature without constants. If a logical relation R ⊆ A × A is a permutation at each type, then R is called a hereditary permutation (see Exercise 8.2.3). We say that an element a ∈ A^{σ} is permutation-invariant if R(a, a) for every hereditary permutation R ⊆ A × A. Show that for every closed term M, its meaning A[[M]] in A is permutation invariant.

Exercise 8.2.15 Let A be the full classical hierarchy over a signature with single type constant b, with A^{b} = {0, 1}.

(a) Find some function f ∈ A^{b → b} that is permutation invariant (see Exercise 8.2.14), but not the meaning of a closed lambda term. You may assume that every term has a unique normal form.

(b) Show that if f ∈ A^{b → b} has the property that R(f, f) for every logical relation R ⊆ A × A, then f is the meaning of a closed lambda term. (This is not true for all types, but that is tricky to prove.)

Exercise 8.2.16 Prove the basic lemma for combinatory algebras. More specifically show that if R ⊆ A × B is a logical relation over combinatory algebras A and B and η_{a} and η_{b} are related environments with η_{a}, η_{b} ⊧ Γ, then

R(A[[Γ ▷ M : σ]]η_{a}, B[[Γ ▷ M : σ]]η_{b})

for every typed combinatory term Γ ▷ M : σ. (Do not consider it part of the definition of logical relation that R(K, K) and R(S, S) for combinators K and S of each type.)

8.2.3 Partial functions and theories of models

A logical relation R ⊆ A × B is called a logical partial function if each R^{σ} is a partial function from A^{σ} to B^{σ}, i.e.,

R^{σ}(a, b_{1}) and R^{σ}(a, b_{2}) implies b_{1} = b_{2}.

Logical partial functions are related to the theories of typed lambda models by the following lemma.

Lemma 8.2.17 If R ⊆ A × B is a logical partial function from model A to model B, then Th(A) ⊆ Th(B).

Proof Without loss of generality, we will only consider equations between closed terms. Let R ⊆ A × B be a partial function and suppose A[[M]] = A[[N]] for closed M, N. Writing R(·) as a function, we have

R(A[[M]]) = B[[M]] and R(A[[N]]) = B[[N]]

by the Basic Lemma. Thus B[[M]] = B[[N]].

By Corollary 4.5.23 (completeness for the pure theory of β, η-conversion) we know there is a model A satisfying Γ ▷ M = N : σ iff ⊢ Γ ▷ M = N : σ. Since the theory of this model is contained in the theory of every other model, we may show that a model B has the same theory by constructing a logical partial function R ⊆ B × A. This technique was first used by Friedman to show that β, η-conversion is complete for the full set-theoretic type hierarchy over any infinite ground types [Fri75, Sta85a].

Corollary 8.2.18 Let A be a model of the pure theory of β, η-conversion. If R ⊆ B × A is a logical partial function and B is a model, then Th(B) = Th(A).

We use Friedman’s technique, and extensions, in Section 8.4 to show completeness for full settheoretic, recursive and continuous models.

Since logical partial functions are structure-preserving mappings, it is tempting to think of logical partial functions as the natural generalization of homomorphisms. This often provides useful intuition. However, the composition of two logical partial functions need not be a logical relation. It is worth noting that for a fixed model A and environment η, the meaning function A[[ ]]η from T to A is not necessarily a logical relation. In contrast, meaning functions in algebra are always homomorphisms.

Exercise 8.2.19 Find logical partial functions R ⊆ A × B and S ⊆ B × C whose composition S ∘ R = {S^{σ} ∘ R^{σ}} ⊆ A × C is not a logical relation. (Hint: Try C = A and S = R^{−1} .)

8.2.4 Logical partial equivalence relations

Another useful class of logical relations are the logical partial equivalence relations (logical per’s), which have many of the properties of congruence relations. If we regard typed applicative structures as multi-sorted algebras, we may see that logical partial equivalence relations are somewhat more than congruence relations. Specifically, any logical per R is a congruence, since R is an equivalence relation closed under application, but R must also be closed under lambda abstraction.

Before looking at the definition of logical partial equivalence relation, it is worth recalling the definition of partial equivalence relation from Section 5.6.1. The first of two equivalent definitions is that a partial equivalence relation on a set A is an equivalence relation on some subset of A, i.e., a pair ⟨A′, R⟩ with A′ ⊆ A and R ⊆ A′ × A′ an equivalence relation. However, because R determines A′ = { a | R(a, a) } uniquely and R is an equivalence relation on A′ iff R is symmetric and transitive on A, we may give a simpler definition.

A logical partial equivalence relation on A is a logical relation R ⊆ A × A such that each R^{σ} is symmetric and transitive. We say a partial equivalence relation is total if each R^{σ} is reflexive, i.e., R^{σ}(a, a) for every a ∈ A^{σ}. From the following lemma, we can see that there are many examples of partial equivalence relations.

Lemma 8.2.20 Let R ⊆ A × A be a logical relation. If R^{b} is symmetric and transitive, for each type constant b, then every R^{σ} is symmetric and transitive.

The proof is given as Exercise 8.2.21.

Intuitively, this lemma shows that being a partial equivalence relation is a “hereditary” property; it is inherited at higher types. In contrast, being a total equivalence relation is not. Specifically, there exist logical relations which are total equivalence relations for each type constant, but not total equivalence relations at every type. This is one reason for concentrating on partial instead of total equivalence relations.

Exercise 8.2.21 Prove Lemma 8.2.20 for λ^{→} by induction on type expressions.

Exercise 8.2.22 Find a λ^{→} Henkin model A and logical relation R ⊆ A × A such that R^{b} is reflexive, symmetric and transitive, for each type constant b, but some R^{σ} is not reflexive. (Hint: Almost any model will do.)

Exercise 8.2.23 Let Σ be a signature with type constants B = {b_{0}, b_{1}, …} and (for simplicity) no term constants. Let D be a partial combinatory algebra and let A_{D} be a λ^{×,→} combinatory algebra for signature Σ constructed using subsets of D as in Section 5.6.2. Let R ⊆ A_{D} × A_{D} be any logical partial equivalence relation. Show that for all types σ and τ, the product per R^{σ} × R^{τ} ⊆ D is identical to the relation R^{σ × τ}, and similarly for R^{σ → τ}. (Hint: There is something to check here, since the definition of R^{σ × τ} depends on A^{σ × τ} but, regarding R^{σ} and R^{τ} as pers over D, the definition of R^{σ} × R^{τ} does not.)

8.2.5 Quotients and extensionality

If R is a logical partial equivalence relation over applicative structure A, then we may form a quotient structure A/R of equivalence classes from A. This is actually a “partial” quotient, since some elements of A may not have equivalence classes with respect to R. However, to simplify terminology, we will just call A/R a “quotient.” One important fact about the structure A/R is that it is always extensional. Another is that under certain reasonable assumptions, A/R will be a model with the meaning of each term in A/R equal to the equivalence class of its meaning in A.

Let R ⊆ A × A be a logical partial equivalence relation on the applicative structure A = ⟨{A^{σ}}, {App^{σ,τ} }, Const}⟩. The quotient applicative structure

A/R = ⟨{A^{σ}/R}, {App^{σ,τ} /R}, Const/R⟩

is defined as follows. If R^{σ}(a, a), then the equivalence class [a]_{R} of a with respect to R is defined by

[a]_{R} = { a′ | R(a, a′) }.

Note that a ∈ [a]_{R}. We let A^{σ}/R = { [a]_{R} | R^{σ}(a, a) } be the collection of all such equivalence classes and define application on equivalence classes by

(App^{σ,τ} /R) [a] [b] = [App^{σ,τ} a b]

The map Const/R interprets each constant c as the equivalence class [Const(c)]_{R}. This completes the definition of A/R. It is easy to see that application is well-defined: if R^{σ → τ} (a, a′) and R^{σ}(b, b′), then since R is logical, we have R^{τ} (App^{σ,τ} a b, App^{σ,τ} a′ b′).

Lemma 8.2.24 If R ⊆ A × A is a logical partial equivalence relation, then A/R is an extensional applicative structure.

Proof Let [a_{1}], [a_{2}] ∈ A^{σ → τ} /R and suppose that for every [b] ∈ A^{σ}/R, we have App/R [a_{1}] [b] = App/R [a_{2}] [b]. This means that for every b_{1}, b_{2} ∈ A^{σ}, we have R^{σ}(b_{1}, b_{2}) ⊃ R^{τ} (App a_{1} b_{1}, App a_{2} b_{2}). Since R is logical, this gives us R^{σ → τ} (a_{1}, a_{2}), which means that [a_{1}] = [a_{2}]. Thus A/R is extensional.

A special case of this lemma is the extensional collapse, A^{E}, of an applicative structure A; this is also called the Gandy hull of A, and appears to have been discovered independently by Zucker [Tro73] and Gandy [Gan56]. The extensional collapse A^{E} is defined as follows. Given A, there is at most one logical relation R with

R^{b}(a_{1}, a_{2}) iff a_{1} = a_{2} ∈ A^{b}

for each type constant b. (Such an R is guaranteed to exist when the type of each constant is either a type constant or first-order function type.) If there is a logical relation R which is the identity relation for all type constants, then we define A^{E} = A/R.

Corollary 8.2.25 (Extensional Collapse) Let A be an applicative structure for signature Σ. If there is a logical relation R that is the identity relation on each type constant, then the extensional collapse A^{E} is an extensional applicative structure for Σ.

In some cases, A/R will not only be extensional, but also a Henkin model. This will be true if A is a model to begin with. In addition, since A/R is always extensional, we would expect to have a model whenever A has “enough functions,” and β -equivalent terms are equivalent modulo R. If A[[ ]] is an acceptable meaning function, then this will guarantee that A has enough functions. When we have an acceptable meaning function, we can also express the following condition involving β -equivalence. We say R satisfies (β) with respect to A[[ ]] if, for every term Γ, x: σ ▷ M : τ and environment η ⊧ Γ, x: σ with R^{Γ,x:σ}(η, η), we have

R(A[[Γ, x: σ ▷ (λx: σ.M)x]]η, A[[Γ, x: σ ▷ M]]η).

It follows from properties of acceptable meaning function A that if R satisfies (β), then R relates β -equivalent terms (Exercise 8.2.28) and R is admissible (Exercise 8.2.29). In addition, if A is a combinatory algebra with standard meaning function as described in Example 8.2.8, then by Exercise 8.2.16 and the equational properties of combinators, every R over A satisfies (β).

To describe the meanings of terms in A/R, we will associate an environment η_{R} for A/R with each environment η for A with R^{Γ}(η, η). We define η_{R} by

η_{R}(x) = [η(x)]_{R},

and note that η ⊧ Γ iff η_{R} ⊧ Γ. Using these definitions, we can give useful conditions which imply that A/R is a model, and characterize the meanings of terms in A/R.

Lemma 8.2.26 (Quotient Models) Let R ⊆ A × A be a partial equivalence relation over applicative structure A with acceptable meaning function A[[ ]], and suppose that R satisfies (β). Then A/R is a model such that for any A-environment η ⊧ Γ with R^{Γ}(η, η), we have

(A/R)[[Γ ▷ M : σ]]η_{R} = [A[[Γ ▷ M : σ]]η]_{R}.

In other words, under the hypotheses of the lemma, the meaning of a term Γ ▷ M : σ in A/R is the equivalence class of the meaning of Γ ▷ M : σ in A, modulo R. Lemma 8.2.26 is similar to the “Characterization Theorem” of [Mit86c], which seems to be the first use of this idea (see Theorem 9.3.46). Proof We use induction on the structure of terms. By Exercise 8.2.29, R is admissible. It follows from the general version of the Basic Lemma that the equivalence class [A[[Γ ▷ M : σ]]η]_{R} of the interpretation of any term in A is nonempty. This is essential to the proof.

For any variable Γ ▷ x : σ, it is clear that

(A/R)[[Γ ▷ x : σ]]η_{R} = η_{R}(x) = [η(x)]_{R} = [ A[[Γ ▷ x : σ]]η]_{R}

by definition of η_{R} and acceptability of A[[ ]]. The case for constants is similarly straightforward. The application case is also easy, using the definition of application in A/R. For the abstraction case, recall that

(A/R)[[Γ ▷ λx: σ.M : σ → τ]]η_{R} = f,

where, by definition, f satisfies the equation

(App/R) f [a]_{R} = (A/R)[[Γ, x: σ ▷ M : τ]]η_{R}[x ↦ [a]]

for all [a]_{R} ∈ A^{σ}/R^{σ}. We show that [A[[Γ ▷ λx: σ.M : σ → τ]]η]_{R} satisfies the equation for f, and hence the meaning of Γ ▷ λx: σ.M : σ → τ exists in A/R. Since A/R is extensional by Lemma 8.2.24, it follows that A/R is a Henkin model.

For any [a]_{R} ∈ A^{σ}/R^{σ}, we have

(App/R) [A[[Γ ▷ λx: σ.M : σ → τ]]η]_{R} [a]_{R} = [App (A[[Γ ▷ λx: σ.M : σ → τ]]η) a]_{R}

by definition of application in A/R. Using the definition of acceptable meaning function, it is easy to see that

A[[Γ ▷ λx: σ.M : σ → τ]]η = A[[Γ, x: σ ▷ λx: σ.M : σ → τ]]η[x ↦ a]

since x is not free in λx: σ.M. Since a = A[[Γ, x: σ ▷ x : σ]]η[x ↦ a], it follows from the definition of acceptable that

App (A[[Γ ▷ λx: σ.M : σ → τ]]η) a = A[[Γ, x: σ ▷ (λx: σ.M)x : τ]]η[x ↦ a]

Therefore, using the assumption that R satisfies (β), we may conclude that

[App (A[[Γ ▷ λx: σ.M : σ → τ]]η) a]_{R} = [A[[Γ, x: σ ▷ M : τ]]η[x ↦ a] ]_{R}

By the induction hypothesis, it follows that [A[[Γ ▷ λx: σ.M : σ → τ]]η]_{R} satisfies the equation for f. This proves the lemma.

A straightforward corollary, with application to per models, is that the quotient of any combinatory algebra by a partial equivalence relation is a Henkin model.

Corollary 8.2.27 Let A be a combinatory algebra and R ⊆ A × A a logical partial equivalence relation. Then A/R is a Henkin model, with the meaning of term Γ ▷ M : σ the equivalence class

A/R[[Γ ▷ M : σ]]η_{R} = [ A[[Γ ▷ cl(M) : σ]]η]_{R}

of the interpretation of the combinatory term cl(M) in A.

The proof is simply to apply Lemma 8.2.26 to combinatory algebras, with acceptable meaning function as described in Example 8.2.8, noting that by Exercise 8.2.16 and the equational properties of combinators, every relation over A satisfies (β).

Corollary 8.2.27 implies that any hierarchy of partial equivalence relations over a partial combinatory algebra (see Sections 5.6.1 and 5.6.2) forms a Henkin model. More specifically, for any partial combinatory algebra D, any hierarchy of pers over D forms a logical partial equivalence relation over a typed (total) combinatory algebra A_{D}, as described in Exercise 8.2.23. Therefore, we may show that pers over D form a Henkin model by showing that the quotient A_{D}/R of a combinatory algebra by a logical partial equivalence relation R ⊆ A_{D} × A_{D} is a Henkin model. This is immediate from Corollary 8.2.27. In addition, Corollary 8.2.27 shows that the interpretation of a lambda term is the equivalence class of its translation into combinators. Since the combinators of A_{D} are exactly the untyped combinators of D, according to the proof of Lemma 5.6.8, it follows that the meaning of a typed term in A_{D}/R is the equivalence class of the meaning of its translation into untyped combinators in D.

Exercise 8.2.28 Show that if R satisfies (β) with respect to A[[ ]] then, for every pair of terms Γ, x: σ ▷ M : τ and Γ ▷ N : σ, and environment η ⊧ Γ with R^{Γ}(η, η), we have

R(A[[Γ ▷ (λx: σ.M)N : τ]]η, A[[Γ ▷ [N/x]M : τ]]η).

Exercise 8.2.29 Show that if R satisfies (β) with respect to A[[ ]], then R is admissible.

Exercise 8.2.30 Let A be an applicative structure and let {x_{1}: σ_{1}, …, x_{k}: σ_{k}} ▷ M : τ be a term without lambda abstraction. An element a ∈ A^{σ_{1} →... → σ_{k} → τ} represents M if A ⊧ {x_{1}: σ_{1}, …, x_{k}: σ_{k}} ▷ ax_{1} … x_{k} = M : τ, using a as a constant denoting a. Note that since M contains only applications, this equation makes sense in any applicative structure. Show that if R ⊆ A × A is a logical partial equivalence relation and a represents Γ ▷ M : σ in A, then [a] represents Γ ▷ M : σ in A/R.

8.3 Proof-Theoretic Results

8.3.1 Completeness for Henkin models

In universal algebra, we may prove equational completeness (assuming no sort is empty) by showing that any theory E is a congruence relation on the term algebra T , and noting that T /E satisfies an equation M = N iff M = N ∈ E. We may give similar completeness proofs for typed lambda calculus, using logical equivalence relations in place of congruence relations. We will illustrate the main ideas by proving completeness for models without empty types. A similar proof is given for Henkin models with possibly empty types in Exercise 8.3.3. It is also possible to present a completeness theorem for Kripke models (Section 7.3) in this form, using a Kripke version of logical relations.

Throughout this section, we let T be the applicative structure of terms typed using infinite type assignment H, with meaning function T [[ ]] defined by substitution. (These are defined in Example 8.2.7.) We assume H provides infinitely many variables of each type, so each T^{σ} is infinite. If E is any set of equations, we define the relation R_{E} = {R^{σ}} over T × T by taking

R^{σ}(M, N) iff E ⊢ Γ ▷ M = N : σ for some finite Γ ⊆ H.

Note that since E ⊢ x: σ ▷ x = x : σ for each x: σ ∈ H, no R^{σ} is empty.

Lemma 8.3.1 For any theory E, the relation R_{E} ⊆ T × T is a logical equivalence relation.

Proof It is easy to see that R = R_{E} is an equivalence relation. To show that R is logical, suppose that R^{σ → τ} (M, M′) and R^{σ}(N, N′). Then E ⊢ Γ_{1} ▷ M = M′ : σ → τ and E ⊢ Γ_{2} ▷ N = N′ : σ, for some Γ_{1}, Γ_{2} ⊆ H. By (add hyp) and rule (μ) we have E ⊢ Γ_{1} ∪ Γ_{2} ▷ MN = M′N′ : τ. Therefore R^{τ} (MN, M′N′). It remains to show that if E ⊢ Γ ▷ MN = M′N′ : τ for every N, N′ with E ⊢ Γ ▷ N = N′ : σ, then E ⊢ Γ ▷ M = M′ : σ → τ. This is where we use the assumption that H provides infinitely many variables of each type.

Let x be a variable that is not free in M or M′ and with x: σ ∈ H. Since E ⊢ Γ, x: σ ▷ x = x : σ, we have E ⊢ Γ, x: σ ▷ Mx = M′x : τ with Γ, x: σ ⊆ H. By (ξ), we have

E ⊢ Γ ▷ λx: σ.Mx = λx: σ.M′x : σ → τ.

We now apply (η) to both sides of this equation to derive E ⊢ Γ ▷ M = M′ : σ → τ. By reflexivity, R respects constants. This proves the lemma.

From Lemma 8.2.26, and the straightforward observation that any R_{E} satisfies (β), we can form a quotient model from any theory. This allows us to prove “least model” completeness for Henkin models without empty types.

Theorem 8.3.2 (Henkin completeness without empty types) Let E be any theory closed under (nonempty), and let A = T /R_{E}. Then A is a Henkin model without empty types satisfying precisely the equations belonging to E.

Proof By Lemma 8.3.1, the theory E determines a logical equivalence relation R_{E} over T . Since R_{E} clearly satisfies (β), the relation R_{E} is admissible by Exercise 8.2.29. Let us write R for R_{E} and A for T /R. By Lemma 8.2.26, A is a model with A[[Γ ▷ M : σ]]η_{R} = [ηM]_{R}, for every T -environment (substitution) η satisfying Γ. It remains to show that A satisfies precisely the equations belonging to E.

Without loss of generality, we may restrict our attention to closed terms. The justification for this is that it is easy to prove the closed equation

∅ ▷ λx_{1}: σ_{1}…. λx_{k}: σ_{k}.M = λx_{1}: σ_{1}…. λx_{k}: σ_{k}.N : σ_{1} → … → σ_{k} → τ

from the equation

{x_{1}: σ_{1}…. x_{k}: σ_{k}} ▷ M = N : τ

between open terms, and vice versa. Let η be the identity substitution. Then for any closed equation ∅ ▷ M = N : τ ∈ E, since η_{R} ⊧ ∅, we have

A[[∅ ▷ M : τ]]η_{R} = [M]_{R} = [N]_{R} = A[[∅ ▷ N : τ]]η_{R}

This shows that A satisfies every equation in E. Conversely, if A satisfies ∅ ▷ M = N : τ, then A certainly must do so at environment η_{R}. This implies [M]_{R} = [N]_{R}, which means E ⊢ Γ ▷ M = N : τ for some Γ ⊆ H. Since M and N are closed, we have ∅ ▷ M = N : τ ∈ E by rule (nonempty). This proves the theorem.

Exercise 8.3.3 A quotient construction, like the one in this section for models without empty types, may also be used to prove deductive completeness of the extended proof system with proof rules (empty I ) and (empty E) for models that may have empty types. (This system is described in Sections 4.5.5 and 4.5.6.) This exercise begins the model construction and asks you to complete the proof. To prove deductive completeness, we assume that Γ_{0} ▷ M_{0} = N_{0} : σ_{0} is not provable from some set E of typed equations and construct a model A = T_{H}/R_{E} with A ⊧ E, but A |̸= Γ_{0} ▷ M_{0} = N_{0} : σ_{0} . The main new idea in this proof is to choose an infinite set of typed variables carefully so that some types may be empty.

We decide which types to make empty by constructing an infinite set H of typing hypotheses of the form x: σ and emptiness assertions of the form empty(σ) such that

(i) Γ_{0} ⊆ H,

(ii) for every type σ, we either have empty(σ) ∈ H or we have x: σ ∈ H for infinitely many variables x (but not both),

(iii) for every finite Γ ⊆ H containing all the free variables of M_{0} and N_{0} , the equation Γ ▷ M_{0} = N_{0} : σ_{0} is not provable from E.

The set H is constructed in infinitely many stages, starting from H_{0} = Γ_{0} . If τ_{0}, τ_{1}, … is an enumeration of all type expressions, then H_{i+1} is determined from H_{i} by looking at equations of the form Γ, x: τ_{i} ▷ M_{0} = N_{0} : σ_{0} , where Γ ⊆ H_{i} and x is not in H_{i} and not free in M_{0} or N_{0} . If

E ⊢^{(emptyI ,E)} Γ, x: τ_{i} ▷ M_{0} = N_{0} : σ_{0}

for any finite Γ ⊆ H_{i} with the above equation well-formed, then we let

H_{i+1} = H_{i} ∪ {empty(τ_{i})}.

Otherwise, we take

H_{i+1} = H_{i} ∪ { x: τ_{i} | infinitely many fresh x }.

Let H be the union of all the H_{i}.

Given H, the model A = T_{H}/R_{E} is defined as in this section. As described in Example 4.5.1, T_{H} is an applicative structure for any H. However, while Lemma 8.3.1 does not require (nonempty), the proof does assume that H provides infinitely many variables of each type.

(a) Show that properties (i) and (ii) hold for H.

(b) Show that R_{E} is a logical equivalence relation, re-proving only the parts of Lemma 8.3.1 that assume H provides infinitely many variables of each type. (Hint: You will need to use proof rule (empty I ).)

(c) Show that A does not satisfy Γ_{0} ▷ M_{0} = N_{0} : σ_{0} . (This is where you need to use rule (empty E). The proof that A satisfies E proceeds as before, so there is no need for you to check this.)

8.3.2 Normalization

Logical relations may also be used to prove various properties of reduction on typed terms. In this section, we show that every λ^{→} term is strongly normalizing. More precisely, we show that for every typed term Γ ▷ M : σ, we have SN (M), where SN is defined by

SN (M) iff there is no infinite sequence of β, η-reductions from M.

While the proof works for terms with term constants, we state the results without term constants to avoid confusion with more general results in later sections. We generalize the argument to other reduction properties and product types in the next section and consider reductions associated with constants such as + and fix in Section 8.3.4.

The normalization proof for λ^{→} has three main parts:

1. Define a logical predicate P on the applicative structure of terms.

2. Show that P^{σ}(M) implies SN (M).

3. Show that P is admissible, so that we may use the Basic Lemma to conclude that P^{σ}(M) holds for every well-typed term Γ ▷ M : σ.

Since the Basic Lemma is proved by induction on terms, the logical relation P is a kind of “induction hypothesis” for proving that all terms are strongly normalizing. To make the outline of the proof as clear as possible, we will give the main definition and results first, postponing the proofs to the end of the section.

Let T = T_{H} be an applicative structure of terms, as in Examples 4.5.1 and 8.2.7, where H provides infinitely many variables of each type. We define the logical predicate (unary logical relation) P ⊆ T by taking P^{b} to be all strongly normalizing terms, for each type constant b, and extending to function types by

P^{σ → τ} (M) iff ∀N ∈ T^{σ}. P^{σ}(N) ⊃ P^{τ} (MN).

It is easy to see that this predicate is logical. (If we have a signature with term constants, then it follows from Lemma 8.3.4 below that P is logical, as long as only β, η-reduction is used in the definition of SN.) The next step is to show that P contains only strongly normalizing terms. This is a relatively easy induction on types, as long as we take the correct induction hypothesis. The hypothesis we use is the conjunction of (i) and (ii) of the following lemma.

Lemma 8.3.4 For each type σ, the predicate P^{σ} satisfies the following two conditions.

(i) If xM_{1} … M_{k} ∈ T^{σ} and SN (M_{1}), … SN (M_{k}), then P^{σ}(xM_{1} … M_{k}).

(ii) If P^{σ}(M) then SN (M).

The main reason condition (i) is included in the lemma is to guarantee that each P^{σ} is non-empty, since this is used in the proof of condition (ii). Using Lemma 8.2.11, we may show that the logical predicate P is admissible.

Lemma 8.3.5 The logical predicate P ⊆ T is admissible.

From the two lemmas above, and the Basic Lemma for logical relations, we have the following theorem.

Theorem 8.3.6 (Strong Normalization) For every well-typed term Γ▷M : σ, we have SN (M).

Proof of Theorem 8.3.6 Let Γ ▷ M : σ be a typed term and consider the applicative structure T defined using variables from H with Γ ⊆ H. Let η_{0} be the environment for T with η_{0}(x) = x for all x. Then since T [[ ]] is acceptable and the relation P is admissible, by Lemma 8.3.5, we have P^{σ}( T [[Γ ▷ M : σ]]η_{0} ), or, equivalently, P^{σ}(M). Therefore, by Lemma 8.3.4, we conclude SN (M).

Proof of Lemma 8.3.4 We prove both conditions simultaneously using induction on types. We will only consider variables in the proof of (i), since the constant and variable cases are identical. For a type constant b, condition (i) is straightforward, since SN (xM_{1} … M_{k}) whenever SN (M_{i}) for each i. Condition (ii) follows trivially from the definition of P. So, we move on to the induction step.

For condition (i), suppose xM_{1} … M_{k} ∈ T^{σ → τ} and for each M_{i}, we have SN (M_{i}). Let N ∈ T^{σ} with P^{σ}(N). By the induction hypothesis (ii) for type σ, we have SN (N). Therefore, by the induction hypothesis (i) for type τ, we have P^{τ} (xM_{1} … M_{k}N). Since this reasoning applies to every N ∈ P^{σ}, we conclude that P^{σ → τ} (xM_{1} … M_{k}).

We now consider condition (ii) for type σ → τ. Suppose M ∈ T^{σ → τ} with P^{σ → τ} (M) and x ∈ T^{σ}. By the induction hypothesis (i) we have P^{σ}(x) and so P^{τ} (Mx). Applying the induction hypothesis (ii) we have SN (Mx). However, this implies SN (M), since any infinite sequence of reductions from M would give us an infinite sequence of reductions from Mx. Proof of Lemma 8.3.5 This lemma is proved using Lemma 8.2.11, which gives us a straightforward test for each type constant. To show that P is admissible, it suffices to show that for each type constant b, term N and term ([N/x]M)N_{1} … N_{k} of type b,

SN (N) and SN (([N/x]M)N_{1} … N_{k}) imply SN ((λx: σ.M)NN_{1} … N_{k}).

With this in mind, we assume SN (N) and SN (([N/x]M)N_{1} … N_{k}) and consider the possible reductions from (λx: σ.M)NN_{1} … N_{k}. It is clear that there can be no infinite sequences of reductions solely within N, because SN (N). Since ([N/x]M)N_{1} … N_{k} is strongly normalizing, we may conclude SN (M), and SN (N_{1}), …, SN (N_{k}), since otherwise we could produce an infinite reduction sequence from ([N/x]M)N_{1} … N_{k} by reducing one of its subterms. Therefore, if there is any infinite reduction sequence with β -reduction occurring at the left, the reduction sequence must have an initial segment of the form

(λx: σ.M)NN_{1} … N_{k} → → (λx: σ.M′)N′N′_{1} … N′_{k} → ([N′/x]M′)N′_{1} … N′_{k} → → …,

where M → → M′, N → → N′ and N_{i} → → N′_{i} for 1 ≤ i ≤ k. But then clearly we may reduce

([N/x]M)N_{1} … N_{k} → → ([N′/x]M′)N′_{1} … N′_{k} → → …

as well, giving us an infinite sequence of reductions from ([N/x]M)N_{1} … N_{k}. The other possibility is an infinite reduction sequence with η-reduction occurring at the left, which would have the form

(λx: σ.M)NN_{1} … N_{k} → → (λx: σ.M′x)N′N′_{1} … N′_{k} → M′N′N′_{1} … N′_{k} → → …

But since the last reduction shown could also have been carried out using β -reduction, we have already covered this possibility above. Since no infinite reduction sequence is possible, the lemma is proved.

Exercise 8.3.7 We can show weak normalization of β -reduction directly, using an argument devised by A.M. Turing sometime between 1936 and 1942 [Gan80]. For this exercise, the degree of a β -redex (λx: σ. M)N is the length of the type σ → τ of λx: σ. M when written out as a string of symbols. The measure of a term M is the pair of natural numbers ⟨i, j⟩ such that the redex of highest degree in M has degree i, and there are exactly j redexes of degree i in M. These pairs can be ordered lexicographically by ⟨i, j⟩ < ⟨i′, j′⟩ iff either i < i′ or i = i′ and j < j′. The main idea is to show that every term not in normal form can be reduced in a way that decreases the measure of the term.

(a) Show that if (λx: σ. M)N has degree n, and no redex within this term has degree greater than n − 1, then [N/x]M has no redex of degree greater than n − 1.

(b) Show that for any term M not in normal form, there is some reduction M → M′ such that the measure of M′ is less than the measure of M. Use this to conclude that every typed lambda term must have at least one normal form.

(c) Show that this assignment of measures to terms does not prove strong normalization by finding a term M and reduction M → M′ with the measure of M′ greater than the measure of M.

8.3.3 Confluence and other reduction properties

We may also prove confluence and other properties of typed reduction using logical relations. While it is well-known that β, η-reduction is confluent on untyped lambda terms, this does not immediately carry over to typed reduction; some proof is necessary. In particular, with variables distinguished by type, α-conversion on typed terms is slightly different from untyped α-conversion. For this reason, β, η-reduction is not confluent on un-type-checked terms with typed variables, as discussed in Section 4.4.2. We will prove confluence using logical relations, discuss alternative proofs, and extend the method to λ^{×,→} at the end of the section.

Many parts of the confluence proof are identical to the proof of strong normalization. Rather than simply repeat the lemmas of the last section, we will state a general theorem about properties of typed terms, based on [Mit86c]. To be precise, let S be a property of typed lambda terms, which we may regard as a typed predicate S = {S^{σ}} on a term applicative structure T . (We do not assume that S is logical.) We say S is type-closed if the following three conditions are satisfied.

(a) If S(M_{1}), …, S(M_{k}), then S(xM_{1} … M_{k}), where x is any variable of the appropriate type,

(b) If S^{τ} (Mx) holds for every variable x of type σ, then S^{σ → τ} (M),

(c) If S^{σ}(N) and S^{b}(([N/x]M)N_{1} … N_{k}), then S^{b}((λx: σ.M)NN_{1} … N_{k}) for each type constant b.

In verifying that a particular predicate satisfies (b), we generally assume S(Mx) for x not free in M and show S(M). (It easy to see that if there is some x such that S^{τ} (Mx) implies S^{σ → τ} (M), then when S^{τ} (Mx) holds for all x, we must have S^{σ → τ} (M).)

Theorem 8.3.8 If S is any type-closed property of typed λ^{→} terms, then S(M) for every term Γ ▷ M : σ.

Proof The proof of this theorem follows the proof of strong normalization in the last section exactly, since all of the properties of strong normalization used in Section 8.3.2 are included in the definition of type-closed property. More specifically, we construct predicate P ⊆ T from S and prove a variant of Lemma 8.3.4 with SN replaced by S in statements (i) and (ii) of the lemma. This shows that P is logical and that P(M) implies S(M). It is straightforward to show that P is admissible, using Lemma 8.2.11 as in the proof of Lemma 8.3.5, since the condition needed on S is part (c) of the definition of type-closed. It follows by the Basic Lemma that for any Γ ▷ M : σ, we have P^{σ}(M) and hence S^{σ}(M).

We may obtain strong normalization and confluence as relatively straightforward corollaries. In addition, as pointed out in [Sta85b], we may also prove termination of standard reduction, completeness of standard reduction and η-postponement, which are traditional topics in untyped lambda calculus, using logical relations. (See Exercise 8.3.13.) These are all corollaries of Theorem 8.3.8. In the rest of this section, we will prove confluence of β, η-reduction for λ^{→} and show how the method may be extended to λ^{×,→}.

Confluence for λ^{→}

We may regard confluence as a predicate on typed λ^{→} terms by defining

CR(M) iff ∀M_{1}, M_{2}[ M → → M_{1} ∧ M → → M_{2} ⊃ ∃N. M_{1} → → N ∧ M_{2} → → N].

In verifying that CR is type-closed, the most difficult condition is (b). While it is easy to see that SN (Mx) ⊃ SN (M), it is not immediate that CR(Mx) ⊃ CR(M), since there may be reductions of Mx that do not apply to M. A general property that suggests confluence is more subtle than termination is that when a set of reduction rules is terminating, every subset must also be terminating. However, not every subset of a confluent system is confluent.

Lemma 8.3.9 The predicate CR is type-closed.

Proof Condition (a) is straightforward, since CR(xM_{1} … M_{k}) whenever CR(M_{i}) for each i.

For condition (b), we let x be any variable not free in M and assume CR(Mx). We must prove CR(M). Suppose M → → M_{1} and M → → M_{2} . Then clearly Mx → → M_{1}x and Mx → → M_{2}x, so by CR(Mx) there is a term N with M_{1}x → → N and M_{2}x → → N. We will use these reductions to construct a common reduct of M_{1} and M_{2} .

There are two cases to consider for the reduction path M_{1}x → → N. The first case is that no reduction involves x, which implies N ≡ N′x and M_{1} → → N′. The second case is that

M_{1}x → → (λy: ρ.M_{3})x →^{β} [x/y]M_{3} → → N.

It is easy to see that in this case, λy: ρ.M_{3} → → λx: σ.N, since the typing rules guarantee σ = ρ. Therefore, we have

M_{1} → → λy: ρ.M_{3} → → λx: σ.N.

The same two cases apply for M_{2}x → → N.

We now find a common reduct for M_{1} and M_{2} , depending on the forms of the reduction paths M_{1}x → → N and M_{2}x → → N. If neither involves x, then we have M_{1} → → N′ and M_{2} → → N′, while if both paths contain a reduction with x, we have M_{1} → → λx: σ.N and M_{2} → → λx: σ.N. The remaining case is M_{1} → N′ and M_{2} → → λx: σ.N ≡ λx: σ.N′x. Recall that x was chosen not to occur in M, and so x cannot be free in the reduct N′ of M. Therefore λx: σ.N′x →^{η} N′, and condition (b) is established.

To prove condition (c), we assume CR(([N/x]M)N_{1} … N_{k}) and show CR((λx: σ.M)NN_{1} … N_{k}). The main idea is to show that if P may be obtained from (λx: σ.M)NN_{1} … N_{k} by reduction, then we may reduce P to some term that may be obtained from ([N/x]M)N_{1} … N_{k}. This gives us CR((λx: σ.M)NN_{1} … N_{k}) as a consequence of CR(([N/x]M)N_{1} … N_{k}).

There are three cases to consider. First, suppose we have a reduction sequence

(λx: σ.M)NN_{1} … N_{k} → → (λx: σ.M′)N′N′_{1} … N′_{k}

which does not involve λx. We wish to show that (λx: σ.M′)N′N′_{1} … N′_{k} and ([N/x]M)N_{1} … N_{k} reduce to a common term. But clearly both reduce to ([N′/x]M′)N′_{1} … N′_{k}. The second case is that we have a reduction sequence

(λx: σ.M)NN_{1} … N_{k} → → (λx: σ.M′)N′N′_{1} … N′_{k} →^{β} ([N′/x]M′)N′_{1} … N′_{k} → → P

which eliminates λx by β -reduction. Reasoning as above, we also have ([N/x]M)N_{1} … N_{k} → → P. The last possibility is a reduction sequence

(λx: σ.M)NN_{1} … N_{k} → → (λx: σ.M′x)N′N′_{1} … N′_{k} →^{η} M′N′N′_{1} … N′_{k} → → P

eliminating λx by η-reduction. In this case, we have [N/x]M → → M′N′ and so ([N/x]M)N_{1} … N_{k} → → P. This proves the lemma.

Combining Lemma 8.3.9 with Theorem 8.3.8, we have confluence of β, η-reduction.

Theorem 8.3.10 (Confluence) β, η-Reduction is confluent on typed lambda terms.

This is not the only way to prove that typed β, η-reduction is confluent. An alternative proof involves the subject reduction theorem (Lemma 4.4.16), and inspection the proof of confluence for untyped lambda calculus. Specifically, one begins by observing that if the variables of untyped lambda calculus are partitioned into infinite disjoint sets, and α-conversion is restricted to variables in the same equivalence class, then untyped lambda calculus remains confluent. Confluence of typed reduction then follows by the subject reduction theorem.

Another proof of confluence involves verifying local confluence directly, by case analysis. Recall that local confluence, also called the weak Church-Rosser property, is

M → M_{1} ∧ M → M_{2} implies ∃N. M_{1} → → N ∧ M_{2} → → N.

which we regard as a predicate by defining

WCR(M) iff ∀M_{1}, M_{2}. M → M_{1} ∧ M → M_{2} ⊃ ∃N. M_{1} → → N ∧ M_{2} → → N.

By the Newman’s Lemma (Proposition 3.7.32), we may prove confluence by establishing WCR(M) for every well-typed term M. This may be done directly, by a case analysis. On the other hand, if we try to prove local confluence by logical relations, it seems difficult to show directly that WCR is type-closed. The problem lies in condition (c), where the hypothesis that WCR(([N/x]M)N_{1} … N_{k}) does not seem strong enough to show WCR((λz: σ.M)NN_{1} … N_{k}). In contrast, as noted above, this is straightforward for CR .

Since η-reduction is used in verifying condition (b), in the proof of Lemma 8.3.9, the method of logical relations and type-closed properties does not appear to yield confluence of β -reduction alone. However, with β -reduction only, we have termination by the logical relations proof and therefore, by Newman’s Lemma (Proposition 3.7.32), it suffices to check local confluence. This is quite easy for β -reduction alone.

Extension to cartesian products

We may extend Theorem 8.3.8 to λ^{×,→} using an extension of the definition of type-closed to product types. A useful auxiliary concept is an elimination context, which was also mentioned in Exercise 5.4.21. The name comes from the fact that elimination contexts only involves term forms that arise from elimination rules for types. For λ^{×,→}, the elimination forms are application and projection, given in typing rules (→ Elim) and (× Elim). To be precise, we define elimination contexts by the following grammar:

E[ ] ::= [ ] | E[ [ ] M] | E[Proj_{i} [ ] ]

Elimination contexts can be typed according to the kind of term that may be inserted and the type of term produced. We say E[ ] is a σ, τ -context if, whenever M: σ, we have E[M]: τ. It is easy to see from the form of elimination contexts that if E[ ] is a σ, τ -context, then τ must be a subexpression of σ.

As a convenient shorthand, we write S(E[ ]) to mean that S holds for each term that appears in E[ ]. For example, if E[ ] ≡ (Proj_{1}([ ] N_{1}))N_{2} , then S(E[ ]) is short for S^{σ_{1}}(N_{1}) ∧ S^{σ_{2}}(N_{2}).

A property S of λ^{×,→} terms is type-closed if the following conditions are satisfied.

(a) S(E[ ]) implies S^{ρ}(E[x]), for any variable x of the appropriate type,

(b) If S^{τ} (Mx) for every variable x of type σ, then S^{σ → τ} (M),

(c) If S^{b}(E[[N/x]M]) and S^{σ}(N), then S^{b}(E[(λx: σ. M)N]),

(d) If S^{σ_{i}}(Proj_{i}M), for i = 1, 2, then S^{σ_{1} × σ_{2}}(M),

(e) If S^{b}(E[M]) and S^{σ}(N), then S^{b}(E[Proj_{1}⟨M, N⟩]) and S^{b}(E[Proj_{2}⟨N, M⟩]).

We have the following extension of Theorem 8.3.8 to λ^{×,→}.

Theorem 8.3.11 If a property S of λ^{×,→} terms is type-closed, then S(M) holds for every welltyped term M of λ^{×,→}.

Proof Since the proof is similar to the proof of Theorem 8.3.8, many of the details are omitted. We define a typed predicate P = {P^{σ}} by

P^{b}(M)  iff S(M)
P^{σ × τ} (M) iff P^{σ}(Proj_{1}M) and P^{τ} (Proj_{2}M)
P^{σ → τ} (M) iff ∀N. P^{σ}(N) implies P^{τ} (MN)

and show that P(M) implies S(M) by a variant of Lemma 8.3.4. More specifically, we show the two conditions (i) If E[x] ∈ T^{σ} and S(E[ ]) then P^{σ}(E[x]), for any variable x of the appropriate type,

(ii) If P^{σ}(M) then S^{σ}(M).

simultaneously by induction on types. The base case and induction step for function types are as in the proof of Lemma 8.3.4. The induction step for cartesian products is straightforward and left to the reader.

The next step is to prove that P is admissible by an argument similar to Lemma 8.2.11. Specifically, admissible with product types requires that if P^{τ_{1}}(A[[M_{1}]]η) and P^{τ_{2}}(A[[M_{2}]]η), then P^{τ_{1} × τ_{2}}(A[[⟨M_{1}, M_{2}⟩]]η), in addition to the condition on lambda abstractions used as the definition of admissible for λ^{→}. Admissibility may be proved by showing

If P^{ρ}(E[[N/x]M]) and P^{σ}(N), then P^{ρ}(E[(λx: σ. M)N]),
If P^{ρ}(E[M]) and P^{σ}(N), then P^{ρ}(E[Proj_{1}⟨M, N⟩]) and P^{ρ}(E[Proj_{2}⟨N, M⟩]).

by induction on types. The first is the generalization of the induction hypothesis of Lemma 8.2.11 to elimination contexts for λ^{×,→}, while the second is the analogous condition for products. The base case of the induction is immediate from properties (c) and (e) of type-closed S. The induction steps are similar to the proof of Lemma 8.2.11.

Termination and confluence of β, η, proj , sp -reduction on λ^{×,→} terms are shown in Exercises 8.3.14 and 8.3.15.

Exercise 8.3.12 Show by direct argument that under the typing assumptions Γ ▷ x : σ and Γ▷M : τ, if CR(M), then CR(λx: σ.M). Remember that M might have the form M ≡ (λy: ρ.M_{1})x with x ∉ F V (λy: ρ.M_{1}).

Exercise 8.3.13 We say η-postponement holds from M, and write EP(M) if, whenever M → → N, there is some term P with M → →^{β} P and P → →^{η} N. Show that EP is type-closed and conclude, by Theorem 8.3.8, that EP(M) for every λ^{→} term Γ ▷ M : σ.

Exercise 8.3.14 Using Theorem 8.3.11, we can prove termination of β, η, proj , sp -reduction on λ^{×,→} terms by showing that the property SN defined as in Section 8.3.2 (but for β, η, proj , sp - reduction on λ^{×,→} terms) is type-closed. This means we must check conditions (a)–(e) of the definition. Since conditions (a)–(c) are verified essentially as in the proofs of Lemmas 8.3.4 and 8.3.5, this exercise only asks you to prove conditions (d) and (e).

(a) Show that if M: σ_{1} × σ_{2} and SN (Proj_{i}M), for i = 1, 2, then SN (M).

(b) Show that if SN (E[M]) and SN (N), then SN (E[Proj_{1}⟨M, N⟩]) and SN (E[Proj_{2}⟨N, M⟩]).

Exercise 8.3.15 Using Theorem 8.3.11, we can prove confluence of β, η, proj , sp -reduction on λ^{×,→} terms by showing that the property CR defined as in Section 8.3.3 (but for β, η, proj , sp - reduction on λ^{×,→} terms) is type-closed. This means we must check conditions (a)–(e) of the definition. Since conditions (a)–(c) are verified essentially as in the proof of Lemma 8.3.9, this exercise only asks you to prove conditions (d) and (e). Since (e) is easier, you are asked to prove this first. (The next line is part (a) of this exercise. Parts (b)–(d) follow after further explanation.)

(a) Show that if CR(E[M]) and CR(N), then CR(E[Proj_{1}⟨M, N⟩]) and CR(E[Proj_{2}⟨N, M⟩]).

Condition (d) is divided into cases, in the remaining parts of this question, with symmetric possibilities omitted. Assume M: σ_{1} × σ_{2} and CR(Proj_{i}M) for i = 1, 2. Suppose N ← ← M → → P. It follows that Proj_{i}N ← ← Proj_{i}M → → Proj_{i}P for i = 1, 2 and therefore, by assumption, there exist terms Q_{1} , Q_{2} with Proj_{i}N → → Q_{i} ← ← Proj_{i}P. Show that N → → ∘ ← ← P in each of the following cases.

(b) Suppose that Proj_{1}N → → Q_{1} ≡ Proj_{1}Q′_{1} and similarly Proj_{1}P → → Q_{1} ≡ Proj_{1}Q′_{1} , with neither reduction involving proj -reduction on the left-most Proj_{1} in any term.

(c) Suppose that the reductions to Q_{1} and Q_{2} have the forms

Proj_{1}N → → Proj_{1}⟨N_{1}, N_{2}⟩ → N_{1} → → Q_{1}
Proj_{1}P → → Proj_{1}⟨P_{1}, P_{2}⟩ → P_{1} → → Q_{1}
Proj_{2}N → → Proj_{2}⟨N_{3}, N_{4}⟩ → N_{4} → → Q_{2}
Proj_{2}P → → Proj_{2}⟨P_{3}, P_{4}⟩ → P_{4} → → Q_{2}

where the reductions prior to the indicated proj -reduction do not involve proj -reduction on the left-most Proj_{i} in any term. (Hint: Since ⟨Q_{1}, N_{2}⟩ ← ← M → → ⟨N_{1}, Q_{2}⟩, the assumption CR(Proj_{1}M) implies Q_{1} → → ∘ ← ← N_{1} , for example.)

(d) Suppose we have reductions of the form

Proj_{1}N → → Proj_{1}⟨N_{1}, N_{2}⟩ → N_{1} → → Q_{1}
Proj_{1}P → → Q_{1} ≡ Proj_{1}Q′_{1}

where the reduction from Proj_{1}P does not involve proj -reduction on the left-most Proj_{i}. If there is another reduction Proj_{1}P → → Proj_{1}⟨P_{1}, P_{2}⟩, then we may proceed as in the previous case, so assume that there are no terms P_{1}, P_{2} such that P → → ⟨P_{1}, P_{2}⟩. It follows that we may assume without loss of generality that N_{2} → → Q_{2} and Proj_{2}P → → Q_{2} ≡ Proj_{2}Q′_{2} . (Hint: Explain why it suffices to show Q′_{1} → → ∘ ← ← Q′_{2} and use Proj_{i}Q′_{1} ← ← Proj_{i}M → → Proj_{i}Q′_{2} .)

8.3.4 Reduction with fix and additional operations

In this section, we analyze reduction for typed lambda calculus with fix and other operations, of the form used in PCF, for example. We include product types so that these results apply to PCF as formulated in Chapter 2. Some important consequences of the general theorems here, mentioned in earlier chapters, are the confluence of PCF, confluence and termination of labeled PCF reduction, and the completeness of left-most reduction for finding PCF normal forms. An important idea for handling fix is to label each occurrence of a fixed-point operator in a term with a bound on the number of reductions that may be applied. This produces a confluent and terminating reduction relation. We use confluence of labeled reduction to prove this property for unlabeled reduction and termination of labeled reduction to prove the completeness of left-most reduction for unlabeled reduction. All of the results in this section hold with or without products and proj -reduction.

Labeled reduction

Labeled terms and labeled reduction were described briefly in Section 5.4.1. We will consider two versions of labeled reduction here, one needed to prove the semantic results in Section 5.4.1, and the other used to prove the syntactic reduction properties considered in the rest of this section. Similar labeling techniques for untyped lambda calculus were developed by Hyland, Lévy and Wadsworth [Bar84, Hyl76, Lév75, Wad76].

If we begin with simply-typed lambda calculus over signature Σ, containing fixed-point constants at some types, then the labeled terms over Σ are defined using the extended signature Σ_{lab} ⊇ Σ obtained by adding a constant, fix_{σ}^{n}, for each type σ that has a fixed point operator in Σ and for each natural number n ≥ 0. The constant fix_{σ}^{n} is called the labeled fixed-point operator with label n. For the semantic results in Section 5.4.1, we also add a constant ⊥_{σ} for each type σ that has a fixed-point operator. We use the notation Σ_{lab,⊥} for the signature Σ_{lab,⊥} ⊇ Σ_{lab} ⊇ Σ with labeled fixed-point operators and constants ⊥_{σ} at appropriate types. We say M is a labeled term over Σ if M is a well-typed term over Σ_{lab,⊥} and M does not contain any fix without a label. We write lab(M) for the set of labeled terms that become syntactically identical to M when we replace each fix_{σ}^{n} by fix_{σ}.

The two forms of labeled reduction for typed lambda terms containing labeled fixed-point operators are defined using the following reduction axioms:

\begin{aligned}fix_{σ}^{n+1} & → & λf: σ → σ. f(fix_{σ}^{n}f), \\ fix_{σ}^{0} & → & λf: σ → σ. ⊥_{σ} . \end{aligned}

We will call reduction using the first reduction axiom positive labeled reduction, and refer to this using the symbol lab_{+} . The second reduction will be indicated by lab_{0} . Reduction with both reduction axioms will be called labeled reduction and denoted lab_{+,0} . We use lab_{+(0)} for either lab_{+} or lab_{+,0} . It is also possible to add reduction rules for ⊥, such as (⊥_{σ → τ} M) →⊥_{τ}, but we will not need them.

In semantic analysis, we wish to treat fix_{σ} as one of its semantic approximants, λf: σ → σ. f^{n}(⊥ ). This is precisely what happens if we label an occurrence of fix_{σ} with the number n and use lab_{+,0} reduction. The problem with full lab_{+,0} reduction, for the purpose of analyzing reduction without labels, is that the reduction of fix_{σ}^{0} M to (λf: σ → σ. ⊥_{σ}) M allows us to discard the subterm M on subsequent β -reduction. This make it impossible to use confluence of β, lab_{+,0} -reduction to prove confluence of β, fix -reduction, for example, in any direct way. Therefore, we need both forms reduction.

In PCF, we also have reduction axioms for operations like addition and conditional. We develop some general connections between labeled reduction and unlabeled reduction below, in a setting that allows for a set R of additional rewrite axioms. Like the rewrite axioms for PCF addition and conditional, these must be left-linear (see Section 3.7.5). Just to clarify notation, we write R, β, proj , lab_{+} for the combination of reduction given by a set R of reduction axioms, β -reduction, proj -reduction, and positive labeled reduction lab_{+} . Since this long string of names does not fit very well over an arrow, we will abbreviate proj to p and write ⟶^{R,β,p,lab_{+}} , for example. Two basic and useful connections are given in the following lemmas.

Lemma 8.3.16 Suppose R is left-linear and M ⟶^{R,β,p,fix} N. There is a natural number k such that if M^{∗} ∈ lab(M), with each label in M^{∗} at least k, then M^{∗} ⟶^{R,β,p,lab_{+}} N^{∗} for some N^{∗} ∈ lab(N).

Lemma 8.3.17 If M^{∗} ⟶^{R,β,p,lab_{+}} N^{∗}, where M^{∗} ∈ lab(M) and N^{∗} ∈ lab(N), then M ⟶^{R,β,p,fix} N.

Both are proved by easy inductions on the length of reduction sequences. In Lemma 8.3.16, the number k is essentially the length of the reduction sequence from M to N, since any single reduction could be carried out by labeling any fix that is reduced with any number at least 1. The importance of assuming that R is left-linear is discussed below. Since lab_{+,0} contains lab_{+} , the first lemma also holds for R, β, proj , lab_{+,0} . However, Lemma 8.3.17 fails for lab_{+,0} , since the rule for fix^{0} cannot be simulated using unlabeled fix . These two lemmas are used to prove the basic connection between confluence of labeled and unlabeled reduction.

Proposition 8.3.18 If R, β, proj , lab_{+} -reduction is confluent on labeled terms, and R is leftlinear, then R, β, proj , fix -reduction is confluent on unlabeled terms.

Proof Suppose N ← ⟵^{R,β,p,fix} M ⟶^{R,β,p,fix} P. By Lemma 8.3.16, there are labeling M^{∗}, N^{∗}, and P^{∗} of these terms (respectively) such that N^{∗} ← ⟵^{R,β,p,lab_{+}} M^{∗} ⟶^{R,β,p,lab_{+}} P^{∗}. Since R, β, proj , lab_{+} -reduction is confluent, N^{∗} and P^{∗} must have a common reduct Q^{∗}. By Lemma 8.3.17, we may erase labels to obtain N ⟶^{R,β,p,fix} Q ← ⟵^{R,β,p,fix} P. This shows that R, β, proj , fix -reduction is confluent.

It is important to understand how left-linearity is used in the proof of Lemma 8.3.16. The critical step is the base case for a reduction from R. The property that we may choose labels arbitrarily, as long as they are all big enough, may fail if we have a non-linear rule, since some reduction rule may be applicable only if two subterms have the same label. For example, consider the following algebraic rewrite rules for Eq?: nat → nat → bool , succ: nat → nat and true, false: nat .

Eq? x x  → true
Eq? x (succ x) → false

Lemma 8.3.16 fails if R consists solely of either one of these rules, or both of them. These rules also provide a counter-example to Proposition 8.3.18, if we drop the assumption that R is leftlinear, since we may reduce Eq? (fix succ) (fix succ) to both true and false . The first reduction is immediate, while the second proceeds by

Eq? (fix succ) (fix succ) → → Eq? (fix succ) (succ (fix succ)).

If we label Eq? (fix succ) (fix succ) in any way, then at most one of these reductions will be possible. A related phenomenon occurs with surjective pairing, as discussed in Section 4.4.3.

Extend type-closed method to constants

We prove properties of labeled and other reduction by extending the “type-closed” method of the last section to λ^{×,→} terms with constants. With constants, the proof that every term has a type-closed property S has four main parts:

1. Define a predicate P on the applicative structure of terms, from S, by

P^{b}(M)  iff S(M)
P^{σ × τ} (M) iff P^{σ}(Proj_{1}M) and P^{τ} (Proj_{2}M)
P^{σ → τ} (M) iff ∀N. P^{σ}(N) implies P^{τ} (MN)

2. Show that P^{σ}(M) implies S(M).

2′. Show that P^{σ}(c) for each term constant c: σ.

3. Show that P is admissible, so that we may use the Basic Lemma to conclude that P^{σ}(M) holds for every well-typed term Γ ▷ M : σ.

The main idea is that in treating constant c, we may need some properties of P in proving P^{σ}(c). We therefore insert an extra step (2′) in the middle of the proof to accommodate constants.

Rather that try to identify a sufficient condition for step 2′ to succeed, we simply state a theorem that says the method works when it works. We will illustrate this below using labeled PCF reduction.

Theorem 8.3.19 Let S be a type-closed property of λ^{×,→} terms and let P be the predicate on terms defined from S as above. If P (c_{1}), …, P (c_{k}), for term constants c_{1}, …, c_{k}, then S(M) holds for every well-typed λ^{×,→} term M over c_{1}, …, c_{k}.

Proof The proof is identical to the proof of Theorem 8.3.11, except for the addition of term constants. However, the only way that constants affect the proof is that we need to know P (c) for each constant c in order to conclude that P is logical. Since this is stated explicitly in the hypothesis of the theorem, the proof goes through essentially unchanged.

Termination of labeled reduction and its corollaries

As an application of the Theorem 8.3.19, we show that labeled PCF is strongly normalizing. We use pcf to indicate reduction using the axioms of PCF, and pcf_{+} for PCF reduction with lab_{+} replacing fix -reduction. It is a simple matter to extend the argument to show that pcf_{+,0} -reduction, with lab_{0} added, is terminating.

We begin by defining the property we wish to establish, namely

S(M) iff pcf_{+} -reduction is terminating from M

where M may be any labeled PCF term, i.e., any λ^{×,→} term over the signature type constants nat and bool , numerals, boolean constants true and false , addition, equality test Eq? on nat , conditional on each type, and labeled fixed point constants fix_{σ}^{n} for each type σ and all n ≥ 0. Let T be the term applicative structure over this signature, constructed using infinitely many variables at each type.

Let P ⊆ T be the typed predicate defined from S as above. It is easy to see that this is a logical predicate, provided we can establish P(c) for each constant of the signature. The numerals and boolean constants are covered by the fact that P^{b}(c) iff S(c), since all of these constants are normal forms. It remains to show that P holds for each of the remaining constants.

A useful fact to notice is that by Theorem 8.3.11, we have P(M) for every term without constants. A consequence is that for every type σ, there is a σ, b-elimination context E[ ] with P(E[ ]) and therefore S(E[ ]). This is easily verified by induction on types, using a variable wherever we need a term M with P^{σ}(M).

The following lemma will be useful in reasoning about constants. The first two parts do not depend on the choice of S, only the definition of P from S. Part (iii) relies only on the fact that S is closed under reduction.

Lemma 8.3.20 Let M ∈ T^{σ} and let b be nat or bool .

(i) If P^{b}(E[M]) for every σ, b-context E[ ] with P(E[ ]), then P^{σ}(M). (ii) If P^{σ}(M) and E[ ] is a σ, b-context with P(E[ ]), then P^{b}(E[M]).

(iii) If P^{σ}(M) and M ⟶^{pcf_{+}} N, then P^{σ}(N).

Proof We prove (i) by induction on the type of M. If M: b, then the only b, b-elimination context is E[ ] = [ ] and the lemma clearly holds. If M: σ → τ, then every relevant σ → τ, b-elimination context has the form E[[ ]N_{0}], where P^{σ}(N_{0}) and E[ ] is a τ, b-elimination context with P(E[ ]). Let N ∈ T^{σ} be any term with P^{σ}(N), and consider any τ, b-elimination context E[ ] with P(E[ ]). By the inductive hypothesis for MN ∈ T^{τ}, we have P^{τ} (MN). Since N was chosen arbitrarily, if follows that P^{σ → τ} (M). The proof for term M: σ × τ is similar. This proves (i). Part (ii) may be proved by an easy induction on types.

We prove part (iii) from (i) and (ii) using the fact that if S(M) and M ⟶^{pcf_{+}} N, then S(N). More specifically, suppose P^{σ}(M) and let E[ ] be any σ, b-elimination context with P(E[ ]). By

(ii), we have P^{b}(E[M]). If M ⟶^{pcf_{+}} N, then E[M] ⟶^{pcf_{+}} E[N]. Since P^{b}(Q) iff Q ∈ S, we therefore have P^{b}(E[N]). Since this is true for every σ, b-context E[ ] with P(E[ ]), we have P^{σ}(N) by (i). This proves the lemma.

Lemma 8.3.21 For P defined from strong normalization of pcf_{+} -reduction, we have P (+), P (Eq?), P (if then else ), and P (fix_{σ}^{n}) for each type σ and natural number n ≥ 0.

Proof For addition, we assume P^{nat}(M) and P^{nat}(N) and show P^{nat}(M + N). It suffices to show that M + N is strongly normalizing. However, this follows immediately since M and N are both strongly normalizing and the reduction axioms for + only produce a numeral from two numerals. The proof for equality test, Eq?, is essentially the same.

For conditional, we assume P^{bool}(B), P^{σ}(M), P^{σ}(N) and demonstrate P^{σ}(if B then M else N). By Lemma 8.3.20, it suffices to show that if E[if B then M else N] ∈ T^{b}, for P(E[ ]) and b ≡ nat or b ≡ bool , then E[if B then M else N] is strongly normalizing. However, this is an

easy case analysis, according to whether B ⟶^{pcf_{+}} true , B ⟶^{pcf_{+}} false , or neither, using (ii) of Lemma 8.3.20.

The remaining case is a labeled fixed-point constant fix_{σ}^{n}. For this, we use induction on the label. The base case, for fix_{σ}^{0} , is easy since there is no associated reduction. For fix_{σ}^{n+1} , we assume P^{σ → σ}(M) and let E[ ] be any elimination context with P(E[ ]) and E[fix_{σ}^{n+1}M] ∈ T^{b}. We prove the lemma by showing that E[fix_{σ}^{n+1}M] is strongly normalizing. If there is an infinite reduction sequence from this term, it must begin with steps of the form

E[fix_{σ}^{n+1}M] ⟶^{pcf_{+}} E′[fix_{σ}^{n+1}M′] →^{lab_{+}}E′[(λf: σ → σ. f(fix_{σ}^{n}f))M′]

⟶^{pcf_{+}} E′′[(λf: σ → σ. f(fix_{σ}^{n}f))M′′] →^{β} E′′[M′′(fix_{σ}^{n}M′′)] ⟶^{pcf_{+}} …

However, by the induction hypothesis and (ii) of Lemma 8.3.20, we have P^{σ → σ}(M′′), P^{σ}(fix_{σ}^{n}M′′) and P(E′′[ ]), which implies that an infinite reduction sequence of this form is impossible. This completes the induction step and proves the lemma.

Since Lemma 8.3.21 is easily extended to pcf_{+,0} , we have the following corollary of Theorem 8.3.19.

Theorem 8.3.22 Both pcf_{+} and pcf_{+,0} -reduction are strongly normalizing on labeled PCF terms.

We also wish to show that both forms of labeled PCF reduction are confluent. A general theorem that could be applied, if we did not have conditional at all types, is given in [BT88, BTG89] (see Exercise 8.3.29). The general theorem is that if typed lambda calculus is extended with a confluent, algebraic rewrite system, the result is confluent. The proof of this is nontrivial, but is substantially simplified if we assume that R is left-linear. That is in fact the case we are interested in, since left-linearity is essential to Proposition 8.3.18 anyway. An adaptation of this proof to typed lambda calculus with labeled fixed-point operators has been carried out in [HM90, How92]. For the purposes of proving our desired results as simply as possible, however, it suffices to prove weak confluence, since confluence then follows by Proposition 3.7.32. To emphasize the fact that the argument does not depend heavily on the exact natural number and boolean operations of PCF, we show that adding β, proj , lab_{+(0)} to any weakly confluent reduction system preserves weak confluence, as long as there are no symbols in common between R and the reduction axioms of β, proj , lab_{+(0)} . This is essentially an instance of orthogonal rewrite systems, as they are called in the literature on algebraic rewrite systems [Toy87], except that application is shared. A related confluence property of untyped lambda calculus is Mitschke’s δ-reduction theorem [Bar84], which shows that under certain syntactic conditions on R, untyped R, β -reduction is confluent.

Lemma 8.3.23 Let R be a set of reduction axioms of the form L → R, where L and R are lambda terms of the same type and L does not contain an application xM of a variable to an argument or any of the symbols λ, Proj_{i}, fix or any fix_{σ}^{n}. If R is weakly confluent, then R, β, proj , lab_{+(0)} is weakly confluent.

Proof The proof is a case analysis on pairs of redexes. We show two cases involving β -reduction and reduction from R. The significance of the assumptions on the form of L is that these guarantee that if a subterm of a substitution instance [M_{1}, …, M_{k}/x_{1}, …, x_{k}]L of some left-hand-side contains a β, proj , lab_{+(0)} redex, then this redex must be entirely within one of M_{1}, …, M_{k}. The lemma would also hold with any other hypotheses guaranteeing this property.

The first case is an R-redex inside a β -redex. This gives a term of the form

(λy: σ.(… [M_{1}, …, M_{k}/x_{1}, …, x_{k}]L …))N

reducing to either of the terms

(… [N/y][M_{1}, …, M_{k}/x_{1}, …, x_{k}]L …) (λy: σ.(… [M_{1}, …, M_{k}/x_{1}, …, x_{k}]R …))N

the first by β -reduction and the second by an axiom L → R from R. It is easy to see that both reduce in one step to

(… [N/y][M_{1}, …, M_{k}/x_{1}, …, x_{k}]R …)

The other possible interaction between β -reduction and R begins with a term of the form

(… [M_{1}, …, M_{k}/x_{1}, …, x_{k}]L …)

where one of M_{1}, …, M_{k} contains a β -redex. If M_{i} → M′_{i}, then this term reduces to either of the two terms

(… [M_{1}, …, M′_{i}, …, M_{k}/x_{1}, …, x_{k}]L …) (… [M_{1}, …, M_{i}, …, M_{k}/x_{1}, …, x_{k}]R …)

in one step. We can easily reduce the first to

(… [M_{1}, …, M′_{i}, …, M_{k}/x_{1}, …, x_{k}]R …)

by one R step. Since we can also reach this term by some number of β -reductions, one for each occurrence of x_{i} in R, local confluence holds. The cases for other reductions in a substitution instance of the left-hand-side of an R axiom are very similar.

By Lemma 3.7.32, it follows that pcf_{+} and pcf_{+,0} are confluent. We may use Proposition 8.3.18 to derive confluence of pcf -reduction from confluence of pcf_{+} . This gives us the following theorem.

Theorem 8.3.24 The reductions pcf_{+} and pcf_{+,0} are confluent on labeled PCF terms and pcf - reduction is confluent on ordinary (unlabeled) PCF terms.

Completeness of leftmost reduction

The final result in this section is that if R is a set of “left-normal” rules (defined below), and R, β, proj , lab_{+} is confluent and terminating, then the leftmost reduction strategy defined in Section 2.4.3 is complete for finding R, β, proj , fix -normal forms. Since the PCF rules are left-normal, it follows from Proposition 2.4.15 that lazy reduction is complete for finding normal forms of PCF programs.

A reduction axiom is left-normal if all the variables in the left-hand side of the rule appear to the right of all the term constants. For example, all of the PCF rules for natural numbers and booleans are left-normal. If we permute the arguments of conditional, however, putting the boolean argument at the end, then we would have reduction axioms

cond x y true ⟶ x,
cond x y false ⟶ y.

These are not left-normal since x and y appear to the left of the constants true and false . Intuitively, if we have left-normal rules, then may safely evaluate the arguments of a function from left to right. In many cases, it is possible to replace a set of rules with essentially equivalent left-normal ones by either permuting arguments or introducing auxiliary function symbols (see Exercise 8.3.28). However, this is not possible for inherently “non-sequential” functions such as parallel-or.

We will prove the completeness of left-most reduction using strong normalization and confluence of positive labeled reduction, and the correspondence between labeled and unlabeled reduction. Since labeled fix reduction may terminate with fix^{0} where unlabeled fix reduction could continue, our main lemma is that any fix^{0} occurring to the left of the left-most redex will remain after reducing the left-most redex.

Lemma 8.3.25 Let R be a set of left-normal reduction axioms with no left-hand-side containing fix^{0} . If M ⟶^{R,β,p,lab_{+}} N by the left-most reduction step, and fix^{0} occurs to the left of the left-most redex of M, then fix^{0} must also occur in N, to the left of the left-most redex if N is not in normal form.

Proof Suppose M ≡ C[L] → C[R] ≡ N by contracting the left-most R, β, proj , lab_{+} -redex and assume fix^{0} occurs in C[ ] to the left of [ ]. If N ≡ C[R] is in normal form, then fix^{0} occurs in N since fix^{0} occurs in C[ ]. We therefore assume N is not in normal form and show that fix^{0} occurs to the left of the left-most redex in N.

Suppose, for the sake of deriving a contradiction, that fix^{0} occurs within, or to the right of, the left-most redex of N. Since a term beginning with fix^{0} is not a redex, the left-most redex of N must begin with some symbol to the left of fix^{0} , which is to the left of R when we write N as C[R]. The proof proceeds by considering each possible form of redex.

Suppose the left-most redex in N is Proj_{i}⟨N_{1}, N_{2}⟩, with fix^{0} and therefore R occurring to the right of Proj_{i}. Since fix^{0} must occur between Proj_{i} and R, R cannot be ⟨N_{1}, N_{2}⟩, and so a redex of the form Proj_{i}⟨ , ⟩ must occur in M to the left of L. This contradicts the assumption that L is the leftmost redex in M. Similar reasoning applies to a β -redex; the fix case is trivial.

It remains to consider a redex SL′ with S some substitution and L′ → R′ in R. We assume fix^{0} and therefore R occur to the right of the first symbol of SL′. Since fix^{0} is not in L′, by hypothesis, and the rule is left-normal, all symbols to the right of fix^{0} , including R if it occurs within L′, must be the result of substituting terms for variables in L′. It follows that we have a redex in M to the left of L, again a contradiction. This proves the lemma.

Theorem 8.3.26 Suppose R, β, proj , lab_{+} is confluent and terminating, with R left-linear and left-normal. If M ⟶^{R,β,p,fix} N and N is a normal form, then there is a R, β, proj , fix -reduction from M to N that contracts the leftmost redex at each step.

Proof If M ⟶^{R,β,p,fix} N then, by Lemma 8.3.16 there exist labelings M^{∗} and N^{∗} of these terms such that M^{∗} ⟶^{R,β,p,lab_{+}} N^{∗}. Since R, β, proj , lab_{+} -reduction is confluent and terminating, we may reduce M^{∗} to N^{∗} by reducing the left-most redex at each step.

We show that the left-most R, β, proj , lab_{+} -reduction of M^{∗} to N^{∗} is also the left-most R, β, proj , fix -reduction of M to N (when labels are removed). It is easy to see that this is the case if no term in the reduction sequence has fix^{0} to the left of the left-most redex, since this is the only term that would be an unlabeled redex without being a labeled one. Therefore, we assume that the final k steps of the reduction have the form

M_{k}^{∗} ≡ C[L] → C[R] ≡ M_{k−1}^{∗} → M_{k−2}^{∗} → … → N^{∗},

where fix^{0} occurs to the left of L in M_{k}. But by Lemma 8.3.25 and induction on k, fix^{0} must also be present in N^{∗}, which contradicts the fact that N is a R, β, proj , fix -normal form. It follows from Lemma 8.3.16 that by erasing labels we obtain a leftmost reduction from M to N.

A related theorem in [Klo80] shows that left-most reduction is normalizing for the untyped lambda calculus extended with any left-normal, linear and non-overlapping term rewriting system. Our proof is simpler since we assume termination, and since type restrictions make fix the only source of potential nontermination.

Since the rules of PCF satisfy all the conditions above, Theorem 8.3.26 implies the completeness of leftmost reduction for finding PCF normal forms. This was stated as Proposition 2.4.12 in Section 2.4.3.

Exercise 8.3.27 Gödel’s system T of primitive recursive functionals is λ^{→} over type constant nat and term constants

0  : nat
succ : nat → nat
R_{σ} : σ →(σ → nat → σ) → nat → σ

for each type σ, with the following reduction axioms

\begin{matrix}R_{σ}MN0 → M \\ R_{σ}MN(succ x) → N(R_{σ}MNx)x \end{matrix}

The primitive recursion operator R_{σ} of type σ is essentially the same as prim_{σ} of Exercise 2.5.7, with cartesian products eliminated by currying.

Extend the proof in this section to show that Gödel’s T is strongly normalizing. You need not repeat proof steps that are given in the text. Just point out where additional arguments are needed and carry them out. Historically, Gödel’s T was used to prove the consistency of first-order Peano arithmetic [Göd58], by a reduction also described in [HS86, Tro73] and mentioned briefly in [Bar84, Appendix A.2]. It follows from this reduction that the proof of strong normalization of T cannot be formalized in Peano arithmetic. Given this, it is particularly surprising that the proof for T involves only the same elementary reasoning used for λ^{→}.

Exercise 8.3.28 Consider the following set of algebraic reduction axioms.

f true true y ⟶ true
f true false y ⟶ false
f false x true ⟶ false
f false x false ⟶ true.

This system is not left-normal. Show that by adding a function symbol not with axioms

not true ⟶ false
not false ⟶ true.

we may replace the four reduction axioms by two left-normal ones in a way that gives exactly the same truth-table for f.

Exercise 8.3.29 [BT88, BTG89] This exercise is concerned with adding algebraic rewrite rules to typed lambda calculus. Recall from Section 4.3.2 that if Σ_{alg} = ⟨S, F ⟩ is an algebraic signature, we may construct a similar λ^{→} signature Σ = ⟨B, F′⟩ by taking the sorts of Σ_{alg} as base types, and letting each algebraic function have the corresponding curried type. This allows us to view algebraic terms as a special case of typed lambda terms.

Let R be an algebraic rewrite system over Σ_{alg}. Thinking of R as a set of rewrite rules for λ^{→} terms over Σ, it makes sense to ask whether the reduction system consisting of R together with the usual reduction rules (β)_{red} and (η)_{red} of typed lambda calculus is confluent. This turns out to be quite tricky in general, but it gets much simpler if we drop (η)_{red} and just consider R plus β -reduction (modulo α-conversion of terms). We call the combination of R and β -reduction R, β - reduction. The problem is to prove that if R is confluent (as an algebraic rewrite system), then R, β -reduction is confluent on typed lambda terms over Σ. (This also holds with proj -reduction added [HM90, How92].)

Some useful notation is to write → →_{R} for reduction using rules from R, similarly → →_{R,β} for R, β -reduction, and βnf (M) for the normal form ofM under β -reduction. Note that βnf (M) may still be reducible using rules from R. You may assume the following facts, for all Γ ▷ M : σ and Γ ▷ N : σ.

1. If R is confluent on algebraic terms over signature Σ_{alg}, then → →_{R} is confluent on typed lambda terms over Σ.

2. If M is a β -normal form and M → →_{R} N, then N is a β -normal form.

3. If M → →_{R,β} N, then βnf (M) → →_{R} βnf (N).

The problem has two parts.

(a) Using 1–3 above, show that if R is confluent (as an algebraic rewrite system), then R, β - reduction is confluent on typed lambda terms over Σ. (This problem has a 4 or 5-sentence solution, using a picture involving → →_{R}, → →_{R,β} and ordinary β -reduction → →_{β}.)

(b) Show that (a) fails if we add fix-reduction. Specifically, find a confluent algebraic rewrite system R such that R, β, fix -reduction on typed lambda terms over signature Σ∪{fix_{σ}: (σ → σ) → σ} is not confluent. (Hint: try to find some algebraic equations that become inconsistent when fixed points are added.)

8.4 Partial Surjections and Specific Models

In Sections 8.4.1–8.4.3, we prove completeness of β, η-conversion for three specific models, the full classical, recursive and continuous hierarchies. These theorems may be contrasted with the completeness theorems of Section 8.3.1, which use term models to show that provability coincides with semantic implication. The completeness theorems here show that the specific theory of β, ηconversion captures semantic equality between pure typed lambda terms in three specific, nonsyntactic models.

One way of understanding each of these theorems is to consider a specific model as characterizing a specific form of “distinguishability.” Suppose we have two terms, M, N: (b → b) → b, for example. These will be equal in the full classical hierarchy if the functions defined by M and N produce equal values of type b for all possible function arguments. On the other hand, in a recursive model A where A^{b → b} only contains recursive functions, these terms will be equal if the functions they define produce equal values when applied to all recursive functions. Since not all set-theoretic functions are recursive, there may be some equations (at this type) that hold in the recursive model but not in the full set-theoretic hierarchy. Surprisingly, the completeness theorems show that these two forms of semantic equivalence are the same, at least for pure typed lambda terms without constants. The third case, the full continuous hierarchy, is also interesting for its connection with PCF extended with parallel-or. Specifically, we know from Theorem 5.4.14 that two terms of PCF + por are equal in the continuous hierarchy over nat and bool iff they are operationally equivalent. In other words, two lambda terms are equal in the continuous model iff they are indistinguishable by PCF program contexts. Therefore, our completeness theorem for the full continuous hierarchy shows that β, ηconversion captures PCF operational equivalence for pure typed lambda terms without the term constants of PCF. A technical point is that this only holds for terms whose types involve only nat and →; with bool , the theorem does not apply since we only prove completeness of β, η-conversion for the full continuous hierarchy over infinite cpo’s.

A more general theorem, which we do not consider, is Statman’s so-called 1-section theorem [Rie94, Sta85a, Sta82]. Briefly, Statman’s theorem gives a sufficient condition on a Henkin model A implying that two terms have the same meaning in A iff the terms are β, η-convertible. It is called the “1-section theorem” since the condition only involves the first-order functions of A. Although the 1-section theorem implies all of the three completeness theorems here, the proof is more complex and combinatorial than the logical relations argument used here, and the generalization to other lambda calculi is less clear.

We will work with λ^{→}, and type frames instead of arbitrary applicative structures. Recall that a λ^{→} type frame is an extensional applicative structure A such that the elements of A^{σ → τ} are functions from A^{σ} to A^{τ} and App f x = f(x). We therefore write fx in place of App f x.

8.4.1 Partial surjections and the full classical hierarchy

It is tempting to think of any λ^{→} type frame B as a “subframe” of the full classical hierarchy P with the same interpretation of type constants. This seems quite natural, since at every type σ → τ, the set B^{σ → τ} is a subset of the set of all functions from B^{σ} to B^{τ}. However, we do not have B^{σ → τ} ⊆ P^{σ → τ} in general. This is because B^{σ} may be a proper subset of P^{σ} if σ is a functional type, and so the domain of a function in B^{σ → τ} is different from a function in P^{σ → τ}. However, the intuitive idea that P “contains” B is reflected in a certain kind a logical relation between P and B. Specifically, a logical relation R ⊆ A × B is called a partial surjection if each R^{σ} is a partial surjection, i.e., R is a partial function and for each b ∈ B^{σ} there is some a ∈ A^{σ} with R^{σ}(a, b).

In this section, we prove that if we begin with partial surjections R^{b}: P^{b} → B^{b} for each type constant b of some frame B, then the induced logical relation from the full classical hierarchy P to B is a partial surjection. By choosing B isomorphic to a β, η-term model, we may conclude that any full classical P with each P^{b} large enough has the same theory as B. Consequently, an equation Γ ▷ M = N : σ holds in the full classical hierarchy over any infinite types iff M and N are β, η-convertible. This was first proved in [Fri75].

Lemma 8.4.1 (Surjections for Classical Models) Let R ⊆ P × B be a logical relation over a full classical hierarchy P and type frame B. If R^{b} ⊆ P^{b} × B^{b} is a partial surjection for each type constant b, then R is a partial surjection.

Proof We assume R^{σ} and R^{τ} are partial surjections and show that R^{σ → τ} is also a partial surjection. Recall that

R^{σ → τ} = { ⟨a, b⟩ | R^{σ}(a′, b′) ⊃ R^{τ} (aa′, bb′) }.

We first show that R^{σ → τ} is onto by letting b ∈ B^{σ → τ} and finding a ∈ P^{σ → τ} related to b. Writing R^{σ} and R^{τ} as functions, a can be any function satisfying

aa_{1} ∈ (R^{τ})^{−1}(b(R^{σ}a_{1})) all a_{1} ∈ Dom(R^{σ}).

Since P is the full type hierarchy, R^{σ} is a function on its domain Dom(R^{σ}) and R^{τ} is onto, there is at least one such a ∈ P^{σ → τ}.

To see that R^{σ → τ} is a partial function, we suppose that R^{σ → τ} (a, b_{1}) and R^{σ → τ} (a, b_{2}). Let f: B^{σ} → P^{σ} be any “choice function” satisfying

R^{σ}(fb′, b′) all b′ ∈ B^{σ}.

Then for every b′ ∈ B^{σ}, we have R^{τ} (a(fb′), b_{i}b′) for i = 1, 2. But since R^{τ} is a function, it follows that b_{1}b′ = b_{2}b′ for every b′ ∈ B^{σ}. Thus, by extensionality of B, we have b_{1} = b_{2} . This proves the lemma.

It is now an easy matter to prove the completeness of β, η-conversion for the full classical hierarchy over any infinite sets.

Theorem 8.4.2 (Completeness for Classical Models) Let P be the full classical λ^{→} hierarchy over any infinite sets. Then for any pure lambda terms, Γ ▷ M, N : σ without constants, we have P ⊧ Γ ▷ M = N : σ iff M and N are β, η-convertible.

Proof Let B ≅ T /R_{E} be isomorphic to a Henkin model of equivalence classes of terms, as in Theorem 8.3.2, where E is the pure theory of β, η-conversion. Let R ⊆ P × B be a logical relation with R^{b} a partial surjection. We know this is possible since P^{b} is infinite and each B^{b} is countably infinite. By Lemma 8.4.1, R is a partial surjection. Consequently, by Lemma 8.2.17, Th(P) ⊆ Th(B). But since every theory contains Th(B), it follows that Th(P) = Th(B).

8.4.2 Full recursive hierarchy

In this subsection, we prove a surjection theorem for modest sets. Just as any frame A with an arbitrary collection of functions is the partial surjective image of a full classical hierarchy, we can show that any frame A containing only recursive functions is the partial surjective image of a full recursive hierarchy. Since we may view the term model as a recursive model, the surjection lemma for recursive models also implies that β, η-conversion is complete for recursive models with infinite interpretation of each type constant.

In order to carry out the inductive proof of the surjection lemma, we need to be able to show that for every function in a given recursive frame B, we can find some related recursive function in the full recursive hierarchy A. The way we will do this is to establish that for every type, we have functions that “recursively demonstrate” that the logical relation R is a partial surjection. Following the terminology of Kleene realizability [Kle71], we say that a function f_{σ} realizes R^{σ} is surjective by computing f_{σ}b with R^{σ}(f_{σ}b, b) for every element b ∈ B^{σ}. Similarly, a recursive function g_{σ} realizes R^{σ} is a partial function by computing the unique g_{σ}a = b with R^{σ}(a, b) from any a in the domain of R^{σ}. We adapt the classical proof to modest sets by showing that the inductive hypothesis is realized by recursive functions.

The assumption we will need for the interpretation of type constants is a form of “recursive embedding.” If ⟨A, e_{A}⟩ and ⟨B, e_{b}⟩ are modest sets, then we say ⟨f, g⟩ is a recursive embedding of ⟨B, e_{b}⟩ into ⟨A, e_{A}⟩ if f and g are recursive functions

f: ⟨B, e_{b}⟩ → ⟨A, e_{A}⟩ and g: ⟨A, e_{A}⟩ → ⟨B, e_{b}⟩

whose composition g ∘ f = id_{B} is the identity function on B. We incorporate such functions into a form of logical relation with the following definition. Let A and B be type frames with each type interpreted as a modest set. We say a family {R^{σ}, f_{σ}, g_{σ}} of relations and functions is a recursive partial surjection from A to B if R ⊆ A × B is a logical partial surjection, and

f_{σ}: ⟨B^{σ}, e′_{σ}⟩ → ⟨A^{σ}, e_{σ}⟩, g_{σ}: ⟨A^{σ}, e_{σ}⟩ → ⟨B^{σ}, e′_{σ}⟩

are recursive functions with f_{σ} realizing that R^{σ} is surjective and g_{σ} realizing that R^{σ} is a partial function.

Lemma 8.4.3 (Surjections for Recursive Models) Let A, B be frames of recursive functions and modest sets, for a signature without term constants, with A a full recursive hierarchy. If B^{b} is recursively embedded in A^{b} for each type constant b, then there is a recursive partial surjection {R^{σ}, f_{σ}, g_{σ}} from A to B.

Proof For each type constant b, we define R^{b} from the recursive embedding ⟨f_{b}, g_{b}⟩ by R^{b}(x, y) iff g_{b}x = y. It is easy to check that ⟨R^{b}, f_{b}, g_{b}⟩ has the required properties. We define the logical relation R ⊆ A × B by extending to higher types inductively.

For the inductive step of the proof, we have three conditions to verify, namely

(i) R^{σ → τ} is a surjective partial function,

(ii) There is a recursive f_{σ → τ}: ⟨B^{σ → τ} , e′_{σ → τ} ⟩ → ⟨A^{σ → τ} , e_{σ → τ} ⟩ with R^{σ → τ} (fb, b) for all b ∈ B^{σ → τ}, and

(iii) There is a recursive g_{σ → τ}: ⟨A^{σ → τ} , e_{σ → τ} ⟩ → ⟨B^{σ → τ} , e′_{σ → τ} ⟩ with R^{σ → τ} (a, ga) for all a ∈ Dom(R^{σ → τ}).

Since (i) follows from (ii) and (iii), we check only (ii) and (iii), beginning with (ii). Given b ∈ B^{σ → τ}, we must find some recursive function a ∈ A^{σ → τ} with R^{σ → τ} (a, b). Writing R(·) as a function, a must have the property

aa_{1} ∈ (R^{τ})^{−1}(b(R^{σ}a_{1}))

for all a_{1} ∈ Dom(R^{σ}). It is easy to see that this condition is satisfied by taking a = f_{τ} ∘ b ∘ g_{σ}, since g_{σ} computes the function R^{σ} and f_{τ} chooses an element f_{τ} (b(R^{σ}a_{1})) ∈ (R^{τ})^{−1}(b(R^{σ}a_{1})) whenever there is one. We can also compute a as a function of b by composing with recursive functions.

For condition (iii), we assume a ∈ Dom(R^{σ → τ}) so that R^{σ → τ} (a, b) for some b. We need to show how to compute b uniquely from a. It suffices to show how to compute the function value bb_{1} for every b_{1} ∈ B^{σ}, and that the value bb_{1} is uniquely determined by a and b_{1} . If b_{1} ∈ B^{σ}, then R^{σ}(f_{σ}b_{1}, b_{1}) and so we have R^{τ} (a(f_{σ}b_{1}), bb_{1}). Therefore g_{τ} (a(f_{σ}b_{1})) = bb_{1} and this equation determines the value bb_{1} uniquely. Thus we take g_{σ → τ} a = g_{τ} ∘ a ∘ f_{σ}, which, as we have just seen, gives the correct result for every a ∈ Dom(R^{σ → τ}).

The completeness theorem is now proved exactly as for the full classical hierarchy, with Lemma 8.4.3 in place of Lemma 8.4.1, and with the term model viewed as a frame of recursive functions and modest sets, as explained in Examples 5.5.3, 5.5.4 and Exercise 5.5.13, instead of as a frame of classical functions.

Theorem 8.4.4 (Completeness for Recursive Models) Let A be the full recursive type hierarchy over any infinite modest sets ⟨A^{b_{0}}, e_{0}⟩, … with the natural numbers N recursively embedded in each A^{b}. Then for any pure lambda terms, Γ ▷ M, N : σ without constants, we have A ⊧ Γ ▷ M = N : σ iff M and N are β, η-convertible.

8.4.3 Full continuous hierarchy

We may also prove a completeness theorem for models consisting of all continuous functions on some family of complete partial orders. While similar in outline to the completeness proofs of the last two sections, the technical arguments are more involved. The proof is from [Plo82].

The main lemma in each of the preceding sections is the surjection lemma. In each case, the main step in its proof is, given b ∈ B^{σ → τ}, finding some a ∈ A^{σ → τ} satisfying

aa_{1} ∈ (R^{τ})^{−1}(b(R^{σ}a_{1})) all a_{1} ∈ Dom(R^{σ}).

With the full classical hierarchy, we use the fact that all functions belong to A^{σ → τ}. This allows us to choose one satisfying the conditions. In the case of recursive functions on modest sets, we built up recursive functions between A and B by induction on type, and used these to define a. In this section, we will build up similar continuous functions between A and the cpo obtained by lifting the set of equivalence classes of terms. Since there is no available method for regarding each type of the term structure as a “usefully” ordered cpo, the proof will involve relatively detailed reasoning about terms and free variables.

The analogue of “recursive embedding” is “continuous retract.” If D = ⟨D, ≤_{D}⟩ and E = ⟨E, ≤_{e}⟩ are cpo’s, then ⟨i, j⟩ form a retract from D to E if

i: E → (D)_{⊥} and j: D → E

are continuous and i ∘ j = id_{D}. A cpo E has a discrete infinite retraction is there is a retract from some infinite set D to E.

Lemma 8.4.5 Let Σ be a λ^{→} signature with no term constants and let B = T /R be the Henkin model for Σ consisting of terms over infinitely many free variables of each type, modulo β, ηconversion. Let A be a full continuous λ^{→} hierarchy for Σ such that each ⟨A^{b}, ≤_{b}⟩ has a discrete infinite retraction. Then there is a logical partial surjection R ⊆ A × B from A to B and a pair of continuous functions i_{σ}: A^{σ} → (B^{σ})_{⊥} and j_{σ}: B^{σ} → A^{σ} at each type such that (i) R^{σ}(j_{σ}b, b) for all b ∈ B^{σ}, and

(ii) R^{σ}(a, i_{σ}a) all a ∈ Dom(R^{σ}).

Proof The proof is by induction on types. For the base case, we may assume that the discrete infinite retraction of A^{b} is B^{b}, by making the language as large as necessary. We define R^{b} from i_{b} as in the proof of Lemma 8.4.3 and extend to function types inductively.

For the inductive step, we define j first, since this is easier. For any b ∈ B^{σ → τ}, let j_{σ → τ} b be the function

(j_{σ → τ} b)a′ = \{ \begin{matrix}j_{τ} (b (i_{σ}a′)) & if i_{σ}a′ ≠⊥, \\ ⊥ & otherwise. \end{matrix}

The continuity of j_{σ → τ} b follows from continuity of i_{σ} and j_{τ}.

The definition of i_{σ → τ} is considerably more involved. It can be motivated by considering how i should act on elements in the range of R^{σ → τ}. We will then define i_{σ → τ} in another way, which makes it easier to see that it is continuous.

Suppose R^{σ → τ} (a, b) and consider the equivalence class of some variable, [x] ∈ B^{σ}. By the inductive hypothesis, we have

[x] ∈ B^{σ} ⊃ R^{σ}(j_{σ}[x], [x]) ⊃ R^{τ} (a(j_{σ}[x]), b[x]) ⊃ i_{τ} (a(j_{σ}[x])) = b[x].

Since B is a term model, there are equivalence classes of terms [N] = b and [M] = i_{τ} (a(j_{σ}[x])) = [Nx]. We may assume without loss of generality that M and N are β, η-normal forms. If we had the luck or foresight to have chosen a variable x: σ that is not free in M, then we may define i_{σ → τ} a = [λx: σ. M] = [λx: σ.(Nx)] and, since FV (N) ⊆ FV (M), η-reduce to get i_{σ → τ} a = [N] = b. It remains to show how to do this uniformly, without assuming a ∈ Dom(R^{σ → τ}).

For each type σ, we select some variable x_{σ}: σ and, for each finite set V of variables of type σ, choose some variable x_{V}: σ ∉ V . If a ∈ A^{σ → τ}, then we define i_{σ → τ} a by the following three steps.

1. Let b = i_{τ} (a(j_{σ}[x_{σ}])). If b =⊥, then we let i_{σ → τ} a =⊥.

2. Otherwise, let V = FV (nf (b)), where nf (b) is the unique β, η-normal form in the equivalence class b and let b′ = i_{τ} (a(j_{σ}[x_{V}])). If b′ =⊥, then we let i_{σ → τ} a =⊥.

3. Otherwise, let M = nf (b′) and let i_{σ → τ} a = [λx_{V}: σ. M].

Since i_{σ → τ} can be defined from i and j of simpler type using lambda terms and a “make strict” function, i_{σ → τ} is continuous. It follows from the previous paragraph that i_{σ → τ} has the correct behavior, since if a ∈ Dom(R^{σ → τ}), neither of the first two steps above gives us i_{σ → τ} a =⊥. This completes the proof.

The completeness theorem is now proved exactly as for the full recursive hierarchy, with Lemma 8.4.5 in place of Lemma 8.4.3.

Theorem 8.4.6 (Completeness for Continuous Models) Let A be the full recursive type hierarchy over any cpo’s ⟨A^{b_{0}}, ≤_{0}⟩, … with infinite discrete retractions. Then for any pure lambda terms, Γ ▷ M, N : σ without constants, we have A ⊧ Γ ▷ M = N : σ iff M and N are β, ηconvertible.

8.5 Representation Independence

8.5.1 Motivation

One pragmatic motivation for type checking in programming languages is to keep certain implementation details from affecting the behavior of programs. This is important for program portability, for example. If the difference between one’s complement and two’s complement representation of negative integers (with −1 represented as 1 … 10_{2} or 1 … 11_{2} , respectively) were immediately apparent to any program, it could prove difficult to transport programs written on a one’s complement machine to a two’s complement machine. In an “untyped” programming language allowing bit-string operations on integers, a program could distinguish a one’s complement implementation from two’s complement. However, if bit-strings and integers are separate types, then we can show that one’s complement and two’s complement are indistinguishable by proving a “representation independence” theorem.

Intuitively, representation independence is the property that programs do not depend on the way data types are represented, only on the behavior of data types with respect to the operations that are provided. In addition to the portability issue mentioned above, this allows the implementation of a user-defined data type to be optimized after a program using it has been completed. For example, representation independence would guarantee that stacks could be implemented using arrays or linked lists, as long as the push and pop operations give the correct results. In this case, the implementation of stacks could be changed from arrays to linked lists, or vice versa, without altering the correctness of any program that uses stacks.

The intent of a representation independence theorem is to characterize the kinds of implementation decisions that do not effect the meanings of programs. Various formal statements of the property have been proposed in the literature [Don79, Hay84, Rey83, MM85, Mit86b, Mit91a]. Essentially, all of these have the following general form.

If two interpretations A and B are related in a certain way, then the meaning A[[M]] of any closed term M in A is related to the meaning B[[M]] in B in the same certain way.

We generally choose the correspondence between A and B to be the identity for observables such as natural numbers, strings and booleans. The pragmatic consequence of this sort of theorem is that if two programming language interpreters are related in this “certain way,” then the result of executing any program using one interpreter will correspond to the result of executing the same program using the other interpreter. Thus the precise statement of the theorem describes the kind of implementation decisions that do not effect the meanings of programs. Of course, the kinds of relations we are interested in will turn out to be logical relations. The main ideas seem best illustrated by example.

8.5.2 Example language

We will consider multisets of natural numbers, assuming that we observe the behavior of programs by computing natural numbers. Since we do not have type declarations in λ^{→}, we will compare implementations of multisets by assuming the implementations are provided as part of the semantics of a simple programming language. However, the main ideas may also be applied to languages with abstract data type declarations (Section 9.4).

To study programs with multisets, we let Σ be the λ^{→} signature with type constants nat (for natural numbers) and s (for multisets), term constants

0, 1: nat, +: nat → nat → nat

to provide arithmetic, and constants

empty: s, insert: nat → s → s, count: s → nat → nat

for multiset operations. Informally, empty is the empty multiset, insert adds an element to a multiset, and count returns the multiplicity of a multiset element. (An algebraic specification of multisets appears in Table 3.2; see also Exercise 3.4.20.)

In this language, we intend to write programs with natural number inputs and outputs. Multisets and function expressions may occur in programs, but are used only at “intermediate stages.” Our goal is to describe the conditions under which different representations (or implementations) of multisets are indistinguishable by programs. Since our definition will involve quantifying over the collection of all programs, it suffices to consider programs with no input, and only one output. Therefore, we let the programs over Σ be the closed terms M: nat of type natural number, as for PCF in Section 2.3.1.

We will compare different representations of multisets by examining the values of programs over appropriate models. Since we consider natural numbers the “printable output,” we will assume that each model interprets nat as the usual natural numbers 0, 1, 2, . . .. For the purposes of this discussion, we define an implementation for Σ to be a model

A = ⟨{A^{σ}}, 0, 1, +, empty^{A}, insert^{A}, count^{A}⟩

with A^{nat} and 0, 1, + standard, but A^{s} and operations empty, insert, count arbitrary.

Two compilers or interpreters for a programming language would generally be considered equivalent if every program produces identical results on either one. We say that implementations A and B for Σ are observationally equivalent if, for any program M: nat , we have

A[[M: nat]] = B[[M: nat]]

i.e., the meaning of M: nat in A is the same as the meaning of M: nat in B. The rest of this section is devoted to characterizing observational equivalence of implementations.

A first guess might be that A and B are observationally equivalent iff there exists some kind of mapping between multisorted first-order structures

⟨A^{nat}, A^{s}, 0, 1, +, empty^{A}, insert^{A}, count^{A}⟩

and

⟨B^{nat}, B^{s}, 0, 1, +, empty^{B}, insert^{B}, count^{B}⟩,

say a homomorphism preserving 0, 1 and +. This is partly correct, since a first-order homomorphism lifts to a logical relation, and therefore the Basic Lemma guarantees equivalent results for any program. However, there are two reasons why homomorphisms are not an exact characterization. These are worth discussing, since they will sharpen our intuition for observational equivalence of implementations. The first reason has to do with the fact that elements of A^{s} and B^{s} that are not definable by terms are irrelevant. For example, suppose B contains only definable, finite multisets and A is derived from B by adding some “nonstandard” multiset a with the property

insert x a = a for all x.

This will not keep A and B from being observationally equivalent unless the multiset a is definable by some expression. However, there can be no homomorphism h since there is no reasonable choice for h(a).

Another shortcoming of homomorphisms may be explained by describing straightforward computer implementations of multisets. One way of representing a multiset is as a linked list of pairs of the form

⟨element,count⟩

where the natural number count is the number of times element has been inserted. The empty multiset is then the empty linked list, insert adds a new pair or increments the appropriate count, and the function count searches the list and returns the appropriate count. An alternative representation makes sense if we assume that small numbers 1, …, 10 will occur quite frequently, with other numbers much less likely. In this case, we might use an array of length 10 to count the number of times 1, …, 10 are inserted, together with a simple list of other insertions in the order they occur. Note that repeatedly inserting 12, for example, will result in 12 appearing several times in the list. With insert and count implemented properly, these two representations will be observationally equivalent. However, there can be no homomorphism from the first implementation to the second. To see why this is so, consider the result of inserting three elements into the empty multiset. To simplify notation, we will use the abbreviation

insert^{3} x y z =^{def} insert x (insert y (insert z empty)).

In the first representation, assuming x, y > 10, we have

insert^{3} x y x = insert^{3} x x y = ⟨⟨x, 2⟩, ⟨y, 1⟩⟩

whereas in the second representation.

insert^{3} x y x = Array; ⟨x, y, x⟩ ≠ Array; ⟨x, x, y⟩ = insert^{3} x x y.

Any homomorphism h from the first representation to the second would have to map the list of pairs ⟨⟨x, 2⟩, ⟨y, 1⟩⟩ to two values, but this is impossible. Conversely,

insert^{3} 1 2 3 = insert^{3} 3 2 1

in the second representation, since both set Array[1] = Array[2] = Array[3] = 1. However, in the first representation using lists of ⟨element,count⟩ pairs, insert^{3} 1 2 3 and insert^{3} 3 2 1 yield lists in different orders. So there is no homomorphism in either direction.

As the discussion illustrates, the correct characterization must be a combination of homomorphism and quotient of a subset, which is exactly what a logical relation provides. We state this as the following proposition.

Proposition 8.5.1 Implementations A and B for signature Σ with natural number multisets are observationally equivalent with respect to the natural numbers iff there is a logical relation R ⊆ A × B such that R^{nat} is the identity relation on the natural numbers.

We may derive Proposition 8.5.1 as a corollary of Theorem 8.5.4, which is proved in the next section. In general, when implementations A and B are observationally equivalent, there may be more than one logical relation R ⊆ A × B with R^{nat} the identity relation on the natural numbers.

Exercise 8.5.2 If we choose basic operations that treat integers as booleans, then we have less flexibility in reimplementing integers than if integers and booleans were separate types. To make this precise, consider the λ^{→} signature with

0, 1 : int
+, −, Eq? : int → int → int
cond : int → int → int → int

so that, writing if … then … else … for cond as usual, we have the implied typing rule

\frac{M: int, N: int, P: int}{if M then N else P: int}

Describe two implementations (algebras)

A = ⟨A^{int}, 0, 1, +, −, Eq?^{A}, cond^{A}⟩
B = ⟨B^{int}, 0, 1, +, −, Eq?^{B}, cond^{B}⟩

that both interpret 0, 1, +, − in the usual way, interpret if Eq? u v then x else y as x when u, v are equal and y when they are not, yet give different positive integer values to some integer expression without variables. This is similar to the situation for C [KR78], where integers, booleans and pointers are all given the same type. Although C is a typed programming language (with some type checks omitted in most implementations), even programs that do not take advantages of type loopholes such as type casts are more implementation dependent than would be the case if integers, booleans and pointers were separate types.

Exercise 8.5.3 Let A_{0} and B_{0} be multisorted algebras

A_{0} = ⟨A^{nat}, A^{s}, 0, 1, +, empty^{A}, insert^{A}, count^{A}⟩
B_{0} = ⟨B^{nat}, B^{s}, 0, 1, +, empty^{B}, insert^{B}, count^{B}⟩

for natural numbers and multisets, with A^{nat} = B^{nat} = N and A^{s} derived from B^{s} by adding a single multiset element a with the property

insert x a = a for all x ∈ N .

Let A and B be the lambda models defined from A_{0} and B_{0} by letting A^{σ → τ} be all total functions from A^{σ} to A^{τ}, and similarly for B^{σ → τ}. Describe a logical relation R ⊆ A × B with R^{nat} the identity relation. Is there more than one such relation? Explain.

8.5.3 General representation independence

We may generalize Proposition 8.5.1, stated for natural numbers and multisets, to any other data type, or collection of related data types. However, there are two aspects of natural numbers and multisets that are essential to the proposition as stated. The first is that all functions are first-order, which means that none of the function constants associated with natural numbers or multisets take function arguments. This is important, since characterizing observational equivalence of implementations becomes much more complicated with higher-order function constants, as illustrated in Exercise 8.5.6. The second factor is that we need a closed term naming each natural number (i.e., each element of observable type). The general situation is summarized in the following theorem about any signature giving a collection of possibly interdependent types and operations.

Theorem 8.5.4 Let Σ be some signature with type constant nat and let A and B be models, with A^{nat} = B^{nat} = N. If there is a logical relation R ⊆ A × B with R^{nat} the identity relation on natural numbers, then A and B are observationally equivalent. Conversely, if A and B are observationally equivalent, Σ provides a closed term for each element of N, and Σ only contains first-order functions, then there is a logical relation R ⊆ A × B with R^{nat} the identity relation.

Proof The first part of the theorem follows directly from the Basic Lemma (8.2.5). For the proof of the second part, we must construct a logical relation R ⊆ A × B. For each type constant s, we let R^{s} ⊆ A^{s} × B^{s} be the relation containing pair ⟨a, b⟩ iff there is a closed term M of type s whose meaning in A is a and whose meaning in B is b. We must show that for any function symbol f: s_{1} × … × s_{k} → s from Σ, if ⟨a_{i}, b_{i}⟩ ∈ R_{i}^{s} for i = 1, …, k, then ⟨f^{A}(a_{1}, …, a_{k}), f^{B}(b_{1}, …, b_{k})⟩ ∈ R^{s}. This follows easily from the definition of R^{s}. Since Σ provides a closed term for each element of N, it is easy to see that R^{nat} is the identity relation.

Exercise 8.5.5 Let Σ be a λ^{→} signature with type constants nat, s_{1}, …, s_{k} and only first-order function symbols. Let A and B be Henkin models for Σ with A^{nat} = B^{nat} = N and assume that every natural number is definable in A and B by some expression. Suppose A and B are observationally equivalent, let

A_{0} = ⟨A^{nat}, A^{s_{1}}, …, A^{s_{k}}, f_{1}^{A}, … f_{n}^{A}⟩

be the algebra with the same interpretation of type constants and function symbols as A, and define the algebra B_{0} from B similarly. Let ∼_{A}^{s}⊆ A^{s} × A^{s} be the least transitive relation such that if ∃b. R(a, b) ∧ R(a′, b) then a ∼_{A}^{s} a′. Define ∼_{B}^{s}⊆ B^{s} × B^{s} similarly.

(a) Show that {∼_{A}^{s}} is a partial congruence relation on A, as defined in Exercise 3.4.27. (You need not repeat the argument for {∼_{B}^{s}}.)

(b) Show that the two partial quotients A_{0}/ ∼_{A} and B_{0}/ ∼_{B} are isomorphic.

(c) Show that ∼_{A}^{nat} and ∼_{B}^{nat} are both the identity relation on the natural numbers.

Exercise 8.5.6 Let Σ be a λ^{→} signature with type constant nat and with term constants 0, 1, 2, 3, …: nat , +: nat → nat → nat and and f: (nat → nat) → nat . Let A be the full classical hierarchy over A^{nat} = N with 0, 1, 2, 3, … and + interpreted in the standard way and the interpretation of f to be determined. Let B be the same as A, except possibly for the interpretation of f. Show that we can choose f^{A} and f^{B} so that A and B are observationally equivalent, but there is no logical relation of the form described in Theorem 8.5.4, as follows:

(a) Assume we choose f^{A} so that for all computable g ∈ A^{nat → nat} we have f^{A}(g) = 0. Prove that for every term x_{1}: nat, …, x_{k}: nat ▷ M : nat over Σ, the meaning of M is a computable function of the values of x_{1}, …, x_{k}. (Hint: Use induction on terms given by the grammar M ::= x | 0 | … | M + M | f(λx: nat. M).)

(b) Show that if both f^{A} and f^{B} are interpreted as explained in (a), then A and B are observationally equivalent.

(c) Show that there is a choice for f^{A} and f^{B} so that A and B are observationally equivalent but any possible logical relation R ⊆ A × B with R^{nat} the identity fails to relate f^{A} and f^{B}.

8.6 Generalizations of logical relations

8.6.1 Introduction

We have seen that logical relations are useful for proving a variety of theorems about typed lambda calculus and for carrying out certain model-theoretic constructions. One reason to consider variations on the definition used so far in this chapter is that for languages with function constants, we need methods for constructing logical relations that respect the constants. An important example is a fixed-point constant is interpreted over cpo’s as the least-fixed point operator. Since the fixed-point constants are interpreted systematically, we may develop a specialized version of logical relations over cpo’s that are guaranteed to respect fixed-point operators. We will see that a class of directed-complete relations serve this purpose. Another reason to generalize the definition is that it only applies to Henkin models or applicative structures, but not arbitrary ccc’s. There are other forms of models, such as Kripke lambda models, where it is useful to have a form of logical relation. Therefore, we would like some general notion of “logical relation over a cartesian closed category” that would give us directed-complete and Kripke logical relations as special cases.

In the general theory we develop in this section, we form “logical relations” over a cartesian closed category C using a functor F into another category C′. There are two reasons for the functor F : C → C′. The first is that the categorical structure of C′ affects the kind of relation we obtain. For example, if we form relations using the functor | · | : Cpo → Set explained below, then we obtain standard logical relations over cpo’s. However, if we form relations using a particular functor F : Cpo → Cpo , then the cpo structure on the target category forces our relations to be closed under limits of directed sets. This gives us the directed-complete relations. The second reason we use a functor from the category C of interest to some auxiliary category C′ is that we need to be able to do certain operations on relations (or subsets, in the unary case). If C does not have sufficient structure, then we must construct our relations or subsets of objects of C in another category. The kind of categorical structure we need is that C′ must have equalizers (see Exercises 7.2.14 and 7.4.5).

The construction of “categorical logical relations” is motivated in Section 8.6.2, where we describe directed-complete relations over cpo’s, a natural form of Kripke logical relation and show a brief glimpse of their applications. The main mathematical tool is the category-theoretic method of sconing, described in Section 8.6.3. In a sense, the sconing construction gives a mathematical explanation for the definition of logical relation. More specifically, the definition in Section 8.2.1 appears to come out of thin air. We can see, from the list of applications of the Basic Lemma, that the definition is useful. However, it is not at all clear why this definition serves this purpose, or whether another definition would serve equally well. What sconing shows is that if we begin with a category C and try to construct a category of relations or predicates over C (using a functor C → C′), then the conditions we use in the definition of logical relation are exactly the definitions of product and function objects in the category of relations or predicates. Since products and function objects are unique (up to isomorphism) in any cartesian closed category, any other definition with the same uses would have to be isomorphic, in the categorical setting. This shows that there is something mathematical and canonical about the definition of logical relation. This explanation cannot be given using Henkin models alone, it seems, since the category of predicates or relations over a Henkin model is necessarily cartesian closed, but not necessarily a Henkin model (or well-pointed ccc). An interesting open problem is that we have no categorical explanation for logical relations over applicative structures that are not cartesian closed categories, such as the structure of typed lambda terms. The general development can be extended to polymorphic types, however. In treating polymorphic types, a central role is played by relators, which are maps that take objects to objects and relations to relations. The categorical ideas developed here may be used to express relators as functors.

Kripke logical relations over ordinary Henkin models were first used in [Plo80] in a characterization of lambda definability. Kripke logical relations were then adapted to Kripke lambda models in [MM91]. Inclusive relations (as well as strict inclusive relations) are widely used in relating denotational semantics and in proofs by fixed-point induction [MS76, Rey74a, CP92]. This section is based on [MS93], with many of the main ideas developed independently in [MR92]. Some applications may be found in [AJ91, BFSS89, Rey83, Wad89, OT93]. Sconing is described in general in [FS90]; it is called gluing or Freyd covers in [LS86, SS82].

8.6.2 Motivating examples: complete partial orders and Kripke models

Logical relations for complete partial orders

We would like a class of logical relations over cpo’s that respect terms with least fixed-point operators. By the Basic Lemma, it suffices to find logical relations that relate fixed-point operators fix_{σ} for each σ. Since we often construct logical relations by choosing a relation for each type constant, and then extending to all types inductively, we would like a condition that may be applied easily on the interpretation of a type constant. We may achieve this using conditions that resemble the conditions used to define cpo’s, completeness and (since we are interested in least fixed-points) pointedness.

A logical predicate R ⊆ A over an applicative structure of cpo’s is directed complete, or complete for short, if each R^{σ} is closed under limits of directed sets, i.e.,

if S ⊆ R^{σ} is directed, then ⋁ S ∈ R^{σ}.

A logical predicate R ⊆ A over an applicative structure of cpo’s is pointed at type σ if R^{σ}(⊥). Both conditions extend to binary logical relations by considering R ⊆ A × B as a unary logical predicate over the product structure A × B with (A × B)^{σ} = A^{σ} × B^{σ} the product cpo. In the literature, the term directed complete is often used to mean “pointed and directed-complete” since, historically, it has been common to include pointedness in the definition of cpo [MS76, Rey74a].

Lemma 8.6.1 Let R ⊆ A × B be a logical relation over full continuous hierarchies A and B. If R^{σ} and R^{τ} are complete, then so is R^{σ → τ}. Moreover, if A^{τ}, B^{τ} and R^{τ} ⊆ A^{τ} × B^{τ} are pointed, then R^{σ → τ} is pointed.

Proof Suppose R^{σ} and R^{τ} are complete and let S ⊆ R^{σ → τ} ⊆ A^{σ → τ} × B^{σ → τ} be a directed set of pairs of continuous functions. We must show that ⋁ S ∈ R^{σ → τ}, where by Lemma 5.2.2, ⋁ S = ⟨⋁ S_{1}, ⋁ S_{2}⟩, with S_{i} = Proj_{i}S.

Let ⟨a, b⟩ ∈ R^{σ} ⊆ A^{σ} × B^{σ}. It suffices to show that ⟨(⋁ S_{1})a, (⋁ S_{2})b⟩ ∈ R^{τ}. For each ⟨f, g⟩ ∈ S, we have ⟨fa, gb⟩ ∈ R^{τ}. Since {⟨fa, gb⟩ | ⟨f, g⟩ ∈ S} is easily seen to be directed, we have

⋁{⟨fa, gb⟩ | ⟨f, g⟩ ∈ S} ∈ R^{τ} .

It follows by Lemmas 5.2.2 and 5.2.10 that this least upper bound is equal to ⟨(⋁ S_{1})a, (⋁ S_{2})b⟩ and the first part of the lemma follows.

If R^{τ} (⊥, ⊥), then since ⊥_{σ → τ} = λx: σ. ⊥_{τ}, we can easily see that R^{σ → τ} (⊥, ⊥).

An easy argument shows that every complete logical relation which is pointed at the appropriate types preserves least fixed-point operators.

Lemma 8.6.2 Let R ⊆ A × B be a complete logical relation over full continuous hierarchies A and B. If A^{σ}, B^{σ} and R^{σ} ⊆ A^{σ} × B^{σ} are pointed, then R^{(σ → σ) → σ}(fix_{σ}^{A}, fix_{σ}^{B}), where fix_{σ}^{A} is the least fixed point operator on A^{σ → σ}, and similarly for fix_{σ}^{B}.

As a consequence, complete logical relations, appropriately pointed, relate the meanings of terms with fix . Proof For simplicity, we prove the unary case, R ⊆ A; this easily generalizes to n-ary relations using Lemmas 5.2.2 and 5.2.10 as in the proof of Lemma 8.6.1 above.

We must show that, under the conditions of the lemma, if R^{σ → σ}(f), then R^{σ}(fix f). By hypothesis, R^{σ}(⊥) and hence R^{σ}(f ⊥). An easy induction shows R^{σ}(f^{n} ⊥) for all n ≥ 0 and so by completeness and fix f = ⋁{f^{n}(⊥)} we have R^{σ}(fix f).

It follows from these two lemmas that if we wish to construct a logical relation between cpo models for a signature including fix at one or more types, it suffices to construct a complete logical relation, pointed appropriately, and check that it preserves all constants other than fix . This is illustrated in the following example, which gives a deceptively simple proof that parallel-or is not definable in PCF (Theorem 2.5.19). The argument is due to Plotkin (see [AC80]), and Sieber [Sie92], independently.

Example 8.6.3 There is a ternary logical relation R ⊆ A_{pcf} × A_{pcf} × A_{pcf} over the cpo model of PCF (given in Section 5.2.5) which demonstrates that parallel-or is not definable. For b = nat, bool , we let R^{b}(x, y, z) iff either x = y = z or at least one of x, y or z is ⊥ and extend this relation to product and function types inductively. Since each R^{b} is complete and pointed, so is every R^{σ}, by Lemma 8.6.1.

To show that R is a logical relation for PCF, we must check that R(c, c, c) for each constant of the signature. From Lemma 8.6.2, we have R(fix_{σ}, fix_{σ}, fix_{σ}) for each type σ. The remaining constants are +, Eq? and conditional.

For addition, we must show that if R^{nat}(x_{1}, y_{1}, z_{1}) and R^{nat}(x_{2}, y_{2}, z_{2}), then R^{nat}(x_{1} + x_{2}, y_{1} + y_{2}, z_{1} + z_{2}), where for notational simplicity we write + for the strict extension of addition to N_{⊥} × N_{⊥}. If any x_{i}, y_{i} or z_{i} is ⊥, then clearly one of the sums is ⊥. The remaining case, x_{1} = y_{1} = z_{1} and x_{2} = y_{2} = z_{2} , is immediate. The argument for Eq? is identical, since this is also a strict function. The argument for if … then … else … is slightly more interesting, and left as Exercise 8.6.10.

Now suppose that parallel-or is definable by a closed term POR . By the Basic Lemma, it follows that R^{(bool × bool) → bool}(POR, POR, POR). But since R^{bool}(true, ⊥, false) and R^{bool}(⊥, true, false), we must have

R^{bool}(POR true ⊥, POR ⊥ true, POR false false),

or R^{bool}(true, true, false), which is a contradiction.

More complicated methods are required for constructing directed-complete logical relations between recursively-defined domains. Some historical references on this topic are [MS76, Rey74a].

Kripke logical relations

While Kripke structures are not ordinary applicative structures, it is relatively easy to generalize logical relations to Kripke structures. The reason is that Kripke applicative structures are not only models of typed lambda calculus, but also provide a natural interpretation of logic. (This is the interpretation used in Kripke models of intuitionistic logic). In effect, we apply this interpretation of logic to the sentences used to define logical relations at function or product types. The main ideas for Kripke logical relations over ordinary Henkin models were first outlined in [Plo80], and then adapted to Kripke lambda models in [MM91]. We will show that every lambda theory is the theory of a Kripke quotient of a classical (ordinary Henkin) model, but not every Kripke lambda model is isomorphic to such a model.

Instead of having a relation for each type, we have a relation for each type and possible world, with the main condition quantifying over all possible future worlds. Specifically, a Kripke logical relation over Kripke applicative structures A and B sharing the same structure ⟨W, ≤⟩ of possible worlds is a family R = {R_{w}^{σ}} of relations R_{w}^{σ} ⊆ A_{w}^{σ} × B_{w}^{σ} indexed by types σ and worlds w ∈ W satisfying the following three conditions. The first is a “monotonicity” condition

(mon) R_{w}^{σ}(a, b) implies R_{w′}^{σ}(i_{w,w′}^{σ}a, i_{w,w′}^{σ}b) for all w′ ≥ w,

which says that when w ≤ w′, the relation R_{w}^{σ} is contained in R_{w′}^{σ}, modulo the transition functions. The second condition

(compre) R_{w}^{σ → τ} (f, g) iff ∀w′ ≥ w.∀a, b. R_{w′}^{σ}(a, b) implies R_{w′}^{τ}((i_{w,w′}^{σ → τ} f)a, (i_{w,w′}^{σ → τ} g)b),

called “comprehension,” says that the relation R_{w}^{σ → τ} contains all functions mapping related arguments to related results. The third condition is that constants of the language must be related at every possible world. This completes the definition.

It is easy to show that if (mon) holds for each type constant, it holds for all types (Exercise 8.6.11.) We say environments η_{a}, η_{b} are related by R on Γ at w if R_{w}^{τ}(η_{a}xw, η_{b}xw) for all x: τ in Γ. The following Basic Lemma is proved by induction on terms in Exercise 8.6.12.

Lemma 8.6.4 (Basic Lemma for Kripke logical relations) If R ⊆ A × B is a Kripke logical relation over models A and B, and environments η_{a}, η_{b} are related by R on Γ at w, then for every term Γ ▷ M : σ, we have R_{w}^{σ}(A[[Γ ▷ M : σ]]η_{a}w, B[[Γ ▷ M : σ]]η_{b}w)

We can form quotients of Kripke lambda models using Kripke partial equivalence relations. Like logical partial equivalence relations, a Kripke logical partial equivalence relation R ⊆ A × A is a Kripke logical relation such that each R_{w}^{σ} is symmetric and transitive. We will abbreviate the cumbersome phrase “Kripke logical partial equivalence relation” to klper. The following lemma, proved as Exercise 8.6.13, shows that klper’s may be constructed by choosing relations at base types.

Lemma 8.6.5 Let R ⊆ A × A be a Kripke logical relation. If each R_{w}^{c} is symmetric and transitive, for each base type c and world w ∈ W, then every R_{w}^{σ} is symmetric and transitive.

If

A = ⟨W, ≤, {A_{w}^{σ}}, {App_{w}^{σ,τ} }, {i_{w,w′}^{σ}}, Const⟩

is a Kripke applicative structure and R ⊆ A × A is a klper, then the quotient applicative structure

A/R = ⟨W, ≤, {A_{w}^{σ}/R_{w}^{σ}}, {App_{w}^{σ,τ} /R}, {i_{w,w′}^{σ}/R}⟩

is defined as follows:

A_{w}^{σ}/R_{w}^{σ} = { [a]_{R} | R_{w}^{σ}(a, a) }, where [a]_{R} is the equivalence class
[a]_{R} = { a′ ∈ A_{w}^{σ} | R_{w}^{σ}(a, a′) }

(App_{w}^{σ,τ} /R) [a]_{R} [b]_{R} = [App_{w}^{σ,τ} a b]_{R}
(i_{w,w′}^{σ}/R) [a]_{R} = [i_{w,w′}^{σ} a]_{R}

It is a simple exercise, similar to the proof of Lemma 8.2.24, to verify that the quotient structure is well-defined, and a Kripke applicative structure.

Lemma 8.6.6 If R ⊆ A × A is a Kripke partial equivalence relation over Kripke applicative structure A, then A/R satisfies the Kripke extensionality condition (ext).

A straightforward induction on terms similar to the proof of Lemma 8.2.26, may be used to prove the following “quotient model” theorem.

Lemma 8.6.7 If R ⊆ A × A is a klper over Kripke lambda model A, then A/R is a Kripke lambda model such that for every environment η with R_{w}^{τ}(ηxw, ηxw) for all x: τ in Γ, we have

(A/R)[[Γ ▷ M : σ]]η_{R}w = [ A[[Γ ▷ M : σ]]ηw]_{R},

where the environment η_{R} for A/R is defined by taking η_{R}xw = [ηxw]_{R} for all x and w.

In short, the meaning of a term M in the quotient model A/R is the equivalence class of the meaning of M in A.

We now consider Kripke logical relations over classical applicative structures. The simplest way to do this is to regard classical structures as a special case of Kripke structures, as illustrated in Exercise 7.3.5. We say R = {R_{w}^{σ}} is a Kripke logical relation over classical applicative structures A and B if R is a Kripke logical relation over the Kripke models A^{W} and B^{W} defined in Exercise 7.3.5. By Lemma 8.6.7, we can produce Kripke models by taking Kripke quotients of classical models. This gives us a fairly simple class of models with intuitionistic properties. In fact, we can show that every lambda theory is the theory of a model of this form.

Theorem 8.6.8 Let E be any set of equations closed under ⊢. There exists an ordinary (classical) Henkin model A and a Kripke partial equivalence relation R ⊆ A × A such that A/R satisfies precisely those equations that belong to E.

Proof Let B be the Kripke term model for E, as in the proof of Theorem 7.3.7. Since B satisfies precisely the equations in E, we will show that B is isomorphic to a Kripke quotient of the classical term model A of β, η-conversion, which is summarized in the proof of Theorem 4.5.22.

For the specific theory of β, η-conversion, the classical term model A is constructed by choosing an infinite set H of variable typings x: σ with two properties. There must be infinitely many variables of each type and no variable may appear twice. We define the equivalence class [M] of M by

[M] = { N | ⊢ Γ ▷ M = N : τ, some finite Γ ⊆ H }

and let A^{τ} be the collection of all [M] with Γ▷M : τ for some Γ ⊆ H. This gives us an applicative structure, with

App [M] [N] = [MN].

As clarified in Section 8.3.1, this is a model with the meaning of a term obtained by substitution.

Using E, we can define a klper R over A. Our goal is to define R so that the quotient A/R is isomorphic to the Kripke term model B. Since the possible worlds of B are type assignments, we will use type assignments as the worlds of R.

For each σ and Γ, we define the relation R_{Γ}^{σ} ⊆ A^{σ} × A^{σ} by

R_{Γ}^{σ}([M], [N]) iff E ⊢ Γ ▷ M^{0} = N^{0} : σ,

where M^{0} is the β, η-normal form of M, and similarly for N^{0} . This is well defined since each [M] has a unique β, η-normal form. Since provable equality is symmetric and transitive with respect to any Γ, R is clearly a partial equivalence relation. (In general, R_{Γ}^{σ} will not be reflexive on B^{σ}, since some M^{0} may require variables not in in Γ.) By rule (add var), R satisfies the monotonicity condition (mon). The proof that R satisfies (compre) is similar to the proof that Kripke term models are extensional.

It remains easy to show that B is isomorphic to A/R. Every A^{σ}/R_{Γ}^{σ} equivalence class is characterized by a collection of normal forms that are all well-typed in Γ and provably equal using E. Thus for each A^{σ}/R_{Γ}^{σ} equivalence class [M]/R_{Γ}^{σ}, there is a unique [Γ▷M^{0} : σ] ∈ B_{Γ}^{σ}. Conversely, all of the β, η-normal forms in any [Γ ▷ M^{0} : σ] will be equivalent modulo R_{Γ}^{σ}, and so we have a straightforward bijection between B^{σ} and A^{σ}/R_{Γ}^{σ}. It is easy to show that application behaves appropriately, and so we have an isomorphism between A and B/R. This proves the theorem.

However, we can show that some Kripke lambda models are not isomorphic to any Kripke quotient of any classical applicative structure.

Theorem 8.6.9 There is a Kripke lambda model B which is not isomorphic to A/R, for any classical applicative structure A and Kripke partial equivalence relation R. In fact, B is distinguished from all A/R by a formula of predicate logic.

Proof The main idea is relatively simple. Suppose R ⊆ A × A is a Kripke logical partial equivalence relation over a classical applicative structure, and suppose we have two type constants a and b with R_{w}^{a} empty at all possible worlds. Then R_{w}^{a → b}(f, g) for all worlds w and all f, g ∈ A^{a → b}, since the implication

R_{w}^{a}(x, y) implies R_{w}^{b}(Appfx, Appgy)

holds vacuously. In particular, if A^{b}/R^{b} is non-empty at any world, so that A^{a → b} is non-empty, then A^{a → b}/R^{a → b} is nonempty at all possible worlds. Those familiar with the intuitionistic interpretation of predicate logic in Kripke structures will easily see that this property of Kripke quotients of classical structures can be expressed by a formula

if empty(a) and ¬empty(a → b), then inhabited(a → b),

where inhabited(τ) ≡ (∃x: τ.x = x) and empty(τ) ≡ ¬inhabited(τ).

To show that this property fails in some models, we consider the following Kripke lambda model B defined by:

• W is the poset with two elements 0 < 1,

• B at 1 is the full classical hierarchy over B^{a} = ∅ and B^{b} = N,

• B at 0 is the set of lambda-definable elements from B at 1, i.e., the applicative structure whose elements are interpretations of closed λ-terms,

• the transition function i_{0,1} is the inclusion.

Then A_{1}^{a → b} contains exactly one element (the empty function), and therefore B satisfies ¬empty(a → b); but A_{0}^{a → b} is empty (because there are no closed terms of that type), so B does not satisfy inhabited(a → b).

Exercise 8.6.10 Show that for the logical relation R ⊆ A_{pcf} × A_{pcf} × A_{pcf} given in Example 8.6.3, if one of x, y, z ∈ A^{σ} is ⊥_{σ}, then R^{σ}(x, y, z). Use this to show that

R^{(bool × σ × σ) → σ}(cond, cond, cond).

where cond x y z = if x then y else z.

Exercise 8.6.11 Let R ⊆ A × B be a family R = {R_{w}^{σ}} of relations R_{w}^{σ} ⊆ A_{w}^{σ} × B_{w}^{σ} indexed by types σ and worlds w ∈ W of Kripke models A and B satisfying (mon) for type constants only, and (compre) and preserving all constants. Show that R is a Kripke logical relation by showing that A satisfies (mon) at all types.

Exercise 8.6.12 Prove the Basic Lemma for Kripke logical relations by induction on terms.

Exercise 8.6.13 Prove Lemma 8.6.5 by induction on types.

8.6.3 Sconing and relations

As explained in Section 8.6.1, we develop a general form of logical relation over a category C using a functor F : C ⟶ C′, forming the relations or predicates in C′ in some way. Thinking only about the unary case, with predicates, for the moment, we can see that C′ must have a “set-like” character so that we can identify subsets easily and do certain constructions on subsets. For concreteness, we begin by choosing a specific functor into Set , definable from any C with a terminal object. This simplifies the problem of subset operations and lets us focus on the relationship between the category C of interest and the category of subsets of C. We generalize to other categories in Section 8.6.5.

Assuming that C is a category with a terminal object unit , we will use the functor | · | from C to Set which maps each object to its set of global elements. This functor is defined by

|A| = the set of all morphisms unit ⟶ A in C
|x| = the function |A| ⟶ |A′| defined by composition according to

the diagram below, for any morphism x: A ⟶ A′ in C

[figure: 1; A′; x; A]

It is not hard to see that this functor preserves products up to isomorphism, which means that |A × B| ≅ |A| × |B|; see Exercise 8.6.16. The functor also preserves equalizers up to isomorphism, but we will not need this fact. However, equalizers will come into play in the general construction. (Some properties of equalizers are given in Exercise 7.4.5.)

The category Ĉ, called the scone of C, is defined as follows. Intuitively, the scone of C is the category of “set preimages” of objects of C, where “set preimages” are determined after applying the functor | · | into Set . We will specialize this construction below from “preimages” to subsets. The objects of Ĉ are triples ⟨S, f, A⟩, where S is a set, A is an object of C , and f: S ⟶ |A| is a function (in Set ). The morphisms ⟨S, f, A⟩ ⟶ ⟨S′, f′, A′⟩ in Ĉ are pairs ⟨t, x⟩, where t: S ⟶ S′ is a function and x: A ⟶ A′ is a morphism in C such that:

S  t  S′ |A|  |x|  |A′|f′ f

The reader may easily check that ⟨|unit|, id, unit⟩ is a terminal object in Ĉ. There is a canonical “forgetful” functor π: Ĉ ⟶ C which takes ⟨S, f, A⟩ to A and ⟨t, x⟩ to x. Category theorists will recognize the scone as a special case of a comma category, namely Ĉ = (id ↓ | · |), where id is the identity functor on Set (see Exercise 7.2.25). It is common to overload notation and use the symbol Set for the identity functor from sets to sets (and similarly for other categories). With this convention, we may write Ĉ = (Set ↓ | · |).

A remarkable feature of sconing in general is that it preserves almost any additional categorical structure that C might have. Since we are interested in cartesian closed structure, we show that sconing preserves terminal object, products and function objects (exponentials).

Lemma 8.6.14 If C is a cartesian closed category, then Ĉ is cartesian closed and the canonical functor π: Ĉ ⟶ C is a cartesian closed functor.

Proof Let X = ⟨S, f, A⟩ and Y = ⟨S′, f′, A′⟩ be objects of Ĉ. Then the object

X × Y = ⟨S × S′, f × f′, A × A′⟩,

is a product of X and Y , where (f × f′)⟨s, s′⟩ = ⟨f(s), f′(s′)⟩. A function object of X and Y is given by

X → Y = ⟨M, h, A → A′⟩,

where M is the set of morphisms X ⟶ Y in Ĉ and h(⟨t, x⟩): unit ⟶ A → A′ is the morphism in C obtained from x: A ⟶ A′ by currying, i.e., h(⟨t, x⟩) = Curryx. We leave it to the reader, in Exercise 8.6.17, to check that π: Ĉ ⟶ C is a cartesian closed functor.

In order to make a connection with logical predicates or relations, we will be interested in a subcategory C̃ of the scone which we call the subscone of C. The objects of the subscone C̃ are the triples ⟨S, f, A⟩ with f: S ↪ |A| an inclusion of sets. It is possible to let f: S ↪ |A| be any one-to-one map. But, since we are really more interested in the map |x|: |A| ⟶ |A′| in the diagram above than |t|: S ⟶ S′, for reasons that will become clear, we will assume that if ⟨S, f, A⟩ is an object of C̃, then S ⊆ |A| is an ordinary set-theoretic subset and f: S → |A| is the identity map sending elements of S into the larger set |A|. The morphisms ⟨S, f, A⟩ ⟶ ⟨S′, f′, A′⟩ of C̃ are the same as for Ĉ, so C̃ is a full subcategory of Ĉ. If ⟨t, x⟩ is a morphism from ⟨S, f, A⟩ to ⟨S′, f′, A′⟩ in C̃, then the set function t: S ⟶ S′ is uniquely determined by x and S. Specifically, t is the restriction of |x|: |A| ⟶ |A′| to the subset S ⊆ |A|.

The subcategory C̃ inherits the cartesian closed structure of Ĉ, up to isomorphism. More precisely, C̃ is a subcategory of Ĉ that is also cartesian closed. However, given two objects, X and Y , from C̃, the function object X → Y = ⟨M, h, A → A′⟩ given in the proof of Lemma 8.6.14 is not an object of C̃ since M is not a subset of |A → A′|. However, the function object for X and Y in C̃ is isomorphic to the function object in Ĉ. Instead of describing function objects in C̃ directly for arbitrary C, we will take this up in the illustrative special case that C is a product of two ccc’s.

Let us suppose we have a product category C = A × B, where both categories A and B have a terminal object. Recall that the objects of A × B are ordered pairs of objects from A and B and the morphisms ⟨A, B⟩ ⟶ ⟨A′, B′⟩ are pairs ⟨x, y⟩, where x: A ⟶ A′ is a morphism in A and y: B ⟶ B′ is a morphism in B . It is easy to see that when A and B are cartesian closed, so is A × B, with coordinate-wise cartesian closed structure. For example, a terminal object of A × B is ⟨unit, unit⟩. It is easy to see that |⟨A, B⟩|_{C} = |A|_{A} × |B|_{B} , where the cartesian product of |A|_{A} and |B|_{B} is taken in sets. We will often omit the subscripts from various | · |’s, since these are generally clear from context.

The objects of the scone Â×B may be described as tuples ⟨S, f, g, A, B⟩ , with S a set, A an object in A, B an object in B, and f and g functions that form a so-called span:

[figure: S; g; f; |A|; |B|]

The morphisms ⟨S, f, g, A, B⟩ ⟶ ⟨S′, f′, g′, A′, B′⟩ in Â×B may be described as tuples ⟨t, x, y⟩ , with x: A ⟶ A′ a morphism in A, y: B ⟶ B′ a morphism in B, and t: S ⟶ S′ a function such that:

[figure: |A|; |x|; |A′|; f; g; f′; g′; |B|; |y|; |B′|; S; t; S′]

Let us now look at the subcategory Ã×B of Â×B. Working through the definition of Ã×B, we may regard the objects of this subcategory as tuples ⟨S, f, g, A, B⟩, where f and g provide an inclusion S ↪ |A| × |B|. Since S, f and g determine a subset of |A| × |B|, as before, an object ⟨S, f, g, A, B⟩ may be expressed more simply as a triple ⟨S, A, B⟩ with S an ordinary binary relation on |A| × |B|. For any morphisms ⟨t, x, y⟩ between objects of Ã×B, the set map t is again uniquely determined by A and B maps x and y and the relation S. Specifically, t is the restriction of the product map |x| × |y| to the subset S. This allows us to simply write morphisms as pairs, instead of triples. It is easy to see that ⟨x, y⟩ forms a morphism from ⟨S, A, B⟩ to ⟨S′, A′, B′⟩ exactly if, for all morphisms a: unit ⟶ A in A and b: unit ⟶ B in B, we have

a S b implies (x ∘ a) S′ (y ∘ b),

where we use relational notation a S b to indicate that S relates a to b , and similarly for S′.

With some additional notation, we can express the definition of morphism in Ã×B as a form of “commuting square.” To begin with, let us write S: |A| −×|B| to indicate that S is a binary relation on |A| × |B|. The definition of morphism now has an appealing diagrammatic presentation as a pair ⟨x, y⟩ satisfying

|A|  |x|  |A′| |B|  |y|  |B′|S′ S  ⊆

where “⊆” in this diagram means that the relation |y| ∘ S is included in the relation S′ ∘ |x|.

It is instructive to write out the function objects (exponentials) in the cartesian closed category Ã×B. The function object ⟨S, A, B⟩ →⟨S′, A′, B′⟩ may be written ⟨R, A → A′, B → B′⟩, where R: |A → A′| −×|B → B′| is the binary relation such that for all morphisms e: unit ⟶ A → A′ in A and d: unit ⟶ B → B′ in B, we have

e R d iff a S b implies App ∘ ⟨e, a⟩ S′ App ∘ ⟨d, b⟩

for all a: unit ⟶ A in A, b: unit ⟶ B in B.

We may also express products in a similar fashion. As in the general case, the subscone C̃ is a ccc and a full subcategory of Ĉ, and the restriction of the forgetful functor Ĉ ⟶ C to C̃ is also a cartesian closed functor. The main properties of Ã×B are summarized in the following proposition, whose proof is left as Exercise 8.6.18.

Proposition 8.6.15 Let C = A × B be the cartesian product of two ccc’s. Then C̃ is a cartesian closed category, with canonical functor C̃ ⟶ C a cartesian closed functor. Products and function objects in C̃ are given by

⟨S, A, B⟩ ×⟨S′, A′, B′⟩ = ⟨S × S′, A × A′, B × B′⟩,
⟨S, A, B⟩ →⟨S′, A′, B′⟩ = ⟨S → S′, A → A′, B → B′⟩,

where the relations S × S′ and S → S′ have the following characterizations:

a (S × S′) b iff (Proj_{1} ∘ a) S (Proj_{1} ∘ b) and (Proj_{2} ∘ a) S′ (Proj_{2} ∘ b)
e (S → S′) d iff ∀a: unit ⟶ A. ∀b: unit ⟶ B. a S b implies App ∘ ⟨e, a⟩ S′ App ∘ ⟨d, b⟩.

At this point, it may be instructive to look back at the definition of logical relations in Section 8.2.1 and see the direct similarity between the descriptions of products and function objects in this proposition and the definition of logical relations over an applicative structure or Henkin model. The difference is that here we have generalized the definition to any cartesian closed category, forming relations in Set after applying the functor | · |.

Exercise 8.6.16 Show that for any category C with products and terminal object, the functor | · | from C to Set preserves products up to isomorphism, i.e., |A × B| ≅ |A| × |B| for all objects A and B of C.

Exercise 8.6.17 Show that for any ccc C, the map π: Ĉ ⟶ C defined in this section is a functor that preserves terminal object, products and function objects. Begin by showing that π is a functor, then check that π(X × Y) = πX × πY for all objects X = ⟨S, f, A⟩ and Y = ⟨S′, f′, A′⟩ of Ĉ, and similarly for function objects and the terminal object.

Exercise 8.6.18 Prove Proposition 8.6.15.

(a) Show that ⟨S, A, B⟩ ×⟨S′, A′, B′⟩ = ⟨S × S′, A × A′, B × B′⟩ is a product in C̃.

(b) Show that ⟨S, A, B⟩ →⟨S′, A′, B′⟩ = ⟨S → S′, A → A′, B → B′⟩ is a function object in C̃.

(c) Show that the functor π: C̃ ⟶ C is a cartesian closed functor.

Exercise 8.6.19 Show that if C is a well-pointed category, then so is C̃.

8.6.4 Comparison with logical relations

In this section, we describe the connection between logical relations and subscones, for the special case of cartesian closed categories determined from Henkin models, and show how the Basic Lemma may be derived from a simple categorical properties of the subscone. Since a logical predicate P ⊆ A is a family of predicates {P^{σ}} indexed by the types over the signature of A, we can think of a logical predicate as a mapping from types over some signature to subsets of some structure. We will see that a mapping of this form is determined by the categorical interpretation of lambda terms in the subscone of a ccc.

In discussing the interpretation of terms in cartesian closed categories in Section 7.2.4, we used a structure called a Σ-ccc, where Σ may be any λ^{unit,×,→} signature. The difference between a ccc and a Σ-ccc is that a Σ-ccc A is equipped with a specific choice of object A^{b} for each type constant b of Σ, and a morphism ĉ: unit ⟶ A for each term constant of Σ. Since a Σ-ccc associates an object or arrow with each symbol in Σ, we can think of a Σ-ccc as a cartesian closed category A together with a mapping Σ ⟶ A from the signature into the category.

For any λ^{unit,×,→} signature Σ and set E of equations between Σ-terms, there is a ccc C_{Σ}(E) called the term category generated by E, as described in Example 7.2.19. There is a canonical mapping Σ ⟶ C_{Σ}(E) presenting C_{Σ}(E) as a Σ-ccc, namely, the function mapping each type constant to itself and each term constant to its equivalence class, modulo E. As shown in Proposition 7.2.46, there is a unique cartesian closed functor from C_{Σ}(∅) to any other Σ-ccc D. (The categorical name for this is that C_{Σ}(∅) is the free cartesian closed category over signature Σ.) If we draw in the mappings from Σ, then such a cartesian closed functor forms a commuting triangle

[figure: D; C_{Σ}(∅); Σ]

since the interpretation of a type or term constant is determined by the way that D is regarded as a Σ-ccc. As explained in Section 7.2.6, the cartesian closed functor from C_{Σ}(∅) into a Σ-ccc D is the categorical equivalent of the meaning function associated with a Henkin model.

It is really only a matter of unraveling the definitions, and using Proposition 8.6.15, to see that the logical predicates over a Henkin model A for signature Σ correspond to ways of regarding the subscone of the category C_{A} determined A as a Σ-ccc. More specifically, let C = C_{A} be the cartesian closed category determined by Henkin model A, as explained in Section 7.2.5, regarded as a Σ-ccc in the way that preserves the meaning of terms. By Theorem 7.2.41, C is a well-pointed cartesian closed category, with the morphisms unit ⟶ σ exactly the elements of A^{σ} from the Henkin model A. If we consider a cartesian closed functor F from the term category C_{Σ}(∅) into the subscone C̃ of C, then the object map of this functor designates an object F(σ) = ⟨P^{σ}, σ⟩, with P ⊆ |σ| for each type σ. But since |σ| = A^{σ}, a meaning function into the subscone chooses a subset of the Henkin model at each type. It is easy to see from Proposition 8.6.15 that the family of predicates determined by the object map of a cartesian closed functor C_{Σ}(∅) → C̃ is in fact a logical relation. This gives us the following proposition.

Proposition 8.6.20 Let C = C_{A} be the well-pointed Σ-ccc determined by the Henkin model A for signature Σ. Then a logical predicate on A is exactly the object part of a cartesian closed functor from the term category C_{Σ}(∅) over Σ into the Σ-ccc C̃.

Using product categories, Proposition 8.6.20 gives us a similar characterization of logical relations over any number of models. For example, if C = C_{A} × C_{B} is determined from Henkin models A and B, then C and C̃ are again well-pointed cartesian closed categories (see Exercise 8.6.19) and a meaning function into C̃ is a logical relation over Henkin models A and B.

Using the correspondence given in Proposition 8.6.20, we can see that the Basic Lemma for logical relations is a consequence of the commuting diagram given in the following proposition.

Proposition 8.6.21 Let Σ be a λ^{unit,×,→} signature and let C be a cartesian closed category. Consider any mapping Σ → C̃ presenting C̃ as a Σ-ccc. Composing with the canonical functor C̃ ⟶ C, we obtain a corresponding map Σ → C and, by the natural embedding of symbols into the term category, we have a similar map Σ → C_{Σ}(∅) into the term category. Given these three maps from Σ, there exist unique cartesian closed functors from C_{Σ}(∅) into C and C̃ commuting with the canonical functor C̃ ⟶ C as follows:

[figure: C; C̃; Σ; C_{Σ}(∅)]

Proof Let functions from Σ to objects of the ccc’s C, C̃ and C_{Σ}(∅) be given as in the statement of the proposition. It is a trivial consequence of the definitions that the triangle involving Σ, C̃ and C commutes. By Proposition 7.2.46, the cartesian closed functors C_{Σ}(∅) → C and C_{Σ}(∅) → C̃ are uniquely determined. This implies that the two triangles with vertices Σ, C_{Σ}(∅) and either C̃ or C commute. Finally, since the canonical functor π: C̃ ⟶ C is a cartesian closed functor (see Proposition 8.6.15), the two uniquely determined cartesian closed functors from C_{Σ}(∅) must commute with this functor.

It is again a matter of unraveling definitions to see how the Basic Lemma follows from this diagram. Let us consider the binary case with A and B given by Henkin models A and B of simply typed lambda calculus. Then both C = A × B and C̃ are well-pointed cartesian closed categories. The cartesian closed functor C_{Σ}(∅) → C maps a typed lambda term x: σ ▷ M : τ to the pair of morphisms giving the meaning of M in A and, respectively, the meaning of M in B. The cartesian closed functor C_{Σ}(∅) → C̃ maps a typed lambda term x: σ ▷ M : τ to a morphism from some subset S ⊆ |C_{A}[[σ]] × C_{B}[[σ]]| = A^{σ} × B^{σ} to a subset S′ ⊆ |C_{A}[[τ]] × C_{B}[[τ]]| = A^{τ} × B^{τ}, where C_{A}[[σ]] is the object of A named type expression σ, and similarly for C_{B}[[σ]] and so on. As noted in Section 8.6.3, such a morphism in the subscone is a product map f × g with f: C_{A}[[σ]] ⟶ C_{A}[[τ]] and g: C_{B}[[σ]] ⟶ C_{B}[[τ]] which maps a pair ⟨u, v⟩ with u S v to a pair ⟨f(u), g(v)⟩ with f(u) S′ g(v). Because the two cartesian closed functors of C_{Σ}(∅) commute with the functor π: C̃ → C, f must be the meaning f = A[[x: σ ▷M : τ]] of the term M in A, regarded as a function of the free variable x, and similarly g = B[[x: σ ▷ M : τ]]. Because the term x: σ ▷ M : τ was arbitrary, and σ may be a cartesian product of any types, we have shown that given logically related interpretations of the free variables, the meaning of any term in A is logically related to the meaning of this term in B. This is precisely the Basic Lemma for logical relations over Henkin models.

8.6.5 General case and applications to specific categories

The definition of scone and subscone of a category C rely on the functor | · | from C into Set . However, since relatively few properties of Set are used, we can generalize the construction and associated theorems to other functors and categories. We begin by stating the basic properties of the “generalized scone” and “subscone,” then continue by deriving Kripke logical relations and directed-complete logical relations (from Section 8.6.2) as special cases.

Proposition 8.6.14 holds in a more general setting with Set replaced by any cartesian closed category C′ with equalizers and the functor | · |: C ⟶ Set replaced by any functor F: C ⟶ C′ that preserves products up to isomorphism, by essentially the same proof. This takes us from the specific comma category Ĉ = (Set ↓ | · |) to a more general case of the form (C′ ↓ F).

Proposition 8.6.22 Let C and C′ be cartesian closed categories and assume C′ has equalizers. Let F: C ⟶ C′ be a functor that preserves finite products up to isomorphism. Then the comma category (C′ ↓ F) is a cartesian closed category and the canonical functor π: (C′ ↓ F) ⟶ C is a cartesian closed functor.

The next step is to identify generalizations of the subscone. The proof of Proposition 8.6.21 actually establishes the general version where instead of C̃, we may consider any ccc D that has a cartesian closed functor into C. We will be interested in situations where D is a subcategory of a comma category (C′ ↓ F), such that the restriction of the canonical cartesian closed functor π: (C′ ↓ F) ⟶ C to D is a cartesian closed functor.

Proposition 8.6.23 Let C and C′ be cartesian closed categories and assume C′ has equalizers. Let F: C ⟶ C′ be a functor that preserves products and let D be a sub-cartesian-closed category of the comma category (C′ ↓ F). Let Σ be a λ^{unit,×,→} signature and consider any mapping Σ → D presenting D as a Σ-ccc. Composing with the canonical functor D ⟶ C, we obtain a corresponding map Σ → C and, by the natural embedding of symbols into the term category, we have a similar map Σ → C_{Σ}(∅) into the term category. Given these three maps from Σ, there exist unique cartesian closed functors from C_{Σ}(∅) into C and D commuting with the canonical functor D ⟶ C as follows:

[figure: C; D; Σ; C_{Σ}(∅)]

Sconing with Kripke models

If P is a partially ordered set, then we may consider P as a category whose objects are the elements of P and morphisms indicate when one element is less than another, as described in Example 7.2.6. As shown in Section 7.3.7, each Kripke lambda model with P as the set of “possible worlds” determines a cartesian closed category C that is a subcategory of the functor category Set^{P}. The inclusion F of C into category Set^{P} preserves products, since the interpretation of a product type in a Kripke lambda model is the same as cartesian product in Set^{P}. By Exercise 7.2.14, Set^{P} has equalizers and we can apply Propositions 8.6.22 and 8.6.23

For the appropriate analog of subscone, we take the subcategory with an inclusion at each “possible world.” More specifically, let D be the full subcategory of the comma category (Set^{P} ↓ F) that consists of objects ⟨S, f, A⟩ with f_{p}: S(p) ↪ F(A)(p) an inclusion for each p in P. By assuming these are ordinary subsets, we may omit f when referring to objects of D. It may be shown that D is a ccc (Exercise 8.6.24). In describing function objects (exponentials) in D we may use natural transformations F(app_{A,A′}): F(A → A′) × F(A) ⟶ F(A′) because the functor F preserves binary products. For each object C in C and each p ≤ p′ in P, we also use the transition function F(C)(p ≤ p′): F(C)(p) → F(C)(p′) given by the action of the functor F(C): P → Set on the order of P. Specifically, ⟨S, A⟩ →⟨S′, A′⟩ may be given as ⟨P, A → A′⟩, where A → A′ is taken in C and P: P → Set is the functor such that the set P (p) consists of all t in F(A → A′)(p) for which for all p′ ≥ p and all a in F(A)(p′), if a belongs to S(p′), then the element F(app_{A,A′})_{p′}(F(A → A′)(p ≤ p′)(t), a) in F(A′)(p′) belongs to S′(p′). In other words, the object parts of the unique cartesian closed functor from the term category into D in this case amount to the Kripke logical predicates on the Kripke lambda model that corresponds to F.

In the binary case, we let A and B be cartesian closed categories and let F: A → Set^{P} and G: A → Set^{P} finite product preserving functors given by Kripke lambda models A and B, each with P as the poset of possible worlds. Let H: A × B → Set^{P} be the functor given by H(A, B) = F(A) × G(B). Continuing as above, with C = A × B and with H instead of F, we can see that the object parts of the cartesian closed functors into D are exactly the Kripke logical relations on Kripke lambda models A and B.

Sconing with cpo’s

Since Cpo is a cartesian closed category with equalizers (by Exercise 7.2.14), we may also form a generalized scone using functors into Cpo . This is like the case for Kripke models, except that we have the added complication of treating pointed cpo’s properly; our relations must preserve the bottom element in order to preserve fixed points, as illustrated in Section 8.6.2. It might seem reasonable to work with the category Cppo of pointed cpo’s instead, since relations taken in Cppo would have to have least elements. However, the category Cppo does not have equalizers (by Exercise 7.2.14). Moreover, we may wish to construct logical relations which are closed under limits at all types, but which are only pointed where needed to preserve fixed points. A general approach would be to use lifted types, and extend the lifting functor from Cpo to the appropriate comma category. This would give “lifted relations” on lifted types, which would necessarily preserve least elements. A less general alternative, which we will describe below, is to simply work with subcategories where predicates or relations are pointed when needed. This is relatively ad hoc, but is technically simpler and (hopefully) illustrates the main ideas.

Since we are interested in preserving fixed-point operators, we let the signature Σ be a signature that may include fixed-point constants at one or more types, and let E_{fix} be the set of equations of the form fix_{σ} = λf: σ → σ. f(fix f) for each type σ that has a fixed-point operator in Σ. The category C_{Σ}(E_{fix}) is the term category of simply typed lambda calculus with with one or more fixed-point constants, each with its associated equational axiom. By Proposition 7.2.46, there is a unique cartesian closed functor C_{Σ}(E_{fix}) ⟶ C from C_{Σ}(E_{fix}) to any Σ-ccc satisfying the fixed-point equations. In particular, there is a unique such functor into any Σ-ccc of cpo’s.

If we use | · |: Cpo ⟶ Set , then the scone (Set ↓ | · |) allows us to form logical predicates or relations over cpo’s. However, these relations will not be directed complete. Instead, we let I be the identity functor on Cpo and consider the comma category (Cpo ↓ I). This could also be written (Cpo ↓ Cpo), since we are using Cpo as a convenient shorthand for the identity functor on Cpo . To form the subscone, we consider the full subcategory D with objects of the form ⟨P, f, A⟩, where f is an inclusion P ↪ A. In other words, P is a sub-cpo of A, and therefore closed under limits of directed sets. By generalizing Proposition 8.6.15, we can see that D provides logical predicates over cpo models that are closed under limits. However, there is no reason for predicates taken in Cpo to preserve least elements – we have objects ⟨P, f, A⟩ where A is pointed and P is not. This is not a problem in general, but if we wish to have a predicate preserve a fixed-point operator on pointed A, we will need for P to be a pointed subset of A.

In order to preserve fixed points, we consider a further subcategory. Assume we have a map Σ ⟶ Cpo identifying certain cpo’s on which we wish to have fixed-point operators. For this to make sense, we assume that if σ is a type over Σ with a constant fix_{σ}: (σ → σ) → σ, then our mapping from types to cpo’s will guarantee that the interpretation of σ is a pointed cpo. In this case, we are interested in subcategories of D whose objects are of the form ⟨P, A⟩, where if A is the interpretation of a type with a fixed-point constant, then the inclusion P ↪ A is strict. In particular, P must have a least element. The ccc structure of this subcategory remains the same, but in D we also get fixed-point operators where required, and the forgetful functor D → Cpo preserves them. The object parts of the unique cartesian closed functor from C_{Σ}(E_{fix}) into D are exactly the inclusive logical predicates described in Section 8.6.2, pointed where required by the choice of fixed-point constants. In the binary case, we let D be the full subcategory of (Cpo × Cpo ↓ Cpo × Cpo) whose objects are of the form ⟨S, A, B⟩ , where S is a sub-cpo of A × B, and force pointed relations as required.

Exercise 8.6.24 Suppose P is a partially ordered set and C is a Kripke lambda model with P as the set of “possible worlds.” Let F: C ⟶ Set^{P} be the inclusion of C into the category category Set^{P}. Show that the full subcategory D of the comma category (Set^{P} ↓ F) consisting of objects ⟨S, f, A⟩ with f_{p}: S(p) ↪ F(A)(p) an inclusion for each p in P is cartesian closed.