[Prev][Next][Index][Thread]
paper on pre-logical relations available
The following paper is report ECS-LFCS-99-405 of the Laboratory for
Foundations of Computer Science, University of Edinburgh. It is
available in various formats from
http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/99/ECS-LFCS-99-405/
or as hardcopy from Kendal Reid <reports@dcs.ed.ac.uk>.
Comments are welcome!
Don and Furio
----------------------------------------------------------------
Pre-logical Relations
Furio Honsell and Donald Sannella
Abstract:
We study a weakening of the notion of logical relations, called
pre-logical relations, that has many of the features that make logical
relations so useful but having 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
lambda-expressible functions. Pre-logical 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. 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 for first-order
signatures. Pre-logical relations can be used in place of logical
relations to give an account of data refinement where the fact that
pre-logical relations compose explains why stepwise refinement is
sound.