ch:relational-parametricity: ch:relational-parametricity

Suppose $f{=}_{\beta }{f}^{\prime }$, $g{=}_{\beta }{g}^{\prime }$, $a{=}_{\beta }{a}^{\prime }$, and $b{=}_{\beta }{b}^{\prime }$. Compatible beta conversion gives $$fa{=}_{\beta }{f}^{\prime }{a}^{\prime },gb{=}_{\beta }{g}^{\prime }{b}^{\prime }.$$ Since $R$ and $S$ are relations on beta-classes, replacing either endpoint by these equal terms changes no membership assertion. Thus the implication defining $R\Rightarrow S$ is independent of the four representatives. For a graph, also let $k{=}_{\beta }{k}^{\prime }$. Compatible conversion in both the function and argument positions gives $$ka{=}_{\beta }b⟺k^{\prime }{a}^{\prime }{=}_{\beta }{b}^{\prime },$$ so the represented graph is unchanged by replacing $(k,a,b)$ with beta-equivalent representatives $(k^{\prime },a^{\prime },b^{\prime })$. Thus $\mathsf{Gr}(k)$ is well defined on the quotient in all three arguments.

Now let $f:A\to B$ be closed and suppose $[a]{\mathsf{Eq}}_A[b]$. By definition, $a{=}_{\beta }b$; compatible conversion then gives $fa{=}_{\beta }fb$. Hence $$[f]({\mathsf{Eq}}_A\Rightarrow {\mathsf{Eq}}_B)[f].$$ This proves membership, not equality of the lifted relation with ${\mathsf{Eq}}_{A\to B}$. An arrow relation may be vacuous when its domain has no closed terms.

Write $\varrho (Y)=(E_0,E_1,T)$. The two endpoint types are $$\mathrm{\forall }X.(E_0\to X)\to E_0\to X,\mathrm{\forall }X.(E_1\to X)\to E_1\to X.$$ For terms $p$ and $q$ at these endpoints, $$[p][[\mathrm{\forall }X.(Y\to X)\to Y\to X{]]}_{\varrho }[q]$$ means the following. For every pair of closed formed types $C,D$, every relation $S:C\leftrightarrow D$, every pair $$[f](T\Rightarrow S)[g],$$ and every pair $[a]T[b]$, one has $$[p[C]fa]S[q[D]gb].$$ Thus the two function arguments are related by $T\Rightarrow S$, while the two $Y$-arguments are related directly by $T$; applying the related functions turns the latter pair into an $S$-related result pair.

Let the universal subexpression originally be displayed as $\mathrm{\forall }Y.C$. Choose one name $W$ fresh for $X$, $B$, $C$, the finite ranges of both ${\varrho }_0$ and ${\varrho }_1$, and the domain of the ambient split context. Replace the binder by the alpha-equal display $$\mathrm{\forall }W.C^{\prime },C^{\prime }:=C[W/Y].$$ This single replacement handles at once an occurrence of the old name $Y$ in $B$ or in either endpoint substitution: none of those occurrences is captured, because the new binder is $W$.

For an arbitrary relational object $Q=(D_0,D_1,S)$ at $W$, the extension is formed without overwriting an ambient entry and satisfies $${\varrho }_W:({\varrho }_W{)}_0\leftrightarrow ({\varrho }_W{)}_1\mathsf{over}{\mathrm{\Delta }}_0,{\mathrm{\Delta }}_1,W,{\varrho }_W:=\varrho [W\mapsto Q].$$ The body relation on the left of the substitution equation is $$[[C^{\prime }[B/X]{]]}_{{\varrho }_W}.$$ The induction hypothesis changes it to $$\begin{array}{}\text{(}1\text{)}& [[C^{\prime }{]]}_{{\varrho }_W[X\mapsto (B[({\varrho }_W{)}_0],B[({\varrho }_W{)}_1],[[B{]]}_{{\varrho }_W})]}.\end{array}$$ Freshness gives $W\notin \mathrm{ftv}(B)$. Exactly here we use that fact: $$\begin{array}{}\text{(}2\text{)}& B[({\varrho }_W{)}_i]=B[{\varrho }_i](i=0,1),[[B{]]}_{{\varrho }_W}=[[B{]]}_{\varrho }.\end{array}$$ The second equality is irrelevance applied to the same freshness fact. Substituting (2) into (1) makes its environment $$\varrho [W\mapsto Q][X\mapsto (B[{\varrho }_0],B[{\varrho }_1],[[B{]]}_{\varrho })].$$ Since $W\ne X$ and the $X$-entry is independent of $W$, the extensions commute. It is therefore $$\varrho [X\mapsto (B[{\varrho }_0],B[{\varrho }_1],[[B{]]}_{\varrho })][W\mapsto Q],$$ which is precisely the environment used by the body of the right-hand universal clause. The endpoint substitutions commute by the same capture-avoiding freshening. Quantifying over all $Q$ completes the universal case.

Write $$\varrho (Y)=(Y_0,Y_1,R_Y),\varrho (Z)=(Z_0,Z_1,R_Z).$$ The premise induction hypothesis for $q$ says $$[q[{\varrho }_0]][[\mathrm{\forall }X.(X\to Y)\to X\to Y{]]}_{\varrho }[q[{\varrho }_1]].$$ In its universal clause choose endpoint types $Z_0,Z_1$ and the relation $R_Z=[[Z{]]}_{\varrho }$. It gives $$[q[{\varrho }_0][Z_0]][[(X\to Y)\to X\to Y{]]}_{\varrho [X\mapsto (Z_0,Z_1,R_Z)]}[q[{\varrho }_1][Z_1]].$$ For $i=0,1$, this is the endpoint term printed by the type-application conclusion because The first equality is the type-substitution clause for type application; the second is the definition of the endpoint substitution. The endpoint types are $$(Z_0\to Y_0)\to Z_0\to Y_0,(Z_1\to Y_1)\to Z_1\to Y_1.$$ Finally, lemma 6.8 identifies the displayed middle relation with $$[[((X\to Y)\to X\to Y)[Z/X]{]]}_{\varrho },$$ which is exactly the relation at the result type assigned to $q[Z]$ by F-All-E.

Formation gives $\cdot ⊢{\mathsf{Void}}_F\mathsf{type}$ and $\cdot ⊢{\mathsf{Bool}}_F\mathsf{type}$. Weakening the two closed boolean typings under $z:{\mathsf{Void}}_F$ and applying F-Arr-I yields $$\lambda z:{\mathsf{Void}}_F.{\mathsf{true}}_F,\lambda z:{\mathsf{Void}}_F.{\mathsf{false}}_F:{\mathsf{Void}}_F\to {\mathsf{Bool}}_F.$$ The domain relation has no pairs because $\mathsf{Tm}({\mathsf{Void}}_F)=\varnothing$. Consequently the universal condition in the lifted arrow relation has no instance to check. This is the single premise that is never tested. The codomain values need not be related at all.

Replacing the codomain gives, for example, $$\lambda z:{\mathsf{Void}}_F.{\mathsf{zero}}_F,\lambda z:{\mathsf{Void}}_F.\mathrm{\Lambda }X.\lambda x:X.\lambda s:X\to X.sx.$$ They are again related vacuously at $[[{\mathsf{Void}}_F\to {\mathsf{Nat}}_F{]]}_{ϵ}$. Both displayed functions are beta-normal: the first returns the zero Church numeral, while the second returns the one Church numeral written out in normal form. Their bodies are distinct beta-normal terms, so Church–Rosser separates their beta classes.

Let $G=\mathsf{Gr}(k)$ with $G:A\leftrightarrow B$. Self-parametricity of $b$, instantiated at $G$, gives $$[b[A]](G\Rightarrow G\Rightarrow G)[b[B]].$$ By definition of a graph, $$[a_0]G[k{a}_0],[a_1]G[k{a}_1].$$ The first use of arrow lifting applies the related Boolean eliminators to the first related branch pair and gives $$[b[A]a_0](G\Rightarrow G)[b[B](k{a}_0)].$$ The second use applies these related functions to the second branch pair: $$[b[A]a_0{a}_1]G[b[B](k{a}_0)(k{a}_1)].$$ Unfolding $G$ in the last line is exactly $$k(b[A]a_0{a}_1){=}_{\beta }b[B](k{a}_0)(k{a}_1).$$ No classification of $b$ as true or false was used.

Put $G=\mathsf{Gr}(f)$ with $G:A\leftrightarrow B$, and put ${\mathsf{id}}_A=\lambda x:A.x$. Self-parametricity of $r$, instantiated at $G$, gives $$\begin{array}{}\text{(}1\text{)}& [r[A]](([[A{]]}_{ϵ}\Rightarrow G)\Rightarrow G)[r[B]].\end{array}$$ We claim $$\begin{array}{}\text{(}2\text{)}& [{\mathsf{id}}_A]([[A{]]}_{ϵ}\Rightarrow G)[f].\end{array}$$ Indeed, suppose $[a][[A{]]}_{ϵ}[a^{\prime }]$. Identity extension at $A$ is used at this exact point to conclude $a{=}_{\beta }{a}^{\prime }$. Compatible beta conversion then gives $$f({\mathsf{id}}_{A}a){=}_{\beta }fa{=}_{\beta }f{a}^{\prime },$$ which says $[{\mathsf{id}}_{A}a]G[f{a}^{\prime }]$. This proves (2).

Applying the arrow relation in (1) to (2) yields $$[r[A]{\mathsf{id}}_A]G[r[B]f].$$ The graph definition now reads $$f(r[A](\lambda x:A.x)){=}_{\beta }r[B]f,$$ and symmetry gives the equation in the question. For $A={\mathsf{Nat}}_F$, the required identity extension is proposition 6.14.

Without identity extension, an input pair in $[[A{]]}_{ϵ}$ need not consist of beta-equal terms, so the implication needed for (2) need not hold. Replacing that missing step by an assertion of beta equality would repeat exactly the false unrestricted identity-extension claim refuted by proposition 6.15.

Put $$B^{\prime }:={\mathsf{Nat}}_F{\times }_F{\mathsf{Nat}}_F$$ and define Let $[n]R^{\prime }[p]$ mean $p{=}_{\beta }⟨n,n{⟩}_F$. The initial states are related directly. If $[n]R^{\prime }[p]$, the two projection beta laws give $$s^{\prime }p{=}_{\beta }⟨{\mathsf{succ}}_{F}n,{\mathsf{succ}}_{F}n{⟩}_F,$$ so $[{\mathsf{succ}}_{F}n]R^{\prime }[s^{\prime }p]$. The first projection also gives $n{=}_{\beta }{r}^{\prime }p$, hence $$[{\mathsf{succ}}_F](R^{\prime }\Rightarrow R^{\prime })[s^{\prime }],[\lambda n:{\mathsf{Nat}}_F.n](R^{\prime }\Rightarrow {\mathsf{Eq}}_{{\mathsf{Nat}}_F})[r^{\prime }].$$

For $c_2$, the first implementation reduces to $\bar{2}$. In the paired implementation, two steps reduce the state to $⟨\bar{2},\bar{2}{⟩}_F$, and the observer projects the first component. Thus its result also reduces to $\bar{2}$, as predicted by theorem 6.18.

For the empty relation $R=\varnothing$ with $R:A\leftrightarrow A$, the implication defining $R\Rightarrow R$ has no input pair to test. Hence $$[{\mathsf{id}}_A](R\Rightarrow R)[{\mathsf{id}}_A].$$ The abstraction-theorem case for a proposed ${\mathsf{fix}}_A:(A\to A)\to A$ would have to conclude $$[{\mathsf{fix}}_A{\mathsf{id}}_A]R[{\mathsf{fix}}_A{\mathsf{id}}_A],$$ which is impossible because $R$ has no pairs.

Requiring relations to be nonempty removes this particular choice but not the problem. Fix a closed $a:A$ and take $$R=\{([a],[a])\}.$$ If the sole input pair $[a]R[a]$ is supplied to the two identity functions, their outputs are again $[a]R[a]$. Therefore $$[{\mathsf{id}}_A](R\Rightarrow R)[{\mathsf{id}}_A].$$ Parametricity of ${\mathsf{fix}}_A$ would force the pair of fixed-point results to lie in the singleton $R$, hence $${\mathsf{fix}}_A{\mathsf{id}}_A{=}_{\beta }a.$$ But the least fixed point of the identity in a partial language is the designated divergent, or least, computation, not an arbitrary closed $a$. Thus nonemptiness alone admits relations that omit the least computations. One must at least require strictness, relating the two least computations; admissibility can then address closure under limits of finite approximations.