Kripke logical relations

The term Kripke logical relations may refer to either of two closely related of the logical relations technique:

• the logical relation is of fixed arity, but has an extra argument which varies over a Kripke frame
• the arity of the logical relation itself varies over a small category

Over Kripke frames

This type of relation was introduced in Plotkin 1973, 1980 to reason about definability in the simply-typed \lambda-calculus.

In more recent years, such Kripke logical relations have proven to be very useful for reasoning about programming languages with effects.

Varying arity

Logical relations of varying arity were introduced by Jung and Tiuryn 1993, again with a view to characterising definability in the simply-typed \lambda-calculus.

In this setting, it is the arity of the relation that varies. The arities are often given by sets W (often finite). Then, a logical relation is just a subset R_\sigma \subseteq W \to A_\sigma of W-indexed tuples of the interpretation A_\sigma of a type \sigma. For example, if W = \{ 1, 2 \}, we obtain the usual binary logical relations.

The variation in the arities usually happens by setting up a small category of sets W, V, and functions f : W \to V between them. If we are given f : W \to V and a relation R_\sigma \subseteq V \to A_\sigma, we can define a relation

R_\sigma \circ f \subseteq W \to A_\sigma

by letting R_\sigma \circ f = \{ g : W \to A_\sigma \mid g \circ f \in R_\sigma \}.

This set up subsumes the relations that vary over a Kripke world: take a category all of whose objects have the same cardinality (the arity), and all of whose morphisms are bijections, such that the category is isomorphic to the Kripke frame.

References

@techreport{plotkin_lambda_1973,
	type = {Memorandum},
	title = {Lambda {Definability} and {Logical} {Relations}},
	url = {https://homepages.inf.ed.ac.uk/gdp/publications/logical_relations_1973.pdf},
	number = {SAI-RM-4},
	institution = {University of Edinburgh},
	author = {Plotkin, G. D.},
	year = {1973}
}

@incollection{plotkin_lambda-definability_1980,
	address = {New York},
	title = {Lambda-{Definability} in the {Full} {Type} {Hierarchy}},
	url = {https://homepages.inf.ed.ac.uk/gdp/publications/Lambda_Definability.pdf},
	booktitle = {To {H}. {B}. {Curry}: {Essays} in {Combinatory} {Logic}, {Lambda} {Calculus}, and {Formalism}},
	publisher = {Academic Press},
	author = {Plotkin, Gordon D.},
	editor = {Seldin, J. P. and Hindley, J. R.},
	year = {1980},
	pages = {363--373}
}

@inproceedings{jung_1993,
	address = {Berlin/Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {A new characterization of lambda definability},
	volume = {664},
	doi = {10.1007/BFb0037110},
	booktitle = {Typed {Lambda} {Calculi} and {Applications}},
	publisher = {Springer-Verlag},
	author = {Jung, Achim and Tiuryn, Jerzy},
	editor = {Bezem, Marc and Groote, Jan Friso},
	year = {1993},
	pages = {245--257}
}