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 as well as 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 pairs of functions that are expressible by the same lambda term. 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 refi-nement where the fact that pre-logical relations compose explains why stepwise refinement is sound.
|Title of host publication||Computer Science Logic|
|Subtitle of host publication||13th International Workshop, CSL’99 8th Annual Conference of the EACSL Madrid, Spain, September 20–25, 1999 Proceedings|
|Editors||Jörg Flum, Mario Rodriguez-Artalejo|
|Number of pages||16|
|Publication status||Published - 1999|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|