Contents

# Contents

## Idea

In proof theory and the theory of programming languages, the term “logical relations” refers to a certain style of argument used in proving results such as strong normalization? or observational equivalence?. Although there is no precise definition, typically a logical relation (or logical predicate) corresponds to a family of (sometimes unary) relations defined by induction on types, and such that the definition of the relation at a particular type mirrors the logical structure of that type in an appropriate sense.

## Example

As originally described by (Tait 1967) (and presented in (Girard 1990)), logical predicates can be used to prove strong normalization for the simply-typed lambda calculus. The idea is to define a family of predicates $RED_T$ over terms, indexed by types $T$, such that:

• ($T = X$ an atomic type): $t \in RED_X$ iff $t$ is strongly normalizing

• ($T = U \to V$ a function type): $t \in RED_{U \to V}$ iff $\forall u$, $u \in RED_U$ implies $t(u) \in RED_V$.

By induction on $T$, one establishes the following three conditions:

1. if $t \in RED_T$, then $t$ is strongly normalizing

2. if $t \in RED_T$ and $t \to t'$, then $t' \in RED_T$

3. if $t$ is neutral (i.e., either a variable or application) and for all $t \to t'$ we have $t' \in RED_T$, then $t \in RED_T$

Finally, one proves the “fundamental lemma”

• if $t:T$ then $t \in RED_T$

which by condition (1) implies that every simply-typed term is strongly normalizing.

• W. W. Tait. Intensional Interpretations of Functionals of Finite Type I, JSL 32:2, June 1967. (JSTOR)

• Gordon Plotkin. Lambda-definability and logical relations, unpublished manuscript, Edinburgh 1973. (pdf)

• John C. Reynolds, Types, Abstraction and Parametric Polymorphism Information Processing 83(1) (1983), pp. 513-523.

• Jean-Yves Girard, Yves Lafont, and Paul Taylor, Proofs and Types, 1990. (web)

For a recent perspective:

• Claudio Hermida, Uday Reddy, E. Robinson, section 2 of Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming Languages, Electronic Notes in Theoretical Computer Science (2013) (pdf)

• Patricia Johann, Neil Ghani, Logical Relations for Program Verification, research proposal (pdf)

• Thierry Coquand, from slide 63 on in Equality and dependent type theory (pdf)

• Florian Rabe, Kristina Sojakova, Logical Relations for a Logical Framework (pdf)

• Carsten Schürmann, Jeffrey Sarnat, Structural logical relations (pdf)

• Lau Skorstengaard, An Introduction to Logical Relations: Proving Program Properties Using Logical Relations, (pdf)

• Karl Crary, Logical Relations and a Case Study in Equivalence Checking, in Benjamin Pierce (ed.), Advanced Topics in Types and Programming Languages

• Amal Ahmed, Lectures on logical relations at OPLSS 2015, (lecture recordings)

Further discussion: