Relational Parametricity and Abstraction Theorems

Consider a closed term $$h:\mathrm{\forall }X.X\to X.$$ At a closed type $A$, the specialization $h[A]$ is an endomap of $A$. Nothing in its arrow type alone prevents a constant endomap. The universal quantifier is the obstruction: $h$ must be the same program when $A$ is replaced by any other type. Relational preservation makes “the same program” a calculation.

A unary property of terms at one type cannot compare a numeral with a state represented by a pair. Such a comparison needs a relation whose endpoints may be different types. It must be a relation rather than only the graph of a function: empty, singleton, and partial correspondences will all be used.

Here “type”, “term”, and “beta” refer to the Church-style System F of chapter 5; the language has no additional term former or reduction rule.

Relations between programs

The set-theoretic obstruction of theorem 5.40 concerned a denotational model in which types range over arbitrary sets and arrows denote all set-theoretic functions. The relational model instead relates typed syntax to typed syntax.

Assign to each type a binary relation between terms of its two endpoint instances. At $A\to B$, relate functions that send $A$-related arguments to $B$-related results; at $\mathrm{\forall }X.A$, quantify over every relation used for $X$. These clauses define the logical relation, a family of binary relations indexed by types, whose preservation is the central induction of the chapter.

Here ${=}_{\beta }$ is restricted to pairs of terms already typed at $A$; it is therefore an equivalence relation on the displayed set. Subject reduction, proposition 5.14, additionally says that every forward reduct of such a term remains in that set. Syntax is a set—indeed it is countable—so the family, indexed by closed type pairs $(A,B)$, of all subsets of $\mathsf{Tm}(A)\times \mathsf{Tm}(B)$ is one fixed set in the classical ZF metatheory fixed in chapter 5. This is the meta-level, as opposed to a construction expressed inside System F. Every relation used here is a subset of this fixed syntactic set, so Reynolds’ obstruction to full set-theoretic impredicativity does not apply.

Relations need not have equal endpoint types. For example, $$\{([{\mathsf{true}}_F],[\bar{0}]),([{\mathsf{false}}_F],[\bar{1}])\}:{\mathsf{Bool}}_F\leftrightarrow {\mathsf{Nat}}_F$$ is a heterogeneous relation. It pairs observations across two encodings; it is neither an equality relation nor the graph of an endofunction.

Arrow lifting is the binary analogue of chapter 5’s candidate-arrow construction: both require an operation to send admissible inputs to admissible outputs. Here both inputs and outputs come in related pairs. Like the underlying type arrow, $\Rightarrow$ associates to the right.

These definitions use beta-classes, not chosen representatives. For example, if $f{=}_{\beta }{f}^{\prime }$, $a{=}_{\beta }{a}^{\prime }$, and $[fa]S[gb]$, compatible reduction gives $f^{\prime }{a}^{\prime }{=}_{\beta }fa$; changing $g,b$ gives $g^{\prime }{b}^{\prime }{=}_{\beta }gb$ in the same way. Thus the same relation statement holds after changing any representative. Graph relations satisfy the following calculation.

Proof of Lemma 6.3 — Graph calculation

Proof. Suppose first that the lifted relation holds. Since $[a]\mathsf{Gr}(k)[ka]$, its defining implication gives $[fa]\mathsf{Gr}(k)[g(ka)]$, which is the displayed equation.

Conversely, let $[a]\mathsf{Gr}(k)[b]$, so $ka{=}_{\beta }b$. The assumed equation and compatible beta conversion give $$k(fa){=}_{\beta }g(ka){=}_{\beta }gb.$$ This says precisely that $[fa]\mathsf{Gr}(k)[gb]$. ◻

Reading a type as a relation

A free type variable must now carry three pieces of data: a left type, a right type, and a relation between them.

Write $ϵ$ for the unique relation environment over the empty type context. This symbol will not be used for the empty relation.

The endpoint substitutions are simultaneous, capture-avoiding type substitutions in the sense of convention 5.2. Bound type variables are first synchronized away from their finite ranges.

Proof of Lemma 10.6 — Relational alpha-equivariance

Proof. Induct on the displayed representative of $A$. If $A=X$, both sides are $S$. The variable case $A=Z\ne X$ uses the unchanged $Z$-entry of $\varrho$; the freshness hypothesis excludes $Z=Y$. The arrow case applies the two induction hypotheses and then the arrow-lifting clause.

For $A=\mathrm{\forall }Z.B$, first alpha-rename $Z$ away from $\{X,Y\}\cup \mathrm{dom}(\mathrm{\Delta })$ and the finite ranges of ${\varrho }_0,{\varrho }_1$. Take arbitrary closed formed $E,F$ and a relation $T:E\leftrightarrow F$. The two universal clauses compare the body relations under, respectively, $$\begin{array}{c}\varrho [Y\mapsto (C,D,S)][Z\mapsto (E,F,T)],\\ \varrho [X\mapsto (C,D,S)][Z\mapsto (E,F,T)].\end{array}$$ The $Z$-extension commutes with the $X$- and $Y$-extensions. Apply the induction hypothesis to $B$ under $\varrho [Z\mapsto (E,F,T)]$; it equates these body relations. Since $E,F,T$ were arbitrary, the universal clauses are equal.

One alpha-conversion $\mathrm{\forall }X.A{=}_{\alpha }\mathrm{\forall }Y.A[Y/X]$ is therefore interpreted equally. The variable and arrow congruence cases preserve equality of interpretations, and the universal congruence case is the calculation just proved. Reflexivity, symmetry, and transitivity are inherited from equality of relations. Induction on the generation of alpha-equivalence gives independence from every representative. ◻

The tempting clause $$[p][[\mathrm{\forall }X.A{]]}_{\varrho }[q]⟺\mathrm{\forall }C,D,S.[p[C]][[A[C/X]{]]}_{\varrho }[q[D]]$$ is not structurally recursive: $A[C/X]$ need not be a subexpression of $\mathrm{\forall }X.A$. The actual universal clause recurses at the proper syntactic subexpression $A$, under a larger environment. Its quantifiers range over the fixed meta-set described after definition 6.1. The result of the universal clause is itself one of the relations over which such clauses quantify. This impredicative use is Separation over that fixed set of term pairs; it does not construct a new universe of relations.

Proof of Lemma 6.6 — Compatibility with beta-classes

Proof. Compatible beta reduction is closed under both term application and type application. Hence For the arrow clause, changing representatives therefore changes neither the premise class nor the conclusion class of its defining implication. For the universal clause, the second equation shows that, for every $C,D,S$, the two type applications determine the same beta-classes in the recursively defined body relation. Thus both clauses define relations on the quotient sets $\mathsf{Tm}(-)$. ◻

Here is a complete expansion. Suppose $\varrho (Y)=(E_0,E_1,T)$ and put $$P:=\mathrm{\forall }X.(X\to Y)\to X\to Y.$$ Then $[p][[P{]]}_{\varrho }[q]$ means that for every $S:C\leftrightarrow D$, every $$[f](S\Rightarrow T)[g],[a]S[b],$$ one has $$[p[C]fa]T[q[D]gb].$$ The left endpoint of $P$ is $\mathrm{\forall }X.(X\to E_0)\to X\to E_0$; the right endpoint replaces $E_0$ by $E_1$. Every symbol in the expanded assertion is therefore typed.

The endpoint calculation and irrelevant-variable property are:

Proof of Lemma 6.7 — Endpoints and irrelevant variables

Proof. For item 1, induct on $A$. Variables use the corresponding environment entry, and arrows use the induction hypotheses at domain and codomain. For $\mathrm{\forall }X.B$, choose $X$ fresh for both environments. Its endpoint is $(\mathrm{\forall }X.B)[{\varrho }_i]=\mathrm{\forall }X.B[{\varrho }_i]$. If $C$ is closed, type application has endpoint $$((\mathrm{\forall }X.B)[{\varrho }_i])[C]:B[{\varrho }_i][C/X]=B[{\varrho }_i,X\mapsto C],$$ where the equality is the simultaneous/single type-substitution composition equation of equation 5.2. The induction hypothesis types the body relation at these two endpoints.

For item 2, run a second structural induction on $A$. The variable case uses agreement on that variable; the arrow case applies the two induction hypotheses. At $\mathrm{\forall }X.B$, freshen $X$ for both environments and extend each by the same arbitrary triple $(C_0,C_1,S)$. The extended environments agree on $\mathrm{ftv}(B)$, so the induction hypothesis equates the body relations for every such triple. The universal clauses are therefore equal. ◻

Proof of Lemma 6.8 — Relational type substitution

Proof. Induct on $A$. For $A=X$, both sides are $[[B{]]}_{\varrho }$. For a variable $Y\ne X$, both sides are $R_Y$. For an arrow $C\to D$, the induction hypotheses give $[[C[B/X]{]]}_{\varrho }=[[C{]]}_{{\varrho }^{+}}$ and $[[D[B/X]{]]}_{\varrho }=[[D{]]}_{{\varrho }^{+}}$; substituting these equalities into the arrow clause equates the two arrow liftings.

The induction assertion is the displayed split-context statement, with an arbitrary suffix ${\mathrm{\Delta }}_1$. Thus it remains available when a binder is added to that suffix. If we had proved only the case ${\mathrm{\Delta }}_1=\cdot$, the universal case would require the unavailable instance ${\mathrm{\Delta }}_1=Y$. For that case, write $A=\mathrm{\forall }Y.C$ after choosing $Y$ distinct from $X$ and fresh for $B$, both endpoint substitutions, and the domains of the split context ${\mathrm{\Delta }}_0,{\mathrm{\Delta }}_1$. For arbitrary closed $D_0,D_1$ and $S:D_0\leftrightarrow D_1$, the extended judgment $$\varrho [Y\mapsto (D_0,D_1,S)]:{\varrho }_0[Y\mapsto D_0]\leftrightarrow {\varrho }_1[Y\mapsto D_1]\mathsf{over}{\mathrm{\Delta }}_0,{\mathrm{\Delta }}_1,Y$$ is formed without overwriting an existing entry. The left-hand universal clause invokes $$[[C[B/X]{]]}_{\varrho [Y\mapsto (D_0,D_1,S)]}.$$ The induction hypothesis turns this into $$[[C{]]}_{\varrho [Y\mapsto (D_0,D_1,S)][X\mapsto (B[{\varrho }_0],B[{\varrho }_1],[[B{]]}_{\varrho })]}.$$ Because $Y\notin \mathrm{ftv}(B)$, extending at $Y$ does not change $B[{\varrho }_i]$ or $[[B{]]}_{\varrho }$. The two extensions commute, so this is exactly the body relation under $${\varrho }^{+}[Y\mapsto (D_0,D_1,S)]:{\varrho }_0^{+}[Y\mapsto D_0]\leftrightarrow {\varrho }_1^{+}[Y\mapsto D_1]\mathsf{over}{\mathrm{\Delta }}_0,{\mathrm{\Delta }}_1,Y,$$ which is the right-hand universal clause. The endpoint equation is the type-substitution composition equation of equation 5.2. ◻

The abstraction theorem

An open term must be closed twice, once at each endpoint. The two closing substitutions are not assumed equal; their corresponding entries are assumed related.

Thus ${\gamma }_0[[\mathrm{\Gamma }{]]}_{\varrho }{\gamma }_1$ is not an application of the type-relation notation to a context: it denotes the pointwise lifting of the already defined type relations to a pair of closing substitutions.

The theorem’s notation is now all defined: The suffix “over $\mathrm{\Delta }$” distinguishes a relation environment from a single relation $R:A\leftrightarrow B$.

For example, if $\mathrm{\Gamma }=x:X,f:X\to Y$, then related closing substitutions provide $$[{\gamma }_0(x)]R_X[{\gamma }_1(x)],[{\gamma }_0(f)](R_X\Rightarrow R_Y)[{\gamma }_1(f)].$$ The second hypothesis can be applied to the first, yielding related interpretations of $fx$. The abstraction theorem says that every typing derivation is built from this same operation.

Proof of Theorem 6.10 — Abstraction theorem

Proof. Induct on the Church-style typing derivation. There are five final-rule cases. The two rules for the universal type use lemma 6.8; the other three unfold the variable or arrow clause directly.

Variable. If the last rule reads $x:B\in \mathrm{\Gamma }$, the conclusion is exactly the $x:B$ component of ${\gamma }_0[[\mathrm{\Gamma }{]]}_{\varrho }{\gamma }_1$.

Arrow introduction. Suppose the last premise is $\mathrm{\Delta };\mathrm{\Gamma },x:B⊢u:C$. Choose the binder $x$ fresh for the finite ranges of ${\gamma }_0$ and ${\gamma }_1$. To prove the arrow relation, take arbitrary closed $a,b$ with $[a][[B{]]}_{\varrho }[b]$. The extended substitutions $${\gamma }_0[x\mapsto a],{\gamma }_1[x\mapsto b]$$ are related at $\mathrm{\Gamma },x:B$. The induction hypothesis gives related bodies at $[[C{]]}_{\varrho }$. Term beta gives, at each endpoint, $$(\lambda x:B[{\varrho }_i].u[{\varrho }_i][{\gamma }_i])a_i{=}_{\beta }u[{\varrho }_i][{\gamma }_i[x\mapsto a_i]],$$ where $a_0=a$ and $a_1=b$. This is the required arrow clause. The equality on the right uses the term/term substitution-composition equation of equation 5.2, after the displayed binder has been freshened.

Arrow elimination. The operator induction hypothesis gives a pair in $[[B{]]}_{\varrho }\Rightarrow [[C{]]}_{\varrho }$; the argument induction hypothesis gives a pair in $[[B{]]}_{\varrho }$. Applying the definition of arrow lifting gives the conclusion at $[[C{]]}_{\varrho }$.

Universal introduction. Suppose the premise is $\mathrm{\Delta },X;\mathrm{\Gamma }⊢u:B$, with $X$ fresh for $\mathrm{\Delta }$. Let closed $C_0,C_1$ and a relation $S:C_0\leftrightarrow C_1$ be arbitrary. Extend $\varrho$ to $${\varrho }^{\prime }:=\varrho [X\mapsto (C_0,C_1,S)].$$ Every declaration type in $\mathrm{\Gamma }$ was formed under $\mathrm{\Delta }$, so it contains no free $X$. By lemma 6.7, the original ${\gamma }_0,{\gamma }_1$ remain related at $\mathrm{\Gamma }$ under ${\varrho }^{\prime }$. Apply the induction hypothesis to the premise. On endpoint $i$, the resulting body is beta-convertible to the type application of the substituted abstraction: $$((\mathrm{\Lambda }X.u)[{\varrho }_i][{\gamma }_i])[C_i]{=}_{\beta }u[{\varrho }_i,X\mapsto C_i][{\gamma }_i].$$ Type and term substitution commute because every ${\gamma }_i(x)$ is closed; this is the last equation of equation 5.2. Since $C_0,C_1,S$ were arbitrary, the universal relation holds.

Universal elimination. Suppose the premise has type $\mathrm{\forall }X.B$ and the supplied type is $C$. The operator induction hypothesis is a pair in $[[\mathrm{\forall }X.B{]]}_{\varrho }$. Instantiate its defining universal quantifier with $$C[{\varrho }_0],C[{\varrho }_1],[[C{]]}_{\varrho }.$$ The resulting relation is $$[[B{]]}_{\varrho [X\mapsto (C[{\varrho }_0],C[{\varrho }_1],[[C{]]}_{\varrho })]}.$$ By lemma 6.8, it is exactly $[[B[C/X]{]]}_{\varrho }$, the relation required by the conclusion. For $i=0,1$, the endpoint term printed by the conclusion is the same alpha-class as the endpoint term just obtained: The two annotations invoke, respectively, the type-application substitution clause and the term/type substitution-composition equation of equation 5.2; the latter applies because every ${\gamma }_i(x)$ is closed. The variable, arrow-introduction, arrow-elimination, universal-introduction, and universal-elimination cases exhaust the Church typing derivation. ◻

The universal-elimination case is short only because its substitution equation was proved first. Without that lemma one obtains related terms at a relation with the right ingredients but no established connection to the result type printed by F-All-E.

Proof of Corollary 6.11 — Self-parametricity

Proof. Use theorem 6.10 with empty type and term environments. Replacement is legitimate because every relation was defined on beta-classes. ◻

Self-parametricity gives the relation needed to prove the opening equation without normalizing $h$.

Proof of Proposition 6.12 — The polymorphic endomap is pointwise the identity

Proof. Apply self-parametricity and instantiate the universal clause with the singleton relation $$S:=\{([a],[a])\},S:A\leftrightarrow A.$$ The arrow clause sends the unique input pair to an output pair in $S$. Membership in this singleton says $$h[A]a{=}_{\beta }a.$$ ◻

Proof of Corollary 10.15 — Unary preservation

Proof. By proposition 6.12, $h[A]a{=}_{\beta }a$, so the two terms determine the same beta class. Equivalently, instantiate self-parametricity with the diagonal relation on the classes in $P$. ◻

Thus unary preservation is obtained as a corollary of the binary theorem. A unary logical relation could prove it directly, but would not compare two different representations.

The empty relation is equally useful.

Proof of Corollary 6.13 — Parametric emptiness

Proof. If $v:\mathrm{\forall }X.X$ were closed, self-parametricity would allow the universal clause to be instantiated with the empty relation $\varnothing :{\mathsf{Bool}}_F\leftrightarrow {\mathsf{Bool}}_F$. It would then assert $[v[{\mathsf{Bool}}_F]]\varnothing [v[{\mathsf{Bool}}_F]]$, which is impossible. ◻

This is a second relative-consistency proof for pure Church-style System F in the classical ZF metatheory fixed in chapter 5. Unlike corollary 5.36, it does not use strong normalization: the contradiction follows from the syntactic abstraction theorem and the empty external relation alone.

The failure of unrestricted identity extension

It is tempting to expect $$[[A{]]}_{ϵ}={\mathsf{Eq}}_A$$ for every closed $A$. Equation (6.3) is called identity extension at $A$. Self-parametricity proves the inclusion from right to left. The reverse inclusion is false for beta equality. Before constructing the counterexample, proposition 6.14 proves the two observation instances used in proposition 6.15.

Proof of Proposition 6.14 — Identity extension at Church observations

Proof. The inclusions from right to left are corollary 6.11. For the converse, first suppose $[u][[{\mathsf{Bool}}_F{]]}_{ϵ}[v]$. Normalize $u$ and $v$. By proposition 5.39, each normal form is ${\mathsf{true}}_F$ or ${\mathsf{false}}_F$. Unfolding the encoded Boolean gives Take $C=D={\mathsf{Bool}}_F$ and in the universal clause choose $${\mathsf{Eq}}_{{\mathsf{Bool}}_F}:{\mathsf{Bool}}_F\leftrightarrow {\mathsf{Bool}}_F$$ and then choose the related branch pairs $({\mathsf{true}}_F,{\mathsf{true}}_F)$ and $({\mathsf{false}}_F,{\mathsf{false}}_F)$. The two resulting eliminations must be beta-equal. They reduce to the chosen normal forms of $u$ and $v$, so those normal forms are the same boolean. Concretely, for either Boolean normal form $b$, $$b[{\mathsf{Bool}}_F]{\mathsf{true}}_F{\mathsf{false}}_F{=}_{\beta }b;$$ the two eliminations therefore expose the normal forms being compared.

For naturals, normalize and use the same proposition to write the normal forms as $\bar{m}$ and $\bar{n}$. In the universal clause choose ${\mathsf{Eq}}_{{\mathsf{Nat}}_F}$, the related zero pair, and the pair $({\mathsf{succ}}_F,{\mathsf{succ}}_F)$. The latter lies in ${\mathsf{Eq}}_{{\mathsf{Nat}}_F}\Rightarrow {\mathsf{Eq}}_{{\mathsf{Nat}}_F}$ by compatible beta conversion. The two iterator results are therefore beta-equal, but they reduce to $\bar{m}$ and $\bar{n}$. For an endomap $f$, write $f^{0}a=a$ and $f^{k+1}a=f(f^{k}a)$. The required iterator computation follows by induction on the numeral spine: $$\bar{k}[{\mathsf{Nat}}_F]\bar{0}{\mathsf{succ}}_F{⟶}_{\beta }^{\ast }{\mathsf{succ}}_F^k\bar{0}{⟶}_{\beta }^{\ast }\bar{k}.$$ The base case contracts the three encoding binders to $\bar{0}$; the successor case exposes one additional application of ${\mathsf{succ}}_F$ and uses the induction hypothesis on the remaining spine. Uniqueness of normal forms gives $m=n$. ◻

Proof of Proposition 6.15 — Failure of unrestricted beta identity extension

Proof. By corollary 6.13, $\mathsf{Tm}({\mathsf{Void}}_F)$ is empty. Hence the domain relation $[[{\mathsf{Void}}_F{]]}_{ϵ}$ has no pairs. The implication in the arrow lifting is therefore vacuous, so it relates the two displayed functions. They are distinct beta-normal forms, and theorem 5.38 shows that they are not beta-convertible. ◻

The missing principle is extensionality. For simple types alone, a first-order set interpretation may take arrows to be full function sets and prove $${\mathsf{Eq}}_S\Rightarrow {\mathsf{Eq}}_T={\mathsf{Eq}}_{S\to T}$$ using function extensionality: two set-theoretic functions are equal when they agree at every argument. Reynolds’ obstruction says that this simple model cannot be extended with System F’s impredicative universal type. A parametric semantic model may validate its own identity-extension lemma. The syntactic beta-quotient used here does not validate the general equation.

Free theorems by choosing a relation

Consequences obtained by choosing a relation are called free theorems because the type alone yields them through the abstraction theorem; the polymorphic program’s text is never inspected.

The abstraction theorem is fixed; its applications differ mainly in the relation one chooses. We give two calculations in full.

Proof of Proposition 6.16 — Polymorphic application

Proof. Self-parametricity permits two relation choices. At $X$, choose $$R:=\{([a],[a])\},R:A\leftrightarrow A;$$ at $Y$, choose $$S:=\{([fa],[fa])\},S:B\leftrightarrow B.$$ Thus the two universal clauses use equal endpoint types $(A,A)$ and then $(B,B)$; heterogeneous endpoints are available but not needed here. The sole premise in the definition of $R\Rightarrow S$ shows $[f](R\Rightarrow S)[f]$. Applying the resulting arrow relation first to $f$ and then to the unique $R$-pair puts $([q[A][B]fa],[q[A][B]fa])$ in $S$. Membership in $S$ is the claimed beta equation. ◻

The abstraction theorem also implies iterator naturality (theorem 6.17) without classifying the normal form of $h$.

Proof of Theorem 6.17 — Iterator naturality

Proof. By lemma 6.3, the hypothesis is exactly $$[f](\mathsf{Gr}(k)\Rightarrow \mathsf{Gr}(k))[g].$$ Also $[a]\mathsf{Gr}(k)[ka]$. Self-parametricity of $h$, instantiated at the heterogeneous relation $\mathsf{Gr}(k):A\leftrightarrow B$, may therefore be read explicitly as $$[h[A]]((\mathsf{Gr}(k)\Rightarrow \mathsf{Gr}(k))\Rightarrow (\mathsf{Gr}(k)\Rightarrow \mathsf{Gr}(k)))[h[B]].$$ Apply this relation first to $f,g$ and then to $a,ka$. It yields $$[h[A]fa]\mathsf{Gr}(k)[h[B]g(ka)],$$ which unfolds to the desired equation. ◻

The normal-form argument proves this iterator equation by classifying every beta-normal inhabitant of the particular type, separating an eta-short case, and then inducting on an exponent. The abstraction theorem instead follows by one induction on the typing of an arbitrary System F term. Instantiating its relation variable with the graph relation records, in the relation itself, the invariant used by the normal-form proof.

When the chosen relation is $\mathsf{Gr}(k)$, the last calculation says that the operations commute with change of representation along $k$: it is the commuting-square property called naturality. No categorical definition is needed for the proof here; the two uses of arrow lifting are the square written elementwise.

Representation independence

An abstract counter supplies an initial state, a step operation, and an observer. A client that works for every representation type has the Church type $$\mathsf{Client}:=\mathrm{\forall }O.\mathrm{\forall }X.X\to (X\to X)\to (X\to O)\to O.$$ The result type $O$ is also quantified. This lets an application choose the exact observation relation it needs, without invoking general identity extension.

Proof of Theorem 6.18 — Counter representation independence

Proof. Apply self-parametricity of $c$. Instantiate its outer universal clause at $O_0,O_1$ with the relation $S$, and its inner universal clause at $A,B$ with $R$. The remaining type is a chain of three arrows. Apply its relation successively as follows: The result is the asserted $S$-pair. When $S$ is beta identity, membership is beta equality by definition. ◻

Now compare two concrete implementations. Put $$A:={\mathsf{Nat}}_F,B:={\mathsf{Nat}}_F{\times }_F{\mathsf{Bool}}_F.$$ These are the hidden state types. Define their operations by The second representation stores a redundant boolean. Relate the states by $$[n]R[p]⟺p{=}_{\beta }⟨n,{\mathsf{false}}_F{⟩}_F.$$ Then $[i_A]R[i_B]$ by definition. If $[n]R[p]$, the product beta laws give $$s_{B}p{=}_{\beta }⟨{\mathsf{succ}}_{F}n,{\mathsf{false}}_F{⟩}_F,$$ so $[s_{A}n]R[s_{B}p]$. The same hypothesis and the first projection beta law give $$r_{A}n\stackrel{definitionof{r}_A}{=}n\stackrel{(6.5)and{\times }_F-\beta }{=}{\mathsf{fst}}_F(p)\stackrel{definitionof{r}_B}{=}{r}_{B}p.$$ Thus $$[s_A](R\Rightarrow R)[s_B],[r_A](R\Rightarrow {\mathsf{Eq}}_{{\mathsf{Nat}}_F})[r_B].$$ The theorem applies with $O={\mathsf{Nat}}_F$ and $S={\mathsf{Eq}}_{{\mathsf{Nat}}_F}$.

For a visible client, take $$c_2:=\mathrm{\Lambda }O.\mathrm{\Lambda }X.\lambda i:X.\lambda s:X\to X.\lambda r:X\to O.r(s(si)).$$ With the first implementation, $$c_2[{\mathsf{Nat}}_F][A]i_A{s}_A{r}_A{⟶}_{\beta }^{\ast }\bar{2}.$$ With the second, two applications of $s_B$ produce $⟨\bar{2},{\mathsf{false}}_F{⟩}_F$, and the observer projects its first component: $$c_2[{\mathsf{Nat}}_F][B]i_B{s}_B{r}_B{⟶}_{\beta }^{\ast }{\mathsf{fst}}_F(⟨\bar{2},{\mathsf{false}}_F{⟩}_F){⟶}_{\beta }^{\ast }\bar{2}.$$ Representation independence says the same for every closed, well-typed client of (6.4), not merely for this example.

Where the proof stops

The interpretation is structural because types are finite syntax trees, and the relation-preservation induction is uncluttered because the language is pure and has no exceptional constants. Strong normalization entered in proposition 6.14, where canonical forms turned related Church observations into beta equality. Four nearby extensions break four different lines of this account.

1. A hypothetical primitive typecase, with syntax such as $$\mathsf{typecase}X\mathsf{of}\{\begin{array}{l}C\mapsto {\mathsf{true}}_F,\\ \mathrm{\_}\mapsto {\mathsf{false}}_F,\end{array}$$ where $\mathrm{\_}$ is a wildcard matching every type other than the preceding case, could define $d:\mathrm{\forall }X.{\mathsf{Bool}}_F$ whose operational observations at two distinct closed types $C,D$ choose different branches. Keep, however, the beta quotient used by definition 6.5; do not silently enlarge beta equality with a typecase computation equation. Then $d[C]$ and $d[D]$ are distinct typecase-headed beta-normal forms. If one nevertheless tried to validate the same relational clauses, the universal clause could be instantiated with any $R:C\leftrightarrow D$—the empty relation always exists. Because the result type ${\mathsf{Bool}}_F$ ignores $X$, it would require $$[d[C]][[{\mathsf{Bool}}_F{]]}_{ϵ}[d[D]].$$ Unfold the encoded-Boolean relation, choose ${\mathsf{Eq}}_{{\mathsf{Bool}}_F}$, and supply the related branch pairs $({\mathsf{true}}_F,{\mathsf{true}}_F)$ and $({\mathsf{false}}_F,{\mathsf{false}}_F)$. The resulting eliminations remain distinct typecase-headed beta-normal forms, so they are not related by beta identity. This is a direct beta-class counterexample; it neither infers a beta equation from the proposed operational observations nor invokes proposition 6.14. Thus a primitive typecase rule fails the universal case required by the abstraction theorem.

2. Suppose a polymorphic constant $\mathsf{fix}:\mathrm{\forall }X.(X\to X)\to X$ is added, with specializations $\mathsf{fix}[A]$ and the unfolding root $\mathsf{fix}[A]f⟶f(\mathsf{fix}[A]f)$. For the empty relation $R:A\leftrightarrow A$, the two identity functions are vacuously related by $R\Rightarrow R$, but their fixed points cannot be related by $R$. Relations for partial languages therefore require additional order-theoretic conditions; the present relations on terminating beta-classes contain no information about divergence or finite approximation.

3. Mutable state makes the meaning of “related arguments” depend on related heaps before and after evaluation. A world records the heap locations and invariants currently assumed, and the relation must be indexed by that world; the present arrow clause contains no such index.

4. For a recursive type $\mu X.A$, defining its relation by immediately recursing to $A[\mu X.A/X]$ is not structural recursion on a smaller type. This is the same failure of a decreasing structural call that impredicativity caused in section 5.7. Recursive-type semantics replace the simple induction with a construction that controls each recursive unfolding.

These are not four counterexamples to parametricity. They identify the data a stronger logical relation must remember.

The fixed-point obstruction determines the missing closure conditions.

Proof of Proposition 10.23 — Least fixed points preserve strict admissible relations

Proof. Monotonicity and leastness of the bottoms make both approximation sequences increasing. Strictness supplies the base pair ${\mathrm{\perp }}_{A}R{\mathrm{\perp }}_B$. The preservation hypothesis supplies the induction step, so $f^n({\mathrm{\perp }}_A)R{g}^n({\mathrm{\perp }}_B)$ for every $n$. Admissibility now gives $(\mu f)R(\mu g)$.

Continuity calculates $$f(\mu f)=f(\underset{n}{⨆}{f}^n({\mathrm{\perp }}_A))=\underset{n}{⨆}{f}^{n+1}({\mathrm{\perp }}_A)=\mu f;$$ the last equality holds because deleting the least first approximation does not change the supremum. If $f(a){\le }_{A}a$, induction gives $f^n({\mathrm{\perp }}_A){\le }_{A}a$ for every $n$, hence $\mu f{\le }_{A}a$. Thus $\mu f$ is the least fixed point. The same argument with $B,g$ proves the claim for $\mu g$. ◻

The orders, least elements, and chain limits in definition 10.22 belong to a domain semantics for partial computation; none is a hidden premise of the strongly normalizing calculus studied here.

Two established parametricity developments use richer formal interfaces. The following definitions delimit the comparison; no theorem from either interface is used in the abstraction proof above.

Finally distinguish three results that are often given the same name.

• The syntactic abstraction theorem proved here says that every derivable Church-style System F term preserves every external relation on closed typed beta-classes.

• A semantic parametric model equips every semantic element with a relational action. It may validate a genuine identity-extension lemma, but that requires the model’s extensional and coherence structure.

• An internal parametric theory places relations inside a richer type theory rather than keeping them solely in the metatheory. It validates internal terms and equations unavailable in bare System F.

The first result is enough for the free theorems and representation theorem above; the latter two describe strictly richer settings.

Bibliographic notes

Reynolds introduced the relational abstraction method and used it to prove independence of representations in [Rey83]; those pages also expose the identity-extension difficulty. The theorem above is the syntactic version for definition 5.4.

Wadler derives program equations from polymorphic types in [Wad89], states the relational theorem in [Wad89], and discusses fixpoints in [Wad89].

The formula grammar, relation quantifiers, definable relations, parametricity schema, and identity-extension principle isolated in definition 10.24 are the bounded interface of Plotkin and Abadi’s logic [PA93]. Their equality and axioms belong to that internal logic; the chapter does not import their identity-extension result into its beta-quotient.

The value/computation syntax, categorical hypotheses, admissible-relation closures, and Eilenberg–Moore example in definition 10.25 are recorded from Møgelberg and Simpson [MS09]. Their theorem concerns the PE model signature stated there, not bare Church-style System F.