Lax Logical Relations
View/ Open
Date
2000Author
Plotkin, Gordon
Power, John
Sannella, Donald
Tennent, Robert
Metadata
Abstract
Lax logical relations are a categorical generalisation of logical
relations; though they preserve product types, they need not preserve
exponential types. But, like logical relations, they are preserved by the
meanings of all lambda-calculus terms.We show that lax logical relations
coincide with the correspondences of Schoett, the algebraic relations of
Mitchell and the pre-logical relations of Honsell and Sannella on Henkin
models, but also generalise naturally to models in cartesian closed categories
and to richer languages.