Logical Relations and Data Abstraction^{⋆}

John Power^{⋆⋆}^{1} and Edmund Robinson^{⋆ ⋆ ⋆}^{2}

1 Laboratory for the Foundations of Computer Science, University of Edinburgh

                       ajp@dcs.ed.ac.uk

2 Department of Computer Science, Queen Mary and Westfield College,

                    edmundr@dcs.qmw.ac.uk

Abstract. We prove, in the context of simple type theory, that logical relations are sound and complete for data abstraction as given by equational specifications. Specifically, we show that two implementations of an equationally specified abstract type are equivalent if and only if they are linked by a suitable logical relation. This allows us to introduce new types and operations of any order on those types, and to impose equations between terms of any order. Implementations are required to respect these equations up to a general form of contextual equivalence, and two implementations are equivalent if they produce the same contextual equivalence on terms of the enlarged language. Logical relations are introduced abstractly, soundness is almost automatic, but completeness is more difficult, achieved using a variant of Jung and Tiuryn’s logical relations of varying arity. The results are expressed and proved categorically.

1 Introduction

Logical relations are a standard tool for establishing the equivalence of data representations. If one can find a family of relations on corresponding types which is a congruence, i.e., are preserved by operations of the theory, and reduces to equality on observable types, then clearly observable operations will be equal in the two representations. Such a family need not form a logical relation (it may form a lax or pre-logical relation [4, 12]), but logical relations do provide a way to construct such families by induction on type structure. So the establishment of a logical relation suffices to determine equivalence of representation at least for simple types. It has long been known that for algebraic theories with first order operations and equations, equivalent representations are indeed linked by a logical relation, see Mitchell [9, 10]. It has also long been known that standard logical relations are not complete in this sense for higher-order theories.

⋆ Keywords: logical relations, cartesian closed fibrations, interpretations, lambda cal-

culus. ⋆⋆ This work has been done with the support of EPSRC grant GR/M56333 and a

British Council grant. ⋆ ⋆ ⋆ This author would like to acknowledge the support of an EPSRC Advanced Fellow-

ship, EPSRC grant GR/L54639, and ESPRIT Working Group 6811 Applied Semantics

The purpose of this paper is to show that by relaxing the definition of logical relation, we can extend Mitchell’s completeness result to higher-order theories.

The approach we take here has two major sources. The first is the work of Achim Jung and Jerzy Tiuryn [5], who used a form of logical relations to characterise lambda definability in the simple type hierarchy. The second is the thesis of Claudio Hermida [3], which explores the connection between logical predicates and logical formalisms expressed as fibrations defined over the semantic category. Sadly there is still no really accessible reference for the material and ideas in this thesis.

From a practical angle, the notion of abstract type we use here is quite restricted as we only consider equationally specified types, albeit with equations between higher-order operators. This is also the level of generality of Alimohamed’s work on definability [1]. However, it raises a natural question of whether the link with logic exploited in this paper could be further exploited to allow a less restrictive specification language.

Finally, if data abstraction is the study of equivalence of representation, then data refinement is the study of improvements. The two ideas are clearly linked, and the fundamental notion of this paper, that of being “linked by a logical relation”, is closely related to the notion of L-relation in [6] (see also [14]). The work of that paper, which is also about data equivalence but from a purely categorical perspective, and the work of this paper, and those on lax and prelogical relations [4, 12] clearly need to be combined at some point.

A natural question, however, is why we chose to base our work on cartesian closed categories rather than Henkin models.

Henkin models provide a natural extension of classical set-based first-order model theory to the higher-order setting of simply typed lambda calculi. Much of their appeal lies in the immediacy of this relation. Cartesian closed categories, on the other hand, arose out of the desire to express in purely category theoretic terms the characteristic properties of function spaces such as those found in Set. The formal link with typed lambda calculus, though not surprising in itself, came surprisingly late (cf. Lambek and Scott [7]), and prompted a slight redefinition of the notion to allow categories which had products but not arbitrary finite limits.

Cartesian closed categories and Henkin models are intimately linked. If one starts with a Henkin model of λ→ one can easily extend it to model the type theory with products, λ×→ (using the fact that the type (A_{1} × … × A_{n}) → (B_{1}×…×B_{m}) is isomorphic to a product of pre-existing types (A_{1} → (… (A_{n} → B_{1}) …))×…×(A_{1} → (… (A_{n} → B_{m}) …))). If one has a Henkin model of typed lambda calculus with products, then one can obtain a (concrete) cartesian closed category. The objects are types and the morphisms A ⟶ B are the elements of the function type [A → B] in the Henkin model. Conversely if one has a cartesian closed category C, together with a product-preserving functor U : C ⟶ Set, then one obtains an applicative structure with product types. The types are the objects of the category, and the type A is interpreted as the set UA. This automatically has representations of the combinators because of their presence as morphisms in the cartesian closed category. However it is not necessarily a Henkin model because in general different elements of the function type may represent the same function. If, however, C is a concrete category and U its underlying set functor, this will not happen. In that case we do get a Henkin model.

So, from this perspective, cartesian closed categories generalise Henkin models. The question is whether that generality, or that difference in structure, is useful. We believe that it is.

One technical difference between the two approaches is apparent if one thinks of semantics taken in some kind of sets with structure (e.g. domains). It is natural to ask when this collection of sets forms a model of the simply typed lambda calculus. The category-theoretic answer is that one has to specify an appropriate notion of homomorphism. The resulting category is then either cartesian closed, in which case it supports a model structure, or it is not, when it doesn’t. Moreover, if it is cartesian closed then the structure we use to model the lambda calculus is essentially unique. In contrast, it is much less clear what the constraints on a Henkin structure might be, or in what sense the structure would be unique if it existed. Essentially the development has to mimic the categorytheoretic. First one defines an appropriate notion of homomorphism. Then one asks whether the set of homomorphisms between two objects can be made to carry the structure of the objects we are interested in. Or rather, since it almost always can, whether it can be made to do so in a way that makes application and the combinators homomorphisms. It is perhaps because of this apparently greater complexity that domain theorists and others talk about specific categories of domains being cartesian closed, and not about Henkin structures on classes of domains.

Moreover, Henkin models can only talk about models built on sets. This constraint is not always natural. For example it is natural to say that the canonical way of viewing a partially-ordered set as a category turns a Heyting (or Boolean) algebra into a cartesian closed category. It is not natural to say that they carry a Henkin model structure, since that requires presenting the elements of the partial order as themselves sets. A further example comes from the Curry-Howard correspondence. This can be conveniently and precisely expressed by saying that there is an isomorphism between a category whose objects are types and whose morphisms are βη-equivalence classes of λ-terms, and a category whose objects are propositions and whose morphisms are normalisation classes of proofs. The Henkin model account has to be forced to apply to this, most notably because in the event that A is not provable, then a proof of A ⇒ B cannot adequately be described as a function which takes proofs of A to proofs of B.

We now turn to possible directions for our own future work. First, there are links between this work and the work of Honsell and Sannella on pre-logical relations. Unfortunately a preliminary account of these links had to be cut from this paper for reasons of space. We intend to return to this theme. An obvious direction in which to extend this work is to address models of call-by-value lambda-calculi such as the computational lambda-calculus [11].

Several people have been of considerable help in making comments or suggestions: they include Adam Eppendahl, Claudio Hermida, Peter O’Hearn, David Pym, Makoto Takeyama, and Bob Tennent. We would also like to thank the (many) anonymous referees of the original paper. We are sorry that we have not been able to make all the improvements they suggested.

2 Contextual equivalence

In this section, we give a categorical account of a standard Morris-style contextual equivalence. As we are working in the context of simple type theory, and the theory may well be strongly normalising, we use a denotational rather than an operational approach, and observe values produced by computations rather than termination.

The basic structure is as follows. We assume a given cartesian closed category C. For instance, C may be the category Set of small sets, or, if we want to be sure to include fixed point operators to model recursion, we could consider C to be the category of ω-cpo’s with least element, and with maps being functions that preserve the poset structure and sup’s of ω-chains. Other alternatives for C include categories generated by axiomatic domain theory [2], or presheaf categories, or toposes. We simply require that C be cartesian closed. The category C will represent our base category in which we take our denotational semantics.

We further assume that we are given a set of observable pairs of types Obs ⊆ ob(C) × ob(C). The intuition behind this is that we are allowed to form judgements of equality

x : A ⊢ e = e′ : B

where (A, B)ϵObs. An alternative approach is to use a set of observable types, but we think this accords better with our open-term interpretation of the lambda calculus, and will allow a simpler extension to dependent type theory.

We use the structure of observables to generate a contextual equivalence ≈ on C, which allows us to compare f ≈ g when f and g are maps with common domain and codomain: type-theoretically, this amounts to demanding that contextually equivalent terms have the same type and are defined in the same context.

Example 1. 1. The underlying category is CPO, and Obs = {(1, 1_{⊥})}. This gives one of the standard forms of Morris-style contextual equivalence, in which we are allowed to observe termination of closed terms.

2. The underlying category is Set, and Obs = {(1, Bool)}. Here, there is no non-termination, but contexts produce closed terms of type Bool. We can observe the boolean produced.

3. Obs = ob(C) × ob(C). In this case everything is observable. Not surprisingly ≈ is just equality.

Definition 1. Given f, g : X ⟶ Y, we define ∼ by f ∼ g if for all (A, B)ϵObs, and for all α : A ⟶ X and β : Y ⟶ B, we have

[figure: A; α; X; f; Y; β; B]

equals

[figure: A; α; X; g; Y; β; B]

The category theoretic definition of a congruence is often used to mean an equivalence relation on each homset of a category C such that that equivalence relation is respected by composition on either side. Here, by a congruence, we mean that notion together with invariance under products and exponentials. That allows us to make the primary definition of this section as follows.

Definition 2. We define ≈ to be the largest congruence contained in ∼.

Mercifully, we can characterise ≈ more directly by means of the following proposition. We denote the exponential of X raised to the power U by [U, X]. We follow this convention for exponentials in a category, for exponentials of not only objects but maps, and for exponentials of categories, i.e., for functor categories, when we need them.

Proposition 1. Given f, g : X ⟶ Y, the following are equivalent:

1. f ≈ g

2. for all U, V in ob(C), we have [U, f] × V ∼ [U, g] × V

To prove this proposition, apply the following lemma.

Lemma 1. Let ∼ be an equivalence relation on parallel pairs of arrows of a category C. Then

1. composition preserves ∼, and hence C/ ∼ is a category and C ⟶ C/ ∼ is a functor if and only f ∼ g implies β · f · α ∼ β · g · α.

2. if C has finite products, then C/ ∼ has finite products, and passage to the quotient preserves them if and only if 1 holds and f ∼ g implies f ×V ∼ g×V for all V in ob(C).

3. if C is cartesian closed, then C/ ∼ is a cartesian closed category and passage to the quotient is a cartesian closed functor if and only if 1 and 2 hold and f ∼ g implies [U, f] ∼ [U, g] for all U in ob(C), or equivalently if and only if 1 holds and f ∼ g implies [U, f] × V ∼ [U, g] × V for all U,V in ob(C).

We can also make precise the relationship with Morris-style contextual equivalence. Any cartesian closed category can be regarded as a model of an applied lambda calculus in which we have base types corresponding to the objects of the category, and for each morphism f : X ⟶ Y, we are given a term constructor (function) f̂, such that if e is a term of type X, then f(e) is a term of type Y (as in Lambek and Scott [7]). As usual, a context, C[−] is a term with a hole (written [−]), such that when we plug a term of suitable type into the hole, we get something that we can run and observe. Making this precise for typed open terms is always messy. The simplest solution is to consider terms in context. In that case, we demand

\frac{x : X ⊢ e : Y}{a : A ⊢ C[e] : B}

should be an admissible rule for the type system (here, in order to make C[e] directly observable, (A, B) ∈ Obs). This can be achieved by ensuring that

\frac{x : X ⊢ [−] : Y}{a : A ⊢ C[−] : B}

is a derived rule.

Definition 3. Two terms e and e′ (more accurately, two terms in the same context: x : X ⊢ e : Y and x : X ⊢ e′ : Y …) are contextually equivalent, e ≅ e′ if and only if for all contexts C[−], M{C[e]} = M{C[e′]}, where M{e} is the semantics of e as taken in the category C.

Proposition 2. e ≅ e′ if and only if M{e} ≈ M{e′}.

Proof. In the if direction, this is a simple structural induction on the context. In the other, it depends on the expressibility of substitution via abstraction, application, and beta reduction, and on the fact that all morphisms in the category are expressible as terms in the calculus.

3 Abstract types

An equationally specified abstract type consists of a new type equipped with operations linking it to pre-existing types, and certain equations on terms built from those operations. The canonical example is stack. For our purposes, we may as well have a number of new types, and we interpret the operations as (open) terms in context

x : X ⊢ f : Y

where the X and Y may be arbitrary type expressions built up from old and new types. This generates an extended lambda calculus in which the equations are interpreted as equality judgements

x : X ⊢ e = e′ : Y

Such a system freely generates a cartesian closed category E which comes with a cartesian closed functor i : C ⟶ E. This functor is injective on objects, but in general is neither full nor faithful as we can add extra operations between pre-existing types and impose new equations between pre-existing operations. Conversely, given any injective on objects cartesian closed functor i : C ⟶ E, the category E is equivalent to a category constructed from C in this fashion, as we may generate it using all objects in E\i(C) and take all valid equations. So we can take i : C ⟶ E as the extension of C by some abstract types.

We split this construction into two stages: first adjoin types and operations freely to give i : C ⟶ D, and then quotient by the equations to give q : D ⟶ D/ ≈_{E}. In fact, we shall never use the free property of D and can take it to be an arbitrary cartesian closed category. The free property of such a D is fundamental to the work generalising logical relations for an account of data refinement in [6].

An implementation of the abstract type back in C is given by a cartesian closed functor F : D ⟶ C. We do not want to change the interpretation of the operations in C, so require F · i = id_{C}. We also want the interpretation to validate the equations of the abstract type, at least up to a suitable notion of observational congruence. We illustrate the problems with the canonical simple (but first-order) example:

Example 2. Let C be Set and let D consist of Set together with the formal addition of a type stack together with its operations (empty, top, pop and push) and equations (pop(push(n, s)) = s, and top(push(n, s)) = n). An implementation amounts to a realisation of the type stack together with its operations and subject to its equations in Set in both cases. Consider an array implementation, in which stack is implemented by an (unbounded) array and a top pointer, and pop simply decrements the top pointer, leaving the array unchanged. In this implementation, the interpretation of pop(push(n, s)) is not equal to s. Moreover, in Set we can apply an operation which reads the stack one place above the top pointer, and hence observe the difference. Of course this violates the stack abstraction.

The example above tells us that we cannot make the obvious restriction on F: if e = e′ is an equation of the abstract type, then F (M{e}) ≈ F (M{e′}). Instead we must build in the notion that contexts have restricted access to abstract types. This leads to the following definition (cf. definitions 1 and 2):

Definition 4. 1. Suppose F is a functor D ⟶ C, and f, g : X ⟶ Y is a parallel pair of morphisms in D, then f ∼_{F} g if and only if for all (A, B) in Obs, and for all α : iA ⟶ X and β : Y ⟶ iB, we have F (β · f · α) = F (β · g · α).

2. If, in addition, C, D and F are cartesian closed, then ≈_{F} is the largest congruence on D contained in ∼_{F} (i.e. f ≈_{F} g if and only if for all U,V in ob(D), ([U, f] × V) ∼_{f} ([U, g] × V)).

The implementation is valid if and only if all equations x : X ⊢ e = e′ : Y hold up to contextual equivalence, i.e., M{e} ≈_{F} M{e′}, or equivalently, the quotient D ⟶ D/ ≈_{F} factors through D ⟶ D/ ≈_{E}. The only function of the equational theory is to restrict the notion of implementation. It has no effect on when two implementations are equivalent, and so now plays no further role in the story: it just, so to speak, comes along for the ride.

Definition 5. Suppose i : C ⟶ D is an injective-on-objects cartesian closed functor between cartesian-closed categories, and E is a set of parallel pairs of morphisms in D (which we view as the equations of an abstract type system), then an implementation F of (D, E) in C is a cartesian closed functor F : D ⟶ C, such that F · i = id_{C}, and for all (f, g) ∈ E, F (f) ≈_{F} F (g).

We now observe some properties of ≈_{F} that will help us to make precise what we mean by two implementations being equivalent.

Proposition 3. Let F : D ⟶ C be a cartesian closed functor such that F · i = id_{C}. Then the following hold of ≈_{F}:

1. for all f, g : X ⟶ Y in D, if F f ≈ F g, then f ≈_{F} g.

2. for all f, g : X ⟶ Y in C, if f ≈ g, then if ≈_{F} ig.

3. for all f, g : iX ⟶ iY in D, we have f ≈_{F} g if and only if F f ≈ F g.

4. for all f, g : iA ⟶ iB in D, where (A, B)ϵObs, we have f ≈_{F} g if and only if F f = F g.

Proof. 1. Suppose F f ≈ F g. Then, given α : iA ⟶ [U, X] × V and β : [U, Y]×V ⟶ iB, we have F (β·([U, f]×V)·α) = F β·([F U, F f]×F V)·F α = F β · ([F U, F g] × F V) · F α = F (β · ([U, g] × V) · α)

2. Suppose f ≈ g. Then, given α : iA ⟶ [U, iX]×V and β : [U, iY]×V ⟶ iB, we have F (β ·([U, if]×V)·α) = F β ·([F U, F if]×F V)·F α = F β ·([F U, f]× F V) · F α = F β · ([F U, g] × F V) · F α = F β · ([F U, F ig] × F V) · F α = F (β · ([U, ig] × V) · α)

3. Suppose f ≈_{F} g. Then, given α : A ⟶ [U, X] × V and β : [U, Y] × V ⟶ B, we have β ·([U, F f]×V)·α = F iβ ·([F iU, F f]×F iV)·F iα = F (iβ ·([iU, f]× iV) · iα) = F (iβ · ([iU, g] × iV) · iα) = F iβ · ([F iU, F g] × F iV) · F iα = β · ([U, F g] × V) · α. The converse has already been shown.

4. F f ≈ F g if and only if F f = F g for observable types.

Armed with these observations about the interaction of the definitions of ≈ and ≈_{F}, we can now establish relationships between a pair of interpretations F and G, where we understand an interpretation to be defined to be a functor F : D ⟶ C such that F · i = id_{C}.

Proposition 4. Let F, G : D ⟶ C be two interpretations. Then, the following are equivalent:

1. F and G induce the same equivalence: ≈_{F} = ≈_{G}

2. F and G induce the same equivalence on observable operations: ≈_{F} |_{iObs} = ≈_{G} |_{iObs}.

3. the interpretations of operations between pre-existing types are contextually equivalent: for all f : iX ⟶ iY, we have F f ≈ Gf.

4. the interpretations of observable operations are contextually equivalent (in fact, equal): for all f : iA ⟶ iB where (A, B)ϵObs, we have F f ≈ Gf.

Proof. 1 ⇒ 2 and 3 ⇒ 4 are immediate.

2 ⇒ 1. Suppose f ≈_{F} g : X ⟶ Y, and we have α : iA ⟶ [U, X] × V and β : [U, Y]×V ⟶ iB. Then F (β·([U, f]×V)·α) = F (β·([U, g]×V)·α). But these are between observable types, hence by Proposition 3(4), we have β · ([U, f] × V)·α ≈_{F} β ·([U, g]×V)·α. So β ·([U, f]×V)·α ≈_{G} β ·([U, g]×V)·α; and hence by Proposition 3(4) again, we have G(β · ([U, f] × V) · α) = G(β · ([U, g] × V) · α).

1 ⇒ 3. Given f : iX ⟶ iY, we have F f = F iF f, so by Proposition 3(1), we have f ≈_{F} iF f. So f ≈_{G} iF f, and hence by Proposition 3(3), we have Gf ≈ GiF f = F f.

4 ⇒ 2. Given f, g : iA ⟶ iB where (A, B)ϵObs, suppose f ≈_{F} g. Then F f = F g. But by hypothesis, F f = Gf, and F g = Gg, so Gf = Gg. Hence f ≈_{G} g.

Any of the above conditions would be a reasonable definition of equivalence of implementation. So the proposition conveniently justifies the following.

Definition 6. Two interpretations F, G : D ⟶ C are equivalent if they satisfy the equivalent conditions of Proposition 4.

Example 3. 1. Suppose F and G correspond to two implementations of stack, in both of which the underlying type of stack is the product of an unbounded array of integers (giving the stack), and a non-negative integer (giving the top pointer). In F, pop is implemented by decrementing the top pointer, and leaving the stack unchanged. In G, the top pointer is decremented, and the cell popped is set to zero in the array. F and G are otherwise identical. Then F and G are equivalent implementations.

2. It is not necessary for the underlying types to be the same in the two implementations, if F is the array implementation of stack mentioned above, and G is a list implementation, then F and G will be equivalent exactly when they agree about top(empty) and pop(empty).

4 Logical relations

In [8], Ma and Reynolds began by analysing the classical theory of logical relations for simple types. They focussed on the structure needed to prove the fundamental theorem. For binary relations, this amounts to a cartesian closed category B equipped with a cartesian closed functor p = (p_{0}, p_{1}) : B ⟶ C × C, and that cartesian closed functor is typically a fibration [3]. In their theory, B is constructed concretely as a category of relations, and so comes with a standard diagonal Δ : C ⟶ B. This is also a cartesian closed functor.

For instance, consider C being the category Set. Then an object of B consists of a pair (X, Y) of sets together with a subset R of X × Y. The diagonal Δ : C ⟶ B is indeed the diagonal in the usual sense, taking a set X to the subset {(x, x)|x ∈ X} of X × X.

The significance of the fact that B has and all the functors preserve cartesian closed structure, together with the fact that p = (p_{0}, p_{1}) : B ⟶ C × C is a fibration, is that logical relations can be defined on base types, and then extended inductively on the syntax of type expressions as usual. See [3] for a careful analysis of this. Technically, we do not need this much structure for soundness, but having it gives a stronger completeness result and a better link in to logics for reasoning about the type systems. So we take this structure as a characterisation of logical relations, but since our categories are more abstract than those of Ma and Reynolds, we require an abstract characterisation of the diagonal. Moreover, we would like the diagonal to characterise contextual equivalence, not equality.

In the standard relational setting, when R ⊆ X_{0}×X_{1} and S ⊆ Y_{0}×Y_{1}, a map in B from R to S is exactly a pair of maps f_{0} : X_{0} ⟶ Y_{0} and f_{1} : X_{1} ⟶ Y_{1}, such that f_{0} × f_{1} maps R into S, i.e. a pair of maps which respects the relations R and S. In our more abstract setting it is not necessarily true that a map in B is given by a pair of maps in C, and so we shall regard a pair of maps (f_{0}, f_{1}) as respecting the “relations” R and S exactly when there is a map f : R ⟶ S such that p_{0}(f) = f_{0} and p_{1}(f) = f_{1}. This enables us to pick out the essential property we need of the diagonal functor: that if two maps preserve diagonals, then they are contextually equivalent.

Definition 7. Let p = (p_{0}, p_{1}) : B ⟶ C × C be a cartesian closed functor, and let D : C ⟶ B be a cartesian closed functor such that p · D = Δ : C ⟶ C × C. Then we say D is diagonal if, for all f : DX ⟶ DY, it follows that p_{0}f ≈ p_{1}f.

For a formal definition and exposition of the notion of fibration, one may see Claudio Hermida’s thesis [3], half of which is about the relationship between logical relations and fibrations. The idea is that a fibration with structure, in particular cartesian closed structure, provides a category theoretic equivalent to having a predicate logic with which one can build logical relations. Formally, the definition is as follows.

Definition 8. A functor p : P ⟶ C is called a fibration if for every object X of P and every map of the form g : A ⟶ pX in C, there is an arrow g_{X}^{∗} : g^{∗}(X) ⟶ X in P such that p(g^{∗}(X)) = A and p(g^{∗_{X}}) = g, and the following universal property is satisfied:

for every arrow f : Z ⟶ X and every arrow h : pZ ⟶ p(g^{∗}(X)) such that g · h = p(f), there exists a unique arrow k : Z ⟶ g^{∗}(X) such that p(k) = h and g_{X}^{∗} · k = f.

Example 4. We recast our major example of binary relations as follows. C is Set× Set. The objects of P are binary predicates (formally, a pair of sets (X_{0}, X_{1}), together with a predicate R(x_{0}, x_{1}) on them). A morphism from (X_{0}, X_{1}, R(x_{0}, x_{1})) to (Y_{0}, Y_{1}, S(y_{0}, y_{1})) is a pair of functions (f_{0}, f_{1}), such that

⊧ ∀x_{0}, x_{1}. R(x_{0}, x_{1}) ⇒ S(f_{0}(x_{0}), f_{1}(x_{1}))

If X = (X_{0}, X_{1}, R(x_{0}, x_{1})), and g = (g_{0} : Z_{0} ⟶ X_{0}, g_{1} : Z_{1} ⟶ X_{1}), then g^{∗}(X) = (Z_{0}, Z_{1}, R(g_{0}(z_{0}), g_{1}(z_{1}))).

Definition 9. F and G are linked by a logical relation if there is a cartesian closed category B and a cartesian closed fibration p : B ⟶ C × C together with a cartesian closed functor L : D ⟶ B lying over (F, G) (i.e. p_{0} · L = F and p_{1} · L = G) such that D = L · i is diagonal.

B

[figure: L]

[figure: C; i; D; (F, G); C × C; p = (p_{0}, p_{1})]

We can now immediately prove the soundness of this form of logical relation for proving equivalence of implementations.

Proposition 5. If F and G are two implementations which are linked by a logical relation, L, then F and G are equivalent.

Completeness involves a variant of Jung and Tiuryn’s Kripke logical relations of varying arity.

5 Jung-Tiuryn’s logical relations of varying arity

In this section, we outline how we prove the completeness part of our main result. Given equivalent interpretations F, G : D ⟶ C, we seek a cartesian closed fibration p : B ⟶ C × C and a cartesian closed functor from D to B. Our construction is motivated by Jung and Tiuryn’s construction of Kripke logical relations of varying arity [5], though it corresponds to a variant and not their precise construction. (It is possible to prove the result we want in a way that corresponds precisely to theirs. The construction is, however, less compact and less obviously generalisable.)

First, Jung and Tiuryn’s choice of name is questionable. Their paper is concerned with definability in the simple type hierarchy. Definability is a unary predicate, and there is a precise sense in which the relations they define are, despite appearances to the contrary, unary relations. We try to explain this viewpoint below giving first an informal motivational account, and then an account of the machinery which can be used to make the presentation rigorous. Our informal account will confuse terms and their semantics.

Jung and Tiuryn’s work can be reconstructed as follows. We want to provide an invariance property of the lambda definable functions. We hope this can be expressed by a logical relation. In other words, we hope that the set of λdefinable functions is a unary logical relation. Unfortunately in the standard picture, it is not. This is because in the standard theory we can only talk about the elements of the sets which are carriers (closed terms), and there are plenty of functions which send definable elements to definable elements, but are not themselves definable. One way of looking at Jung and Tiuryn’s achievement is that they found a clever way of talking about open terms. This allows us to take our operation and apply it to the definable open term “x”. If the result is definable, by e say, then the operation must have been definable by λx.e.

In Jung and Tiuryn’s account the open terms appear semantically, and stratified by context. That is to say we are given a signature of (typed) variables which may appear in the operation, and the term (say of type D) appears as a function from the set of environments for that signature to D. Instead of viewing this as a function, Jung and Tiuryn view it as a tuple whose components are indexed by environments, and hence as an element of a relation on D whose arity is the set of environments. In order that a property of an open term remains true when we enlarge the environment, Jung and Tiuryn use a Kripke structure in which the worlds are the possible signatures. This means that from their perspective, what they have is a relation which is always on the set D, but whose arity varies as we move between worlds. However, another way of looking at the same structure is that the relation is always unary, but that the set on which is a relation is the set of terms definable at that world, and hence varies from world to world.

The standard way to obtain logical relations is to take a semantics in Set, and to use subsets. A theme of this paper is that this can equally well be regarded as using the standard logic of Set. This can be varied by using other categories and other logics. The technical tool we use for doing this is to interpret a logic as a fibration with structure. If the logic admits ⊤, ∧, → and ∀, as well as substitution, then it yields a category of logical relations. The observation that these operations are all that is required to define product and exponential of logical relations should make that immediately credible, even it does not furnish a proof. These two approaches meet in the standard logic of predicates interpreted as subobjects.

In standard Kripke logical relations for the simple type hierarchy, we are given an indexing category W. The types of the hierarchy are interpreted as constant functors in the presheaf topos [W^{op}, Set], so (Δd)w = d. Kripke logical relations are derived from the natural logic of the topos, that is predicates correspond to subfunctors (a subfunctor of F is a functor G such that at each world w, Gw ⊆ F w). For connected W, the functor Δ : Set ⟶ [W^{op}, Set] is a full and faithful cartesian closed functor. This means that the simple type hierarchy on d in Set is sent by Δ to the simple type hierarchy on Δd in [W^{op}, Set]. So we can either regard this construction as the form of logical relations obtained from a standard logic for a non-standard set in non-standard set theory, or we can regard it as a non-standard logic for a standard set in standard set theory. The Jung-Tiuryn construction resolves this in favour of the second.

In the Jung-Tiuryn construction, W is assumed to be a concrete category, i.e., a category of sets and functions. So they have a functor J : W ⟶ Set, which they assume to be faithful (although never using that), and essentially what they do is replace the functor Δ : Set ⟶ [W^{op}, Set] above by the functor J̃: Set ⟶ [W^{op}, Set], sending d to the functor Set[J−, d].

We make two minor modifications of this. First we start with a functor, F : D ⟶ C. We turn it around to obtain the functor F̃ : C ⟶ [D^{op}, Set] sending X to the functor C(F −, X) : D^{op} ⟶ Set. We get unary logical relations by considering the subobject fibration over [D^{op}, Set] (the standard logic there), and we can take the pullback of that cartesian closed fibration along F̃ to obtain a cartesian closed fibration over C (a non-standard logic). This involves some delicacy. Although the functor F is cartesian closed, it does not follow that F̃ is cartesian closed. But F̃ does preserve finite products, which is sufficient for the results we seek.

Next we take a slightly unexpected binary version of this. It would be normal, given a functor K : C ⟶ [D^{op}, Set] to consider the pullback of a fibration over [D^{op}, Set] × [D^{op}, Set] along K × K. But that is not what we propose. We have functors F̃, G̃ : C ⟶ [D^{op}, Set] and we shall take the pullback along F̃ × G̃. We do obtain the result we seek, but this is a most unusual construction. For instance, there seems no way to lift F̃ ×G̃ to a functor from the binary subobject fibration Sub_{2}(C) over C × C to the binary subobject fibration Sub_{2}([D^{op}, Set]) over [D^{op}, Set] × [D^{op}, Set], but that is a fundamental construction of fibrations, simply not one we need here.

Finally, one needs a little caution. Ideally, we would like the construction of our cartesian closed fibration p : B ⟶ C × C to be independent of the choice of F and G, with F and G only being required in order to construct L : D ⟶ B. But we cannot see how to do that: that is a particular sense in which we see the relationship with Jung and Tiuryn’s work, as they have an extra parameter J : X ⟶ Set in their work too, and it was that extra parameter that inspired us.

6 Completeness of logical relations

In this section, we consider the completeness half of the result we seek. So, given a pair F, G : D ⟶ C of equivalent interpretations, we seek a cartesian closed fibration p : B ⟶ C × C and a cartesian closed functor L : D ⟶ B lying over (F, G) such that the composite L · i is diagonal.

B

[figure: L]

[figure: C; i; D; (F, G); C × C; p = (p_{0}, p_{1})]

As mentioned in the previous section, given an arbitrary functor F : D ⟶ C, we consider the functor H̃ : C ⟶ [D^{op}, Set] that sends an object X of C to the functor C(F −, X) : D^{op} ⟶ Set. It follows from the Yoneda lemma that we have

Proposition 6. For any F : D ⟶ C, if C has finite products, then the functor F̃ : C ⟶ [D^{op}, Set] preserves finite products.

Also, as a standard example of a fibration [3], we have

Example 5. Let C be any category with finite limits. Let Sub_{2}(C) have objects (X, Y, R → X × Y) consisting of a pair (X, Y) of objects of C together with a subobject R of X × Y, and with the evident arrows. Then the forgetful functor Sub_{2}(C) ⟶ C × C is a fibration. If C is cartesian closed, the fibration is a cartesian closed fibration. It is the standard fibration of binary predicates for C.

Proposition 7. Given categories C and C′ with finite products, a finite product preserving functor K : C′ ⟶ C, and a finite product preserving fibration p : P ⟶ C, then the pullback K^{∗}(P) of p along K gives a finite product preserving fibration K^{∗}(P) over C′.

A proof of this result appears in Hermida’s thesis [3], but it can also be verified by direct calculation.

Corollary 1. Given F, G : D ⟶ C where C has finite products, the pullback of Sub_{2}[D^{op}, Set] along F̃ × G̃ gives a finite product preserving fibration (F̃ × G̃)^{∗}(Sub_{2}[D^{op}, Set]) over C × C.

In fact, the fibration (F̃ × G̃)^{∗}(Sub_{2}[D^{op}, Set]) is the one we want, so we shall duly denote it by B. This is essentially a sconing of the ordinary binary subobject fibration on the presheaf category [D^{op}, Set]. It is easy to prove by direct calculation, using some pullbacks in the presheaf category, that we have

Theorem 1. Given F, G : D ⟶ C, supposing C is cartesian closed, then B = (F̃ × G̃)^{∗}(Sub_{2}[D^{op}, Set]) is a cartesian closed fibration over C × C.

Proof. The only point here that requires checking is that B is cartesian closed and that the functor to C × C preserves the cartesian closed structure. This follows from a careful analysis of what the objects of B are. Given an object (X, X′) of C ×C, an object of B over (X, X′) is a subfunctor of C(F −, X)×C(G−, X′). Using cartesian closedness of Sub_{2}([D^{op}, Set] over [D^{op}, Set] × [D^{op}, Set], given subfunctors of C(F −, X) × C(G−, X′) and C(F −, Y) × C(G−, Y′), one can construct a subfunctor of the exponential [C(F −, X) × C(G−, X′), C(F −, Y) × C(G−, Y′)]. Finally, taking the pullback of that subfunctor along the canonical comparison map from C(F −, [X, Y]) × C(F −, [X′, Y′]) to [C(F −, X) × C(G−, X′), C(F −, Y) × C(G−, Y′)] gives the exponential in B that we seek.

This is a specific example of a general construction [3]. Now we have the data we require in order to state and prove our main result.

Theorem 2. If F and G are equivalent interpretations, they are linked by a logical relation.

Proof. Define B as in Theorem 1. It remains to define L : D ⟶ B over (F, G), prove it is cartesian closed, and prove that L · i is diagonal. So for an object d of D, define Ld to be the subfunctor of C(F −, F d) × C(G−, Gd) given by

Ld(c) = {(g : F c ⟶ F d, h : Gc ⟶ Gd) | ∃f : c ⟶ d. F f ≈ g ∧ Gf ≈ h}

It is routine to verify that L preserves finite products; it takes considerably greater but still routine effort to verify that it preserves cartesian closed structure. It follows directly from the definition and the fact that F and G are equivalent that L · i is diagonal.

Combining this completeness result with the soundness result of the previous section, we have a combined soundness and completeness result as follows.

Theorem 3. Two interpretations F and G are equivalent if and only if they are linked by a logical relation.

References

1. Alimohamed, A.: A Characterisation of Lambda Definability in Categorical Models of Implicit Polymorphism. Theoretical Computer Science 146 (1995) 5–23.

2. Fiore, M., Plotkin, G.D.: An axiomatisation of computationally adequate domain-theoretic models of F P C. Proc LICS 94. IEEE Press (1994) 92– 102.

3. Hermida, C.A.: Fibrations, Logical Predicates and Indeterminates. Ph.D. thesis. Edinburgh (1993) available as ECS-LFCS-93-277.

4. Honsell, F., Sannella, D.T.: Pre-logical relations. Proc. CSL 99. LNCS 1683. Flum and Rodriguez-Artalejo (eds.) Springer (1999) 546–562.

5. Jung, A., Tiuryn, J.: A new characterisation of lambda definability. Proc. TLCA. LNCS 664. Bezem and Groote (eds.) Springer (1993) 245–257.

6. Kinoshita, Y., O’Hearn, P., Power, A.J., Takeyama, M., Tennent, R.D.: An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement. Proc TACS 97. LNCS 1281. Abadi and Ito (eds.) Springer (1997) 191–212.

7. Lambek, J., Scott, P.J.: Introduction to higher order categorical logic. Cambridge studies in advanced mathematics. Cambridge University Press (1986)

8. Ma, Q., Reynolds, J.C.: Types, abstraction and parametric polymorphism 2. Math. Found. of Prog. Lang. Sem. Lecture Notes in Computer Science. Springer (1991).

9. Mitchell, J.:Type systems for programming languages. Handbook of Theoretical Computer Science em B. van Leeuwen (ed). North-Holland (1990) 365–458.

10. Mitchell, J.: Foundations for programming languages. Foundations of Computing Series. MIT Press (1996).

11. Moggi, E.: Computational Lambda-calculus and Monads. Proc LICS 89. IEEE Press (1989) 14–23.

12. Plotkin, G.D., Power, A.J., Sannella, D.T., Tennent, R.D.: Lax logical relations. (to appear in ICALP 2000).

13. Reynolds, J.C.: Types, abstraction, and parametric polymorphism. Information Processing 83 Mason (ed) North Holland (1983) 513–523.

14. Tennent, R.D.: Correctness of data representations in ALGOL-like languages. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, A.W. Roscoe (ed.) Prentice-Hall (1994) 405–417.