Prelogical Relations^{1}

Furio Honsell

Dipartimento di Matematica e Informatica, Università di Udine, Italy

         honsell@dimi.uniud.it     www.dimi.uniud.it/~honsell/

and

Donald Sannella

Laboratory for Foundations of Computer Science, University of Edinburgh, Scotland

              dts@dcs.ed.ac.uk     www.dcs.ed.ac.uk/~dts/

We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful as well as further algebraic properties including composability. The basic idea is simply to require the reverse implication in the definition of logical relations to hold only for pairs of functions that are expressible by the same lambda term. Prelogical relations are the minimal weakening of logical relations that gives composability for extensional structures and simultaneously the most liberal definition that gives the Basic Lemma. Prelogical predicates (i.e., unary prelogical relations) coincide with sets that are invariant under Kripke logical relations with varying arity as introduced by Jung and Tiuryn, and prelogical relations are the closure under projection and intersection of logical relations. These conceptually independent characterizations of prelogical relations suggest that the concept is rather intrinsic and robust. The use of prelogical relations gives an improved version of Mitchell’s representation independence theorem which characterizes observational equivalence for all signatures rather than just for first-order signatures. Prelogical relations can be used in place of logical relations to give an account of data refinement where the fact that prelogical relations compose explains why stepwise refinement is sound.

Key Words: logical relations, typed lambda calculus, semantics, representation independence, data refinement

1This is an extended and revised version of [9].

1. INTRODUCTION

Logical relations are structure-preserving relations between models of typed lambda calculus.

Definition 1.1. A logical relation R over A and B is a family of relations {R^{σ} ⊆ [[σ]]^{A} × [[σ]]^{B}}_{σ∈Types(Σ)} such that:

• R^{σ→τ} (f, g) iff ∀a ∈ [[σ]]^{A}.∀b ∈ [[σ]]^{B}.R^{σ}(a, b) ⇒ R^{τ} (App_{A} f a, App_{B} g b).

• R^{σ}([[c]]^{A}, [[c]]^{B}) for every term constant c : σ in Σ.

Logical relations are used extensively in the study of typed lambda calculus and have applications outside lambda calculus, for example to abstract interpretation [1] and data refinement [34]. A good reference for logical relations is [19]. An important but more difficult reference is [33].

The Basic Lemma is the key to many of the applications of logical relations. It says that any logical relation over A and B relates the interpretation of each lambda term in A to its interpretation in B.

Lemma 1.2 (Basic Lemma). Let R be a logical relation over A and B. Then for all Γ-environments η_{A}, η_{B} such that R^{Γ}(η_{A}, η_{B}) and every term Γ ⊳ M : σ, R^{σ}([[Γ ⊳ M : σ]]_{η_{A}}^{A}, [[Γ ⊳ M : σ]]_{η_{B}}^{B}).

Here, R^{Γ}(η_{A}, η_{B}) refers to the obvious extension of R to environments, see Sect. 3 below.

As structure-preserving relations, logical relations resemble familiar algebraic concepts such as homomorphisms and congruence relations but they lack some of the convenient properties of such concepts. In particular, the composition of two logical relations is not in general a logical relation. This calls into question their application to data refinement at least, where one would expect composition to provide an account of stepwise refinement.

We propose a weakening of the notion of logical relations called prelogical relations (Sect. 3) that has many of the features that make logical relations so useful — in particular, the Basic Lemma still holds for prelogical relations (Lemma 4.1) — but having further algebraic properties including composability (Prop. 5.6). The basic idea is simply to require the reverse implication in the definition of logical relations to hold only for pairs of functions that are expressible by the same lambda term. Prelogical relations turn out to be the minimal weakening of logical relations that gives composability for extensional structures (Corollary 7.2) and simultaneously the most liberal definition that gives the Basic Lemma. Prelogical predicates (the unary case of prelogical relations) coincide with sets that are invariant under Kripke logical relations with varying arity as introduced by Jung and Tiuryn [10] (Prop. 6.2). Moreover, prelogical relations are the closure under projection and intersection of logical relations (Theorem 7.4). In view of these many conceptually independent characterizations, prelogical relations appear to be a rather intrinsic and robust concept. The use of prelogical relations in place of logical relations gives an improved version of Mitchell’s representation independence theorem (Corollaries 8.5 and 8.6 to Theorem 8.4) which characterizes observational equivalence for all signatures rather than just for first-order signatures. Prelogical relations can be used in place of logical relations in Reynolds’ and Tennent’s account of data refinement in [34] and then the fact that prelogical relations compose explains why stepwise refinement is sound.

Many applications of logical relations follow a standard pattern where the result comes directly from the Basic Lemma once an appropriate logical relation has been defined. Some results in the literature follow similar lines in the sense that a type-indexed family of relations is defined by induction on types and a proof like that of the Basic Lemma is part of the construction, but the family of relations defined is not logical. Examples can be found in Plotkin’s and Jung and Tiuryn’s lambda-definability results using I-relations [23] and Kripke logical relations with varying arity [10] respectively, and Gandy’s proof of strong normalization using hereditarily strict monotonic functionals [6]. In each of these cases, the family of relations involved turns out to be a prelogical relation (Example 3.12, Sect. 6 and Example 3.13) which allows the common pattern to be extended to these cases as well. Since prelogical relations are more general than logical relations and variants like I-relations, they provide a framework within which these different classes can be compared. Here we begin by studying and comparing their closure properties (Prop. 5.7) with special attention to closure under composition.

See Sect. 11 for a discussion of related work.

2. SYNTAX AND SEMANTICS

We begin with λ^{→}, the simply-typed lambda calculus having → as the only type constructor. Other type constructors will be considered in Sect. 10. We follow the terminology in [19] for the most part, with slightly different notation.

Definition 2.1. The set of types over a set B of base types (or type constants) is given by the grammar σ ::= b | σ → σ where b ranges over B. A signature Σ consists of a set B of type constants and a collection C of typed term constants c : σ. We write Types(Σ) for the set of types over B.

Let Σ = ⟨B, C⟩ be a signature. We assume familiarity with the usual notions of context Γ = x_{1}:σ_{1}, …, x_{n}:σ_{n} and Σ-term M of type σ over a context Γ, written Γ ⊳ M : σ, with the meta-variable t reserved for lambda-free Σ-terms. When we need to make Σ explicit we write Γ ⊳_{Σ} M : σ. If Γ is empty then we write simply M : σ. Capture-avoiding substitution [N/x]M is as usual.

Definition 2.2. A Σ-applicative structure A consists of:

• a carrier set [[σ]]^{A} for each σ ∈ Types(Σ);

• a function App_{A}^{σ,τ} : [[σ → τ]]^{A} → [[σ]]^{A} → [[τ]]^{A} for each σ, τ ∈ Types(Σ);

• an element [[c]]^{A} ∈ [[σ]]^{A} for each term constant c : σ in Σ.

We drop the subscripts and superscripts when they are determined by the context, and we sometimes abbreviate App_{A}^{σ,τ} f x as f x. Two elements f, g ∈ [[σ → τ]]^{A} are said to be extensionally equal if App_{A}^{σ,τ} f x = App_{A}^{σ,τ} g x for every x ∈ [[σ]]^{A}. A Σ-applicative structure is extensional when extensional equality coincides with identity.

A Σ-combinatory algebra is a Σ-applicative structure A that has elements K_{A}^{σ,τ} ∈ [[σ → (τ → σ)]]^{A} and S_{A}^{ρ,σ,τ} ∈ [[(ρ → σ → τ) → (ρ → σ) → ρ → τ]]^{A} for each ρ, σ, τ ∈ Types(Σ) satisfying the equations K_{A}^{σ,τ} xy = x and S_{A}^{ρ,σ,τ} xy z = (xz)(y z).

An extensional combinatory algebra is called a Henkin model. An applicative structure A is a full type hierarchy when [[σ → τ]]^{A} = [[σ]]^{A} → [[τ]]^{A} (the full settheoretic function space) for every σ, τ ∈ Types(Σ) with App_{A}^{σ,τ} f x = f(x) and then it is obviously a Henkin model.

In a combinatory algebra, we can extend the definition of lambda-free Σ-terms by allowing them to contain S and K; we call these combinatory Σ-terms.

A Γ-environment η_{A} assigns elements of an applicative structure A to variables, with η_{A}(x) ∈ [[σ]]^{A} for x : σ in Γ. A lambda-free Σ-term Γ ⊳ t : σ is interpreted in a Σ-applicative structure A under a Γ-environment η_{A} in the obvious way, written [[Γ ⊳ t : σ]]_{η_{A}}^{A}, and this extends immediately to an interpretation of combinatory Σ-terms in combinatory algebras by interpreting K and S as K_{A} and S_{A}. If t is closed then we write simply [[t : σ]]^{A}.

There are various ways of interpreting terms containing lambda abstraction in a combinatory algebra by “compiling” them to combinatory terms so that outermost β holds (see Prop. 2.4 below for what we mean by “outermost β”). In Henkin models, all these compilations yield the same result.

An axiomatic approach to interpreting lambda abstraction requires an applicative structure equipped with an interpretation function that satisfies certain minimal requirements — cf. the notion of acceptable meaning function in [19].

Definition 2.3. A lambda Σ-applicative structure consists of a Σ-applicative structure A together with a function [[·]]^{A} that maps any term Γ ⊳ M : σ and Γ-environment η_{A} over A to an element of [[σ]]^{A}, such that:

• [[Γ ⊳ x : σ]]_{η_{A}}^{A} = η_{A}(x)

• [[Γ ⊳ c : σ]]_{η_{A}}^{A} = [[c]]^{A}

• [[Γ ⊳ M N : τ]]_{η_{A}}^{A} = App_{A} [[Γ ⊳ M : σ → τ]]_{η_{A}}^{A} [[Γ ⊳ N : σ]]_{η_{A}}^{A}

• [[Γ ⊳ λx:σ.M : σ → τ]]_{η_{A}}^{A} = [[Γ ⊳ λy:σ.[y/x]M : σ → τ]]_{η_{A}}^{A} provided y ∉ Γ

• [[Γ ⊳ M : σ]]_{η_{A}}^{A} = [[Γ ⊳ M : σ]]_{η′_{A}}^{A} provided η′_{A} is a Γ-environment such that η_{A}(x) = η′_{A}(x) for all x ∈ Γ

• [[Γ, x:σ ⊳ M : τ]]_{η_{A}}^{A} = [[Γ ⊳ M : τ]]_{η_{A}}^{A} provided x ∉ FV (M)

The relationship between lambda applicative structures and combinatory algebras is as follows, cf. [5].

Proposition 2.4. A lambda applicative structure A such that App_{A}[[Γ⊳λx:σ.M : σ → τ]]_{η_{A}}^{A} a = [[Γ, x:σ ⊳ M : τ]]_{η_{A}[x↦a]}^{A} amounts to a combinatory algebra, and vice versa.

Proof. ⇐: We define [[·]]^{A} via the standard compilation of lambda terms using K and S to combinatory terms.

⇒: K_{A}^{σ,τ} and S_{A}^{ρ,σ,τ} are the interpretations of the usual lambda terms.

The proof of this proposition shows that the interpretation of lambda terms in combinatory algebras via compilation to combinatory terms satisfies the axioms in Def. 2.3 and the additional property in the proposition. Therefore when viewing a combinatory algebra as a lambda applicative structure, this is the interpretation function we have in mind.

3. ALGEBRAIC AND PRELOGICAL RELATIONS We propose a weakening of the definition of logical relations which is closed under

composition and which has most of the attractive properties of logical relations. First we change the two-way implication in the condition on functions to a one-way implication which requires preservation of the relation under application.

Definition 3.1. Let A and B be Σ-applicative structures. An algebraic relation R over A and B is a family of relations {R^{σ} ⊆ [[σ]]^{A} × [[σ]]^{B}}_{σ∈Types(Σ)} such that:

• If R^{σ→τ} (f, g) then ∀a ∈ [[σ]]^{A}.∀b ∈ [[σ]]^{B}.R^{σ}(a, b) ⇒ R^{τ} (App_{A} f a, App_{B} g b).

• R^{σ}([[c]]^{A}, [[c]]^{B}) for every term constant c : σ in Σ.

In lambda applicative structures, we additionally require the relation to preserve lambda abstraction in a sense that is analogous to the definition of admissible relation in [19]. First, we extend a family of relations R = {R^{σ} ⊆ [[σ]]^{A} × [[σ]]^{B}}_{σ∈Types(Σ)} to a relation on Γ-environments: R^{Γ}(η_{A}, η_{B}) if R^{σ}(η_{A}(x), η_{B}(x)) for every x:σ in Γ.

Definition 3.2. Let A and B be lambda Σ-applicative structures. A prelogical relation over A and B is an algebraic relation R such that given Γ-environments η_{A} and η_{B} such that R^{Γ}(η_{A}, η_{B}), and a term Γ, x : σ ⊳ M : τ, if R^{σ}(a, b) implies R^{τ} ([[Γ, x : σ⊳M : τ]]_{η_{A}[x↦a]}^{A}, [[Γ, x : σ⊳M : τ]]_{η_{B}[x↦b]}^{B}) for all a ∈ [[σ]]^{A} and b ∈ [[σ]]^{B}, then R^{σ→τ} ([[Γ ⊳ λx:σ.M : σ → τ]]_{η_{A}}^{A}, [[Γ ⊳ λx:σ.M : σ → τ]]_{η_{B}}^{B}).

This formulation of the definition amounts to defining prelogical relations as simply the class of relations that make the Basic Lemma hold, as we shall see in Lemma 4.1 below. (Indeed, since the Basic Lemma for prelogical relations is an equivalence rather than a one-way implication, an alternative at this point would be to take the conclusion of the Basic Lemma itself as the definition of prelogical relations.)

A simpler and therefore more appealing definition is obtained if we consider combinatory algebras, where the requirement above boils down to preservation of S and K. This is probably the formulation that readers will most want to remember, although the definition for lambda applicative structures is useful for proofs of syntactic properties of lambda calculus.

Proposition 3.3. Let A and B be Σ-combinatory algebras. An algebraic relation R over A and B is prelogical iff R(S_{A}^{ρ,σ,τ} , S_{B}^{ρ,σ,τ}) and R(K_{A}^{σ,τ} , K_{B}^{σ,τ}) for all ρ, σ, τ ∈ Types(Σ).

Proof. Directly from the definitions, using Prop. 2.4 for the inverse implication.

If we incorporate S and K into the signature Σ, then prelogical relations are just algebraic relations on combinatory algebras. One way of understanding the definition of prelogical relations is that the reverse implication in the definition of logical relations is required to hold only for pairs of functions that are expressible by the same lambda term. For combinatory algebras these are exactly the pairs of functions that are denoted by the same combinatory term, and thus this requirement is captured by requiring the relation to contain S and K.

The use of the combinators S and K in the above proposition is in some sense arbitrary: the same result would be achieved by taking any other combinatory basis and changing the definition of combinatory algebra and the interpretation function accordingly. It would be straightforward to modify the definitions to accommodate other variants of lambda calculus, for instance λ_{I} (where in λx:σ.M, the term M is required to contain x) for which a combinatory basis is B, C, I, S, or linear lambda calculi. For languages that include recursion, such as PCF, one would add a Y combinator. For λ^{unit,×,→}, one could add pairing etc. as suggested in Sect. 10 below or alternatively use the “categorical combinators” of [4] as in Theorem 5.1 of [24].

As usual, the binary case of algebraic resp. prelogical relations over A and B is derived from the unary case of algebraic resp. prelogical predicates for the product structure A × B. For instance:

Definition 3.4. Let A be a Σ-applicative structure. An algebraic predicate P over A is a family of predicates {P^{σ} ⊆ [[σ]]^{A}}_{σ∈Types(Σ)} such that:

• If P^{σ→τ} (f) then ∀a ∈ [[σ]]^{A}.P^{σ}(a) ⇒ P^{τ} (App_{A} f a).

• P^{σ}([[c]]^{A}) for every term constant c : σ in Σ.

For most results about prelogical relations below there are corresponding results about prelogical predicates and about algebraic relations and predicates over applicative structures. We omit these for lack of space. Similar comments apply to n-ary relations for n > 2.

Here is one result about prelogical predicates that does not generalize in the obvious way to prelogical relations:

Proposition 3.5. A prelogical predicate over a reachable lambda applicative structure A is a logical predicate on A. (A lambda Σ-applicative structure A is reachable if for any a ∈ [[σ]]^{A} there is a closed Σ-term M : σ such that a = [[M : σ]]^{A}.)

Proof. By a straightforward induction, or alternatively as a corollary of Lemma 4.2

below.

A prelogical relation over reachable lambda applicative structures A and B is not necessarily a logical relation over A and B, because what is required to apply Prop. 3.5 is reachability for the product structure A × B: for any ⟨a, b⟩ ∈ [[σ]]^{A×B} there needs to be a closed Σ-term M : σ such that ⟨a, b⟩ = [[M : σ]]^{A×B} = ⟨[[M : σ]]^{A}, [[M : σ]]^{B}⟩.

The fact that prelogicality is strictly weaker than logicality is demonstrated by the following examples which also provide a number of general methods for defining prelogical relations.

Example 3.6. For any signature Σ and lambda Σ-applicative structure, the predicate P defined by

P^{σ}(v) ⇔ v is the value of a closed Σ-term M : σ

is a prelogical predicate over A. (In fact, P is the least such — see Prop. 5.8 below.) Now, consider the signature Σ containing the type constant nat and term constants 0 : nat and succ : nat → nat and let A be the full type hierarchy over ℕ where 0 and succ have their usual interpretations. P is not a logical predicate over A: any function f ∈ [[nat → nat]]^{A}, including functions that are not lambda definable, takes values in P to values in P and so must itself be in P.

Example 3.7. The identity relation on a lambda applicative structure is a prelogical relation but it is logical iff the structure is extensional.

Example 3.8. A Σ-homomorphism between lambda Σ-applicative structures A and B is a type-indexed family of functions {h^{σ} : [[σ]]^{A} → [[σ]]^{B}}_{σ∈Types(Σ)} such that for any term constant c : σ in Σ, h^{σ}([[c]]^{A}) = [[c]]^{B}, h^{τ} (App_{A}^{σ,τ} f a) = App_{B}^{σ,τ} h^{σ→τ} (f) h^{σ}(a) and h^{σ→τ} ([[Γ ⊳ λx:σ.M : σ → τ]]_{η_{A}}^{A}) = [[Γ ⊳ λx:σ.M : σ → τ]]_{h(η_{A})}^{B} where h(η_{A}) = {x ↦ h^{σ}(η_{A}(x))} for all x:σ in Γ. Any Σ-homomorphism is a prelogical relation. In particular, interpretation of terms in a lambda applicative structure with respect to an environment, viewed as a relation from the lambda applicative structure of terms, is a prelogical relation but is not in general a logical relation.

Example 3.9. Prelogical predicates over a lambda applicative structure A are the natural notion of substructures of A since they require closure under the available operations, see Prop. 4.2 below. When considering extensional structures, we additionally require substructures to be extensional. Logical predicates are unnecessarily constrained for this purpose.

Example 3.10. Let A and B be lambda applicative structures and define R^{σ} ⊆ [[σ]]^{A} × [[σ]]^{B} by R^{σ}(a, b) for a ∈ [[σ]]^{A}, b ∈ [[σ]]^{B} iff there is a closed term M : σ such that [[M : σ]]^{A} = a and [[M : σ]]^{B} = b. This is a prelogical relation but it is not in general a logical relation. Generalizing: the inverse of any prelogical relation is obviously prelogical and according to Prop. 5.6 below the composition of any two prelogical relations is prelogical. Then observe that the above relation is just the composition of closed term interpretation in B (which is prelogical according to Example 3.8) and the inverse of closed term interpretation in A.

Example 3.11. Let A_{1}, …, A_{m} be lambda applicative structures. There are several ways of generating an n-ary prelogical relation from an m-ary one R ⊆ A_{1} × ⋯ × A_{m} when n < m. Projection of any n-tuple of components yields an nary prelogical relation, for example π_{1,2}(R) ⊆ A_{1} ×A_{2}. Another notation for this is ∃, defined as follows: (∃R)^{σ} = {⟨a_{2}, …, a_{m}⟩ | ∃a_{1} ∈ [[σ]]^{A_{1}}.⟨a_{1}, a_{2}, …, a_{m}⟩ ∈ R^{σ}}. The dual of this is ∀, which is another way of reducing the arity of a prelogical relation: (∀R)^{σ} = {⟨a_{2}, …, a_{m}⟩ | ∀a_{1} ∈ [[σ]]^{A_{1}}.⟨a_{1}, a_{2}, …, a_{m}⟩ ∈ R^{σ}}. Finally, if A_{i} = A_{j} for some i, j ≤ m then we can take the subset of tuples in R having the same values in positions i and j: (filter R)^{σ} = {⟨a_{1}, …, a_{i−1}, a_{i+1}, …, a_{m}⟩ | ⟨a_{1}, …, a_{m}⟩ ∈ R^{σ} and a_{i} = a_{j}}. This amounts to a projection of the intersection of R with the cartesian product of the A_{l}’s for l ≠ i, j and the diagonal over A_{i} × A_{j}. All n-ary prelogical relations can be generated from m-ary prelogical relations such that n < m using any of these: to obtain S, apply any of the above to S × A_{1} × ⋯ × A_{1} or alternatively, for the case of projection and filtering, to {⟨a_{1}, …, a_{n}, a_{1}, …, a_{1}⟩ | ⟨a_{1}, …, a_{n}⟩ ∈ S}. If R is a logical relation then so is ∀R, but the projection and filtering of R are not logical relations in general.

Example 3.12. Plotkin’s I-relations [23] give rise to prelogical relations. The family of relations on the full type hierarchy consisting of the tuples which are in a given I-relation at a given world (alternatively, at all worlds) is a prelogical relation which is not in general a logical relation.

A related example concerning Kripke logical relations with varying arity [10] is postponed to Sect. 6 to allow the reader to first become more familiar with prelogical relations.

Example 3.13. Let A be an applicative structure. Given order relations R^{b} on [[b]]^{A} for each base type b, we can define the hereditarily monotonic functionals as the equivalence classes of those elements of A which are self-related with respect to the following inductively defined family of relations on A × A:

R^{σ→τ} (f, g) iff ∀a ∈ [[σ]]^{A}.∀b ∈ [[σ]]^{A}.R^{σ}(a, b) ⇒ (R^{τ} (App_{A} f a, App_{A} g a)
∧R^{τ} (App_{A} f a, App_{A} f b)
∧R^{τ} (App_{A} g a, App_{A} g b))

(This defines simultaneously at each type both the class of functionals we are interested in and the order relation itself.) This method defines a prelogical relation which is not in general a logical relation.

Gandy’s hereditarily strict monotonic functionals [6] can be defined using the above technique with just a small modification of the clause for functionals.

R^{σ→τ} (f, g) iff ∀a ∈ [[σ]]^{A}.∀b ∈ [[σ]]^{A}.
R^{σ}(a, b) ⇒ (f ≠ g ⇒ (R^{τ} \ Δ^{τ})(App_{A} f a, App_{A} g a)
∧
a ≠ b ⇒ ((R^{τ} \ Δ^{τ})(App_{A} f a, App_{A} f b)
∧(R^{τ} \ Δ^{τ})(App_{A} g a, App_{A} g b)))

Again we have a prelogical relation (with respect to the language of λ_{I}) which is not in general a logical relation.

Example 3.14. We can define the continuous functionals, as used in models of PCF, using the same technique. Let A be the full type hierarchy over a given set of base types, and assume that CPO-relations R^{b} on [[b]]^{A} are given. We can define simultaneously at each type both the class of functionals which are continuous and the CPO-relation itself. Namely, define inductively

R^{σ→τ} (f, g) iff ∀a ∈ [[σ]]^{A}.∀b ∈ [[σ]]^{A}.
R^{σ}(a, b) ⇒ (R^{τ} (App_{A} f a, App_{A} g b)
∧f and g continuous w.r.t. R^{σ} and R^{τ}).

In the above definition, continuity has to be taken in the obvious sense, namely (any representative of) the supremum of a directed set w.r.t. R^{σ} is mapped into (a representative of) the supremum w.r.t. R^{τ} of the images of the directed sets. For the definition to make sense we only need to check that R^{σ→τ} induces a CPO-relation on the equivalence classes modulo R^{σ→τ} itself. But this is straightforward.

Again, the continuous functionals are the equivalence classes of those elements of A which are self-related by R^{σ→τ} and the CPO-relation is the order relation induced on these equivalence classes by R^{σ→τ} itself. Again, R is a prelogical relation, which is not logical.

4. THE BASIC LEMMA

We will now consider the extension of the Basic Lemma to prelogical relations. In contrast to Lemma 1.2, we get a two-way implication which says that the requirements on prelogical relations are exactly strong enough to ensure that the Basic Lemma holds. The reverse implication fails for logical relations as Example 3.6 shows (for logical predicates).

Lemma 4.1 (Basic Lemma for prelogical relations). Let R = {R^{σ} ⊆ [[σ]]^{A} × [[σ]]^{B}}_{σ∈Types(Σ)} be a family of relations over lambda Σ-applicative structures A and B. Then R is a prelogical relation iff for all Γ-environments η_{A}, η_{B} such that R^{Γ}(η_{A}, η_{B}) and every Σ-term Γ ⊳ M : σ, R^{σ}([[Γ ⊳ M : σ]]_{η_{A}}^{A}, [[Γ ⊳ M : σ]]_{η_{B}}^{B}).

Proof. ⇒: The proof is by induction on the structure of M. For variables, we use the assumption that R^{Γ}(η_{A}, η_{B}). For constants, we use the fact that prelogical relations are required to respect constants. For an application Γ ⊳ M N : τ, we use the inductive hypothesis for M and N and the fact that prelogical relations are closed under application. As for Γ ⊳ λx:σ.M : σ → τ, by the induction hypothesis we know that for all Γ, x:σ-environments η′_{A}, η′_{B} such that R^{Γ,x:σ}(η′_{A}, η′_{B}) we have R^{σ}([[Γ, x:σ ⊳ M : σ]]_{η′_{A}}^{A}, [[Γ, x:σ ⊳ M : σ]]_{η′_{B}}^{B}). If R^{σ}(a, b) then applying this to η′_{A} = η_{A}[x ↦ a] and η′_{B} = η_{B}[x ↦ b] and taking the condition in the definition of prelogical relations gives the desired result.

⇐: The first condition of algebraic relations follows by taking M to be x y and η_{A} = {x ↦ f, y ↦ a} η_{B} = {x ↦ g, y ↦ b} and the second condition for a term constant c follows by taking M to be c. The additional condition for prelogical relations

holds a fortiori.

The “only if” direction of this result is the analogue in our setting of the general version of the Basic Lemma in [19], but where R is only required to be prelogical. For combinatory algebras, the case of lambda abstraction is handled via conversion to an equivalent combinatory term; comparing this proof with the standard proof of the Basic Lemma, where this case uses the reverse implication in the definition of logical relations, exposes the main idea a little more clearly.

If one applies the Basic Lemma for prelogical relations to Henkin models, the “only if” part of the result is exactly the usual formulation (Lemma 1.2 above), except that R is only required to be prelogical.

The Basic Lemma is intimately connected with the concept of lambda definability. This is most apparent in the unary case:

Lemma 4.2 (Basic Lemma for prelogical predicates). Let P = {P^{σ} ⊆ [[σ]]^{A}}_{σ∈Types(Σ)} be a family of predicates over a lambda Σ-applicative structure A. Then P is a prelogical predicate iff it is closed under lambda definability: P^{Γ}(η) and Γ ⊳ M : σ implies P^{σ}([[Γ ⊳ M : σ]]_{η}^{A}).

5. PROPERTIES OF PRELOGICAL RELATIONS A logical relation on lambda applicative structures is prelogical provided it is

admissible in the following sense.

Definition 5.1. [Mitchell] A logical relation R on lambda applicative structures A and B is admissible if given Γ-environments η_{A} and η_{B} such that R^{Γ}(η_{A}, η_{B}), and terms Γ, x:σ ⊳ M, N : τ,

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

implies

∀a ∈ [[σ]]^{A}, b ∈ [[σ]]^{B}.R^{σ}(a, b) ⇒ R^{τ} (App_{A} [[Γ ⊳ λx:σ.M : σ → τ]]_{η_{A}}^{A} a,
App_{B} [[Γ ⊳ λx:σ.N : σ → τ]]_{η_{B}}^{B} b)

Proposition 5.2. Any admissible logical relation on lambda applicative structures is a prelogical relation.

Proof. Admissibility plus the reverse implication in the definition of logical rela-

tions gives the property in the definition of prelogical relations.

Corollary 5.3. Any logical relation on combinatory algebras is a prelogical relation.

Proof. Logical relations on combinatory algebras are always admissible. Alter-

natively, apply Prop. 3.3.

To understand why the composition of logical relations R over A and B and S over B and C might not be a logical relation, it is instructive to look at examples. When composition fails, the problem is often that the interpretation of some function type in B has “too few values”. But even if we take logical relations over full type hierarchies, where all possible values of function types are present, composition can fail because the required “missing link” in B is not a function:

Example 5.4. Let Σ contain just two type constants, b and b′. Consider three full type hierarchies A, B, C which interpret b and b′ as follows: [[b]]^{A} = {∗} = [[b′]]^{A}; [[b]]^{B} = {∗} and [[b′]]^{B} = {∘, •}; [[b]]^{C} = {∘, •} = [[b′]]^{C}. Let R be the logical relation over A and B induced by R^{b} = {⟨∗, ∗⟩} and R^{b′} = {⟨∗, ∘⟩, ⟨∗, •⟩} and let S be the logical relation over B and C induced by S^{b} = {⟨∗, ∘⟩, ⟨∗, •⟩} and S^{b′} = {⟨∘, ∘⟩, ⟨•, •⟩}. S ∘ R is not a logical relation because it does not relate the identity function in [[b]]^{A} → [[b′]]^{A} to the identity function in [[b]]^{C} → [[b′]]^{C}. The problem is that the only two functions in [[b]]^{B} → [[b′]]^{B} are {∗ ↦ ∘} and {∗ ↦ •}, and S does not relate these to the identity in C.

Example 5.5. In the previous example, add a type constant bool and a term constant c : (b → b′) → bool to Σ. Let [[bool]]^{A} = [[bool]]^{B} = [[bool]]^{C} = {true, false} and take R^{bool} and S^{bool} to be the identity. In each model, let the interpretation of c take constant functions to true and all other functions to false. The resulting R and S are logical relations. As before, S ∘ R is not a logical relation but now the restriction of S ∘ R to base types cannot be lifted to a logical relation either: this would relate the identity function in [[b]]^{A} → [[b′]]^{A} (which is a constant function) to every function in [[b]]^{C} → [[b′]]^{C}, but then the constant function in A would be related to non-constant functions in C, and so [[c]]^{A} could not be related to [[c]]^{C}, otherwise true would be related to false.

Proposition 5.6. The composition S ∘R of prelogical relations R over A, B and S over B, C is a prelogical relation over A, C.

Proof. A proof from the definition is not at all straightforward, but Lemma 4.1 says that prelogicality is equivalent to a property of relations that is obviously closed

under composition.

Obviously, closure under composition opens the way to the use of categories in which prelogical relations are morphisms. Many properties of prelogical relations could then be expressed using the language of category theory, but we do not pursue this here.

Composition of relations is definable in terms of product, intersection and projection:

S ∘ R = π_{1,3}(A × S ∩ R × C)

Closure of prelogical relations under these operations is a more basic property than closure under composition, and is not specific to binary relations. We have:

Proposition 5.7. Prelogical relations are closed under intersection, product, projection, permutation and ∀. Logical relations are closed under product, permutation and ∀ but not under intersection or projection.

To see that logical relations are not closed under intersection, consider two logical predicates P, P′ over A whose intersection at base types is empty. For any logical predicate Q over A which is empty at base types, it is easy to show by induction that for each type σ, either Q^{σ} = [[σ]]^{A} or Q^{σ} = ∅. But in general P ∩ P′ does not have this property.

Concerning closure under projection, recall S from Example 5.4 and observe that π_{2}(S) is not a logical predicate: π_{2}(S)^{b} = [[b]]^{C} and π_{2}(S)^{b′} = [[b′]]^{C} but π_{2}(S)^{b→b′} does not contain the identity function.

Other classes of relations satisfy different closure properties. For instance, Irelations are obviously closed under product, permutation and ∀, and it is easy to see that they are also closed under intersection. They are not closed under composition by Example 5.4 mutatis mutandis, and since composition is definable in terms of product, intersection and projection it follows that they are not closed under projection.

A consequence of closure under intersection is that given a property P of relations that is preserved under intersection, there is always a least prelogical relation satisfying P. We then have the following lambda-definability result (recall Example 3.6 above):

Proposition 5.8. The least prelogical predicate over a given lambda Σ-applicative structure contains exactly those elements that are the values of closed Σ-terms.

In a signature with no term constants, a logical relation may be constructed by defining a relation R on base types and using the definition to “lift” R inductively to higher types. The situation is different for prelogical relations: there are in general many prelogical liftings of a given R, one being of course its lifting to a logical relation (provided this gives an admissible relation). But since the property of lifting a given R is preserved under intersection, the least prelogical lifting of R is also a well-defined relation. Similarly, the least prelogical extension of a given family of relations is well-defined for any signature. Notice that lifting R to a logical relation is not possible in general for signatures containing higher-order term constants, see Example 5.5 (and see [19] for a way of accommodating least fixed-point operators). Extension is also problematic: the cartesian product A × A is a logical relation that trivially extends any binary relation on A, but this is uninteresting. Further ways of defining prelogical relations are indicated by the examples at the end of Sect. 3 and in Sect. 6.

It is easy to see that prelogical relations are not closed under union. And even in a signature with no term constants, the set of prelogical relations that lift a given relation R on base types cannot be endowed with a lattice structure in general. But the only logical relation in this set is one of its maximal elements under inclusion.

6. KRIPKE LOGICAL RELATIONS WITH VARYING ARITY

In [10], Jung and Tiuryn give the following variant of the notion of logical relations:

Definition 6.1. [Jung and Tiuryn] Let C be a small category of sets and let A be a Henkin model. A Kripke logical relation with varying arity (KLRwVA for short) over A is a family of relations R_{σ}^{w} indexed by objects w of C and types σ of Types(Σ), where the elements of R_{σ}^{w} are tuples of elements from [[σ]]^{A} indexed by the elements of w, such that:

• If f : v → w is a map in C and R_{σ}^{w}⟨a_{j}⟩_{j∈w} then R_{σ}^{v}⟨a_{f(i)}⟩_{i∈v}.

• R_{σ→τ}^{w} ⟨g_{j}⟩_{j∈w} iff ∀f : v → w.∀⟨a_{i}⟩_{i∈v}.R_{σ}^{v}⟨a_{i}⟩_{i∈v} ⇒ R_{τ}^{v}⟨App_{A} g_{f(i)} a_{i}⟩_{i∈v}

• R_{σ}^{w}⟨[[c]]^{A}⟩_{j∈w} for every term constant c : σ in Σ.

The above formulation extends Jung and Tiuryn’s definition to take term constants into account.

KLRwVAs give rise to prelogical relations in a similar way to I-relations, see Example 3.12: the family of relations consisting of the w-indexed tuples that are in a given KLRwVA at world w is a |w|-ary prelogical relation which is not in general a logical relation, and those elements that are invariant under a given KLRwVA (i.e. a ∈ [[σ]]^{A} such that R_{σ}^{w}⟨a⟩_{j∈w} for all w) also form a prelogical predicate. More interesting is the fact that every prelogical relation can be obtained in both these ways. We give the unary case first.

Proposition 6.2. Let P = {P^{σ} ⊆ [[σ]]^{A}}_{σ∈Types(Σ)} be a family of predicates over a Henkin model A. The following are equivalent.

1.P is a prelogical predicate.

2.P is the set of elements of A that appear at some world of cardinality 1 for some KLRwVA.

3.P is the set of elements of A that are invariant under some KLRwVA.

Proof. 1 ⇒ 2: Just as in the proof of Lemma 4 in [10], but using terms over Σ expanded by term constants for all values in A. The proof assumes that A is a full type hierarchy but it extends to Henkin models by a minor change of notation.

2 ⇐ 1: From the definitions.

2 ⇔ 3: This follows from the fact that in the KLRwVA constructed in the proof of 1 ⇒ 2, there is only one world of cardinality 1, which is the final object in the cate-

gory C.

The binary and n-ary cases are obtained by applying the above construction to (n-ary) product structures, or, in what amounts to essentially the same thing, to modifying the structure of the category of worlds. If we work out this latter case we then obtain the (apparently more) general result:

Proposition 6.3. Let R = {R^{σ} ⊆ [[σ]]^{A} × ⋯ × [[σ]]^{A}}_{σ∈Types(Σ)} be a family of n-ary relations over a Henkin model A. R is a prelogical relation iff it is the set of n-tuples of A which appear at some world of cardinality n for some KLRwVA.

Finally we point out that the modification to Jung and Tiuryn’s result hinted at in the proof, together with Theorem 3 in [10], can be used to generalize Jung and Tiuryn’s lambda-definability result (their Theorem 5) to signatures containing term constants, cf. [2].

7. PRELOGICAL RELATIONS VIA COMPOSITION OF LOGICAL

RELATIONS

Our weakening of the definition of logical relations may appear to be ad hoc, but for extensional structures it turns out to be the minimal weakening that is closed under composition. There are variants of this result for several different classes of models. We give the version for Henkin models.

Theorem 7.1. Let A and B be Henkin models and let R be a prelogical relation over A and B. Then R factors into a composition of three logical relations over Henkin models.

Proof idea. The key idea is to extend A and B to models A[Y] and B[Y] in such a way that R[Y], a minimally-extended version of R, becomes a logical relation on A[Y] and B[Y]. These models are obtained by adding indeterminates with generic behaviour to the carrier sets of A and B, which ensures that the condition ∀a ∈ [[σ]]^{A[Y]}.∀b ∈ [[σ]]^{B[Y]}.R[Y]^{σ}(a, b) ⇒ R[Y]^{τ} (App_{A[Y]} f a, App_{B[Y]} g b) holds only for f ∈ [[σ → τ]]^{A} and g ∈ [[σ → τ]]^{B} such that R^{σ→τ} (f, g). Roughly speaking, we have that for any indeterminate y : σ, R[Y]^{τ} (App_{A[Y]}f y, App_{B[Y]}gy) iff R^{σ→τ} (f, g). Then R is the composition of the “embedding” of A in A[Y], R[Y], and the inverse of the “embedding” of B in B[Y]. (The word “embedding” is inaccurate since these are not set-theoretic functions. The inverse of the “embedding” of A in A[Y] is a partial surjection in the sense of Sect. 8.4.1 of [19], and likewise for B.)

A detailed proof may be found in the appendix.

It is an open problem whether or not Theorem 7.1 holds if we take the composition of two logical relations rather than three.

Corollary 7.2. The class of binary prelogical relations on Henkin models is the closure under composition of the class of logical relations on such structures.

This gives the following lambda-definability result:

Corollary 7.3. Let A be a Henkin model and a ∈ [[σ]]^{A}. Then ⟨a, a⟩ belongs to all relations over A × A obtained by composing logical relations iff a = [[M : σ]]^{A} for some closed Σ-term M : σ.

Proof. By Corollary 7.2 and a binary version of Prop. 5.8.

The proof of Theorem 7.1 can be generalized to n-ary relations by repeating the same construction in each component and taking an appropriately generalized notion of composition. This yields the following structure theorem:

Theorem 7.4. For any arity n, the class of all n-ary prelogical relations is obtained by closing the class of all logical relations under intersection and then taking projections.

One can see from the proof of Theorem 7.1 and 7.4 that we can rephrase these results by saying that every prelogical relation over a lambda applicative structure is the intersection of two logical relations on a superstructure of A, one of which is A^{n} itself; or equivalently, the restriction to A of a logical relation on a superstructure of A. Moreover, as superstructure we can always take the extension of A with infinitely many indeterminates at each type. Formally, denoting by R ⊆ A the fact that R is a prelogical predicate over A, and by R ⪯ A the fact that R is a logical predicate over A, we have:

Proposition 7.5. Suppose R ⊆ A. Then there exists A′ and R′ such that A ⪯ A′, R′ ⪯ A′ and R = A ∩ R′.

Proof. Simply take R′ = R[X] and A′ = A[X], where these extensions with in-

determinates are as in the proof of Theorem 7.1 in the appendix.

For the remainder of this section we shall focus again on the case of binary relations.

Corollary 7.2 does not hold if we restrict ourselves to considering just finite full type hierarchies: given an element a of a finite structure, it turns out to be co-r.e. whether the pair ⟨a, a⟩ belongs to all binary relations which are obtainable by closing logical relations under intersection and projection (and hence by closure under composition), while by Prop. 5.8 and [12] it is not co-r.e. whether ⟨a, a⟩ belongs to all binary prelogical relations. In the case of arbitrary full type hierarchies, the question is open: the proof of Theorem 7.1 fails if we take a full type hierarchy in place of A[X], and we conjecture that Corollary 7.2 does not hold.

For non-extensional structures the notion of prelogical relations is not the minimal weakening that gives closure under composition. The following variant is the minimal weakening for this case.

Definition 7.6. An algebraic relation is extensional if whenever R^{σ→τ} (f, g), f is extensionally equal to f′ and g is extensionally equal to g′, we have R^{σ→τ} (f′, g′).

All prelogical relations over extensional structures are automatically extensional, and all logical relations over applicative structures (even non-extensional ones) are automatically extensional as well.

Proposition 7.7. Let A and B be combinatory algebras and let R be an extensional prelogical relation over A and B. Then R factors into a composition of three logical relations.

Proof. As for Theorem 7.1 except that we need to take the extensional collapse over A and B respectively in the construction of A[X] and B[X]. The fact

that R is extensional is needed to show that the embeddings are logical relations.

Corollary 7.8. The class of extensional prelogical relations on combinatory algebras is the closure under composition of the class of logical relations on such structures.

These results may suggest that our definition of prelogical relations on nonextensional structures should be strengthened by requiring the relation to be extensional, but this would make the reverse implication of the Basic Lemma fail. So although the notion of extensional prelogical relations is the minimal weakening that gives closure under composition, these are stronger than necessary to give the Basic Lemma.

It would be interesting to continue the above investigations to characterize classes of relations generated by logical relations under operations such as intersection, projection or filtering, particularly on full type hierarchies.

8. REPRESENTATION INDEPENDENCE AND DATA REFINEMENT

Logical relations have been applied to explain the fact that the behaviour of programs does not depend on the way that data types are represented, but only on what can be observed about them using the operations that are provided. “Behaviour of programs” is captured by the notion of observational equivalence.

Definition 8.1. Let A and B be lambda Σ-applicative structures and let OBS, the observable types, be a subset of Types(Σ). Then A is observationally finer than B with respect to OBS, written A ≤_{OBS} B, if for any two closed terms M, N : σ for σ ∈ OBS such that [[M : σ]]^{A} = [[N : σ]]^{A} we have [[M : σ]]^{B} = [[N : σ]]^{B}.

A and B are observationally equivalent with respect to OBS, written A ≡_{OBS} B, if A ≤_{OBS} B and B ≤_{OBS} A.

It is usual to take OBS to be the “built-in” types for which equality is decidable, for instance bool and/or nat. Then A and B are observationally equivalent iff it is not possible to distinguish between them by performing computational experiments.

Mitchell [19] (cf. [18]) gives the following representation independence result:

Theorem 8.2 (Mitchell). Let Σ be a signature that includes a type constant nat, and let A and B be Henkin models, with [[nat]]^{A} = [[nat]]^{B} = ℕ. If there is a logical relation R over A and B with R^{nat} the identity relation on natural numbers, then A ≡_{{nat}} B. Conversely, if A ≡_{{nat}} B, Σ provides a closed term for each element of ℕ having the same value in A and B, and Σ contains no higher-order functions, then there is a logical relation R over A and B with R^{nat} the identity relation.

The statement of this theorem is slightly different from that in [19] — there is an additional minor technical requirement in the second part — because we use a more general notion of observational equivalence than Mitchell does in order to state Theorem 8.4 below.

The following example (Exercise 8.5.6 in [19]) shows that the requirement that Σ contains no higher-order functions is necessary.

Example 8.3. Let Σ have type constant nat and term constants 0, 1, 2, …: nat and f : (nat → nat) → nat. Let A be the full type hierarchy over [[nat]]^{A} = ℕ with 0, 1, 2, … interpreted as usual and [[f]]^{A}(g) = 0 for all g : ℕ → ℕ. Let B be like A but with [[f]]^{B}(g) = 0 if g is computable and [[f]]^{B}(g) = 1 otherwise. Since the difference between A and B cannot be detected by evaluating terms, A ≡_{{nat}} B. But there is no logical relation over A and B which is the identity relation on nat: if R is logical then R^{nat→nat}(g, g) for any g : ℕ → ℕ, and then R^{nat}(App_{A} [[f]]^{A} g, App_{B} [[f]]^{B} g), which gives a contradiction if g is non-computable.

We will strengthen this result by showing that prelogical relations characterize observational equivalence for all signatures. We also generalize to arbitrary sets of observable types and remove the requirement that elements of observable types are denoted by closed terms. This characterization is obtained as a corollary of the following theorem which is a strengthening of Lemma 8.2.17 in [19], again made possible by using prelogical relations in place of logical relations.

Theorem 8.4. Let A and B be lambda Σ-applicative structures and let OBS ⊆ Types(Σ). Then A ≤_{OBS} B iff there exists a prelogical relation over A and B which is a partial function on OBS.

Proof. ⇐: Suppose that R is a prelogical relation over A and B which is a partial function on OBS and let [[M : σ]]^{A} = [[N : σ]]^{A} for σ ∈ OBS. Apply the Basic Lemma to both sides and use the fact that R^{σ} is a partial function to get [[M : σ]]^{B} = [[N : σ]]^{B}.

⇒: Take the relation defined in Example 3.10.

Mitchell’s Lemma 8.2.17 is the “if” direction of this theorem for Henkin models where OBS = Types(Σ) but R is required to be logical rather than just prelogical. Notice that the “only if” direction of Theorem 8.4 does not hold for logical relations, even in the absence of term constants.

Corollary 8.5. Let A and B be lambda Σ-applicative structures and let OBS ⊆ Types(Σ). Then A ≡_{OBS} B iff there exists a prelogical relation over A and B which is a partial function on OBS in both directions.

The following result (instantiated to Henkin models) is the special case of Corollary 8.5 that most directly corresponds to Theorem 8.2.

Corollary 8.6. Let Σ be a signature that includes a type constant nat and let A and B be lambda Σ-applicative structures with [[nat]]^{A} = [[nat]]^{B} = ℕ such that Σ provides a closed term for each element of ℕ having the same value in A and B. There is a prelogical relation R over A and B with R^{nat} the identity relation on natural numbers iff A ≡_{{nat}} B.

Proof. Under the condition that [[nat]]^{A} = [[nat]]^{B} = ℕ, the availability of a closed term for each element of ℕ having the same value in A and B means that the requirement that R^{nat} is the identity relation is equivalent to the requirement that it

is a partial function in both directions.

Example 8.7. Revisiting Example 8.3, the prelogical relation constructed in Example 3.10 has the required property, and it does not relate non-computable functions since they are not lambda definable.

Following [29], it would be interesting to try to characterize finer notions of observational equivalence, e.g. elementary equivalence in first-order logic with equality restricted to observable types. In Example 8.3, note that the sentence ∀g, h : nat → nat.f(g) = f(h) holds in A but not in B.

The standard treatment of data refinement in the context of typed lambda calculus, originating with Reynolds but described most clearly in Sect. 2 of [34], uses logical relations to prove the correctness of refinements: write A ^{R} ⇝ B to indicate that B is a refinement of A as witnessed by the logical relation R over A and B, which is required to be identity on observable types. But then, given refinements A ^{R} ⇝ B and B ^{S} ⇝ C, the composition S ∘R may not be a logical relation and so cannot in general be used as a witness for the composed refinement A ⇝ C. (In fact, sometimes there is no witness for A ⇝ C at all.) This is at odds with the stepwise nature of refinement, and the transitivity of the underlying concept of refinement expressed in terms of observational equivalence. It is one source of examples demonstrating the incompleteness of this proof method; there are other examples that do not involve composition of refinement steps, see for instance Sect. 5 of [8]. A consequence of Theorem 8.2 is that this proof method is complete in the absence of higherorder term constants (if the signature provides a closed term for each element of observable type having the same value in A and B).

If prelogical relations are used in place of logical relations, then the fact that the composition of prelogical relations is again a prelogical relation (Prop. 5.6) explains why stepwise refinement is sound. It follows directly from Corollary 8.5 that the result is a sound and complete proof method for proving the correctness of data refinements (provided we relax the condition on observable types to require a partial function in both directions rather than identity, which also allows us to lift the requirement on closed terms of observable types). This opens the way to further development of the foundations of data refinement along the lines of the firstorder algebraic treatment in [30], and this is pursued in [8]. There, constructive prelogical refinement is a relation between specifications, written SP ^{OBS}_{δ} ∼∼∼∼∼ > SP′. This incorporates a derived signature morphism δ defining the types and constants in the signature of SP by giving terms over the signature of SP′, which allows any model B over the signature of SP′ to be transformed to a model B|_{δ} over the signature of SP. This refinement is correct if for any B ∈ Mod(SP′) there is some A ∈ Mod(SP) with a prelogical relation R over A and B|_{δ} which is a partial function on OBS in both directions. Making refinement into a relation on specifications and adding the construction described by δ gives a non-symmetric relation which incorporates the idea that refinement is a reduction of one as-yet-unsolved problem to another, which is a better fit with the real-life phenomenon being modelled.

9. OTHER APPLICATIONS

There are many other applications of logical relations. Take for instance the proof of strong normalization of λ^{→} in [19]: one defines an admissible logical predicate on a lambda applicative structure of terms by lifting the predicate on base types consisting of the strongly normalizing terms to higher types, proves that the predicate implies strong normalization, and then applies the general version of the Basic Lemma to give the result. The pattern for proofs of confluence, completeness of leftmost reduction, etc., is the same, sometimes with logical relations in place of logical predicates. There are also constructions that do not involve the Basic Lemma because the relations defined are not logical relations, but that include proofs following the same lines as the proof of the Basic Lemma. Examples include Gandy’s proof that the hereditarily strict monotonic functionals model λ_{I} terms [6], Plotkin’s proof that lambda terms satisfy any I-relation [23], and Jung and Tiuryn’s proof that lambda terms satisfy any KLRwVA at each arity (Theorem 3 of [10]).

All of these can be cast into a common mould by using prelogical relations rather than logical relations. If a relation or predicate on a lambda applicative structure is logical and admissible, then it is prelogical, and then the Basic Lemma for prelogical relations gives the result. Plotkin’s, Jung and Tiuryn’s, and Gandy’s relations can be shown to be prelogical (in Gandy’s case with respect to λ_{I}), see Example 3.12, Sect. 6 and Example 3.13 respectively, and then the application of the Basic Lemma for prelogical relations gives the result in these cases as well. In each case, however, the interesting part of the proof is not the application of the Basic Lemma (or the argument that replaces its application in the case of Gandy, Plotkin, and Jung and Tiuryn) but rather the construction of the relation and the proof of its properties. The point of the analysis is not to say that this view makes the job easier but rather to bring forward the common pattern in all of these proofs, which is suggestive of a possible methodology for such proofs.

Proofs of completeness and other applications would make use of the following.

Definition 9.1. A family of binary relations {R^{σ} ⊆ [[σ]]^{A}×[[σ]]^{A}}_{σ∈Types(Σ)} over a Σ-applicative structure A is a partial equivalence relation (abbreviated PER) if it is symmetric and transitive for each type.

Proposition 9.2. Let R be a PER on a Σ-applicative structure A which is algebraic. Define the quotient of A by R, written A/R, as follows:

•[[σ]]^{A/R} = [[σ]]^{A}/R^{σ}, i.e. the set of R-equivalence classes of objects a ∈ [[σ]]^{A} such that R^{σ}(a, a).

•App_{A/R}^{σ,τ} [f]_{A/R} [a]_{A/R} = [App_{A}^{σ,τ} fa]_{A/R}

•[[c]]^{A/R} = [[[c]]^{A}]_{A/R} for each term constant c : σ in Σ.

Then:

1.Let A be a lambda applicative structure. Then A/R is a lambda applicative structure, with [[Γ ⊳ M : σ]]_{η_{A/R}}^{A/R} = [[[Γ ⊳ M : σ]]_{η_{A}}^{A}]_{A/R} (where η_{A}(x) is a representative of the equivalence class η_{A/R}(x)), iff R is prelogical.

2.Let A be a combinatory algebra. Then A/R is a combinatory algebra iff R is prelogical.

3.A/R is an extensional applicative structure iff its restriction to the substructure of A consisting of the elements in Dom(R) is a logical relation.

Proof. The first point amounts to showing that the interpretation function is well-defined, namely that R^{Γ}(η_{A}, η′_{A}) ⇒ R^{σ}([[Γ⊳M : σ]]_{η_{A}}^{A}, [[Γ⊳M : σ]]_{η′_{A}}^{A}), but this follows immediately from the Basic Lemma for lambda applicative structures. The second point follows again from the Basic Lemma. The last point is straightforward

from the definitions.

The last part of the above proposition says that one application of logical relations, that is their use in obtaining extensional structures by quotienting nonextensional structures — the so-called extensional collapse — requires a relation that is logical (on a substructure) rather than merely prelogical.

The above proposition allows us to prove completeness for different classes of structures using the traditional technique of quotienting an applicative structure of terms by a suitable relation defined by provability in a calculus. For non-extensional structures, this is not possible using logical relations because the relation defined by provability is prelogical or algebraic rather than logical.

At this point one could develop a theory analogous to that of homomorphisms, quotients and substructures in universal algebra, but we refrain from doing this here. One would expect analogues of the usual theorems relating these three notions.

10. BEYOND λ^{→} AND APPLICATIVE STRUCTURES Up to now we have been working in λ^{→}, the simplest version of typed lambda

calculus. We will now briefly indicate how other type constructors could be treated so as to obtain corresponding results for extended languages.

As a template, we shall discuss the case of product types. The syntax of types is extended by adding the type form σ × τ and the syntax of terms is extended by adding pairing ⟨M, N⟩ and projections π_{1} M and π_{2} M. If we regard these as additional term constants in the signature, e.g. ⟨·, ·⟩ : σ → τ → σ × τ for all σ, τ, rather than as new term forms, then the definition of prelogical relations remains the same: the condition on term constants says that e.g. R^{σ→τ→σ×τ} ([[⟨·, ·⟩]]^{A}, [[⟨·, ·⟩]]^{B}) and this is all that is required. For models that satisfy surjective pairing, this implies the corresponding condition on logical relations, namely

R^{σ×τ} (a, b) iff R^{σ}(π_{1} a, π_{1} b) and R^{τ} (π_{2} a, π_{2} b).

The treatment of sum types σ +τ is analogous: we just require that inl : σ → σ +τ, inl : τ → σ + τ and case : σ + τ → (σ → ρ) → (τ → ρ) → ρ take related arguments to related results. Notice that this is also the only way to give the definition for logical relations with sum types since applying the usual pattern yields

R^{σ+τ} (a, b) iff
∀ρ.( ∀f ∈ [[σ → ρ]]^{A}, f′ ∈ [[σ → ρ]]^{B}, g ∈ [[τ → ρ]]^{A}, g′ ∈ [[τ → ρ]]^{B}.
R^{σ→ρ}(f, f′) ∧ R^{τ→ρ}(g, g′) ⇒ R^{ρ}(case a f g, case b f′ g′) )

which is not an inductive definition. This demonstrates that the pattern of definition for prelogical relations is more robust than that for logical relations.

A type constructor that has received less attention in the literature is (finite) powerset, P(σ). The treatment would be like that of products and coproducts, given models containing a standard interpretation of bool: we add term constants ∅ : P(σ), {·} : σ → P(σ), ∪ : P(σ) → P(σ) → P(σ) and ∈: σ → P(σ) → bool and require R^{P (σ)}([[∅]]^{A}, [[∅]]^{B}) etc. For models in which the interpretation of the powerset type and these new constants are as usual, this amounts to imposing the following condition:

R^{P(σ)}(α, β) iff ∀a ∈ α.∃b ∈ β.R^{σ}(a, b) and ∀b ∈ β.∃a ∈ α.R^{σ}(a, b).

Note that this is the same pattern used in defining bisimulations.

Various other kinds of types can be considered, including inductive and coinductive data types (see [3]), universally and existentially quantified types (see [20]), and various flavours of dependent types. We have not yet considered these in any detail, but we are confident that for any of them, one could take any existing treatment of logical relations and modify it by weakening the condition on functions as above without sacrificing the Basic Lemma. We expect that this would even yield improved results as it has above, but this is just speculation.

We have so far restricted attention to structures modelling total functions. Admitting partial functions involves consideration of typed partial combinatory algebras, cf. Sect. 5.6.2 of [19]: these are combinatory algebras where App is a partial function, such that K x y↓ (and K x y = x), S x y↓ and S x y z ≃ (x z) (y z). (As usual, t↓ denotes the fact that the term t is defined and t ≃ t′ means that the two terms t and t′ are either both defined and equal or both undefined.) Typed partial combinatory algebras are the appropriate setting for discussing call-by-value combinatory logic or lambda calculus. There is a standard compilation of lambda terms into combinatory terms which maps values (variables, constants and abstractions) to defined terms.

The appropriate notion of prelogical relation for typed partial combinatory algebras coincides with the standard one for combinatory algebras except that the condition for arrow types has to take undefinedness into account. We use the condition

(A) If R^{σ→τ} (f, g) then
∀a ∈ [[σ]]^{A}.∀b ∈ [[σ]]^{B}.R^{σ}(a, b) implies f a↑ ∧ g b↑
or f a↓ ∧ g b↓ ∧ R^{τ} (f a, g b)

which yields both the Basic Lemma (modified slightly to take undefinedness into account) and closure under composition.

Notice that if we had instead taken

(B) If R^{σ→τ} (f, g) then
∀a ∈ [[σ]]^{A}.∀b ∈ [[σ]]^{B}.R^{σ}(a, b) implies f a↓ ∧ g b↓ ∧ R^{τ} (f a, g b),

then there would be structures for which there are no prelogical relations, for instance when such structures interpret term constants that are not in the domain of the interpretation of other term constants. If we had been too liberal, by taking

(C) If R^{σ→τ} (f, g) then
∀a ∈ [[σ]]^{A}.∀b ∈ [[σ]]^{B}.R^{σ}(a, b) implies f a↓ ∧ g b↓ ⇒ R^{τ} (f a, g b),

then closure under composition would fail. In both cases a revised version of the Basic Lemma would hold. Interestingly, the notion of logical relation arising from (A) is not the one usually used for extracting a typed partial combinatory algebra from an untyped partial combinatory algebra. This notion is the one arising from (B).

A different dimension of generalization is to consider models having additional structure — e.g. Kripke applicative structures [21], presheaf models or cartesian closed categories — for which logical relations have been studied. We have not yet examined the details of this generalization but a corresponding weakening of the definition would be interesting to consider. It is worth noting that Prop. 6.2 links prelogical relations to KLRwVAs, which have a logical formulation over appropriate presheaf categories as hinted in [10] and have been extended to cartesian closed categories in [2].

11. RELATED WORK

The definition of prelogical relations is not new. In [31], Schoett uses a first-order version of algebraic relations which he calls correspondences (see also simulations in [16] and weak homomorphisms in [7]), and he conjectures (p. 281) that for Henkin models, what we have called prelogical relations (formulated as in Prop. 3.3) would be closed under composition and yield the Basic Lemma. In [17], Mitchell makes the same suggestion, referring to Schoett and also crediting Abramsky and Plotkin, but as an assertion rather than a conjecture. The idea is not developed any further. An independent but equivalent definition of prelogical relations over cartesian closed categories, based on the account of logical relations in [14], is given in [24] where they are called lax logical relations. It is shown that these compose, that the Basic Lemma holds, and that they coincide with prelogical relations, and an axiomatic account is provided. Earlier, a closely related notion called L-relations was defined in [11] and shown to compose. In contrast to [24] and [11], our treatment is elementary rather than categorical, and covers also combinatory algebras. As far as assessing possible categorical generalizations of prelogical relations, some real scientific work ought to be done first in relating the work in [2], [11], [24] and [28] (cf. [25], [26]). In an appropriate categorical setting, the very notion of logical relation appears to have already some desired properties of prelogical relations, which set-theoretical logical relations do not have: e.g. they characterize λ-definable points [2], or capture observational equivalence [28] (cf. [25], [26]). The appropriate categorical generalization of prelogical relations ought to have all the properties of prelogical relations in Theorem 12.1 below (mutatis mutandis) as well as characterizing observational equivalence. It appears that a slight weakening of lax logical relations might be such a notion.

Another very interesting connection appears with some recent work of Longley, see [13]. He has used applicative morphisms, which are essentially total prelogical relations, to study the relationship between various notions of computability.

Two papers that we came across only after writing this paper but which have some intriguing connections to some of our results and techniques, are [32] and [20]. We believe that the concept of prelogical relation would have a beneficial impact on the presentation and understanding of their results.

In [32], Statman gives a characterization of the lambda-definable functionals of an arbitrary type structure as the “stable solutions to systems of functional equations”. Without giving all the details, we just say that a solution is stable if it is α-stable for all ordinals α, where 1-stability amounts to uniqueness of the solution and a solution is α + 1-stable if it yields α-stable solutions under image and preimage of partial surjective homomorphisms.

Now, partial surjective homomorphisms are just special logical relations, and so α-stability implies stability under suitable α-fold composition of such logical relations. Not surprisingly, the numerology of the number 3 surfaces also in this context, and Statman brilliantly proves that it is enough to look at 3-stable solutions!

Statman does not deal with systems of equations with arbitrary parameters (i.e. signatures). He does not make direct use of indeterminates in proving his results, but these are implicit in the term model of typed lambda calculus. It is not hard to imagine that the notion of prelogical relation and the constructions in the proof of our Theorem 7.1 could shed some light into the essence of this result as well as providing an alternative presentation and possibly a generalization to arbitrary signatures.

Although addressing the issue of logical relations for second-order lambda calculus, the gist of some of Mitchell and Meyer’s results in [20] bears a similar connection to some of our results on prelogical relations. In particular, in their Theorems 4 and 5 Mitchell and Meyer characterize lambda-definable elements of a model and an appropriate notion of observational equivalence between models using logical relations over superstructures defined by adding indeterminates to the given models.

Since [20] is an extended abstract, the proofs of these results cannot be analyzed. But on the basis of our Prop. 7.5 and Corollary 8.5, both Theorems 4 and 5 in [20] appear rather plausible. Again, the use of prelogical relation — if they had been available — would probably have allowed them to phrase their results in a slightly more general fashion.

12. CONCLUSIONS AND DIRECTIONS FOR FUTURE WORK Our feeling is that by introducing the notion of prelogical relation we have,

metaphorically and a little immodestly, removed a “blind spot” in the existing intuition of the use and scope of logical relations and related techniques. This is not to say that some specialists in the field have not previously contemplated generalizations similar to ours, but they have not carried the investigation far enough. We believe that in this paper we have exposed very clearly the fact that in many situations the use of logical relations is unnecessarily restrictive. Using prelogical relations instead, we get improved statements of some results (e.g. Theorem 8.4 and its corollaries), we encompass constructions that had previously escaped the logical paradigm (e.g. Example 3.13), and we isolate the necessary and sufficient hypotheses for many arguments to go through (e.g. Lemma 4.1). We have given several characterizations of prelogical relations, summarized in the following theorem (for the unary case):

Theorem 12.1. Let P = {P^{σ} ⊆ [[σ]]^{A}}_{σ∈Types(Σ)} be a family of predicates over a Henkin model A. The following are equivalent.

1.P is a prelogical predicate.

2.P is closed under lambda definability.

3.P is the set of elements of A that are invariant under some KLRwVA.

4.P is the set of elements of A that are invariant under (or alternatively, the projection or ∀ of) the composition of (three) logical relations.

Proof. 1 ⇔ 2 is Prop. 4.2, 1 ⇔ 3 is Prop. 6.2, and 1 ⇔ 4 is by Corollary 7.2.

The fact that there are so many conceptually independent ways of defining the same class of relations, together with the fact that they characterize observational equivalence, suggests that it is a truly intrinsic notion. Notice that Thm. 12.1(3) gives an inductive flavour to this concept which is not explicit in the definition of prelogical relation; this apparent lack has been regarded as a weakness of the concept, see e.g. p. 428–429 of [17].

Throughout the paper we have indicated possible directions of future investigation, e.g. suggesting in Sect. 10 how to generalize to less elementary type structures. As we point out, there is a standard methodology here: simply require the interpretations of the “relevant” constants in the two structures to be related. Despite its simplicity, this methodology is extremely rewarding, and it allows to harvest serendipitous results also in related areas. A case in point is offered by PER models of System F, where the extra latitude and flexibility given by defining the exponential PER prelogically allows for a number of possibly novel natural model constructions. It is plausible that sharper chararacterizations of representation independence similar to the one presented here for simple types will appear in richer type disciplines.

There is a vast literature on logical relations in connection with areas such as parametricity, abstract interpretation, etc. A treatment of these topics in terms of prelogical relations is likely to be as fruitful and illuminating as it has proved to be for the classical example of simply-typed lambda calculus presented here. One possible direction among many would be to study the impact of prelogical relations on the presentation of fully abstract models as in e.g. [27, 22, 15].

In view of the numerous results, connections, new perspectives, and yes, also some criticism, that prelogical relations have brought with them, one can say that changing a ⇔ to ⇒ in the definition of logical relations was like rubbing Aladdin’s lamp — or, some would say, like opening Pandora’s box!

ACKNOWLEDGMENT

Thanks to Samson Abramsky, Jo Hannay, Martin Hofmann, Shin-ya Katsumata, Andrew Kennedy, Yoshiki Kinoshita, Hans Leiß, John Longley, John Mitchell, Peter O’Hearn, Gordon Plotkin, John Power, Ian Stark, Bob Tennent and an anonymous referee for helpful comments. This work has been partially supported by EPSRC grant GR/K63795, an SOEID/RSE Support Research Fellowship, the ESPRIT-funded CoFI and TYPES working groups, and the MURST TOSCA grant.

REFERENCES

1. S. Abramsky. Abstract interpretation, logical relations, and Kan extensions. Journal of Logic and Computation 1:5–40 (1990).

2. M. Alimohamed. A characterization of lambda definability in categorical models of implicit polymorphism. Theoretical Computer Science 146:5–23 (1995).

3. T. Altenkirch. Logical relations and inductive/coinductive types. Proc. Computer Science Logic, CSL’98, Brno. Springer LNCS 1584, 343–354 (1998).

4. P.-L. Curien. Categorical Combinators, Sequential Algorithms, and Functional Programming, 2nd edition. Birkhäuser (1993).

5. P. Di Gianantonio and F. Honsell. An abstract notion of application. Proc. Intl. Conf. on Typed Lambda Calculi and Applications, Utrecht. Springer LNCS 664, 124–138 (1993).

6. R. Gandy. Proofs of strong normalization. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 457–477. Academic Press (1980).

7. A. Ginzburg. Algebraic Theory of Automata. Academic Press (1968).

8. F. Honsell, J. Longley, D. Sannella and A. Tarlecki. Constructive data refinement in typed lambda calculus. Proc. 2nd Intl. Conf. on Foundations of Software Science and Computation Structures, European Joint Conferences on Theory and Practice of Software (ETAPS’2000), Berlin. Springer LNCS 1784, 149–164 (2000).

9. F. Honsell and D. Sannella. Pre-logical relations. Proc. Computer Science Logic, CSL’99, Madrid. Springer LNCS 1683, 546–561 (1999).

10. A. Jung and J. Tiuryn. A new characterization of lambda definability. Proc. Intl. Conf. on Typed Lambda Calculi and Applications, Utrecht. Springer LNCS 664, 245–257 (1993).

11. Y. Kinoshita, P. O’Hearn, J. Power, M. Takeyama and R. Tennent. An axiomatic approach to binary logical relations with applications to data refinement. Proc. TACS’97, Springer LNCS 1281, 191–212 (1997).

12. R. Loader. The undecidability of λ-definability. In: Logic, Meaning and Computation: Essays in Memory of Alonzo Church. Kluwer Academic (2001).

13. J. Longley. Matching typed and untyped realizability. Proc. Tutorial Workshop on Realizability Semantics and Applications, Trento. Electronic Notes in Theoretical Computer Science 23 No. 1 (1999).

14. Q. Ma and J. Reynolds. Types, abstraction, and parametric polymorphism, part 2. Proc. 7th Intl. Conf. on Mathematical Foundations of Programming Semantics, Pittsburgh. Springer LNCS 598, 1–40 (1992).

15. M. Marz, A. Rohr and T. Streicher. Full abstraction and universality via realisability. Proc. 14th IEEE Symp. on Logic in Computer Science, Trento (1999).

16. R. Milner. An algebraic definition of simulation between programs. Proc. 2nd Intl. Joint Conf. on Artificial Intelligence. British Computer Society, 481–489 (1971).

17. J. Mitchell. Type Systems for Programming Languages. Chapter 8 of Handbook of Theoretical Computer Science, Vol B. Elsevier (1990).

18. J. Mitchell. On the equivalence of data representations. In: Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy (V. Lifschitz, ed.). Academic Press, 305–330 (1991).

19. J. Mitchell. Foundations for Programming Languages. MIT Press (1996).

20. J. Mitchell and A. Meyer. Second-order logical relations. Proc. of the Conf. on Logic of Programs, Brooklyn. Springer LNCS 193, 225–236 (1985).

21. J. Mitchell and E. Moggi. Kripke-style models for typed lambda calculus. Annals of Pure And Applied Logic 51:99–124 (1991).

22. P. O’Hearn and J. Riecke. Kripke logical relations and PCF. Information and Computation 120:107–116 (1995).

23. G. Plotkin. Lambda-definability in the full type hierarchy. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 363–373. Academic Press (1980).

24. G. Plotkin, J. Power, D. Sannella and R. Tennent. Lax logical relations. Proc. 27th Intl. Colloq. on Automata, Languages and Programming, Geneva. Springer LNCS 1853, 85–102 (2000).

25. J. Power and E. Robinson. Logical relations and data abstraction. Proc. Computer Science Logic, CSL 2000, Fischbachau. Springer LNCS 1862 (2000).

26. J. Power and E. Robinson. Logical relations, data abstraction and structured fibrations. Proc. 2nd Intl. Conf. on Principles and Practice of Declarative Programming, Montreal (2000).

27. J. Riecke and A. Sandholm. A relational account of call-by-value sequentiality. Proc. 12th IEEE Symp. on Logic in Computer Science, Warsaw, 258–267 (1997). Information and Computation, to appear.

28. E. Robinson. Logical relations and data abstraction. Report 730, Queen Mary and Westfield College (1996).

29. D. Sannella and A. Tarlecki. On observational equivalence and algebraic specifications. Journal of Computer and System Sciences 34:150–178 (1987).

30. D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25:233–281 (1988).

31. O. Schoett. Data Abstraction and the Correctness of Modular Programming. Ph.D. thesis CST-42-87, Univ. of Edinburgh (1987).

32. R. Statman. λ-definable functionals and βη conversion. Arch. math. Logik 23:21–26 (1983).

33. R. Statman. Logical relations and the typed lambda calculus. Information and Control 65:85– 97 (1985).

34. R. Tennent. Correctness of data representations in Algol-like languages. In: A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall (1994).

APPENDIX

Here we give a detailed proof of the following theorem.

Theorem 7.1. Let A and B be Henkin models and let R be a prelogical relation over A and B. Then R factors into a composition of three logical relations over Henkin models.

See Sect. 7 for the idea of the proof. We proceed as follows:

• We define the model A[Y] and the relation that embeds A in A[Y], and show that this is a logical relation (Lemma A.7). The same applies to B and B[Y].

• We define R[Y] ⊆ A[Y]×B[Y] and show that it is a logical relation (Lemma A.9).

• Finally we show that R is the composition of the embedding of A in A[Y], R[Y], and the inverse of the embedding of B in B[Y] (Lemma A.10).

Let Y be a set of typed variables containing an infinite number of variables for each type in Types(Σ).

Definition A.1. Let ΣA be Σ augmented by a term constant c_{a} : σ for each element a ∈ [[σ]]^{A}. Let Σ[Y] (resp. ΣA[Y]) be Σ (resp. ΣA) augmented by a term constant c_{y} : σ, called an indeterminate, for each variable y : σ in Y.

Definition A.2. The Henkin model A[Y] over Σ[Y] is the (closed) ΣA[Y]-term model of the simply-typed lambda calculus with β and η, and with δ-reductions describing the behaviour of each constant c_{a} with respect to other such constants (and with no δ-reductions involving the indeterminates). This calculus is Church-Rosser and strongly normalizing so each term M has a unique normal form M̂. Although elements in A[Y] are equivalence classes of terms, it is convenient to refer to them using single terms, by which is meant the equivalence class containing that term. Since all terms in a given equivalence class have the same normal form, we will sometimes write â for an element a in A[Y]. If η is a Γ-environment over A then η_{c} is the Γ-environment over A[Y] which assigns each variable x to (the equivalence class of) c_{η(x)}.

Please note that A[Y] is not the construction corresponding to the “free combinatory Σ-algebra” generated by the constants in A, which is more frequently used in the literature. Rather, it is the construction corresponding to the “free Σ-algebra” generated by the constants in A. So the interpretations of pure closed lambda terms, such as K or S, are not preserved in the generic extension. For instance, K ≠ [[c_{K}]]^{A[Y]}.

Lemma A.3. If M →_{βηδ}^{∗} N for Γ ⊳_{ΣA} M, N : σ, then for any Γ-environment η over A, [[M]]_{η}^{A} = [[N]]_{η}^{A} in which we interpret each of the constants c_{a} as a.

Proof. By induction on the structure of the derivation of M →_{βηδ}^{∗} N.

Lemma A.4. Let Γ ⊳_{Σ} M, N : σ. If [[N]]_{η_{c}}^{A[Y]} = [[M]]_{η′_{c}}^{A[Y]} then [[N]]_{η}^{A} = [[M]]_{η′}^{A}.

Proof. If [[N]]_{η_{c}}^{A[Y]} = [[M]]_{η′_{c}}^{A[Y]} then N[η_{c}(x)/x for all x] and M[η_{c}(x)/x for all x] reduce to the same normal form. By Lemma A.3, the reduction sequences that yield this normal form can be reproduced in A to give [[N]]_{η}^{A} = [[M]]_{η′}^{A}.

Lemma A.5. Let Γ ⊳_{Σ} M : σ and Γ ⊳_{Σ[Y]} N : σ. If [[M]]_{η_{c}}^{A[Y]} = [[N]]_{η_{c}}^{A[Y]} then

{ \atop [[N]]_{η_{c}}^{A[Y]}} is a ΣA-term, and moreover the βη-normal form of N contains no indeterminates.

Proof. The presence of indeterminates does not give rise to extra reductions, nor can indeterminates be erased by the δ-reductions associated to the constants c_{a}. Any indeterminate in the βη-normal form of N would therefore falsify the hypothe-

sis.

Definition A.6. The embedding emb of A into A[Y] is defined as follows:

emb^{σ} = {⟨[[M]]_{η}^{A}, [[M]]_{η_{c}}^{A[Y]}⟩ | Γ ⊳_{Σ} M : σ and η a Γ-environment over A}

Although we call emb an embedding, this is inaccurate since it is never a settheoretic function. To be precise, it is the natural lifting to a logical relation of the embedding at base types. It is easy to check however that emb^{−1} is a partial surjection.

Lemma A.7. emb is a logical relation.

Proof. It is easy to see that each constant c in Σ is in relation to itself: just take M = c. Furthermore, suppose emb^{σ→τ} ([[M]]_{η}^{A}, [[M]]_{η_{c}}^{A[Y]}) and emb^{σ}([[N]]_{η′}^{A}, [[N]]_{η′_{c}}^{A[Y]}); we need to show emb^{τ} (App_{A} [[M]]_{η}^{A} [[N]]_{η′}^{A}, App_{A[Y]} [[M]]_{η_{c}}^{A[Y]} [[N]]_{η′_{c}}^{A[Y]}). Without loss of generality (because we can rename variables, and denotations depend only on variables which occur) we can assume that η = η′ and then the result follows from the definition of interpretation: App_{A} [[M]]_{η}^{A} [[N]]_{η}^{A} = [[M N]]_{η}^{A} and similarly for A[Y].

It remains to prove the opposite direction of the implication. Suppose that whenever emb^{σ}(a, d), emb^{τ} (App_{A} f a, App_{A[Y]} g d). We need to show emb^{σ→τ} (f, g).

Consider the normal form ĝ of g. We claim that ĝ is a ΣA-term, i.e. it contains no indeterminates. We know that emb^{σ}(a, [[x]]_{η_{c}}^{A[Y]}) with η_{c}(x) = c_{a}. Since emb^{τ} (App_{A} f a, App_{A[Y]} g [[x]]_{η_{c}}^{A[Y]}), there is a term Γ⊳_{Σ} N : τ and Γ-environment ξ

such that App_{A[Y]} g [[x]]_{η_{c}}^{A[Y]} = [[N]]_{ξ_{c}}^{A[Y]}. Again w.l.o.g. ξ = η, so { \atop App_{A[Y]} g [[x]]_{η_{c}}^{A[Y]}} is a ΣA-term by Lemma A.5, and then so is ĝ. Therefore, consider the Σ-term M and environment η′_{c} such that [[M]]_{η′_{c}}^{A[Y]} = ĝ: M is ĝ with each constant c_{a} replaced by a variable which η′_{c} maps to c_{a}. But now we claim that f is extensionally equal to [[M]]_{η′}^{A}. We have emb^{τ} (App_{A} f a, App_{A[Y]} [[M]]_{η′_{c}}^{A[Y]} c_{a}) so emb^{τ} (App_{A} f a, [[M z]]_{η′_{c}[z↦c_{a}]}^{A[Y]}) for a fresh variable z. By the definition of emb, there is a term Γ ⊳_{Σ} M′ : τ and Γ-environment η′′ such that [[M′]]_{η′′}^{A} = App_{A} f a and [[M′]]_{η′′_{c}}^{A[Y]} = [[M z]]_{η′_{c}[z↦c_{a}]}^{A[Y]}. Again w.l.o.g., η′′_{c} = η′_{c}[z ↦ c_{a}]. Then [[M′]]_{η′′}^{A} = [[M z]]_{η′′}^{A} by Lemma A.4, and thus App_{A} f a = App_{A} [[M]]_{η′}^{A} a which shows that f is extensionally equal to [[M]]_{η′}^{A}. So by extensionality, [[M]]_{η′}^{A} = f giving emb^{σ→τ} (f, g).

We will need to refer to both emb ⊆ A × A[Y] and emb ⊆ B × B[Y] so we use the notation emb_{A} for the former and emb_{B} for the latter.

Definition A.8. The relation R[Y] ⊆ A[Y] × B[Y] is defined as follows:

R[Y]^{σ} = \{⟨[[M]]_{η_{c}}^{A[Y]}, [[M]]_{η′_{c}}^{B[Y]}⟩ | \begin{matrix}Γ ⊳_{Σ[Y]} M : σ and η, η′ are Γ-environments \\ for A, B such that R(η, η′)\} \end{matrix}

Lemma A.9. R[Y] is a logical relation.

Proof. Each constant c in Σ[Y] is in relation to itself: just take M = c. Furthermore, suppose R[Y]([[M]]_{η_{c}}^{A[Y]}, [[M]]_{η′_{c}}^{B[Y]}) and R[Y]([[N]]_{η_{c}}^{A[Y]}, [[N]]_{η′_{c}}^{B[Y]}). (We should assume that we have different environments for [[M]]^{A[Y]} and [[N]]^{A[Y]} and for [[M]]^{B[Y]} and [[N]]^{B[Y]}, but without loss of generality we can assume that the A[Y]-environments are the same and similarly for B[Y].) We need to show that then R[Y](App_{A[Y]} [[M]]_{η_{c}}^{A[Y]} [[N]]_{η_{c}}^{A[Y]}, App_{B[Y]} [[M]]_{η′_{c}}^{B[Y]} [[N]]_{η′_{c}}^{B[Y]}). We get the result by the definition of interpretation: App_{A[Y]} [[M]]_{η_{c}}^{A[Y]} [[N]]_{η_{c}}^{A[Y]} = [[MN]]_{η_{c}}^{A[Y]} and similarly for B[Y].

It remains to prove the opposite direction of the implication. Suppose we have f ∈ A[Y] and g ∈ B[Y] such that for every Σ[Y]-term P and environments η, η′ for A and B such that R(η, η′), R[Y](App_{A[Y]} f [[P]]_{η_{c}}^{A[Y]}, App_{B[Y]} g [[P]]_{η′_{c}}^{B[Y]}). Then take P to be an indeterminate c_{y} which does not occur in f̂or ĝ. (We need an infinite number of indeterminates to ensure that there is one that is different from all those that are already used in the terms f̂ and ĝ.) We know that there exists a Σ[Y]-term M and environments ξ, ξ′ for A and B such that R(ξ, ξ′), App_{A[Y]}f [[c_{y}]]_{ξ_{c}}^{A[Y]} = [[M]]_{ξ_{c}}^{A[Y]} and App_{B[Y]} g [[c_{y}]]_{ξ′_{c}}^{B[Y]} = [[M]]_{ξ′_{c}}^{B[Y]}. Consider the Σ[Y]-term Q = λc_{y}.M. (Formally speaking, we should really take λx.M[x/c_{y}] so that we are abstracting a variable rather than a constant, but the meaning is clear.) We claim that f is extensionally equal to [[Q]]_{ξ_{c}}^{A[Y]}. Let a ∈ A[Y]. Now consider the reduction sequences from App_{A[Y]} f [[c_{y}]]_{ξ_{c}}^{A[Y]} and App_{A[Y]} [[λc_{y}.M]]_{ξ_{c}}^{A[Y]} [[c_{y}]]_{ξ_{c}}^{A[Y]} to a common reduct S. If we replace all unbound occurrences of c_{y} in these reduction sequences with a, we obtain valid reduction sequences from App_{A[Y]}f a and App_{A[Y]}[[λc_{y}.M]]_{ξ_{c}}^{A[Y]}a to the common reduct S[a/c_{y}]. This works because c_{y} is “sterile”, with generic behaviour. Similarly, g is extensionally equal to [[Q]]_{ξ′_{c}}^{B[Y]}. Therefore, since A[Y] and B[Y] are extensional, R[Y](f, g).

Lemma A.10. The composition of emb_{A}, R[Y] and (emb_{B})^{−1} is R.

Proof. It is easy to see that R is included in the composition: take M in Definition A.6 to be a fresh variable, then if R(a, b), we have η(x) = a, η_{c}(x) = c_{a}, η′_{c}(x) = c_{b}, η′(x) = b. As for the converse, suppose ((emb_{B})^{−1} ∘ R[Y] ∘ emb_{A})(a, b). By definition of emb_{A} there exists a Σ-term N and environment ηA such that a = [[N]]_{ηA}^{A}. By definition of emb_{B} there exists a Σ-term N′ and environment ηB such that b = [[N′]]_{ηB}^{B}. By definition of R[Y] there exists a Σ[Y]-term M and environments η, η′ such that [[N]]_{ηA_{c}}^{A[Y]} = [[M]]_{η_{c}}^{A[Y]}, [[N′]]_{ηB_{c}}^{B[Y]} = [[M]]_{η′_{c}}^{B[Y]} and R(η, η′). W.l.o.g. we can assume that ηA = η and ηB = η′ and that M is in βη-normal

form. By Lemma A.5 we know that { \atop [[M]]_{η_{c}}^{A[Y]}} and { \atop [[M]]_{η′_{c}}^{B[Y]}} are ΣA- and ΣB-terms respectively, and that M contains no indeterminates. By Lemma A.4 we know that a = [[N]]_{η}^{A} = [[M]]_{η}^{A} and b = [[N′]]_{η}^{B} = [[M]]_{η′}^{B}. So by the Basic Lemma, R(a, b).