Pre-logical Relations

12 years 4 months ago
Pre-logical Relations
Abstract. 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 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 ...
Furio Honsell, Donald Sannella
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where CSL
Authors Furio Honsell, Donald Sannella
Comments (0)