§ Logical Relations (Sterling)

• Key idea is to consider relations $R_\tau$ between closed terms of types $\tau_l$ and $\tau_r$. That is, we have have a relation $R_\tau \subseteq \{ (t_l, t_r): (\cdot \vdash t_l : \tau_l), (\cdot \vdash t_r : \tau_r)$.
• We write a relation between two closed terms $\tau_L$ and $\tau_R$ as: $R_{\tau} \equiv (\cdot \vdash \tau_L) \times (\cdot \vdash \tau_R)$.
• A morphism of relations $f: R_\sigma to R_\tau$ is given by two functions $f_l: \sigma_l \to \tau_l$ and $f_r: \sigma_r \to \tau_r$such that $aR_\sigma b \implies f_l(a) R_\tau f_r(b)$.

§ 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 $R_\sigma$ and $R_\tau$, we build $R_{\sigma \to \tau}$ to be the relation between types $(\cdot \vdash \sigma_l \to \tau_l) \times (\cdot \vdash \sigma_r \to \tau_r)$, and given by the formula:

• This satisfies the universal property of functions in the category of logical relations, ie, there is an adjunction between $R_{\rho \to \sigma} \to R_{\tau}$ and $R_{\rho} \to R_{\sigma \to \tau}$.
• Next, we can interpret a base type like bool by the logical relation that encodes equality on that type. so $R_{\texttt{bool}} : (\cdot \vdash \texttt{bool}) \times (\cdot \vdash \texttt{bool})$ and is given by:

§ Logical relations for data types

§ Logical relations for parametric types

• for a type of the form $\tau(\alpha)$ that is parametric in $\alpha$, suppose we have a family of relations $R_{\tau \alpha} \subseteq \{ (\cdot \vdash \tau_l(\alpha_l) \times (\cdot \vdash \tau_r(\alpha_r) \}_{R_\alpha}$which vary in $R_\alpha$.
• Then we define the logical relation for the type $R_{\forall \alpha, \tau(\alpha)} \subseteq (\cdot \vdash \forall \alpha \tau_l(\alpha)) \times (\cdot \vdash \forall \alpha \tau_r(\alpha))$ as:

§ Proving things using logical relations

• For $f: \forall \alpha, \alpha \to \texttt{bool}$, we have that $f @\texttt{unit} (()) = f @ \texttt{bool}(\texttt{true})$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 $(f, f) \in R_{\forall \alpha. \alpha \to \texttt{bool}}$. On unwrapping this, this means that:

• Plugging in $R_{\texttt{bool}}$, this gives us an equality:

• We now choose $R_\alpha \subseteq (\cdot \vdash \texttt{unit}) \times (\cdot \vdash \texttt{bool})$, with the singleton element $\{ ((), \texttt{true}) \}$.

• Jon Talk

§ $(x/p)$ is $x^{(p-1)/2}$

• Since $x$ is coprime to $p$, we have that $1 \equiv x^{p-1}$
• This can be written as $1^2 - x^{({p-1}/2)^2} = 0$. [ $(p-1)$ is even when $p>2$].
• That is, $(1 - x^{(p-1)/2})(1 + x^{(p-1)/2}) = 0$.
• Since we are in an integral domain (really a field), this means that $x^{(p-1)/2} \equiv \pm 1 (\mod p)$.