Furio Honsell - Pre-logical relations

Logical relations have proved to be a very useful tool in the study of the syntax and semantics of typed lambda calculi. However, they have some drawbacks deriving from the fact that they are too rigid to be closed under set-theoretic operations, such as intersection or composition. For instance, there is no canonical way of extending a relation at base types to a logical relation at higher types in the presence of higher-order constants, so they cannot be used with arbitrary signatures, and they do not give a satisfactory account of the process of data refinement.

A weakening of the notion of logical relation, called pre-logical relation [1], will be presented, that has many of the features that make logical relations so useful as well as being closed under the above operations.

This notion is rather intrinsic. Prelogical relations subsume many of the previous generalizations of logical relations. They are the minimal weakening of logical relations that gives composability for extensional structures and simultaneously the most liberal definition that gives the Basic Lemma. Moreover prelogical predicates coincide precisely with the predicates which are invariant under Kripke logical relations with varying arity, in the sense of Jung and Tiuryn. The use of pre-logical relations in place of logical relations gives an improved version of Mitchell's representation independence theorem which characterizes observational equivalence for all signatures rather than just first order ones.

A number of intriguing open questions concerning the theory of pre-logical relations will be discussed.

If time permits we shall speculate on possible generalizations of this notion to other type disciplines and richer languages.

[1] F.Honsell, D.Sannella: Pre-logical Relations - to appear in CSL'99 Proceedings, (extended version available at http://www.dcs.ed.ac.uk/home/dts/pub/prelogrel-long.ps).

(joint work with Don Sannella)