Lax Logical Relations

Gordon Plotkin^{1}^{}, John Power^{1}^{}, Donald Sannella^{1}^{}, and Robert Tennent^{1 2}^{}

1 Laboratory for Foundations of Computer Science University of Edinburgh, Edinburgh, U.K. EH9 3JZ

                  gdp,ajp,dts @dcs.ed.ac.uk

2 Department of Computing and Information Science Queen’s University, Kingston, Canada K7L 3N6

                      rdt@cs.queensu.ca

Abstract. Lax logical relations are a categorical generalisation of logical relations; though they preserve product types, they need not preserve exponential types. But, like logical relations, they are preserved by the meanings of all lambda-calculus terms. We show that lax logical relations coincide with the correspondences of Schoett, the algebraic relations of Mitchell and the pre-logical relations of Honsell and Sannella on Henkin models, but also generalise naturally to models in cartesian closed categories and to richer languages.

1 Introduction

Logical relations and various generalisations are used extensively in the study of typed lambda calculi, and have many applications, including

characterising lambda definability [Pl73, Pl80, JT93, Al95]; relating denotational semantic definitions [Re74, MS76]; characterising parametric polymorphism [Re83]; modelling abstract interpretation [Ab90]; verifying data representations [Mi91]; defining fully abstract semantics [OR95]; and modelling local state in higher-order languages [OT95, St96].

The two key properties of logical relations are

1. the so-called Basic Lemma: a logical relation is preserved by the meaning of every lambda term; and

2. inductive definition: the type-indexed family of relations is determined by the base-type components.

This author was supported by EPSRC grants GR/J84205 and GR/M56333. This author was supported by EPSRC grants GR/J84205 and GR/M56333, and by a

grant from the British Council. This author was supported by EPSRC grant GR/K63795.

This author was supported by a grant from the Natural Sciences and Engineering Research Council of Canada.

It has long been known that there are type-indexed families of conventional relations that satisfy the Basic Lemma but are not determined inductively in a straightforward way. Schoett [Sc87] uses families of relations that are preserved by algebraic operations to treat behavioural inclusion and equivalence of algebraic data types; he terms them “correspondences,” but they have also been called “simulations” [Mi71] and “weak homomorphisms” [Gi68]. Furthermore, Schoett conjectures (pages 280–81) that the Basic Lemma will hold when appropriate correspondences are used between models of lambda calculi, and that such relations compose. Mitchell [Mi90, Sect. 3.6.2] terms them “algebraic relations,” attributing the suggestion to Gordon Plotkin^{1} and Samson Abramsky, independently, and asserts that the Basic Lemma is easily proved and (binary) algebraic relations compose. But Mitchell concludes that, because logical relations are easily constructed by induction on types, they “seem to be the important special case for proving properties of typed lambda calculi.”

Recently, Honsell and Sannella [HS99] have shown that such relation families, which they term “pre-logical relations,” are both the largest class of conventional relations on Henkin models that satisfy the Basic Lemma, and the smallest class that both includes logical relations and is closed under composition. They give a number of examples and applications, and study their closure properties.

We briefly sketch two of their applications.

The composite of (binary) logical relations need not be logical. It is an easy exercise to construct a counter-example; see, for instance, [HS99]. But the composite of binary pre-logical relations is a pre-logical relation.

Mitchell [Mi91] showed that the use of logical relations to verify data representations in typed lambda calculi is complete, provided that all of the primitive functions are first-order. In [HS99], this is strengthened to allow for higher-order primitives by generalising to pre-logical relations. Honsell, Longley et al. [HL^{+} ] give an example in which a pre-logical relation is used to justify the correctness of a data representation that cannot be justified using a conventional logical relation.

In this work, we give a categorical characterisation of algebraic relations (simulations, correspondences) between Henkin models of typed lambda calculi. The key advantage of this characterisation is its generality. By using it, one can immediately generalise from Henkin models to models in categories very different from Set, and to languages very different from the simply typed lambda calculus, for example to languages with co-products or tensor products, or to imperative languages without higher-order constructs.

The paper is organised as follows. In Sect. 2, we recall the definition of logical relation and a category theoretic formulation. In Sect. 3, we give our categorical notion of lax logical relation, proving a Basic Lemma, with a converse. In Sect. 4, we explain the relationship with pre-logical relations and in Sect. 5 give

1 Plotkin recalls that the suggestion was made to him by Eugenio Moggi in a conversation.

another syntax-based characterisation. In Sect. 6 we consider models in cartesian closed categories. In Sect. 7, we generalise our analysis to richer languages.

2 Logical Relations

Let be a signature of basic types and constants for the simply typed -calculus with products [Mi90], generating a language . We use and to range over types in . We denote the set of functions from a set to a set by [ ].

Definition 2.1. A model of in Setconsists of

for each , a set _{}, such that _{}= [ _{}_{}], _{}= _{}_{}, and

1 = ; for each constant of of type , an element ( ) of _{}.

A model extends inductively to send every judgement : of to a function ( : ) from _{}to _{}, where _{}is the evident finite product in Set. These are “full” type hierarchies; larger classes of models, such as Henkin models and cartesian closed categories, will be discussed later.

Definition 2.2. Given a signature and two models, and , of the language generated by , a (binary) logical relation from to consists of, for each type of , a relation _{}_{}_{}such that

for all  _{}and  _{}, we have _{}if and only if for all  _{}

and _{}, if _{}then ( ) _{}( ); for all ( _{0} _{1}) _{}and ( _{0} _{1}) _{}, we have ( _{0} _{1}) _{}( _{0} _{1}) if

and only if _{0} _{}_{0} and _{1} _{}_{1}; 1 ; ( ) _{}( ) for every constant in of type .

The data for a binary logical relation are therefore completely determined by its behaviour on base types. The fundamental result about logical relations underlying all of their applications is the following.

Lemma 2.3 (Basic Lemma for Logical Relations). Let be a binary logical relation from to ; for any term : of in context , if _{}, then

(  : ) _{}(  : )  ,

where _{}is an abbreviation for _{}_{_{}}_{}for all where _{1} _{}is the sequence of types in . It is routine to define -ary logical relations for an arbitrary natural number , in the spirit of Definition 2.2. The corresponding formulation of the Basic Lemma holds for arbitrary too.

We now outline a categorical formulation of logical relations [MR91, MS92]; this will be relaxed slightly to yield our semantic characterisation of algebraic relations for typed lambda calculi with products.

The language determines a cartesian closed term category, which we also denote by , such that a model of the language in any cartesian closed category such as Set extends uniquely to a cartesian closed functor from to Set [Mi96, Sect. 7.2.6]; i.e., a functor that preserves products and exponentials strictly (not just up to isomorphism). We may therefore identify the notion of model of the language in Setwith that of a cartesian closed functor from to Set.

Definition 2.4. The category Rel_{2} is defined as follows: an object ( ) consists

of a pair of sets and , and a binary relation  ; a map from (  )
to ( ^{}^{}^{}) is a pair of functions ( :  ^{}:  ^{}) such that  implies

( ) ^{}( ):

[figure: ; ^{}; ; ^{}; ; ^{}; ; ]

Composition is given by ordinary composition of functions.

We denote the forgetful functors from Rel_{2} to Setsending ( ) to or to by _{0} and _{1}, respectively.

Proposition 2.5. Rel_{2} is cartesian closed, and the cartesian closed structure is strictly preserved by the functor ( _{0} _{1}): Rel_{2} Set Set .

For example, ( _{0}  _{0}) ( _{1}  _{1}) is ([ _{0}  _{1}] (  ) [ _{0}  _{1}])
where ( ) iff, for all  _{0} and  _{0}, implies ( ) ( ).

These properties of Rel_{2}, combined with the fact that is freely generated by a signature for cartesian closed categories (i.e., is the generic model on a suitable sketch [KO^{+} 97]), are the key to understanding logical relations categorically, as shown by the following.

Proposition 2.6. To give a binary logical relation from to is equivalent to giving a cartesian closed functor : Rel_{2} such that ( _{0} _{1}) = ( ):

[figure: ; Set Set; Rel_{2}; ( ); ( _{0} _{1}); ]

Proof. Given a binary logical relation, one immediately has the object function of : Rel_{2}. The equation ( _{0} _{1}) = ( ) determines the behaviour of on arrows. The fact that, for any term of type in context , the pair ( : ) ( : ) satisfies the condition making it an arrow in Rel_{2} from _{}to _{}follows from (and is equivalent to) the Basic Lemma.

The converse construction is given by taking the object part of a cartesian closed functor : Rel_{2}. It is routine to verify that the two constructions are mutually inverse.

This situation generalises to categories other than and Rel_{2}, the central point being that both categories are cartesian closed and ( _{0} _{1}) is a cartesian closed functor. We outline the following important example which arises in domain theory to deal with logical relations in the context of least fixed points. Let be the category of -cpos with and continuous maps, and be the class of admissible monos; then there is an evident cartesian closed functor from 2( ), the category of admissible binary relations between cpos, to . A logical relation in this framework is then a cartesian closed functor from to 2( ) (coherent with appropriate models of in ).

Obviously, one can define a category Rel_{}of -ary relations for an arbitrary natural number ; Propositions 2.5 and 2.6 generalise routinely to arbitrary .

3 Lax Logical Relations

In this section, we generalise the categorical notion of logical relation to what we call a lax logical relation.

Definition 3.1. Given a signature and the language generated by , and two models and of in Set, a (binary) lax logical relation from to is a functor : Rel_{2} that strictly preserves finite products and satisfies ( _{0} _{1}) = ( ).

Note that exponentials are not necessarily preserved. Evidently, one can adapt this definition to one for -ary lax logical relations for arbitrary .

The origin of our terminology is as follows. Any finite-product preserving functor : between cartesian closed categories induces a family of lax maps App_{}: _{}[ _{}_{}] obtained by taking the Currying in of the composites

( ) _{}

where the first map is determined by preservation of finite products, and the second map is obtained by applying to the evaluation map in . This is an instance of (op)lax preservation of structure, specifically, exponential structure.

The notion of Henkin model is closely related to this definition. A Henkin model of the simply typed -calculus is a finite-product preserving functor from to Set such that the induced lax maps are injective. This is a kind of lax model, but is not quite the same as giving a unary lax logical relation; nevertheless, it is a natural and useful generalisation of the notion of model we have used, and one to which our results routinely extend.

The Basic Lemma for logical relations extends to lax logical relations; in fact, the lax logical relations can be characterised in terms of a Basic Lemma.

Lemma 3.2 (Basic Lemma for Lax Logical Relations). Let and be models of in Set. A family of relations _{}_{}_{}for every type of determines a lax logical relation from to if and only if, for every term : of in context , if

, then (  : ) _{}(  : ) ,

where _{}is an abbreviation for _{}_{_{}}_{}for all when _{1} _{}is the sequence of types in .

Proof. For the forward (only-if) direction, suppose has sequence of types 1 _{}. The expression : is a map in from _{1} _{}to , so sends it to the unique map from _{_{1} _{}}to _{}in Rel_{2} that lifts the pair

(  : ) (  : ) :

[figure: ( _{1}  _{}); ( ); ( _{1}  _{}); ( ); _{_{1}  _{}}; _{}; (  : ); (  : )]
If _{}_{_{}}_{}for all then ( _{1}  _{}) _{_{1}  _{}}( _{1}  _{}) because preserves
finite products, and so the result is now immediate, as  ( _{1}  _{}) =
( _{1}  _{}) ( _{1})  ( _{}) and similarly for .

For the converse, first taking to be a singleton, the condition uniquely determines maps ( : ): ( ) ( ) in Rel_{2}, giving a graph morphism from to Setsuch that ( _{0} _{1}) = ( ). Such a graph morphism is trivially necessarily a functor. Taking : to be : 1, where is the unique constant of type 1, the condition yields _{1} , so preserves the terminal object. Taking : to be : _{0} : _{1} ( ): _{0} _{1} yields that if _{0} _{_{0}} _{0} and 1 _{_{1}} _{1}, then ( _{0} _{1}) _{_{0} _{1}} ( _{0} _{1}). And taking : to be : _{0} _{1} : _{}for = 0 1 give the converse. So preserves finite products.

We conclude this section by showing how lax logical relations can be used for the two applications of [HS99] previously discussed.

Definition 3.3. If is a type-indexed family of binary relations from to and is a type-indexed family of binary relations from to , their composite ; is defined component-wise; i.e., ( ; )_{}= _{}; _{}

where ; on the right-hand side denotes the conventional composition of binary relations.

Proposition 3.4. If is a binary lax logical relation from to and is a binary lax logical relation from to , then ; is a lax logical relation from to .

Proof. We must show that if : Rel_{2} and : Rel_{2} strictly preserve finite products, then so does ; . But ( _{0} _{1}) ( ; )_{}( _{0} _{1}) if and only if there exists ( _{0} _{1}) such that ( _{0} _{1}) _{}( _{0} _{1}) and ( _{0} _{1}) _{}( _{0} _{1}), and that is so if and only if _{0} ( ; )_{}_{0} and _{1} ( ; )_{}_{1}. The proof for a terminal object is trivial.

Various other closure properties (such as closure with respect to conjunction and universal and existential quantification) have been proved in [HS99] for pre-logical relations; the results in the following section show that lax logical relations also have these closure properties.

Definition 3.5. Let and be models of in Set, and OBSbe a set of types; then and are said to be observationally equivalent with respect to OBS (written OBS ) when, for all OBSand all closed ^{}: , ( ) = ( ^{}) if and only if ( ) = ( ^{}).

Proposition 3.6. _{OBS} if and only if there exists a lax logical relation from to which is one-to-one for every OBS.

Proof. For the forward direction, consider the family of relations _{}_{}_{} defined by _{}if and only if there exists a closed term : such that ( ) = and ( ) = . This is one-to-one on observable types because of observational equivalence and a lax logical relation because _{}= _{}_{}.

For the converse, suppose _{}_{}_{}determine a lax logical relation; if OBSthen, for all closed : , ( ) _{}( ) by the Basic Lemma and ( ) = ( ^{}) if and only if ( ) = ( ^{}) because _{}is one-to-one.

4 Pre-logical Relations

We can use the Basic Lemma of Sect. 3 and the corresponding result of [HS99] to see immediately that, for models as we defined them in Sect. 2, the notions of lax logical relation and pre-logical relation coincide. However, in this section we give a more direct exposition of the connection for a larger class of models. In [HS99], the analysis is primarily in terms of the simply typed -calculus without product types. But they mention the case of -calculi with products and models that satisfy surjective pairing. Hence, consider models now to be functors : Set that strictly preserve finite products (but not necessarily exponentials); these include Henkin models. Everything we have said about lax logical relations extends routinely to this class of models.

Definition 4.1. A pre-logical relation from to consists of, for each type , a relation _{}_{}_{}such that

1. if _{}and _{}, then App_{}_{}App_{}, where maps App_{}are determined by finite-product preservation of and , respectively, as discussed in Sect. 3;

2. ( ) _{}( ) for every constant of type , where the constants are deemed to include all constants in , : 1, ( ): ( ),

0 :  and _{1} :  , and
all instances of combinators _{}: (  ) ( )  and

: .

Theorem 4.2. A type-indexed family of relations _{}_{}_{}determines a lax logical relation from to if and only if it is a pre-logical relation from to .

Proof. For the second clause in the forward direction, treat all constants as maps in with domain 1. For the first clause, note that _{}_{}= _{( )} , so applying functoriality of to the evaluation map ev: ( ) in , the result follows immediately.

For the converse, the second condition implies that, for all closed terms , ( ) ( ); that fact, combined with the fact that every map in is an un-Currying of a closed term, plus the first condition, imply that is a graph morphism making ( _{0} _{1}) = ( ), hence trivially a functor. Since : 1 is a constant and ( ) = = ( ), we have ( ) _{1} ( ); so preserves the terminal object. Since ( ) is a constant, it follows that if _{0} _{_{0}} _{0} and _{1} _{_{1}} _{1}, then ( _{0} _{1}) _{_{0} _{1}} ( _{0} _{1}). The inverse holds because _{0} and _{1} are maps in . So preserves finite products.

5 Another Syntax-Based Characterisation

The key point in the pre-logical characterisation above is that every map in the category is generated by the constants. In this section, we give an alternative syntax-based characterisation that generalizes more directly to other languages. For simplicity of exposition, we assume, as previously, that models preserve exponentials as well as products.

Theorem 5.1. To give a lax logical relation from to is equivalent to giving, for each type of , a relation _{}_{}_{}such that

1. if _{( )} , then ( ) _{}( )

2. App _{(( )} App

3. if _{0} _{}_{0} and _{1} _{}_{1}, then ( _{0} _{1}) _{( )} ( _{0} _{1})

4. _{0} _{}_{0} and _{1} _{}_{1}

5. if _{}and ^{}_{}^{}, then ( ^{}) _{}( ^{})

6. _{}

7. _{}if and only if _{1}

8. ( ) _{}( ) for every base term in of type .

We chose the conditions above because the first four conditions seem particularly natural from the perspective of the -calculus, the following two, which are about substitution, are natural category theoretic conditions, the seventh is mundane, and the last evident; cf. the “categorical combinators” of [Cu93].

Proof. For the forward direction, the relations _{}are given by the object part of the functor. The conditions follow immediately from the fact of being a functor, thereby having an action on all maps, and from the fact that it strictly preserves finite products. For instance, there is a map in from ( ) ( ) to ( ), so that map is sent by to a map in Rel_{2}, and strictly preserves finite products, yielding the third condition. So using the definition of a map in Rel_{2}, and the facts that ( _{0} _{1}) = ( ) and that and are strict structure preserving functors, we have the result.

For the converse, the family of relations gives the object part of the functor . Observe that the axioms imply

( _{0} _{1}) _{}( _{0} _{1}) if and only if _{0} _{}_{0} and _{1} _{}_{1} 1 , where is the unique element of _{1} = _{1} = 1 So, strictly preserves finite products providing it forms a functor. The data for and and the desired coherence condition ( _{0} _{1}) = ( ) on the putative functor determine its behaviour on maps. It remains to check that the image of every map in actually lies in Rel_{2}. But the conditions inductively define the Currying of every map in , so unCurrying by the fifth and seventh conditions, the result follows. It is routine to verify that these constructions are mutually inverse.

The result holds for the more general class of models we have discussed, but an exposition would be encumbered by numerous occurrences of App_{}. It is routine to generalise Theorems 4.2 and 5.1 to -ary relations for arbitrary .

6 Models in Cartesian Closed Categories

Cartesian closed categories are a more general class of models for typed lambda calculi. In this section, we consider a model to be a functor from to a cartesian closed category, strictly preserving finite products and exponentials.

To discuss “relations” in this context, we adopt the sub-scone approach described in [La88, MR91, MS92, Al95]. Let be a cartesian closed category, be a finitely complete cartesian closed category, and : be a functor that preserves products (up to isomorphism). A typical example of a suitable functor is hom(1 ): , the global-elements functor; other examples may be found in the references given above. Then these data determine a category

- _{2} of categorical (binary) relations on as follows.

Let Rel_{2}( ) be the category of binary relations on with evident forgetful functor Rel_{2}( ) ; then pulling back along determines a category - _{2} and a forgetful functor to . In detail, the objects of - _{2} are triples ( _{0} _{1}) where _{0} and _{1} are objects of and is a sub-object of ( _{0}) ( _{1}); the morphisms from ( _{0} _{1}) to ( _{0} _{1}) are triples ( _{0} _{1}) such that _{}: _{}_{}in , : dom dom in , and the following diagram commutes:

[figure: ; ; ( _{0}) ( _{1}); ( _{0}) ( _{1}); ; ( _{0}) ( _{1}); ; ]

Composition and identities are evident. The forgetful functors _{}: - _{2} for = 0 1 are defined by _{}( _{0} _{1}) = _{}and similarly for morphisms.

Proposition 6.1. - _{2} is a cartesian closed category and the cartesian closed structure is strictly preserved by ( _{0} _{1}): - _{2} ; furthermore, this functor is faithful.

Definition 6.2. Given a signature and the language generated by , two models and of in a cartesian closed category , and a category - _{2} of binary categorical relations on , a (binary) lax logical relation from to is a functor : - _{2} that satisfies ( _{0} _{1}) = ( ) and strictly preserves finite products.

Lemma 6.3 (Basic Lemma for Categorical Lax Logical Relations). Let and be models of in a cartesian closed category , be a finitely complete cartesian closed category, and : preserve finite products up to isomorphism; then a family of sub-objects _{}:[figure: ; ( _{}) ( _{})] for every type of determines a lax logical relation from to if and only if, for every term of of type in context , there exists a unique map that makes the following diagram commute:

[figure: ; ; ( _{}_{_{}}) ( _{}_{_{}}); ( _{}) ( _{}); . . . . . . .; ; ( )  ( ); _{}_{_{}}; _{}]

where _{1} _{}is the sequence of types in .

Proof. For the forward direction, maps : to a map

[figure: ; ; ( _{_{}_{}}) ( _{_{}_{}}); ( _{}) ( _{}); ; ( )  ( ); _{_{}_{}}; _{}]

The result follows because , and preserve products.

In the converse direction, the morphism part of the functor is determined

by the assumed maps. Taking  : to be : _{0} : _{1} ( ): _{0}  _{1} shows
that _{_{0}}  _{_{1}}  _{_{0} _{1}} , using the fact that , and all preserve products,
and taking  : to be : _{0}  _{1}  _{}: _{}for = 0 1 shows the converse.
Finally, taking  : to be  : 1 shows that _{1} is the “true” sub-object of

( _{1}) ( _{1}). So preserves products.

This result can be generalised: replace - _{2} and ( _{0} _{1}) by any category with finite products and a faithful finite-product preserving functor to . This would amount to a lax version of Peter Freyd’s suggestion [Mi90, Section 3.6.4] of studying logical relations as subcategories that respect cartesianclosed (here, cartesian) structure, except generalised from subcategory to faithful functor. But many applications require entailments to, or from, the “relations,” and so a lax version of Hermida’s [He93] fibrations with structure to support a ( ) logic might be a more appropriate level of generality.

To consider composition of (binary) lax logical relations in this context, assume first that is the usual category of sets and functions; then the objects of

- _{2} are subsets of sets of the form ( ) ( ).

Proposition 6.4. Composition of (binary) categorical lax logical relations can be defined component-wise.

To allow recursion in , consider again the category _{2}( ) discussed at the end of Section 2, with being the category of -cpos with and being the admissible monos. Using the sconing functor = (1 ): Setgives us a category - _{2} as above; because this is constructed as a pullback, there exists a strict finite-product preserving functor from _{2}( ) to - _{2}.

Given any logical relation functor : _{2}( ), composing with gives a strict finite-product preserving functor from to - _{2} (i.e., a lax logical relation) between the original models. This shows how composition is supported in the context of relations on -cpos.

More generally, if is assumed to be a regular category [Bo94], a relational composition can be defined. Any pre-sheaf category Set^{}, or indeed any topos, is a regular category, so this is a mild assumption. An axiomatic treatment of composition of generalized logical relations, including lax logical relations as discussed here, can be found in [KO^{+} 97], which emerged from category theoretic treatments of data refinement in which composition of refinements is crucial [JH90, KP96, KP].

7 Generalising from the -Calculus

In Sect. 3, the fundamental facts that gave rise to our definition of lax logical relation were the correspondence between the simply typed -calculus and cartesian closed categories, and the fact that a signature gave rise to a cartesian closed category such that a model of could be seen as a functor from into Set (or, more generally, any cartesian closed category) that strictly preserved cartesian closed structure. So in generalising from the simply typed -calculus, we generalise the latter fact. This may be done in terms of algebraic structure, or equivalently (finitary) monads, on Cat. The central paper about that is Blackwell, Kelly and Power’s [BKP89]. We can avoid much of the subtlety here by restricting our attention to maps that preserve structure strictly.

We shall first describe the situation for an arbitrary (finitary) monad on Catextending finite-product structure. One requires Set(or, more generally, any small category ) to have -structure, to be the free -algebra generated by a signature, and define a model of to be a strict -algebra map, cf. [KO^{+} 97].

A natural general setting in which to define the notion of lax logical relation involves assuming the existence of a small category (with finite products) of relations, and a strict finite-product preserving forgetful functor ( _{0} _{1}) from to . One then adds to these data further categorical structure inside the category of small categories and functors that strictly preserve finite products to generalise the composition of binary relations. These definitions and related results appear in [KO^{+} 97]. Here, we aim to state a Basic Lemma in familiar terms, and so restrict attention to the special case that = Setand = Rel_{2}.

A lax logical relation is a strict finite-product preserving functor from into Rel_{2} such that composition with ( _{0} _{1}) yields ( ).

We can generalise the Basic Lemma to this level of generality as follows.

Lemma 7.1 (Basic Lemma for Lax Logical Relations with Algebraic Structure). A family of relations _{}_{}_{}for every type of determines a lax logical relation from to if and only if, for every term of of type in context ,

if _{}, then (  : ) _{}(  : )

The proof is exactly as in Sect. 3; similarly, Proposition 7.2. Binary lax logical relations (at the current level of generality) compose component-wise.

In the above we have tacitly assumed that contexts are modelled by finite products. In general, there is no need to make this assumption: contexts could be modelled by a symmetric monoidal structure or, more generally, by a symmetric pre-monoidal structure, or Freyd structure. It would be straightforward to generalise our analysis to include such possibilities, but it may be simpler to deal with them case by case. For an analysis of the notion of lax logical relations where contexts are modelled by a Freyd structure, see [KP99].

We next want to generalise Theorem 5.1. In order to do that, we need to consider the formulation of finitary monads in terms of algebraic structure on Cat, and we need to restrict to a particular class of such structures. The general notion of algebraic structure, and the relevant results, appear in [KP93] and [Po97], and we have included it in the Appendix. Using the notation of the Appendix, we consider a special class of algebraic structure.

Definition 7.3. Algebraic structure ( ) on Catis discrete if ( ) = 0 whenever is not a discrete category, i.e., whenever is not the discrete category on a finite set.

It follows from the definition that any discrete algebraic structure may be presented by two families of operations: object operations, which have algebras given by functors of the form ^{}, and arrow operations, which are given by natural transformations between object operations. One may put equations between these to obtain all operations of any discrete algebraic structure, which are given by functors ^{}^{}, where is a small category.

Assuming Set has ( )-structure for some given discrete algebraic structure ( ), a model of an ( )-algebra in Setis a functor that strictly preserves ( )-structure .

Examples of discrete algebraic structure have models given by small categories with finite products, with finite coproducts, with monoidal structure, symmetric monoidal structure, a monad [Mo91], an endofunctor, a natural transformation between endofunctors, or any combination of the above.

In order to extend Theorem 5.1, rather than give an analogue, we must include exponentials, although they are not instances of discrete algebraic structure as we have defined it. So we henceforth assume that we are given discrete algebraic structure on Catextending finite-product structure; that is generated by the simply typed -calculus, a signature, and the discrete algebraic structure; that and are models of in Setstrictly preserving the algebraic structure, and, restricting our definition above, that a lax logical relation from to is a finite-product preserving functor from to Rel_{2} such that composition with ( _{0} _{1}) yields ( ).

A methodology for extending Theorem 5.1 is as follows. Algebraic structure on is given by an equational presentation. That equational presentation has operations defining objects and arrows. For each operation defining an arrow, one adds an axiom to the list in the statement of Theorem 5.1 in the same spirit. For instance, to define a monoidal structure, one has operations that assign to each pair of maps ( ), a map , and gives associative maps and their inverses, and left and right unit maps and their inverses. So one would add axioms

if _{0} _{_{0} _{0}}  _{0} and _{1} _{_{1} _{1}}  _{1} then ( _{0} _{1}) _{( _{0} _{1}) ( _{0} _{1})} ( _{0} _{1});
( )  ( )  , _{( )} and _{( )} ;
1 _{( ) ( )}  ^{1} , ^{1} _{( )}  ^{1} and ^{1} _{( )}  ^{1} .

Theorem 7.4. For any discrete algebraic structure on Cat extending finite-product structure, to give a lax logical relation from to is equivalent to giving a family of relations _{}_{}_{}satisfying the conditions of Theorem 5.1 and also

for any -ary object operation , if _{}_{_{}_{}}_{}for all 1 , then

( _{1}  _{}) _{( _{1}  _{}) ( _{1}  _{})} ( _{1}  _{})

for any -ary arrow operation , we have

( _{1}  _{}) _{}( _{1}  _{})
where = dom ( _{1}  _{}) cod ( _{1}  _{})

for any -ary arrow operation , if _{}_{_{}_{}}_{}for all 1 , then

dom ( _{1}  _{}) _{}dom ( _{1}  _{})
where = dom ( _{1}  _{}) dom ( _{1}  _{}), and similarly with dom

systematically replaced by cod.

The final two rules here may seem unfamiliar at first sight. An arrow operation takes a -ary family of objects to an arrow, so syntactically, takes a -ary family of types to an equivalence class of terms. That leads to our penultimate rule. That a -ary arrow operation is functorial means that every -ary family of arrows is sent to a commutative square. So we need rules to the effect that every arrow in that square behaves as required. The penultimate rule above accounts for two arrows of the square, and the final rule accounts for the other two, where the domain of the commutative square is the arrow of the square uniquely determined by the definitions.

Proof. Follow the proof of Theorem 5.1. The conditions show inductively that for every arrow of the category freely generated by the given discrete algebraic structure applied to the signature, one obtains an arrow in Rel.

Note that this allows for dropping exponentials, as well as adding various kinds of structure such as finite co-products and tensor products. We hope this generality will lead to interesting new applications.

References

[Ab90] S. Abramsky. Abstract interpretation, logical relations and Kan extensions. J. of Logic and Computation, 1:5–40, 1990.

[Al95] M. Alimohamed. A characterization of lambda definability in categorical models of implicit polymorphism. Theoretical Computer Science, 146:5–23, 1995.

[BKP89] R. Blackwell, H. M. Kelly, and A. J. Power. Two dimensional monad theory. J. of Pure and Applied Algebra, 59:1–41, 1989.

[Bo94] Francis Borceux. Handbook of Categorical Algebra 2, volume 51 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994.

[Cu93] P.-L. Curien. Categorical Combinators, Sequential Algorithms, and Functional Programming. Birkhauser, Boston, 1993.

[FRA99] J. Flum and M. Rodriguez-Artalejo, editors. Computer Science Logic, 13th International Workshop, CSL’99, volume 1683 of Lecture Notes in Computer Science, Madrid, Spain, September 1999. Springer-Verlag, Berlin (1999).

[Gi68] A. Ginzburg. Algebraic Theory of Automata. Academic Press, 1968.

[He93] Claudio A. Hermida. Fibrations, logical predicates, and indeterminates. Ph.D. thesis, The University of Edinburgh, 1993. Available as Computer Science Report CST–103–93 or ECS–LFCS–93–277.

[HL^{+} ] F. Honsell, J. Longley, D. Sannella, and A. Tarlecki. Constructive data refinement in typed lambda calculus. To appear in the Proceedings of FOSSACS 2000, Springer-Verlag Lecture Notes in Computer Science.

[HS99] F. Honsell and D. Sannella. Pre-logical relations. In Flum and Rodriguez-Artalejo [FRA99], pages 546–561.

[JH90] He Jifeng and C. A. R. Hoare. Data refinement in a categorical setting. Technical monograph PRG-90, Oxford University Computing Laboratory, Programming Research Group, Oxford, November 1990.

[JT93] A. Jung and J. Tiuryn. A new characterization of lambda definability. In M. Bezen and J. F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 245–257, Utrecht, The Netherlands, March 1993. Springer-Verlag, Berlin.

[KO^{+} 97] Y. Kinoshita, P. O’Hearn, A. J. Power, M. Takeyama, and R. D. Tennent. An axiomatic approach to binary logical relations with applications to data refinement. In M. Abadi and T. Ito, editors, Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science, pages 191–212, Sendai, Japan, 1997. Springer-Verlag, Berlin.

[KP] Y. Kinoshita and A. J. Power. Data refinement by enrichment of algebraic structure. To appear in Acta Informatica.

[KP93] G. M. Kelly and A. J. Power. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra, 89:163–179, 1993.

[KP96] Y. Kinoshita and A. J. Power. Lax naturality through enrichment. J. Pure and Applied Algebra, 112:53–72, 1996.

[KP99] Y. Kinoshita and J. Power. Data refinement for call-by-value programming languages. In Flum and Rodriguez-Artalejo [FRA99], pages 562–576.

[La88] Y. Lafont. Logiques, Categories et Machines. Thèse de Doctorat, Université de Paris VII, 1988.

[Mi71] R. Milner. An algebraic definition of simulation between programs. In Proceedings of the Second International Joint Conference on Artificial Intelligence, pages 481–489. The British Computer Society, London, 1971. Also Technical Report CS-205, Computer Science Department, Stanford University, February 1971.

[Mi90] J. C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 365–458. Elsevier, Amsterdam, and The MIT Press, Cambridge, Mass., 1990.

[Mi91] J. C. Mitchell. On the equivalence of data representations. In V. Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 305–330. Academic Press, 1991.

[Mi96] J. C. Mitchell. Foundations for Programming Languages. The MIT Press, 1996.

[Mo91] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991.

[MR91] QingMing Ma and J. C. Reynolds. Types, abstraction, and parametric polymorphism, part 2. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Semantics, Proceedings of the 7th International Conference, volume 598 of Lecture Notes in Computer Science, pages 1–40, Pittsburgh, PA, March 1991. Springer-Verlag, Berlin (1992).

[MS76] R. E. Milne and C. Strachey. A Theory of Programming Language Semantics. Chapman and Hall, London, and Wiley, New York, 1976.

[MS92] J. C. Mitchell and A. Scedrov. Notes on sconing and relators. In E. Börger, G. Jäger, H. Kleine Büning, S. Martini, and M. M. Richter, editors, Computer Science Logic: 6th Workshop, CSL ’92: Selected Papers, volume 702 of Lecture Notes in Computer Science, pages 352–378, San Miniato, Italy, 1992. Springer-Verlag, Berlin (1993).

[OR95] P. O’Hearn and J. Riecke. Kripke logical relations and PCF. Information and Computation, 120(1):107–116, 1995.

[OT95] P. W. O’Hearn and R. D. Tennent. Parametricity and local variables. J. ACM, 42(3):658–709, May 1995.

[Pl73] G. D. Plotkin. Lambda-definability and logical relations. Memorandum SAI-RM-4, School of Artificial Intelligence, University of Edinburgh, October 1973.

[Pl80] G. D. Plotkin. Lambda-definability in the full type hierarchy. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pages 363–373. Academic Press, 1980.

[Po97] A. J. Power. Categories with algebraic structure. In M. Nielsen and W. Thomas, editors, Computer Science Logic, 11th International Workshop, CSL’99, volume 1414 of Lecture Notes in Computer Science, pages 389–405, Aarhus, Denmark, August 1997. Springer-Verlag, Berlin (1998).

[Re74] J. C. Reynolds. On the relation between direct and continuation semantics. In J. Loeckx, editor, Proc. 2nd Int. Colloq. on Automata, Languages and Programming, volume 14 of Lecture Notes in Computer Science, pages 141–156. Springer-Verlag, Berlin, 1974.

[Re83] J. C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513–523, Paris, France, 1983. North-Holland, Amsterdam.

[Sc87] O. Schoett. Data abstraction and the correctness of modular programming. Ph.D. thesis, University of Edinburgh, February 1987. Report CST-42-87.

[St96] I. Stark. Categorical models for local names. Lisp and Symbolic Computation, 9(1):77–107, February 1996.

Appendix: Algebraic Structure on Categories

In ordinary universal algebra, an algebra is a set together with a family of basic operations : ^{}, subject to equations between derived operations. In order to define algebraic structure on categories, one must replace the set by a category . One also replaces the finite number by a finitely presentable category . All finite categories are finitely presentable, and finite categories are the only finitely presentable categories we need in this paper. One also allows not only functions from the set ( ) into the set of objects of , but also functions from the set ( ) into the set of arrows in . These are subject to equations between derived operations. It follows that the category of small such categories with structure and functors that strictly preserve the structure is equivalent to the category of algebras, - , for a finitary monad on .

All structures relevant to this paper are instances of a slightly more restricted situation: that of -enriched algebraic structure. So we shall restrict to -enriched structures here. Let denote the 2-category of small categories. So ( ) denotes the category of functors from to . Let _{}denote the full sub-2-category of given by (isomorphism classes of) finitely presentable categories.

Definition A.1. A signature on is a 2-functor : ob _{}, regarding ob _{}as a discrete 2-category.

For each ob _{}, ( ) is called the category of basic operations of arity . Using , we construct _{}: _{}as follows: set

0 = , the inclusion of _{}into , and +1 = + _{ob _{}}_{}( ) ( );

and define

0: _{0}  _{1} to be :  + _{ob _{}}_{0}( ) ( ); and
+1 : _{+1} _{+2} to be + _{ob _{}}_{}( ) ( ).

Then _{}= colim_{}_{}, where the colimit exists because is cocomplete, and it is a colimit in a functor category with base . In many cases of interest, each _{}is a monomorphism, so _{}is the union of _{}_{}. For each , we call _{}( ) the category of derived -ary operations.

A signature is typically accompanied by equations between derived operations. So we say

Definition A.2. The equations of an algebraic theory with signature are given by a 2-functor : ob _{}together with 2-natural transformations _{1} _{2}: _{}( ) , where : ob _{}_{}is the inclusion.

Definition A.3. Algebraic structure on consists of a signature , together with equations ( _{1} _{2}).

We generally denote algebraic structure by ( ), suppressing _{1} and _{2}.

We now define the algebras for a given algebraic structure.

Definition A.4. Given a signature , an -algebra consists of a small category together with a functor _{}: ( ) ( ) for each .

So, an -algebra consists of a carrier and an interpretation of the basic operations of the signature. This interpretation extends canonically to the derived operations, giving an _{}( ) -algebra, as follows.

0: ( ) _{0}( ) is the identity; using the fact that ( ) preserves colimits, to give a functor _{+1} from ( )

to _{+1} ( ) is equivalent to giving a functor from ( ) to ( ), which we will make the identity, and, for each in ob _{}, a functor from ( ) to ( _{}( ) ( ) ) or, equivalently, a functor from ( ) _{}( ) to ( ) which can be inductively defined by

[figure: ( )  _{}( ); _{}( )  _{}( ); ( ); ( ); _{}id; comp; _{}]

Definition A.5. Given algebraic structure ( ), an ( )-algebra is an -algebrathat satisfies the equations, i.e., an -algebra ( ) such that both legs of

[figure: ( ); _{}( ); ( ); _{}; ( _{1}_{}); ( _{2}_{})]

agree.

Given ( )–algebras ( ) and ( ), we define the hom-category

( )-Alg ( ) ( )

to be the equaliser in of

[figure: ( ); _{}( ( ) ( )); _{}( ( ( ) ) ( ( ) )); _{}( ( ) ( ( ) )); ^{( ( ) ) ^{ob _{}}}; _{}( _{}( ( ) )); _{}( ( ) _{}); ( ( ) ) _{ob _{}}]

This agrees with our usual universal-algebraic understanding of the notion of homomorphism of algebras, internalising it to . ( )-Alg can then be made into a 2-category in which composition is induced by that in . An arrow in ( )-Alg is a functor : such that, for all finitely presentable ,

( ) = _{}( ): ( ) ( )

i.e., a functor that commutes with all basic -ary operations for all .

A special case of the main result of [KP93] says

Theorem A.6. A 2-category is equivalent to ( )-Alg for algebraic structure ( ) on if and only if there is a finitary 2-monad on such that the 2-categoryis equivalent to -Alg.

See [Po97] for an account directed towards a computer science readership.