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 ...

• Type: Conference
• Year: 1999
• Where: CSL
• Authors: Furio Honsell, Donald Sannella
• Keywords: Automated Reasoning, CSL 1999, Logical Relations, Pre-logical Relations, Prelogical Relations