Binary Logical Relation - Universal quantification

[Bohun9]

Can someone share intuition/motivation for this definition? I think it is difficult to follow without prose explaining how one should think about it.

[ppolesiuk]

I see two things that need some explanations and intuitions.

1. We define a relation inductively on the structure of (syntactic) types. The typing rule of quantifier elimination substitutes an arbitrary type in another (τ{τ'/α}). In the naive definition of denotation of type ∀α.τ, type τ{τ'/α} may be arbitrarily large, giving no chance to well founded structural recursion. In order to avoid these problems, we perform substitution on the semantic level, i.e., we use environment η to interpret variables (instead of syntactically substituting for them). Since we interpret variables as semantic types, we can quantify over all semantic types in this definition, resulting well founded structural recursion. This is the same story as for unary relation, but has far-reaching consequences (see the next point).
2. The relation is binary (we define logical equivalence) and it has the same structure as an unary relation, with the difference that it works pointwise on pair of terms. For quantifiers, we quantify over all possible semantic types, which are arbitrary relations. These relations are not necessarily equivalence relations or results of denotations of syntactic types. This is particularly important for describing equivalences between two different representations of the same thing hidden under existential quantification: for instance, our motivating example of two implementations of pairs. This additional freedom is also important for universal quantifiers. Firstly, universal quantification can be used to encode existential one. Secondly, it allows us to formally treat the notion of "parametricity", which informally says that polymorphic functions cannot depend on elements of universally quantified type (and therefore, there is only one pure and total function of type ∀α.α→α). We will learn more about parametricity on the next lecture.

I hope, this answers your question.