§ Logical Relations (Sterling)
- Key idea is to consider relations between closed terms of types and . That is, we have have a relation .
- We write a relation between two closed terms and as: .
- A morphism of relations is given by two functions and such that .
§ Logical relations for function spaces
- Given this, we can build up logical relations for more complex cases like function types and quantified types. For example, given logical relations and , we build to be the relation between types , and given by the formula:
- This satisfies the universal property of functions in the category of logical relations, ie, there is an adjunction between and .
- Next, we can interpret a base type like
bool by the logical relation that encodes equality on that type. so and is given by:
§ Logical relations for data types
§ Logical relations for parametric types
- for a type of the form that is parametric in , suppose we have a family of relations which vary in .
- Then we define the logical relation for the type as:
§ Proving things using logical relations
- For , we have that That is, the function value at
() : unit determines the value of the function also at
true: bool (and more generally, everwhere).
- To prove this, we first invoke that by soundness , we have that . On unwrapping this, this means that:
- Plugging in , this gives us an equality:
- We now choose , with the singleton element .
- Since is coprime to , we have that
- This can be written as . [ is even when ].
- That is, .
- Since we are in an integral domain (really a field), this means that .