ch:system-f: ch:system-f

We prove the equation simultaneously with the corresponding equation for types, since the annotation of a term abstraction invokes the type case. The type grammar has three constructor cases. In the variable case, a variable distinct from $X$ and $Y$ is unchanged; at $X$, both sides are $B[C/Y]$; and at $Y$, both sides are $C$, using $X\notin \mathrm{ftv}(C)$. Arrow types follow componentwise. For a universal type $\mathrm{\forall }Z.A$, alpha-rename $Z$ fresh for $B,C,X,Y$; the type induction hypothesis gives

The term-variable case is immediate. The term-abstraction and application cases are the componentwise calculations The first line uses the type and term induction hypotheses; the second uses the two term induction hypotheses. Term binders have first been chosen fresh for the terms under discussion.

For a type abstraction whose displayed binder is already suitable, say $t=\mathrm{\Lambda }Z.s$ with $Z\ne X,Y$ and $Z\notin \mathrm{ftv}(B,C)$, the calculation is If the displayed $Z$ occurs in $B$ or $C$, choose one variable $W$ fresh for $s,B,C,X,Y$ and first use alpha-equivalence $$\mathrm{\Lambda }Z.s{=}_{\alpha }\mathrm{\Lambda }W.s[W/Z].$$ Both sides are then calculated with this same display: This is the freshening step that would be lost by silently changing the binder on only one side.

Finally, type application changes both of its components: The type-abstraction calculation and this last calculation exhaust the two System F term forms not already present in the simply typed calculus, so the induction proves the equation for every $t$.

Write $I=\mathrm{\forall }X.X\to X$. The closed formation tree needed by the type application is $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{X\in X}{X⊢X\mathsf{type}}}\mathrm{F}-\mathrm{Ty}-\mathrm{Var}\\ {\displaystyle \frac{X\in X}{X⊢X\mathsf{type}}}\mathrm{F}-\mathrm{Ty}-\mathrm{Var}\end{array}}{X⊢X\to X\mathsf{type}}}\mathrm{F}-\mathrm{Ty}-\mathrm{Arr}}{\cdot ⊢I\mathsf{type}}\mathrm{F}-\mathrm{Ty}-\mathrm{All}.$$ With the subscripts serving only to mark the two occurrences of the same variable, the complete term tree is $$\frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{f:I\in f:I}{\cdot ;f:I⊢f_{\mathrm{op}}:I}}\mathrm{F}-\mathrm{Var}\\ {\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{X\in X}{X⊢X\mathsf{type}}}\mathrm{F}-\mathrm{Ty}-\mathrm{Var}\\ {\displaystyle \frac{X\in X}{X⊢X\mathsf{type}}}\mathrm{F}-\mathrm{Ty}-\mathrm{Var}\end{array}}{X⊢X\to X\mathsf{type}}}\mathrm{F}-\mathrm{Ty}-\mathrm{Arr}}{\cdot ⊢I\mathsf{type}}}\mathrm{F}-\mathrm{Ty}-\mathrm{All}\end{array}}{\cdot ;f:I⊢f_{\mathrm{op}}[I]:I\to I}}\mathrm{F}-\mathrm{All}-\mathrm{E}\\ {\displaystyle \frac{f:I\in f:I}{\cdot ;f:I⊢f_{\arg }:I}}\mathrm{F}-\mathrm{Var}\end{array}}{\cdot ;f:I⊢f_{\mathrm{op}}[I]f_{\arg }:I}}\mathrm{F}-\mathrm{Arr}-\mathrm{E}}{\cdot ;\cdot ⊢\lambda f:I.f[I]f:I\to I}}\mathrm{F}-\mathrm{Arr}-\mathrm{I}\\ {\displaystyle \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 ⊢\mathrm{\Lambda }X.\lambda x:X.x:I}}\mathrm{F}-\mathrm{All}-\mathrm{I}\end{array}}{\cdot ;\cdot ⊢d\mathsf{id}:I}\mathrm{F}-\mathrm{Arr}-\mathrm{E}.$$ Thus the operator occurrence of $f$ first synthesizes $I$ and, after F-All-E, synthesizes $I\to I$; the argument occurrence synthesizes $I$ without instantiation.

Put $I=\mathrm{\forall }Y.Y\to Y$. Its closed formation derivation is $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{Y\in Y}{Y⊢Y\mathsf{type}}}\mathrm{F}-\mathrm{Ty}-\mathrm{Var}\\ {\displaystyle \frac{Y\in Y}{Y⊢Y\mathsf{type}}}\mathrm{F}-\mathrm{Ty}-\mathrm{Var}\end{array}}{Y⊢Y\to Y\mathsf{type}}}\mathrm{F}-\mathrm{Ty}-\mathrm{Arr}}{\cdot ⊢I\mathsf{type}}\mathrm{F}-\mathrm{Ty}-\mathrm{All}.$$ Substitution $[I/X]$ sends the context $f:X\to X,x:X$ to $f:I\to I,x:I$. The transformed term derivation is $$\frac{\begin{array}{c}{\displaystyle \frac{f:I\to I\in f:I\to I,x:I}{\cdot ;f:I\to I,x:I⊢f:I\to I}}\mathrm{F}-\mathrm{Var}\\ {\displaystyle \frac{x:I\in f:I\to I,x:I}{\cdot ;f:I\to I,x:I⊢x:I}}\mathrm{F}-\mathrm{Var}\end{array}}{\cdot ;f:I\to I,x:I⊢fx:I}\mathrm{F}-\mathrm{Arr}-\mathrm{E}.$$ Term substitution cannot produce this tree: it replaces a term variable by a term and leaves every annotation and declaration type unchanged. Here the operation replaces the type variable in both declarations and in the result classifier.

Inverting the final application gives a type $A$ and premises $$\mathrm{\Delta };\mathrm{\Gamma }⊢(\mathrm{\Lambda }X.t)[C]:A\to D,\mathrm{\Delta };\mathrm{\Gamma }⊢u:A.$$ Inverting the type application supplies a body type $B$ such that $$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathrm{\Lambda }X.t:\mathrm{\forall }X.B,\mathrm{\Delta }⊢C\mathsf{type},B[C/X]=A\to D.$$ Inverting the type abstraction finally gives $$\mathrm{\Delta },X;\mathrm{\Gamma }⊢t:B.$$ Context formation for the abstraction ensures that $X$ is absent from the types in $\mathrm{\Gamma }$. Type substitution therefore yields $$\mathrm{\Delta };\mathrm{\Gamma }⊢t[C/X]:B[C/X]=A\to D.$$ The reduct of the left subterm is exactly $t[C/X]$. Reusing the unchanged argument premise rebuilds the final rule: $$\frac{\begin{array}{c}\mathrm{\Delta };\mathrm{\Gamma }⊢t[C/X]:A\to D\\ \mathrm{\Delta };\mathrm{\Gamma }⊢u:A\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢t[C/X]u:D}\mathrm{F}-\mathrm{Arr}-\mathrm{E}.$$ This is preservation for the congruence step induced by the type-beta contraction.

Use the boolean itself as its eliminator: Inside the first term, $b[X]:X\to X\to X$, so the reversed arguments give an $X$; the three introductions produce the required boolean. Inside the second, instantiation at ${\mathsf{Bool}}_F$ makes the two branch arguments have the required common type.

The reductions are The second step of the first trace and the third step of each conjunction trace are type beta; all remaining contractions are term beta.

Define Under $s:A{+}_{F}B$ we have $s[X]:(A\to X)\to (B\to X)\to X$. The two displayed lambdas have types $A\to X$ and $B\to X$, since $f:A\to A^{\prime }$ and $g:B\to B^{\prime }$. The body consequently has type $X$; the three introductions give $${\mathsf{map}}_{+}:A{+}_{F}B\to A^{\prime }{+}_F{B}^{\prime }.$$ For the two constructors, compatible beta reduction gives If $s$, $f$, and $g$ are variables, applying the mapper has instead the variable-headed beta-normal form $$\mathrm{\Lambda }X.\lambda h:A^{\prime }\to X.\lambda k:B^{\prime }\to X.s[X](\lambda a:A.h(fa))(\lambda b:B.k(gb)).$$ There is no root redex at $s[X]$, so no constructor case can be selected.

Iterate addition of the second argument once for every successor in the first: $${\mathsf{mult}}_F:=\lambda m:{\mathsf{Nat}}_F.\lambda n:{\mathsf{Nat}}_F.m[{\mathsf{Nat}}_F]{\mathsf{zero}}_F({\mathsf{add}}_{F}n).$$ The iterator typing gives the required result type. Its calculation at two and three is

Put $P={\mathsf{Nat}}_F{\times }_F{\mathsf{Nat}}_F$ and define Both projections in $\mathsf{step}$ have type ${\mathsf{Nat}}_F$, so $\mathsf{step}:P\to P$ and the iterator produces a $P$. At zero, $${\mathsf{pred}}_F{\mathsf{zero}}_F{⟶}_{\beta }^{\ast }{\mathsf{fst}}_F(p_0){⟶}_{\beta }^{\ast }{\mathsf{zero}}_F.$$ Writing $p_j=⟨\overline{j-1},\bar{j}{⟩}_F$ for $j\ge 1$, the projection laws give $$p_0\stackrel{\mathsf{step}}{\to }⟨\bar{0},\bar{1}{⟩}_F\stackrel{\mathsf{step}}{\to }⟨\bar{1},\bar{2}{⟩}_F\stackrel{\mathsf{step}}{\to }⟨\bar{2},\bar{3}{⟩}_F.$$ Consequently $${\mathsf{pred}}_F\bar{3}{⟶}_{\beta }^{\ast }{\mathsf{fst}}_F⟨\bar{2},\bar{3}{⟩}_F{⟶}_{\beta }^{\ast }\bar{2}.$$ All arrows in the displayed state trace abbreviate the beta contractions of the Church projections followed by the successor contraction.

Two closed decorations of the Curry identity are $$\lambda x:I.x:I\to I,\mathrm{\Lambda }X.\lambda x:X.x:I.$$ Both erase to $\lambda x.x$, but their types differ. Their Curry derivations are respectively $$\frac{{\displaystyle \frac{x:I\in x:I}{\cdot ;x:I{⊢}_{C}x:I}}\mathrm{C}-\mathrm{Var}}{\cdot ;\cdot {⊢}_C\lambda x.x:I\to I}\mathrm{C}-\mathrm{Arr}-\mathrm{I}$$ and $$\frac{{\displaystyle \frac{{\displaystyle \frac{x:X\in x:X}{X;x:X{⊢}_{C}x:X}}\mathrm{C}-\mathrm{Var}}{X;\cdot {⊢}_C\lambda x.x:X\to X}}\mathrm{C}-\mathrm{Arr}-\mathrm{I}}{\cdot ;\cdot {⊢}_C\lambda x.x:I}\mathrm{C}-\mathrm{All}-\mathrm{I}.$$

For a Curry term containing an application, take $m=\lambda f.(\lambda x.x)f$. It has the following two Church decorations at the same type: The first Curry tree uses the direct $I\to I$ typing of the inner identity: $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{x:I\in f:I,x:I}{\cdot ;f:I,x:I{⊢}_{C}x:I}}\mathrm{C}-\mathrm{Var}}{\cdot ;f:I{⊢}_C\lambda x.x:I\to I}}\mathrm{C}-\mathrm{Arr}-\mathrm{I}\\ {\displaystyle \frac{f:I\in f:I}{\cdot ;f:I{⊢}_{C}f:I}}\mathrm{C}-\mathrm{Var}\end{array}}{\cdot ;f:I{⊢}_C(\lambda x.x)f:I}}\mathrm{C}-\mathrm{Arr}-\mathrm{E}}{\cdot ;\cdot {⊢}_{C}m:I\to I}\mathrm{C}-\mathrm{Arr}-\mathrm{I}.$$ In the second tree, replace the left premise of that C-Arr-E by $$\frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{x:X\in f:I,x:X}{X;f:I,x:X{⊢}_{C}x:X}}\mathrm{C}-\mathrm{Var}}{X;f:I{⊢}_C\lambda x.x:X\to X}}\mathrm{C}-\mathrm{Arr}-\mathrm{I}}{\cdot ;f:I{⊢}_C\lambda x.x:I}}\mathrm{C}-\mathrm{All}-\mathrm{I}\\ \cdot ⊢I\mathsf{type}\end{array}}{\cdot ;f:I{⊢}_C\lambda x.x:I\to I}\mathrm{C}-\mathrm{All}-\mathrm{E}.$$ Decoration of the first tree inserts no universal constructors at the inner identity; decoration of the replacement inserts $\mathrm{\Lambda }X$ and then the type application $[I]$. Erasure makes the two resulting Church terms equal to the same $m$.

Erasure gives $$(\lambda f.ff)(\lambda x.x).$$ Algorithm W assigns the lambda-bound $f$ one fresh monotype $\alpha$. Typing the body application treats the left occurrence as a function with fresh result $\beta$ and the right occurrence as its argument, producing $$\alpha \doteq \alpha \to \beta .$$ The occurs check rejects this equation.

The Curry derivation instead assigns $f:I$. Universal elimination is inserted at the function occurrence, decorating it as $f[I]:I\to I$; the argument occurrence remains $f:I$. The body therefore decorates to $f[I]f:I$, and the whole term becomes the Church term of equation 5.1. No first-order unifier can repair the HM equation, because a finite monotype cannot equal a proper arrow tree containing itself. The successful derivation changes the typing discipline: it instantiates the polymorphic type of a lambda-bound variable.

Let $\mathrm{\Delta }⊢A\mathsf{type}$. Define $${\mathsf{abort}}_A:=\lambda z:{\mathsf{Void}}_F.z[A].$$ Under $z:{\mathsf{Void}}_F=\mathrm{\forall }X.X$, universal elimination gives the open judgment $$\mathrm{\Delta };z:{\mathsf{Void}}_F⊢z[A]:A.$$ Arrow introduction therefore derives $$\mathrm{\Delta };\cdot ⊢{\mathsf{abort}}_A:{\mathsf{Void}}_F\to A.$$

The construction is an eliminator, not an inhabitant of its domain. The consistency corollary says that no closed term can be supplied as its ${\mathsf{Void}}_F$ argument. Applying the eliminator would require exactly the closed inhabitant excluded by that corollary.

For item 1, let $n$ be a neutral beta-normal form with no free type variables. It has no one-step reducts. The premise of (CR3) is therefore vacuous, so $n$ belongs to every candidate.

For item 2, define $$R{\Rightarrow }^{\prime }S=\{t\mid t\text{ has no free type variables and }\mathrm{\forall }u\in R,tu\in S\}.$$ Choose distinct variables $x,z$ fresh for $t$. Item 1 gives $z\in R$, so $tz\in S\subseteq \mathsf{SN}$. Put $s:=tx$. Then $s[z/x]=tz$, and reflection through the fresh substitution gives $tx\in \mathsf{SN}$. An infinite reduction from $t$ would lift through the left application context to an infinite reduction from $tx$; hence $t\in {\mathsf{SN}}_0$. This proves (CR1) for every member of $R{\Rightarrow }^{\prime }S$.

For (CR2), suppose $t\in R{\Rightarrow }^{\prime }S$ and $t{⟶}_{\beta }{t}^{\prime }$. For every $u\in R$, compatibility gives $tu{⟶}_{\beta }{t}^{\prime }u$, and (CR2) for $S$ gives $t^{\prime }u\in S$. Type-closedness is preserved by reduction, so $t^{\prime }\in R{\Rightarrow }^{\prime }S$.

For (CR3), let $t$ be neutral and type-closed, and suppose every $t{⟶}_{\beta }{t}^{\prime }$ lies in $R{\Rightarrow }^{\prime }S$. Fix $u\in R$. The application $tu$ is neutral. Induct on $n=\nu (u)$, with induction hypothesis $tv\in S$ for every $v\in R$ satisfying . This measure is finite by (CR1) for $R$. An immediate reduct $t^{\prime }u$ lies in $S$ by the premise on $t^{\prime }$. An immediate reduct $t{u}^{\prime }$ has $u^{\prime }\in R$ by (CR2), and ; the induction hypothesis therefore puts $t{u}^{\prime }$ in $S$. There is no root contraction because $t$ is neutral. Thus (CR3) for $S$ gives $tu\in S$, and consequently $t\in R{\Rightarrow }^{\prime }S$. The three clauses prove that $R{\Rightarrow }^{\prime }S$ is exactly the arrow candidate used in the chapter.

For item 3, take $t=q[D]$. The term $t[C]=(q[D])[C]$ is a type application whose operator is itself a type application, not a type abstraction, so it has no outer root contraction. Its immediate reducts are: $$(q^{\prime }[D])[C]\text{when }q{⟶}_{\beta }{q}^{\prime },s[D/Y][C]\text{when }q=\mathrm{\Lambda }Y.s.$$ Types do not reduce, so neither $D$ nor $C$ contributes another case. Both displayed forms are $t^{\prime }[C]$ for an immediate reduct $t^{\prime }$ of $t$. The universal-candidate premise puts every such $t^{\prime }$ in the universal candidate; its defining clause then puts $t^{\prime }[C]$ in $F(C,R)$. Applying (CR3) in $F(C,R)$ proves $t[C]\in F(C,R)$.

For $p:A{\times }_{F}B$, expansion of every abbreviation turns the reconstructed pair into $$\mathrm{\Lambda }X.\lambda k:A\to B\to X.k(p[A](\lambda a:A.\lambda b:B.a))(p[B](\lambda a:A.\lambda b:B.b)).$$ The comparison term is the neutral variable $p$. It is beta-normal. The expanded term is also beta-normal: both occurrences of $p$ are neutral, the two projection continuations contain no redex, and the final applications are headed by the variable $k$. Its outer constructor is $\mathrm{\Lambda }$, whereas the outer shape of $p$ is neutral, so the two normal forms are not alpha-equal and hence are not beta-convertible.

Likewise, with $${\mathsf{Bool}}_F=\mathrm{\forall }X.X\to X\to X,$$ the two boolean candidates are $$b\text{and}\mathrm{\Lambda }X.\lambda t:X.\lambda f:X.b[X]tf.$$ For neutral $b$, the operator $b[X]$ is not a type abstraction, and its two term applications are not lambda-headed. Both candidates are therefore beta-normal, but again one is neutral and the other begins with $\mathrm{\Lambda }$.

The first absent equation is the primitive product uniqueness rule $⟨\mathsf{fst}(p),\mathsf{snd}(p)⟩=p$. The second is the corresponding Boolean uniqueness, or eta, rule saying that a Boolean is uniquely reconstructed by eliminating it into its two branches. The Church encodings validate their constructor–eliminator beta laws, not these primitive eta laws under beta conversion alone.

Normalize a closed inhabitant and invert its typing. Its initial form is forced to be $$\mathrm{\Lambda }X.\lambda f:X\to X.r,f:X\to X⊢r:X\to X.$$ If $r$ is neutral, its head must be the only term variable in the context, namely $f$. Since $f$ already has the required arrow type, no application may follow it. This gives the eta-short normal form $$\mathrm{\Lambda }X.\lambda f:X\to X.f.$$ Otherwise inversion makes $r=\lambda x:X.u$, where $f:X\to X,x:X⊢u:X$. A normal term at the atomic type $X$ is neutral. Its head is $x$, giving $u=x$, or it is headed by $f$ and has the form $f{u}^{\prime }$. Repeating the same argument on the strictly smaller $u^{\prime }$ gives a unique $n\ge 0$ with $u=f^{n}x$. Thus all remaining forms are exactly $$\mathrm{\Lambda }X.\lambda f:X\to X.\lambda x:X.f^{n}x.$$ The normal/neutral shape lemma proves that no third case exists, and Church–Rosser makes the member of the list unique under beta conversion. Function eta would add $$\lambda x:X.fx{=}_{\eta }f(x\notin \mathrm{fv}(f)),$$ which identifies the long member with $n=1$ and the eta-short member. Beta conversion alone does not identify them.

Fix a closed type $C$ and a candidate $R$, and put $${\eta }^{\prime }:=\eta [X\mapsto (C,R)].$$ For every declaration $x:B$ in $\mathrm{\Gamma }$, the side condition $X\notin \mathrm{ftv}(\mathrm{\Gamma })$ gives $X\notin \mathrm{ftv}(B)$. Interpretation irrelevance therefore gives $$[[B{]]}_{{\eta }^{\prime }}=[[B{]]}_{\eta }.$$ Each image $\sigma (x)$ belongs to the right side, so the same substitution $\sigma$ is ${\eta }^{\prime }$-reducible for $\mathrm{\Gamma }$.

Apply the induction hypothesis to the premise under ${\eta }^{\prime }$. It gives $$t[\widehat{{\eta }^{\prime }}][\sigma ]\in [[A{]]}_{{\eta }^{\prime }}.$$ The valuation $\widehat{{\eta }^{\prime }}$ first performs $\hat{\eta }$ and then $[C/X]$. Every image of $\sigma$ has no free type variables, so the term–type substitution equation yields $$t[\widehat{{\eta }^{\prime }}][\sigma ]{=}_{\alpha }t[\hat{\eta }][\sigma ][C/X]=s[C/X].$$ Since $C$ and $R$ were arbitrary, this proves $s[C/X]\in [[A{]]}_{{\eta }^{\prime }}$ for every pair required by the universal candidate.

The type-abstraction expansion lemma also requires normalization of $s$. Choose $$C=I:=\mathrm{\forall }Y.Y\to Y,R={\mathsf{SN}}_0.$$ The membership just proved and (CR1) give $s[I/X]\in \mathsf{SN}$. Reflection through the closed type substitution gives $s\in \mathsf{SN}$. Type-abstraction expansion now yields $$\mathrm{\Lambda }X.s\in [[\mathrm{\forall }X.A{]]}_{\eta },$$ which is exactly the transformed conclusion of F-All-I.

The replacement abandons item 3 of definition 9.47: an arrow is no longer interpreted as the full set $V^U$. The selected family $\mathcal{F}(U,V)$ still supplies the functions needed to interpret abstraction and application, and at least one of these sets is a proper subset of $V^U$. The cardinality step $|T(X)|=|B^{B^X}|$ in theorem 5.40 is no longer available.

This semantic restriction changes none of the chapter’s syntactic results. Preservation remains true because its proof uses typing inversion and the two substitution lemmas, not a set interpretation. Strong normalization remains true because its proof uses reducibility candidates over syntax. Syntactic consistency remains true because it follows from normalization, subject reduction, and the normal-form shape lemma. Hence the exact answers are: preservation holds, normalization holds, and there is still no closed term of $\mathrm{\forall }X.X$. Reynolds’ theorem rules out one simultaneous package of set-theoretic clauses; it does not refute any of these local theorems.