Informatics Report Series


Report   

EDI-INF-RR-0559


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Prelogical relations
Authors: Furio Honsell ; Donald Sannella
Date:Oct 2002
Publication Title:Information and Computation
Publisher:Elsevier
Publication Type:Journal Article Publication Status:Published
Volume No:178(1) Page Nos:23-43
DOI:10.1006/inco.2002.311
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 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. Prelogical 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. Prelogical predicates (i.e., unary prelogical relations) coincide with sets that are invariant under Kripke logical relations with varying arity as introduced by Jung and Tiuryn, and prelogical relations are the closure under projection and intersection of logical relations. These conceptually independent characterizations of prelogical relations suggest that the concept is rather intrinsic and robust. The use of prelogical 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. Prelogical relations can be used in place of logical relations to give an account of data refinement where the fact that prelogical relations compose explains why stepwise refinement is sound.
Links To Paper
in ScienceDirect (subscription required)
author's copy of the final published manuscript
Bibtex format
@Article{EDI-INF-RR-0559,
author = { Furio Honsell and Donald Sannella },
title = {Prelogical relations},
journal = {Information and Computation},
publisher = {Elsevier},
year = 2002,
month = {Oct},
volume = {178(1)},
pages = {23-43},
doi = {10.1006/inco.2002.311},
url = {http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B6WGK-470V6MH-3-1&_cdi=6825&_user=809099&_orig=search&_coverDate=10%2F10%2F2002&_sk=998219998&view=c&wchp=dGLbVtz-zSkWW&md5=58352d8bcaeb126aa3929dc8c7fbb88e&ie=/sdarticle.pdf},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh