System F, Impredicativity, and Normalization

Hindley–Milner polymorphism gives a let-bound variable a fresh monotype at each use. It does not make a polymorphic value into an ordinary argument. Three pieces of notation make that missing operation visible. The type $\mathrm{\forall }X.A$ describes a term that works at every type $X$; the term $\mathrm{\Lambda }X.t$ abstracts over that type; and $t[A]$ supplies the type $A$ to such an abstraction. The following display retains its annotations so that the three roles remain visible: $$(\lambda f:I.f[I]f)(\mathrm{\Lambda }X.\lambda x:X.x),I:=\mathrm{\forall }X.X\to X.$$ The right-hand argument is the polymorphic identity. Inside the left-hand abstraction, the parameter $f$ is first instantiated at the polymorphic type $I$ and then applied to itself. This is self-application, not recursion. Its three beta steps are: the outer lambda substitutes the identity for $f$, the type application substitutes $I$ for $X$, and the remaining lambda $\lambda x:I.x$ substitutes the identity for $x$ and returns it. Nevertheless its erasure cannot be typed by Algorithm W of definition 3.28. A lambda-bound variable has one monotype $\alpha$ there, and typing $ff$ demands $\alpha =\alpha \to \beta$, which fails the occurs check.

The remedy is to make abstraction over a type, and application to a type, part of the term language. In the annotated, or Church-style, calculus, those two operations remain in the term. Its annotations make checking syntax directed and its reductions make the opening calculation literal. Under Curry–Howard, types are propositions and terms are proofs. The logic is second-order because the formula $\mathrm{\forall }X.A$ quantifies over a proposition—represented here by the type variable $X$—rather than over an element of one fixed domain. Type abstraction introduces that quantified variable, and type application eliminates its universal quantifier.

The metatheory consists of mathematical statements about System F syntax, typing, and reduction, rather than formulas expressed inside System F. Unless a result states a smaller base theory, this chapter proves its metatheorems in classical ZF set theory. Finite syntax carries a fixed numerical coding. A Turing machine has finitely many states and tape symbols, an unbounded tape with one symbol under a read–write head, and a finite table that specifies the symbol to write, the next state, and the head’s next move. It computes an output when it halts. Accordingly, an “algorithm” here is such a machine that halts on every stated input code, and an “effective” translation is the total map on codes that it computes.

The Church-style calculus

Two sorts of variables

System F has term variables $x,y,z,\dots$ and type variables $X,Y,Z,\dots$. Confusing their two substitutions is a reliable way to make the universal rules look simpler than they are. We therefore keep separate contexts from the beginning.

Thus $\lambda x:X.x$ has the type variable $X$ free, whereas $\mathrm{\Lambda }X.\lambda x:X.x$ does not. The expression $\mathrm{\Lambda }X.\lambda x:Y.x$ is syntactically legal. If $Y$ has been declared available as a type variable, the expression has type $\mathrm{\forall }X.Y\to Y$. With no available type variables it is not typable, because the annotation $Y$ refers to an undeclared name. Syntax alone does not supply the missing scope.

The type-application substitution clause deserves attention. Substituting $B$ for $X$ in $t[A]$ changes both the operator $t$ and the supplied type $A$. Choose $C$ with a free $Y$, where $Y$ differs from $X$. Choose a type variable $Z$ fresh for $C$ and different from $X$. Renaming $Y$ to $Z$ prevents the type binder from capturing the free $Y$ of $C$. The alpha-renaming and substitution steps are Changing only the annotation in the lambda, or only the argument of the type application, would not define substitution on this syntax.

Formation and typing

Rule F-All-I does not need a separate side condition $X\notin \mathrm{ftv}(\mathrm{\Gamma })$. Its premise uses the unchanged context $\mathrm{\Gamma }$, which was already formed under $\mathrm{\Delta }$; context formation gives that freshness. If one allowed arbitrary unformed contexts, the rule would be unsound. For instance, the tempting derivation of $\mathrm{\Lambda }X.x:\mathrm{\forall }X.X$ from $x:X$ cannot even begin with a context $x:X$ formed under the empty type context. The obstruction occurs before typing: $$\cdot ⊬x:X\mathsf{ctx},\text{so there is no premise from which F-All-I can bind }X\text{.}$$ If the unformed declaration were admitted, the locally bound type name would escape through the unchanged declaration of $x$. This is a scope error, not a closed program whose evaluation happens to get stuck.

Now type the opening term. Put $$\mathsf{id}:=\mathrm{\Lambda }X.\lambda x:X.x,d:=\lambda f:I.f[I]f.$$ The identity has the derivation $$\frac{{\displaystyle \frac{{\displaystyle \frac{x:X\in x:X}{X;x:X⊢x:X}}\mathrm{F}-\mathrm{Var}}{X;\cdot ⊢\lambda x:X.x:X\to X}}\mathrm{F}-\mathrm{Arr}-\mathrm{I}}{\cdot ;\cdot ⊢\mathsf{id}:I}\mathrm{F}-\mathrm{All}-\mathrm{I}.$$ For the body of $d$, universal elimination at the type $I$ gives $$\frac{\begin{array}{c}\cdot ;f:I⊢f:\mathrm{\forall }X.X\to X\\ \cdot ⊢I\mathsf{type}\end{array}}{\cdot ;f:I⊢f[I]:I\to I}\mathrm{F}-\mathrm{All}-\mathrm{E}.$$ Together with $f:I$, arrow elimination gives $f[I]f:I$; hence $d:I\to I$ and the complete expression $d\mathsf{id}$ has type $I$. The decisive step is the instantiation $X:=I$. An impredicative quantifier ranges over types that themselves contain the same kind of quantifier; hence the universal quantifier of System F is impredicative. A predicative design instead stratifies types into levels and permits quantification only over a lower level. The reducibility family in chapter 2 recursed on a type: its arrow clause used only the immediate component types. A universal clause would have to interpret $A[B/X]$ for every formed $B$, including $I$; that type need not be a strict subexpression of $\mathrm{\forall }X.A$ and can contain more type constructors. The subexpression recursion used in chapter 2 does not license those calls, so the normalization argument needs a different construction.

Structural lemmas

There are two binders and therefore two substitution lemmas. Type substitution must transform the types stored in a term context; term substitution does not. Proving the easy lemma first prevents the two operations from being mixed in the preservation proof.

Proof of Lemma 5.5 — Scope and weakening

Proof. For item 1, induct on the typing derivation simultaneously with type and context formation. The variable leaf uses the formation derivation of its declaration. At F-All-I, the bound type variable is removed from the free-variable set in the conclusion; at F-All-E, the premise $\mathrm{\Delta }⊢B\mathsf{type}$ ensures that every free variable of the type argument lies in $\mathrm{\Delta }$. At F-Arr-I, the induction hypothesis bounds the body’s free variables, while formation of $\mathrm{\Gamma },x:A$ gives $\mathrm{ftv}(A)\subseteq \mathrm{dom}(\mathrm{\Delta })$ for the lambda annotation. These are the only binder-specific scope cases.

For item 2, induct on typing. In the variable case the old membership is unchanged. In an F-Arr-I case, alpha-rename the lambda binder away from $y$ before applying the induction hypothesis to the premise; the extended context then retains distinct variable names. For context formation, induct on the length of the suffix ${\mathrm{\Gamma }}_1$. The empty suffix is immediate. If ${\mathrm{\Gamma }}_1={\mathrm{\Gamma }}_1^{\prime },z:C$, insert $y:B$ before ${\mathrm{\Gamma }}_1^{\prime }$ by the induction hypothesis and then rebuild the final declaration $z:C$ with F-$\mathrm{\Gamma }$-Ext. For item 3, first induct on type and context formation, and then on typing. At a universal binder choose its name fresh for the inserted variable and use the induction hypothesis in the doubly extended type context. The argument uses neither a conversion rule that changes the derived type nor an exchange rule that that reorders context declarations: it constructs the weakened derivation under the extended context directly. ◻

Proof of Lemma 5.6 — Type substitution

Proof. Type substitution preserves formation and typing. Type formation is an induction on its derivation. At a type-variable leaf, the distinguished variable becomes $C$ and uses the weakening of its given formation derivation through ${\mathrm{\Delta }}_1$; every other variable remains a variable. Arrow formation uses the two induction hypotheses. At $\mathrm{\forall }Y.A$, first choose $Y\ne X$ fresh for $C,{\mathrm{\Delta }}_0,{\mathrm{\Delta }}_1$. The induction hypothesis applies under $Y$ and F-Ty-All reattaches the binder. Context formation follows declaration by declaration from item 1.

For typing, induct on the final rule. The variable case uses the corresponding declaration in $\mathrm{\Gamma }[C/X]$. Arrow introduction and elimination use the induction hypotheses, with the term binder freshened if needed. At universal introduction, display its bound variable as $Y\ne X$, fresh for $C$; apply the induction hypothesis under ${\mathrm{\Delta }}_0,X,{\mathrm{\Delta }}_1,Y$ and reapply F-All-I.

The only calculation occurs at universal elimination. Its premise has $t:\mathrm{\forall }Y.A_0$ and a formed argument $B$. After the induction hypothesis we obtain $$t[C/X]:(\mathrm{\forall }Y.A_0)[C/X]=\mathrm{\forall }Y.A_0[C/X]$$ and $B[C/X]$ is formed by item 1. Elimination therefore returns $$A_0[C/X][B[C/X]/Y].$$ After freshening $Y$ away from $C$, the substitution-composition equation of convention 5.2 gives $A_0[C/X][B[C/X]/Y]=(A_0[B/Y])[C/X]$, the required conclusion. ◻

Proof of Lemma 5.7 — Term substitution

Proof. Induct on the typing derivation of $t$. At a variable leaf, the distinguished variable is replaced by the weakened derivation of $u$; another variable remains a variable. Arrow introduction first freshens its binder away from $u$ and applies the induction hypothesis under the extended context. Arrow elimination applies the two hypotheses. Universal introduction freshens its type binder away from all type variables in the derivation $\mathrm{\Delta };{\mathrm{\Gamma }}_0⊢u:A$, uses lemma 5.5(3) to weaken that derivation in the new type context, and applies the induction hypothesis. Universal elimination changes only the operator term, so its induction hypothesis and the old type-formation premise reapply the rule. ◻

Evaluation and safety

Type abstraction is computationally inert until a type is supplied. It is therefore a value, just as a term abstraction is. Type application does not inspect the run-time representation of its type argument; it merely removes an annotation-level binder.

The opening term now performs the promised calculation: The type argument $I$ leaves no run-time component.

Proof of Lemma 5.9 — Canonical forms

Proof. Invert the final typing rule after observing that the two type constructors $\to$ and $\mathrm{\forall }$ are disjoint and injective. A lambda can only end in F-Arr-I, and a type abstraction only in F-All-I; variables are impossible in the empty term context. Thus the outer constructor of the type selects the corresponding value form. ◻

Proof of Theorem 5.10 — Preservation

Proof. Induct on the evaluation-context decomposition of the step. Congruence cases rebuild the same typing rule from the induction hypothesis. There are two redexes.

For term beta, inversion gives $$\mathrm{\Delta };\mathrm{\Gamma },x:B⊢s:A,\mathrm{\Delta };\mathrm{\Gamma }⊢v:B.$$ Term substitution yields $\mathrm{\Delta };\mathrm{\Gamma }⊢s[v/x]:A$.

For type beta, inversion gives $$\mathrm{\Delta },X;\mathrm{\Gamma }⊢s:B,\mathrm{\Delta }⊢C\mathsf{type},$$ where context formation entails $X\notin \mathrm{ftv}(\mathrm{\Gamma })$. Type substitution, with empty trailing type context, yields $\mathrm{\Delta };\mathrm{\Gamma }⊢s[C/X]:B[C/X]$, which is exactly the type assigned to $(\mathrm{\Lambda }X.s)[C]$ by F-All-E. ◻

Proof of Theorem 5.11 — Progress

Proof. Induct on the typing derivation. A variable case is impossible. Both introduction forms are values. For $t_1{t}_2$, apply the two induction hypotheses from left to right. A step in either premise gives an evaluation context step. If both are values and the operator has arrow type, canonical forms gives $t_1=\lambda x:B.s$, so term beta applies.

For $t_0[C]$, the induction hypothesis either steps $t_0$, giving the context $[][C]$, or returns a value. Its type is universal, so canonical forms gives $t_0=\mathrm{\Lambda }X.s$ and type beta applies. These cases exhaust the typing rules. ◻

Proof of Corollary 5.12 — Safety

Proof. Repeated preservation types $u$ at $A$; progress says that $u$ is a value or takes another step. ◻

Safety does not yet say that evaluation terminates. Progress permits an infinite sequence of well-typed steps. The strong normalization theorem later in this chapter rules those sequences out for the larger compatible beta relation, and therefore for call-by-value evaluation as well.

Data represented by quantification

Call-by-value reduction deliberately stops beneath abstractions. Equations between encoded programs require a relation that may calculate in every subterm. We fix it before introducing the encodings.

The preservation proof for ${⟶}_{\beta }$ repeats theorem 5.10; reducing beneath a binder uses its premise typing derivation, and the two contractions use the same substitution lemmas. We record the result because every calculation below uses it.

Proof of Proposition 5.14 — Subject reduction for compatible beta

Proof. Induct on the generation of the compatible step. The term- and type-beta roots are exactly the two cases of the preservation proof. For closure under application and type application, rebuild F-Arr-E or F-All-E. For closure under $\lambda$ and $\mathrm{\Lambda }$, apply the induction hypothesis in the extended term or type context and rebuild the corresponding introduction rule. Application-left, application-right, type-application, term-abstraction, and type-abstraction are precisely the compatible-context constructors. ◻

Booleans

A boolean chooses one of two continuations. The tempting monomorphic type $X\to X\to X$ gives two selectors at one fixed $X$, but the same selector cannot then be used once at $A$ and once at $B$. Abstracting the result type repairs precisely that failure: quantifying over the common result type makes the choice usable at every result type.

Two applications of F-Arr-I abstract the two value variables, and F-All-I then gives $$\cdot ;\cdot ⊢{\mathsf{true}}_F:{\mathsf{Bool}}_F,\cdot ;\cdot ⊢{\mathsf{false}}_F:{\mathsf{Bool}}_F.$$ If $\mathrm{\Delta };\mathrm{\Gamma }⊢b:{\mathsf{Bool}}_F$ and $\mathrm{\Delta };\mathrm{\Gamma }⊢u,v:A$, then universal elimination followed by two arrow eliminations gives $\mathrm{\Delta };\mathrm{\Gamma }⊢{\mathsf{if}}_A(b;u,v):A$. The computations expose all three beta steps: Call a term beta-normal when no compatible beta step applies, and call a beta-normal term variable-headed when it is built from a free term variable by term and type applications. If $b$ is variable-headed, then $b[A]uv$ has no beta redex at its head. The typing rules provide two branches, but do not guess which branch the variable will select. The broader technical notion needed for beta expansion is given in definition 5.24.

Products and sums

A monomorphic consumer type $(A\to B\to X)\to X$ fixes one result type and therefore cannot support both projections when $A\ne B$. Quantifying $X$ makes every consumer available. Dually, a sum is determined by what every pair of branch functions does with its injection.

The introduction derivation ends in F-All-I; its premise types $kab:X$ under $a:A,b:B,k:A\to B\to X$. Universal elimination gives $p[A]:(A\to B\to A)\to A$, so the first projection has type $A$; the second projection is typed by instantiating at $B$ and supplying the selector $\lambda a:A.\lambda b:B.b:A\to B\to B$. For the first beta law, The second beta law exposes the changed result type and selector:

The corresponding monomorphic sum candidate $(A\to C)\to (B\to C)\to C$ fixes its branch result $C$. A value built at that type cannot later be eliminated once to $C$ and once to a different type $D$. Universal quantification must therefore abstract the branch result type as well.

If $f:A\to C$ and $g:B\to C$, then ${\mathsf{case}}_C(s;f,g):C$. The two constructor calculations are

The beta laws above describe constructor followed by eliminator. They do not yet supply a product uniqueness law $⟨{\mathsf{fst}}_F(p),{\mathsf{snd}}_F(p){⟩}_F{=}_{\beta }p$, nor a commuting conversion that pushes an outer elimination into both branches of a variable-headed sum case. For example, such a conversion would identify $$q({\mathsf{case}}_C(s;f,g))\text{with}{\mathsf{case}}_D(s;\lambda a:A.q(fa),\lambda b:B.q(gb)).$$ It is also useful to name the dual of a beta law. A beta law computes an eliminator applied to a constructor; an eta, or uniqueness, law reconstructs an object from all its observations. Its function and product forms are $$\lambda x:A.fx=f(x\notin \mathrm{fv}(f)),⟨\mathsf{fst}(p),\mathsf{snd}(p)⟩=p.$$ These equations are not generated by the beta relation of definition 5.13. Call $f$ or $p$ in these equations eta-short; applying the corresponding eta-expansion produces the reconstructed term on the left. The compatible beta equality ${=}_{\beta }$, the symmetric transitive closure of definition 5.13, does not identify that expansion with its eta-short source. When $f$ and $p$ are variables, both $f$ and $\lambda x.fx$, and both $p$ and $⟨\mathsf{fst}(p),\mathsf{snd}(p)⟩$, are beta-normal and syntactically distinct. The encodings reproduce the constructor computations, not every judgmental equation one might choose for primitive products and sums.

Natural numbers

A natural number is an instruction to iterate an endomap—a function from a type to itself—starting at a chosen point. The monomorphic candidate $A\to (A\to A)\to A$ can iterate only at its fixed carrier $A$. The same numeral cannot then count once in $\mathsf{Nat}$ and once in ${\mathsf{Bool}}_F$. Quantifying the carrier is the missing move.

The numeral and successor terms have types $${\mathsf{zero}}_F:{\mathsf{Nat}}_F,{\mathsf{succ}}_F:{\mathsf{Nat}}_F\to {\mathsf{Nat}}_F.$$ If $z:A$ and $s:A\to A$, then $n[A]zs:A$. The two iterator equations are calculations rather than additional rules: This is the general meaning of a Church encoding: an encoded datum is the operation that folds it. Here $n[A]zs$ is simultaneously the eliminator and the fold of $n$, with algebra data $z:A$ and $s:A\to A$. Write $\bar{n}$ for the result of applying ${\mathsf{succ}}_F$ to ${\mathsf{zero}}_F$ exactly $n$ times.

Addition can now be discovered rather than guessed. To add $m$ to $n$, start the $m$-fold iteration after the $n$-fold iteration has already been performed: $$\begin{array}{r}{\mathsf{add}}_F:=\lambda m:{\mathsf{Nat}}_F.\lambda n:{\mathsf{Nat}}_F.\mathrm{\Lambda }X.\lambda z:X.\lambda s:X\to X.m[X](n[X]zs)s.\end{array}$$ Its type is ${\mathsf{Nat}}_F\to {\mathsf{Nat}}_F\to {\mathsf{Nat}}_F$. For example, $${\mathsf{add}}_F\bar{1}\bar{2}{⟶}_{\beta }^{\ast }\mathrm{\Lambda }X.\lambda z:X.\lambda s:X\to X.s(s(sz)){⟵}_{\beta }^{\ast }\bar{3}.$$ Notice what was proved: addition computes on displayed numerals. The term ${\mathsf{add}}_F{\mathsf{zero}}_{F}n$ expands to a type and two term abstractions around $n[X]zs$; beta reduction alone does not remove those abstractions when $n$ is variable-headed. Explicitly, $${\mathsf{add}}_F{\mathsf{zero}}_{F}n{⟶}_{\beta }^{\ast }\mathrm{\Lambda }X.\lambda z:X.\lambda s:X\to X.n[X]zs,$$ which is beta-normal when $n$ is a variable but is not literally $n$.

The Curry-style judgment

Erasing type abstractions and applications leaves an ordinary untyped lambda term. One can nevertheless assign System F types to that raw term by allowing universal introduction and elimination to occur in a derivation without leaving syntax behind. This is a different calculus, not shorthand for the Church rules.

The raw identity $\lambda x.x$ has type $X\to X$ under type context $X$, and then C-All-I gives it type $I$ in the empty type context. The same raw term also has many monomorphic types. A Curry term therefore does not determine where polymorphism was introduced or eliminated.

Proof of Theorem 5.21 — Erasure and decoration

Proof. For item 1, induct on the Church typing derivation. Variable, lambda, and application rules erase to their Curry counterparts. A Church type abstraction erases its constructor and the induction hypothesis is followed by C-All-I. A Church type application likewise erases and is followed by C-All-E with the same type argument.

For item 2, induct on the Curry derivation and construct the decoration. At a variable use the same variable. At arrow introduction, decorate the premise to $t$ and use $\lambda x:A.t$; at arrow elimination, decorate both premises and apply the resulting terms. At C-All-I, decorate the premise to $t$ and return $\mathrm{\Lambda }X.t$. At C-All-E, decorate the premise to $t$ and return $t[B]$. Each construction has erasure $m$ because the two universal constructors erase. These five cases are all the Curry rules. ◻

For the opening expression, the Curry derivation decorates its two occurrences of $f$ differently: the function occurrence becomes $f[I]$ and the argument occurrence remains $f$. Erasure forgets this choice and returns $(\lambda f.ff)(\lambda x.x)$. Algorithm W cannot reconstruct the choice because it insists that a lambda-bound $f$ have a monotype.

Checking and inference are different problems

For Church syntax, every polymorphic choice is written. A checker follows the outer term constructor, recursively computes one type, and compares finite type trees modulo alpha-equivalence.

Proof of Proposition 5.22 — Decidable Church checking

Proof. First decide $\mathrm{\Delta }\mathsf{typectx}$ and $\mathrm{\Delta }⊢\mathrm{\Gamma }\mathsf{ctx}$ by their displayed formation rules; reject if either check fails. Then recurse on $t$. A variable looks up its unique declaration. For $\lambda x:A.u$, first decide formation of $A$, recurse on $u$ under $x:A$ after alpha-freshening $x$ away from $\mathrm{\Gamma }$, and return $A\to B$. For $t_1{t}_2$, recurse on both subterms; accept exactly when the first result is an arrow whose domain is alpha-equal to the second result. For $\mathrm{\Lambda }X.u$, alpha-freshen the displayed binder away from $\mathrm{\Delta }$, recurse under $X$, and return $\mathrm{\forall }X.A$. For $u[B]$, decide formation of $B$, recurse on $u$, and accept exactly when its result is $\mathrm{\forall }X.A$, returning $A[B/X]$. Each call is on a strict subterm; formation and alpha-equality of finite types are decidable by structural recursion. Induction on $t$ proves soundness, and inversion of the five typing rules proves completeness and uniqueness. ◻

The corresponding question for Curry syntax is harder because the input does not say where to insert C-All-I and C-All-E. There are two decision problems:

• typability: given $m$, does any $\mathrm{\Delta },\mathrm{\Gamma },A$ yield $\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{C}m:A$?

• Curry type checking: given $\mathrm{\Delta },\mathrm{\Gamma },m,A$, is the displayed judgment derivable?

The second phrase must not be confused with checking a fully annotated Church term.

Proof of Theorem 5.23 — Undecidability boundary

Proof. This is the one decision-theoretic import in the chapter. Wells proves the result for raw lambda terms, arrows, and universal types. His type-variable context is implicit: from our finite input one forgets $\mathrm{\Delta }$, while in the other direction one takes $\mathrm{\Delta }=\mathrm{ftv}(\mathrm{\Gamma },A)$ after checking scope. These translations are effective. Wells also works with canonical representatives that identify harmless permutations of independent quantifiers and erase a universal quantifier $\mathrm{\forall }X.A$ when $X\notin \mathrm{ftv}(A)$; such a quantifier is called vacuous. His comparison with ordinary type syntax proves that this canonical presentation does not alter derivability [Wel99]. His TYP and TC problems are, respectively, typability of a raw term and checking a supplied raw-term/type pair. They are therefore effectively equivalent to the two problems displayed above. Their effective equivalence and undecidability are [Wel99]. No consequence for the Church checker is being claimed. ◻

Thus the imported fact has one operational consequence for this chapter: the annotations and explicit type applications of Church syntax support the terminating checker above, while erasing them produces a Curry judgment for which even checking a proposed type is undecidable.

Strong normalization

Safety excludes stuck states, but not infinite calculation. Weak normalization merely supplies one path to a normal form and therefore cannot exclude a different divergent path. Strong normalization excludes every infinite beta sequence. We prove that every well-typed term admits no infinite sequence of compatible beta steps, even when reduction is allowed beneath both kinds of abstraction. Write $\mathsf{SN}$ provisionally for the System F terms with no infinite compatible beta-reduction sequence. The attempted type-indexed definition next fails at universal types, motivating the candidate-valued definition in definition 5.25.

A first attempt copies the simple-type proof. If reducibility at $A$ were already defined as a set ${\mathcal{R}}_A$, the tempting universal clause would be $$t\in {\mathcal{R}}_{\mathrm{\forall }X.A}⟺t\in \mathsf{SN}\text{ and }t[C]\in {\mathcal{R}}_{A[C/X]}\text{ for every closed type }C.$$ This is not a structural recursive definition. Take $A=X\to X$ and $C=I=\mathrm{\forall }Y.Y\to Y$. Defining ${\mathcal{R}}_I$ would require the not-yet-defined set ${\mathcal{R}}_{I\to I}$, whose index is larger than $I$, not a proper subexpression of it. In chapter 2, every recursive call was at a proper subexpression of the current type; impredicative instantiation destroys precisely that decrease.

The repair turns the old proof inside out. The three saturation properties proved for simple-type reducibility in lemma 2.40 become the definition of an admissible interpretation. We then quantify over every set satisfying them. Such a set is a reducibility candidate: a candidate for being the interpretation assigned to a type. The arbitrary candidate, not the syntax of a representing type, breaks the circle. The repaired interpretation recurses on the proper syntactic body $A$ of $\mathrm{\forall }X.A$ under an extended valuation. It never recurses on the substituted type $A[C/X]$ that caused the failed definition above.

The proof has four stages. First define the admissible candidate sets and prove that the operations needed by arrows and universals preserve them. Second interpret each type as a candidate under a valuation. Third prove the two expansion lemmas that run term and type introduction backwards. Finally induct on typing to obtain reducibility, and hence normalization.

A valuation assigns an arbitrary reducibility candidate and a closed type to each type variable. The interpretation of $\mathrm{\forall }X.A$ recurses on the proper body $A$ under every extension of that valuation, never on the larger substitution instance $A[C/X]$.

The proof uses the following operations. Their definitions appear in the order in which the four stages need them.

Candidates

Condition (CR3) includes variables: a variable is neutral and has no reducts, so it belongs to every candidate. If a neutral redex has all one-step reducts in $R$, the same condition puts the redex itself in $R$. This is beta expansion after all competing reductions have already been controlled. Without the neutrality side condition, every irreducible abstraction would belong to every candidate vacuously, and elimination could then create an uncontrolled root redex.

There is no size ambiguity in “every candidate.” Finite Church terms form a countable meta-level set, so candidates form a subcollection of its power set in the fixed classical ZF metatheory. The quantifier in the universal candidate construction below ranges over that fixed set; it is not a quantifier inside System F. The construction is nevertheless impredicative: the candidate being defined is itself among the candidates over which its membership condition may quantify. This is legitimate set formation by Separation—the axiom saying that a definable subcollection of a fixed set is itself a set—over the already fixed power set of terms, rather than a construction of that power set. No claim that this particular construction is predicative is intended.

The universal candidate construction below accepts a family $F(C,R)$ of a closed formed type and a candidate. Although $C$ does not occur syntactically in its membership test, the type component later closes annotations and type applications in the interpreted term, while $R$ determines which closed terms count as reducible at the quantified variable. Identifying these two jobs would make the interpretation recurse on substituted types and recreate the impredicative circularity above.

Proof of Lemma 5.26 — Elementary candidate constructions

Proof. For item 1, (CR1) follows from the definition and (CR2) because an infinite sequence from a reduct would extend to one from its predecessor. For (CR3), if a neutral term had an infinite reduction, its first reduct would also admit an infinite reduction, contradicting the assumption that every reduct lies in ${\mathsf{SN}}_0$.

Intersections inherit all three clauses pointwise. We prove the arrow case in detail. Its (CR1) is part of the definition. If $t$ is in $R\Rightarrow S$ and $t{⟶}_{\beta }{t}^{\prime }$, then $t^{\prime }$ is strongly normalizing. For $u\in R$, the step $tu{⟶}_{\beta }{t}^{\prime }u$ and (CR2) for $S$ give $t^{\prime }u\in S$; hence $t^{\prime }\in R\Rightarrow S$.

For (CR3), let $t$ be neutral and suppose every reduct of $t$ is in $R\Rightarrow S$. If $t$ had an infinite reduction, its first reduct would contradict (CR1) for $R\Rightarrow S$; hence $t$ is strongly normalizing. Fix $u\in R$ and induct on its reduction height $\nu (u)$. The application $tu$ is neutral. Each of its one-step reducts has one of two forms: $$t^{\prime }u(t{⟶}_{\beta }{t}^{\prime }),t{u}^{\prime }(u{⟶}_{\beta }{u}^{\prime }).$$ The first belongs to $S$ because $t^{\prime }\in R\Rightarrow S$. For the second, (CR2) gives $u^{\prime }\in R$ and , so the induction hypothesis applies. There is no root beta step because $t$ is not a lambda. Thus (CR3) for $S$ gives $tu\in S$.

For item 4, (CR1) is again built in. If $t$ takes a step, then so does $t[C]$ in its operator; (CR2) of every $F(C,R)$ proves closure. Finally let $t$ be neutral and all its reducts belong to $\mathrm{\forall }F$. It is strongly normalizing by the first-step argument. For fixed $C,R$, the term $t[C]$ is neutral. Its reducts are precisely $t^{\prime }[C]$ with $t{⟶}_{\beta }{t}^{\prime }$: no type beta occurs because $t$ is not a type abstraction. Every such reduct belongs to $F(C,R)$, so its (CR3) gives $t[C]\in F(C,R)$. Hence $t\in \mathrm{\forall }F$. ◻

Interpreting types

Proof of Lemma 9.28 — Candidate-component independence

Proof. Induct structurally on $A$, universally quantifying the valuation domains and both valuations in the induction hypothesis. Variables use the assumed candidate equality, and arrows use the two induction hypotheses. At $\mathrm{\forall }X.B$, extend both valuations by pairs $(C,R)$ having the same candidate component. For every closed $C$ and candidate $R$, the induction hypothesis gives $$[[B{]]}_{\eta [X\mapsto (C,R)]}=[[B{]]}_{{\eta }^{\prime }[X\mapsto (C,R)]}.$$ Intersecting these equal membership conditions proves the claim. ◻

The first component $C_X$ tells us what to substitute into the annotations of a term. The second component $R_X$ tells us which terms count as reducible at $X$. Identifying these two jobs would recreate the circularity: the set interpreting a type is not defined merely by inspecting the syntax of the closed type assigned to it. A candidate may therefore be assigned to any closed type, including a universal type syntactically larger than the type whose body is being interpreted. The phrase “assigned to a type” means precisely the pair $(C_X,R_X)$ in a valuation.

Here is the smallest useful calculation. Let $\eta (X)=(I,R_0)$, where $R_0$ is any candidate. Then The bound $Y$ ranges over a fresh pair $(C,R)$; the free $X$ continues to use the fixed pair $(I,R_0)$. This is the distinction that makes the universal clause impredicative without making its definition circular. For a concrete instance, take $R_0={\mathsf{SN}}_0$ and a term variable $x:I$. Then $$\mathrm{\Lambda }Y.\lambda y:Y.x\in [[\mathrm{\forall }Y.Y\to X{]]}_{X\mapsto (I,{\mathsf{SN}}_0)}.$$ Fix a closed $C$, a candidate $R$, and $u\in R$. Put $q_C:=(\mathrm{\Lambda }Y.\lambda y:Y.x)[C]$. By (CR1), $u\in {\mathsf{SN}}_0$, so its reduction height $\nu (u)$ is defined. The function $\lambda y:C.x$ is beta-normal; hence the immediate reducts of $(\lambda y:C.x)u$ are exactly $x$ and the terms $(\lambda y:C.x)u^{\prime }$ with $u{⟶}_{\beta }{u}^{\prime }$. Induction on $\nu (u)$ puts the latter in ${\mathsf{SN}}_0$, so no infinite reduction can begin at the displayed term. A second induction on $\nu (u)$ proves $q_{C}u\in {\mathsf{SN}}_0$: its immediate reducts are $(\lambda y:C.x)u$ and the terms $q_C{u}^{\prime }$ at smaller height. The term $q_C$ itself has the single reduct $\lambda y:C.x$, hence lies in ${\mathsf{SN}}_0$; this supplies the leading strong-normalization condition in the definition of $R\Rightarrow {\mathsf{SN}}_0$. Therefore $q_C\in R\Rightarrow {\mathsf{SN}}_0$ for every $C,R$. The outer type abstraction is beta-normal and type-closed, so the universal candidate clause gives the displayed membership.

Proof of Lemma 5.28 — Interpretations are candidates

Proof. Induct on $A$, universally quantifying $\mathrm{\Delta }$ and $\eta$ in the induction hypothesis. A variable is assigned a candidate. An arrow uses item 3 of lemma 5.26. At $\mathrm{\forall }X.A$, the induction hypothesis says that $(C,R)\mapsto [[A{]]}_{\eta [X\mapsto (C,R)]}$ is a candidate-valued family for every closed $C$ and candidate $R$. Item 4 of the same lemma is exactly the displayed universal clause. ◻

Proof of Lemma 9.30 — Interpretation irrelevance

Proof. Agreement of valuations implies equality of their candidate components at every free variable of $A$. Apply lemma 9.28. ◻

Universal elimination instantiates a syntactic type while extending its candidate valuation. For $B$ formed over the domain of $\eta$, the required commuting equation is $$[[A[B/X]{]]}_{\eta }=[[A{]]}_{\eta [X\mapsto (B[\hat{\eta }],[[B{]]}_{\eta })]}.$$

Proof of Lemma 5.29 — Candidate substitution

Proof. Induct on $A$, universally quantifying $\eta$, $B$, and their well-formed domains in the induction hypothesis. If $A=X$, both sides are $S_B$. If $A=Y\ne X$, both sides are $R_Y$. The arrow case applies the two induction hypotheses to the domain and codomain.

Let $A=\mathrm{\forall }Y.A_0$. Choose $Y$ distinct from $X$ and fresh for $B,\eta$. Membership of a term $t$ in the left side means that, for every closed $C$ and candidate $R$, $$t[C]\in [[A_0[B/X]{]]}_{\eta [Y\mapsto (C,R)]}.$$ Apply the induction hypothesis to $A_0$ under the extended valuation. The instance supplied by that hypothesis initially contains the pair $$(B[\widehat{\eta [Y\mapsto (C,R)]}],[[B{]]}_{\eta [Y\mapsto (C,R)]}).$$ Because $Y\notin \mathrm{ftv}(B)$, simultaneous type substitution and interpretation irrelevance give $$B[\widehat{\eta [Y\mapsto (C,R)]}]=B[\hat{\eta }]=B_{\eta },[[B{]]}_{\eta [Y\mapsto (C,R)]}=[[B{]]}_{\eta }=S_B.$$ After these equalities identify the inserted pair, the two map extensions commute because $X\ne Y$: $$\eta [Y\mapsto (C,R)][X\mapsto (B_{\eta },S_B)]=\eta [X\mapsto (B_{\eta },S_B)][Y\mapsto (C,R)].$$ Thus the displayed membership condition is exactly membership in the right side’s interpretation of $\mathrm{\forall }Y.A_0$. The built-in $t\in {\mathsf{SN}}_0$ condition is identical on both sides. Hence the two sets are equal. ◻

Proof of Lemma 5.32 — Reflection through a fresh substitution

Proof. Each displayed substitution carries every compatible beta step $s{⟶}_{\beta }{s}^{\prime }$ to a compatible beta step between the substituted terms. Constructor steps follow directly. A term-beta root has the form $(\lambda z:A.r)u$. Alpha-rename its binder so that $z\notin \{x,y\}\cup \mathrm{fv}(u)$. Then $$((\lambda z:A.r)u)[y/x]\stackrel{\beta }{{⟶}_{\beta }}r[y/x][u[y/x]/z]\stackrel{composition}{=}r[u/z][y/x].$$ At a type-beta root under the term substitution, the term and type substitutions commute: $$((\mathrm{\Lambda }Y.r)[B])[y/x]\stackrel{{\beta }_{\mathrm{\forall }}}{{⟶}_{\beta }}r[y/x][B/Y]\stackrel{commutation}{=}r[B/Y][y/x].$$ For substitution by $[C/X]$, the term-beta root uses the mixed composition equation in equation 5.2. At a type-beta root, alpha-rename its binder so that $Y\ne X$ and $Y\notin \mathrm{ftv}(C)\cup \mathrm{ftv}(B)$, and calculate $$((\mathrm{\Lambda }Y.r)[B])[C/X]\stackrel{{\beta }_{\mathrm{\forall }}}{{⟶}_{\beta }}r[C/X][B[C/X]/Y]\stackrel{composition}{=}r[B/Y][C/X].$$ Thus an infinite reduction from $s$ would be carried step for step to an infinite reduction from $s[y/x]$ or $s[C/X]$. Either hypothesis excludes that possibility. ◻

Expansion through abstractions

Candidate closure is directed from a redex to its reduct. Introduction rules require the reverse move: from reducibility of every substituted body to reducibility of the abstraction. Lemma 5.30, Lemma 5.31 prove that expansion principle for term and type abstraction, respectively.

Proof of Lemma 5.30 — Term-abstraction expansion

Proof. Choose a term variable $y\notin \mathrm{fv}(s)$. It is neutral and normal, so (CR3) gives $y\in R$. The hypothesis gives $s[y/x]\in S$, hence $s[y/x]\in \mathsf{SN}$ by (CR1). Item 1 of lemma 5.32 gives $s\in \mathsf{SN}$; the hypothesis that $s$ has no free type variables then gives $s\in {\mathsf{SN}}_0$. The abstraction is strongly normalizing because all its reductions occur in $s$.

We prove simultaneously, for every strongly normalizing type-closed body $s$ satisfying the displayed hypothesis and every $u\in R$, that $(\lambda x:A.s)u\in S$. Induct on the lexicographic pair $(\nu (s),\nu (u))$: first compare the left components and compare the right components only when the left ones are equal. The required induction is ordinary induction on $\nu (s)$, nested with ordinary induction on $\nu (u)$ at a fixed first component. The redex is neutral, so use (CR3) for $S$. Its one-step reducts are:

1. the root reduct $s[u/x]$, which belongs to $S$ by the displayed hypothesis;

2. $(\lambda x:A.s^{\prime })u$ for $s{⟶}_{\beta }{s}^{\prime }$;

3. $(\lambda x:A.s)u^{\prime }$ for $u{⟶}_{\beta }{u}^{\prime }$.

In the second case, $s^{\prime }$ is strongly normalizing and, for every $w\in R$, $s[w/x]{⟶}_{\beta }{s}^{\prime }[w/x]$; the displayed hypothesis and (CR2) give $s^{\prime }[w/x]\in S$. The outer induction hypothesis applies. In the third case, (CR2) gives $u^{\prime }\in R$ and the inner measure decreases. Therefore every reduct lies in $S$, and (CR3) completes the proof. ◻

The quantifiers in item 2 below are essential: the same substituted body $s[C/X]$ must lie in every candidate value $F(C,R)$ supplied at $C$; it is not enough to choose one convenient candidate for each type.

Proof of Lemma 5.31 — Type-abstraction expansion

Proof. Choose the closed type $I$ and candidate ${\mathsf{SN}}_0$. The hypothesis and (CR1) give $s[I/X]\in \mathsf{SN}$, so item 2 of lemma 5.32 gives $s\in \mathsf{SN}$. The type abstraction is strongly normalizing and has no free type variables: its body is strongly normalizing, and $\mathrm{\Lambda }X$ binds its only possible free type variable. Fix $C,R$. Prove $(\mathrm{\Lambda }X.s)[C]\in F(C,R)$ by induction on $\nu (s)$ and use (CR3). The root reduct $s[C/X]$ belongs by hypothesis. Every other reduct is $(\mathrm{\Lambda }X.s^{\prime })[C]$ with $s{⟶}_{\beta }{s}^{\prime }$. Then $s^{\prime }[D/X]$ is a reduct of $s[D/X]$ for every closed $D$; (CR2) preserves all the hypotheses for $s^{\prime }$, whose reduction height is smaller. The induction hypothesis puts each competing reduct in $F(C,R)$. Hence (CR3) gives the required membership. ◻

In the proof of theorem 5.34, replacing a free term or type variable by a fresh closed witness first proves normalization of the substituted term. In particular, normalization of $s[C/X]$ for one closed $C$ gives normalization of $s$ by item 2 of lemma 5.32; the type-abstraction case uses exactly this step.

The fundamental theorem

Proof of Theorem 5.34 — Fundamental theorem of reducibility

Proof. Induct on the typing derivation, organized by its final rule.

For F-Var, the transformed term is $\sigma (x)$, which belongs to the required candidate by definition of reducible substitution.

For F-Arr-E, the induction hypotheses give $$t[\hat{\eta }][\sigma ]\in [[A{]]}_{\eta }\Rightarrow [[B{]]}_{\eta },u[\hat{\eta }][\sigma ]\in [[A{]]}_{\eta }.$$ The definition of the arrow candidate puts their application in $[[B{]]}_{\eta }$.

For F-Arr-I, choose the binder $x$ away from every free variable occurring in the finite family $\{\sigma (y)\mid y\in \mathrm{dom}(\mathrm{\Gamma })\}$. Put $s=t[\hat{\eta }][\sigma ]$, leaving $x$ free. We verify the two hypotheses of term-abstraction expansion. The type $A[\hat{\eta }]$ is closed. Moreover $s$ has no free type variables: scope bounds the free type variables of $t$ by $\mathrm{\Delta }$, $\hat{\eta }$ replaces all of them by closed types, and every image of $\sigma$ is type-closed.

Every candidate contains a variable $y$ chosen fresh for $s$ and all substitution images. Extend $\sigma$ by $x\mapsto y$; the induction hypothesis and the term/term composition equation in equation 5.2 give $$t[\hat{\eta }][\sigma ,x\mapsto y]=s[y/x]\in [[B{]]}_{\eta }.$$ Thus $s[y/x]$ is strongly normalizing, and lemma 5.32 gives $s\in \mathsf{SN}$. For every $u\in [[A{]]}_{\eta }$, extend $\sigma$ by $x\mapsto u$. The same term/term equation and the induction hypothesis give $s[u/x]\in [[B{]]}_{\eta }$. Term-abstraction expansion yields $$\lambda x:A[\hat{\eta }].s\in [[A{]]}_{\eta }\Rightarrow [[B{]]}_{\eta }.$$ This lambda is exactly the transformed conclusion term.

For F-All-E, the induction hypothesis gives $$t[\hat{\eta }][\sigma ]\in [[\mathrm{\forall }X.A{]]}_{\eta }.$$ Use the universal clause with the closed type $C=B[\hat{\eta }]$ and candidate $R=[[B{]]}_{\eta }$. It gives the transformed type application in $[[A{]]}_{\eta [X\mapsto (C,R)]}$. Candidate substitution gives $$[[A{]]}_{\eta [X\mapsto (C,R)]}=[[A[B/X]{]]}_{\eta },$$ the interpretation of the conclusion type.

Finally consider F-All-I. Put $s=t[\hat{\eta }][\sigma ]$, leaving $X$ free, and write ${\eta }^{\prime }:=\eta [X\mapsto (C,R)]$ for arbitrary closed $C$ and candidate $R$.

Since $X\notin \mathrm{ftv}(\mathrm{\Gamma })$, every declaration $x:B$ in $\mathrm{\Gamma }$ satisfies $X\notin \mathrm{ftv}(B)$. Interpretation irrelevance gives $[[B{]]}_{\eta }=[[B{]]}_{{\eta }^{\prime }}$ for each such declaration. Thus the same $\sigma$ is also ${\eta }^{\prime }$-reducible for $\mathrm{\Gamma }$, and the induction hypothesis under ${\eta }^{\prime }$ gives $$t[\widehat{{\eta }^{\prime }}][\sigma ]\in [[A{]]}_{{\eta }^{\prime }}.$$ Every closed-type component of $\eta$ is type-closed, so $\widehat{{\eta }^{\prime }}$ is $\hat{\eta }$ followed by the single substitution $[C/X]$. Because the images of $\sigma$ have no free type variables, the type substitution does not alter those images. The term–type composition equation in equation 5.2 therefore gives $$t[\widehat{{\eta }^{\prime }}][\sigma ]{=}_{\alpha }s[C/X].$$ Choose $C=I$, where $I=\mathrm{\forall }Y.Y\to Y$ as in equation 5.1, and choose $R={\mathsf{SN}}_0$. The displayed membership and (CR1) give $s[I/X]\in \mathsf{SN}$, so lemma 5.32 gives $s\in \mathsf{SN}$. Type-abstraction expansion, with the displayed family of body candidates, yields $\mathrm{\Lambda }X.s\in [[\mathrm{\forall }X.A{]]}_{\eta }$. This is the transformed conclusion. The induction is complete. ◻

Proof of Theorem 5.35 — Strong normalization

Proof. Assign every $X\in \mathrm{\Delta }$ the closed type $I$ and the candidate ${\mathsf{SN}}_0$. For each $x:A$ in $\mathrm{\Gamma }$, use the same term variable $x$ as its substitution image. Every candidate contains every variable by (CR3), so this is a reducible substitution. The fundamental theorem gives $t[\hat{\eta }]\in [[A{]]}_{\eta }$, hence $t[\hat{\eta }]\in \mathsf{SN}$ by (CR1). If $t$ admitted an infinite compatible reduction, apply the second clause of lemma 5.32 successively to the finite family of closed type images in $\hat{\eta }$. Each application is licensed because the image is a closed formed type, and the step-preservation calculation in that lemma carries the infinite reduction through the substitution. The result would be an infinite reduction of $t[\hat{\eta }]$. Therefore $t$ is strongly normalizing. A maximal reduction ends in a normal form, and the call-by-value relation is a subrelation. ◻

A neutral spine $h\cdot \mathcal{S}$ consists of a head term variable $h$ followed by a finite, possibly empty, sequence of term arguments and type arguments in their original order. This notation records mixed applications without placing every term argument before every type argument.

Proof of Lemma 9.38 — Normal and neutral shapes

Proof. Induct on the typing derivation, using inversion and normality in the two elimination cases. A variable is neutral. Lambdas and type abstractions are the two introduction cases. If $n=tu$, inversion types $t$ at an arrow and $u$ at its domain. Normality excludes a term-abstraction operator, and typing inversion excludes a type abstraction because its type has universal, not arrow, head. The induction hypothesis gives $t=h\cdot \mathcal{S}$ for a head variable $h$; appending the normal $u$ preserves $h$. For $n=t[B]$, inversion types $t$ at a universal type. Normality excludes a type-abstraction operator, while typing inversion excludes a term abstraction; the induction hypothesis again gives a neutral $t$ with the same head variable. These cases exhaust the typing rules.

For the typed conclusion at $X$, inversion excludes both abstractions: their conclusion types have arrow and universal heads. The remaining neutral’s head is a free term variable, and the variable rule places it in $\mathrm{\Gamma }$. With empty $\mathrm{\Gamma }$, no such neutral exists. ◻

Proof of Corollary 5.36 — Syntactic consistency

Proof. Suppose $\cdot ;\cdot ⊢t:\mathrm{\forall }X.X$. Normalize $t$ and use subject reduction. Its normal form must be $\mathrm{\Lambda }X.u$, with $X;\cdot ⊢u:X$: by lemma 9.38, a closed normal term cannot be neutral and the universal conclusion excludes a term lambda. The same lemma gives $u=h\cdot \mathcal{S}$ with $h$ declared in the empty term context. This contradiction proves the claim. ◻

The eta boundary of the encodings

To prove that two distinct normal forms are not beta-convertible, we need one final property of reduction. Strong normalization alone is insufficient: a terminating relation may still lead to two different normal forms. Compatible beta reduction is confluent.

Trying to prove a diamond directly for one compatible beta step fails when substitution duplicates a redex. Put $r=(\lambda y.y)z$. Then $$(\lambda x.fxx)r$$ reduces in one step either to $frr$ or to $(\lambda x.fxx)z$. The latter reaches $fzz$ in one step, whereas the former needs one contraction in each copy of $r$. The reducts therefore need not rejoin in one ordinary step. Parallel reduction repairs this by contracting any finite family of redexes, including both copies, at once.

Proof of Lemma 5.37 — Parallel substitution

Proof. Prove the term-substitution assertion by induction on the derivation $s{\Rrightarrow }_{\beta }{s}^{\prime }$. A distinguished variable uses $u{\Rrightarrow }_{\beta }{u}^{\prime }$; another variable is reflexive. Constructor clauses apply their induction hypotheses after freshening binders away from $u,u^{\prime }$. In the term-beta root case, alpha-freshen the contracted binder $y$ so that $y\ne x$ and $y\notin \mathrm{fv}(u)\cup \mathrm{fv}(u^{\prime })$. Then use the two induction hypotheses and the composition equation $$s_0[v/y][u/x]=s_0[u/x][v[u/x]/y]$$ from equation 5.2; this is precisely the term obtained by substituting into the contracted parallel reduct. The type-beta root is structural for term substitution.

The type-substitution assertion is the same induction. Its type-beta root first alpha-freshens the contracted binder $Y$ so that $Y\ne X$ and $Y\notin \mathrm{ftv}(A)$, and then uses the type-substitution composition equality in equation 5.2. The term-beta root uses the term–type commutation equation there after the term binder has been freshened. Thus both the term-beta and type-beta roots commute with type substitution. ◻

Proof of Lemma 9.42 — Parallel diamond

Proof. Use simultaneous induction on two parallel derivations with a common source. The possible last-rule pairs are determined by the source’s outer constructor: For every constructor/constructor pair, apply the induction hypothesis to each immediate subterm. A parallel step either preserves the outer constructor or contracts one of the two beta-redex shapes; those shapes have different eliminators.

It remains to treat pairs in which at least one derivation contracts the root. For a term-beta source $(\lambda x:A.s)u$, suppose one derivation contracts the root to $s_1[u_1/x]$ while the other preserves application and reaches $(\lambda x:A.s_2)u_2$. Inverting the preserving derivation’s left premise $\lambda x:A.s{\Rrightarrow }_{\beta }\lambda x:A.s_2$ forces its last rule to be P-Lam, and therefore supplies the body derivation $s{\Rrightarrow }_{\beta }{s}_2$ needed by the induction hypothesis. The induction hypotheses give common parallel reducts $s_{\ast }$ of $s_1,s_2$ and $u_{\ast }$ of $u_1,u_2$. Parallel substitution gives $$s_1[u_1/x]{\Rrightarrow }_{\beta }{s}_{\ast }[u_{\ast }/x],$$ while the root clause gives $(\lambda x:A.s_2)u_2{\Rrightarrow }_{\beta }{s}_{\ast }[u_{\ast }/x]$. If both derivations contract the root, the same substitution calculation joins them. For a type-beta source $(\mathrm{\Lambda }X.s)[A]$, the body induction hypotheses give reducts with a common successor $s_{\ast }$, parallel type substitution sends the contracted branch to $s_{\ast }[A/X]$, and P-TBeta sends the constructor branch there. Hence the parallel relation has the diamond property. ◻

Proof of Lemma 9.43 — Sequentializing parallel reduction

Proof. Every one-step beta contraction is a parallel step. Conversely, induction on a derivation $t{\Rrightarrow }_{\beta }{t}^{\prime }$ gives $t{⟶}_{\beta }^{\ast }{t}^{\prime }$. The variable case is empty. Each of P-Lam, P-App, P-TLam, and P-TApp uses the induction hypotheses under its compatible contexts. In the P-Beta case they give $$(\lambda x:A.s)u{⟶}_{\beta }^{\ast }(\lambda x:A.s^{\prime })u^{\prime }{⟶}_{\beta }{s}^{\prime }[u^{\prime }/x].$$ The P-TBeta root instead ends $(\mathrm{\Lambda }X.s^{\prime })[A]{⟶}_{\beta }{s}^{\prime }[A/X]$. Thus parallel steps can be sequentialized. ◻

Proof of Theorem 5.38 — Church–Rosser

Proof. The diamond property of lemma 9.42 extends from one parallel step to its reflexive transitive closure by tiling. In the following diagrams every solid arrow is one ${\Rrightarrow }_{\beta }$ step. A row or column denotes the composite ${\Rrightarrow }_{\beta }^{\ast }$ path. The left square is one diamond. Repeating that square along the upper path gives the strip on the right; adjoining one strip for each step of the other path tiles a rectangle. Diagram The represented invariant is that the two paths around every square have a common endpoint. First prove the strip property: if $a{\Rrightarrow }_{\beta }b$ and $a{\Rrightarrow }_{\beta }^{\ast }c$, then some $d$ satisfies $b{\Rrightarrow }_{\beta }^{\ast }d$ and $c{\Rrightarrow }_{\beta }^{\ast }d$. Induct on the second path. Its empty case takes $d=b$. In its successor case $a{\Rrightarrow }_{\beta }{c}_1{\Rrightarrow }_{\beta }^{\ast }c$, the diamond for the two first steps produces $e$ with $b{\Rrightarrow }_{\beta }e$ and $c_1{\Rrightarrow }_{\beta }e$; the induction hypothesis applied to $c_1{\Rrightarrow }_{\beta }e$ and $c_1{\Rrightarrow }_{\beta }^{\ast }c$ completes the strip. Now induct on the first path in a peak $b{\Leftarrow }_{\beta }^{\ast }a{\Rrightarrow }_{\beta }^{\ast }c$, using one strip for its first step. This tiles the whole rectangle and gives a common parallel reduct.

Ordinary beta paths embed into parallel paths, and parallel paths sequentialize back to ordinary beta paths; hence compatible beta reduction is confluent. Two normal forms with a common reduct must themselves be alpha-equal, which proves uniqueness. ◻

Proof of Corollary 9.45 — Conversion has a common reduct

Proof. Induct on the construction of $u{=}_{\beta }v$. Reflexivity and a single forward or backward step are immediate; symmetry exchanges the two legs. For transitivity, suppose $u{⟶}_{\beta }^{\ast }p{⟵}_{\beta }^{\ast }v$ and $v{⟶}_{\beta }^{\ast }q{⟵}_{\beta }^{\ast }w$. Confluence joins the two reductions from $v$ at some $r$: $p{⟶}_{\beta }^{\ast }r{⟵}_{\beta }^{\ast }q$. Appending the outer legs gives $u{⟶}_{\beta }^{\ast }r{⟵}_{\beta }^{\ast }w$, as required. ◻

Proof of Proposition 5.39 — Closed normal booleans and naturals

Proof. Invert the typing of a closed normal term. At either universal type it must begin with $\mathrm{\Lambda }X$ by lemma 9.38. Repeating inversion at the arrow types produces the displayed term lambdas.

For booleans, the remaining body has type $X$ under $t:X,f:X$. A neutral normal form of atomic type must be headed by a variable, and neither variable is a function. Hence the body is $t$ or $f$.

For naturals, the remaining context is $z:X,s:X\to X$. A neutral normal form of type $X$ is either $z$ or $su$. Apply the head-form argument recursively to $u:X$: the only arrow-typed variable in scope is $s$, so no other application head is possible. Since the term is finite, it is $s^{n}z$ for a unique $n$. For every closed typed term $t$, strong normalization gives $t{⟶}_{\beta }^{\ast }n$ with $n$ normal, subject reduction preserves its type, and Church–Rosser gives uniqueness of $n$ up to alpha-equivalence. ◻

We can now state the exact boundary of the encodings. Let $p:A{\times }_{F}B$ be a variable. Both $$p\text{and}⟨{\mathsf{fst}}_F(p),{\mathsf{snd}}_F(p){⟩}_F$$ are beta-normal after the abbreviations are expanded, and they are not alpha-equal: the second begins with a type abstraction, while the first is neutral. By Church–Rosser they are not beta-convertible. Thus the product encoding has both projection beta laws, but not product eta as a beta law.

The corresponding sum boundary is visible without inventing an eta law. For variables $$s:A{+}_{F}B,f:A\to C,g:B\to C,q:C\to D,$$ the two normal terms $$q(s[C]fg)\text{and}s[D](\lambda a:A.q(fa))(\lambda b:B.q(gb))$$ are distinct. A primitive sum calculus may choose a commuting conversion equating them; the Church encoding under beta conversion does not. These facts do not diminish the constructor calculations already proved. They say exactly which equations those calculations establish.

Why the full-function set interpretation fails

The reducibility interpretation was designed to prove termination, not to assign an ordinary mathematical value to every term. It is natural to ask for a classical set interpretation that extends the familiar model of simple types: interpret $A\to B$ by the full set of all functions and find some set interpreting $\mathrm{\forall }X.A$. Impredicativity obstructs this request.

Double brackets always denote an interpretation; their subscript identifies which one. Thus $[[A{]]}_{\eta }$ above is a reducibility candidate, whereas $[[A{]]}_{\mathsf{set}}$ below would be a set in the assumed classical model.

Proof of Lemma 9.49 — Functor laws for T

Proof. For $\varphi :(X\to B)\to B$ and $k:X\to B$, $T(\mathrm{id})(\varphi )(k)=\varphi (k\circ \mathrm{id})=\varphi (k)$. For $h:X\to Y$, $g:Y\to Z$, and $k:Z\to B$, $$T(g\circ h)(\varphi )(k)=\varphi (k\circ g\circ h)=T(h)(\varphi )(k\circ g)=T(g)(T(h)(\varphi ))(k).$$ Since $k$ was arbitrary, $T(g\circ h)(\varphi )=T(g)(T(h)(\varphi ))$; since $\varphi$ was arbitrary, $T(g\circ h)=T(g)\circ T(h)$. The first calculation, with ${\mathrm{id}}_X$ in place of $g\circ h$, gives $T({\mathrm{id}}_X)={\mathrm{id}}_{T(X)}$. ◻

Proof of Theorem 9.50 — Imported stable-restriction interface

Proof. Put $\mathbf{B}:={\mathsf{Bool}}_F$. For a type variable $S$, put $$\mathbf{W}(S):=(((S\to \mathbf{B})\to \mathbf{B})\to S)\to S,\mathbf{P}:=\mathrm{\forall }S.\mathbf{W}(S).$$ Reynolds gives an explicit System F term $\mathbf{H}:((\mathbf{P}\to \mathbf{B})\to \mathbf{B})\to \mathbf{P}$. The ordinary variable, abstraction, and application clauses interpret it as a structure map $H:T(P)\to P$, where $P=[[\mathbf{P}{]]}_{\mathsf{set}}$ and $T(X)=(X\to B)\to B$. For an arbitrary algebra $f:T(X)\to X$, interpreting $p[X]f$ defines ${\rho }_f:P\to X$. Term substitution and both beta laws calculate ${\rho }_f\circ H=f\circ T({\rho }_f)$, so this algebra is weakly initial. For $p\in P$, call $p$ stable when every $T$-algebra homomorphism $\alpha :(X,f)\to (Y,g)$ satisfies $$\alpha ({\rho }_f(p))={\rho }_g(p).$$ Let $P^{\prime }\subseteq P$ be the set of stable elements. Reynolds proves that $H$ restricts to a map $H^{\prime }:T(P^{\prime })\to P^{\prime }$ and supplies, for each algebra $(X,f)$, a homomorphism ${\rho }_f^{\prime }:P^{\prime }\to X$. Put $e:={\rho }_{H^{\prime }}^{\prime }:P^{\prime }\to P^{\prime }$. The factorization clause of Reynolds’s Lemma 3, applied to $e$, gives $e\circ e=e$. Hence $e$ is an idempotent endomap of $P^{\prime }$. Splitting $e$ in the sense of definition 9.48 produces a carrier $P^{″}$ on which the induced map $H^{″}:T(P^{″})\to P^{″}$ has exactly one homomorphism into every $T$-algebra. Reynolds’s Lemmas 1–4 supply the explicit terms, the restriction to $P^{\prime }$, the factorization clause, and the splitting [Rey84]. ◻

Proof of Lemma 9.51

Proof. The map sending $x\in X$ to the characteristic function of the singleton $\{x\}$ is injective. It remains to exclude an injection in the other direction.

Suppose $i:2^X\to X$ were injective. Define $r:X\to 2^X$ by $$r(i(g))=g,r(x)=\text{the constant-zero function when }x\notin \mathrm{im}(i).$$ Injectivity of $i$ makes the first clause unambiguous, and every $g\in 2^X$ equals $r(i(g))$; hence $r$ is surjective. Define $d\in 2^X$ by $d(x)=1-r(x)(x)$. Surjectivity gives an $a\in X$ with $r(a)=d$, whence $d(a)=1-d(a)$, a contradiction. Thus no injection $2^X\to X$ exists. ◻

Proof of Theorem 5.40 — Reynolds' set-theoretic obstruction

Proof. Assume such a package. The denotations of ${\mathsf{true}}_F$ and ${\mathsf{false}}_F$ are distinct: instantiate both at a two-element set and use the full-function arrow clause together with the variable, abstraction, type-application, and type-beta clauses. Choose their distinct denotations $b_0,b_1\in B$, where $B=[[{\mathsf{Bool}}_F{]]}_{\mathsf{set}}$.

By theorem 9.50, $T$ has an initial algebra $(X,\alpha )$. Its structure map is an isomorphism. Let $h:(X,\alpha )\to (T(X),T(\alpha ))$ be the unique homomorphism. Both $\alpha \circ h$ and ${\mathrm{id}}_X$ are endomorphisms of the initial algebra, so they are equal. The homomorphism equation for $h$ then gives $$h\circ \alpha =T(\alpha )\circ T(h)=T(\alpha \circ h)={\mathrm{id}}_{T(X)}.$$ Hence $\alpha :T(X)\to X$ is a bijection.

It remains to compare cardinalities without assuming that $B$ has exactly two elements. Map $0$ to $b_0$ and $1$ to $b_1$ to obtain an injection $j:2\hookrightarrow B$. Postcomposition with $j$ gives an injection $j^X:2^X\hookrightarrow B^X$. Every function $F:2^X\to 2$ determines a function $\bar{F}:B^X\to B$ by Restriction along $j^X$ recovers $j\circ F$, so the assignment $F\mapsto \bar{F}$ is injective. Its domain is the function set $2^{2^X}$, whose cardinal is $2^{|2^X|}=2^{2^{|X|}}$. Consequently $$|T(X)|=|B^{B^X}|\ge 2^{2^{|X|}}.$$ Let $i:2^{2^X}\hookrightarrow T(X)$ be the injection just constructed, and let $s:X\hookrightarrow 2^X$ send $x$ to the characteristic function of $\{x\}$. Composing $i$ with the bijection $\alpha :T(X)\to X$ and then with $s$ gives an injection $$2^{2^X}\hookrightarrow 2^X.$$ The Cantor diagonal lemma at the set $2^X$ forbids this injection. The imported interface supplies only the initial algebra; the cardinal comparison and the contradiction are local [Rey84]. ◻

This is not a contradiction in System F. Syntactic consistency was proved in corollary 5.36. Nor does the theorem say that System F has no semantics constructed within set theory. A semantic package avoids clause 3 of definition 9.47 when it assigns to some pair of interpreted sets $U,V$ a proper subset of $V^U$. Such subsets must still contain the denotation of every typed abstraction, and clause 4 must interpret $tu$ by evaluating the element denoted by $t$ at the element denoted by $u$. The obstruction tells us which naive extension of the simple set model fails, not that impredicative syntax is meaningless.

The remaining question: uniformity

Normalization can classify the inhabitants of one chosen closed type. Repeating that calculation separately at every polymorphic type supplies no induction clause for an arrow or a universal type. We first see this limit at the iterator type $H:=\mathrm{\forall }X.(X\to X)\to X\to X$.

Proof of Lemma 5.41 — Normal iterators

Proof. Normalize and invert typing. Write the forced initial abstractions as $\mathrm{\Lambda }X.\lambda f:X\to X.r$. The residual term $r$ has type $X\to X$ under $f:X\to X$. If $r$ is neutral, it must be the variable $f$: applying $f$ even once would produce atomic type $X$. Otherwise it is $\lambda x:X.u$, where $u:X$ is normal under $f:X\to X,x:X$. The neutral-head argument from proposition 5.39 gives $u=f^{n}x$ for a unique $n$. Church–Rosser gives uniqueness of the resulting member of the list. ◻

The proof inspects the particular normal forms of $H$; it does not extend by induction on an arbitrary type. To obtain arrow and universal clauses, relate inputs at two types and lift that relation through each type constructor.

The arrow $R\Rightarrow S$ here deliberately has the same shape as the candidate arrow in lemma 5.26: both say that related or admitted inputs are sent to related or admitted outputs. It is unrelated to parallel reduction, which is written ${\Rrightarrow }_{\beta }$.

Put $H:=\mathrm{\forall }X.(X\to X)\to X\to X$, and let $\cdot ;\cdot ⊢h:H$ be closed. Let also $f:A\to A$, $g:B\to B$, $a:A$, and $b:B$ be closed.

Proof of Proposition 5.43 — Relational uniformity of iterators

Proof. Use lemma 5.41. If the normal form is $\mathrm{\Lambda }X.\lambda f.f$, the two terms in the conclusion reduce to $fa$ and $gb$; the arrow-relation hypothesis relates their classes. Otherwise the normal form is the long iterator for some $n$. Since $R$ is a relation on beta-equivalence classes, it suffices to prove $[f^{n}a{]}_{\beta }R[g^{n}b{]}_{\beta }$. Induct on $n$. The zero case is $[a{]}_{\beta }R[b{]}_{\beta }$; the successor case applies $[f{]}_{\beta }(R\Rightarrow R)[g{]}_{\beta }$ to the induction hypothesis. ◻

Every term in the proposition is typed, and $R$ was arbitrary. For a closed $k:A\to B$, define its graph on beta-equivalence classes of closed $a:A$ and closed $b:B$ by $$[a{]}_{\beta }{R}_k[b{]}_{\beta }⟺[ka{]}_{\beta }=[b{]}_{\beta }.$$ The definition of $R_k$ is independent of the chosen representatives because application respects beta conversion. The equation $k(fa){=}_{\beta }g(ka)$ for every closed $a:A$ says precisely that $[f{]}_{\beta }(R_k\Rightarrow R_k)[g{]}_{\beta }$. The proposition then gives $$k(h[A]fa){=}_{\beta }h[B]g(ka).$$ In words, transporting an input by $k$ before iterating gives the same result as iterating first and transporting afterward; the square formed by $f$, $g$, and $k$ commutes.

This proof is ad hoc: it classifies the normal forms of $H$, handles the eta-short form directly, and then inducts on the exponent of every long form. The strong-normalization theorem by itself does not state equation 5.5, and repeating a new normal-form classification at every polymorphic type is not a method. A relational semantics must interpret every type as a binary relation and show, by induction on typing, that every polymorphic term preserves the relation assigned to each type variable.