ch:fomega-self-representation: ch:fomega-self-representation

The type of the unquoter gives $$\alpha ::U;x:\mathsf{Exp}\alpha ⊢\mathsf{unquote}[\alpha ]x:\mathsf{Op}\mathsf{Id}\alpha .$$ Hence an application to the same $x$ would require, for some formed type $B$, $$\begin{array}{}\text{(}1\text{)}& \mathsf{Op}\mathsf{Id}\alpha {=}_{\beta }\mathsf{Exp}\alpha \to B.\end{array}$$ The left side has the constructor reduction $$\mathsf{Op}\mathsf{Id}\alpha {\to }_{\beta }^{\ast }\alpha \mathsf{Id}.$$ Because $\alpha$ is a constructor variable, the application $\alpha \mathsf{Id}$ is neutral and constructor-normal. The right side of (1) has arrow head. Constructor confluence and disjointness of normal heads therefore refute (1).

Now let $A$ be closed and let $\mathcal{D}:e:A$ be a closed derivation. Then $\hat{\mathcal{D}}:\mathsf{Exp}\hat{A}$, while type recovery gives the annotated chain $$\mathsf{Op}\mathsf{Id}\hat{A}\stackrel{unfold\mathsf{Op},\hat{A}}{{\to }_{\beta }^{\ast }}{\mathsf{pre}}_{\mathsf{Id}}(A)\stackrel{lemma7.66}{{\to }_{\beta }^{\ast }}A.$$ Thus $\mathsf{unquote}[\hat{A}]\hat{\mathcal{D}}$ is well typed at $A$ by constructor conversion. This calculation uses constructor normalization only; it makes no appeal to term strong normalization.

The copied abstraction and polymorphic identity contain no application node, so the only inserted occurrence of $i$ is at the root: $$(\lambda x:I.x){\mathsf{id}}_I{⇝}_{\mathrm{s}\mathrm{h}}i[I\to I](\lambda x:I.x){\mathsf{id}}_I.$$ Substituting the closed polymorphic identity gives Before the substitution, the application is headed by the variable $i$. Its proper subterms are normal, so the prequotation is normal even though the represented source has a beta-redex at its root.

The recursively chosen constructors at the relevant kinds are Rule K-All gives $S_{\mathsf{Ty}}::\mathsf{Ty}$. Rule K-Abs first gives $S_{\mathsf{Ty}\to \mathsf{Ty}}::\mathsf{Ty}\to \mathsf{Ty}$ and, with a binder of kind $\mathsf{Ty}\to \mathsf{Ty}$, gives $S_{\kappa }::\kappa$.

In the context $X::\mathsf{Ty},T::\kappa \to \mathsf{Ty}$, put $K_X=\lambda A::\mathsf{Ty}.X$. Then $K_X::\mathsf{Ty}\to \mathsf{Ty}$ and $T{S}_{\kappa }::\mathsf{Ty}$. Expand the stripping term as Under the three displayed term binders, universal elimination gives Here $K_X(T{S}_{\kappa }){⟶}_{\beta }X$, but conversion is not needed to match the argument and domain: they are already the same constructor expression. The two term lambdas and outer type lambda therefore give $${\mathsf{strip}}_{K_X,\kappa ,T}:\mathsf{Strip}{K}_X(\mathrm{\forall }u::\kappa .K_X(Tu)).$$

For the calculation, let $q$ have the type required under $u::\kappa$. Suppressing only annotations already displayed above, This is (7.10) at the stated higher kind.

The term tree consists of a variable, a term abstraction, a constructor abstraction, and the final constructor application. Hence $|e|=4$. Its operator $$\mathrm{\Lambda }A::\mathsf{Ty}.\lambda x:A.x$$ is normal but not neutral, so the strengthened normality fold first produces $\mathsf{TF}$. The final type-application case copies that pair’s neutral component, which is false, into both positions. It therefore produces $\mathsf{FF}$, and the public projection gives $\mathsf{isNormal}[\widehat{I\to I}]\hat{\mathcal{D}}{⟶}_{\beta }^{\ast }\mathsf{false}$. This agrees with the visible type-beta redex at the root. The same outer constructor makes $\mathsf{isAbs}[\widehat{I\to I}]\hat{\mathcal{D}}$ reduce to $\mathsf{false}$, while the size theorem gives $$\mathsf{size}[\widehat{I\to I}]\hat{\mathcal{D}}{⟶}_{\beta }^{\ast }\underset{―}{4}.$$

The copied variable has type $FZ$. Thus the term-abstraction case is instantiated at source domain and codomain $Z$, giving $$q_{\mathrm{a}\mathrm{b}\mathrm{s}}=\mathit{abs}[Z][Z](\lambda z:FZ.z):F(FZ\to FZ).$$ Abstracting $Z$ produces a family of type $$\mathrm{\Lambda }Z::\mathsf{Ty}.q_{\mathrm{a}\mathrm{b}\mathrm{s}}:\mathrm{\forall }Z::\mathsf{Ty}.F(FZ\to FZ)=P_F.$$ Put $T_F:={\mathsf{pre}}_F(\lambda Z::\mathsf{Ty}.Z\to Z)$. Then $$T_{F}Z{\to }_{\beta }(FZ\to FZ),$$ so the strip term has type $${\mathsf{strip}}_{F,\mathsf{Ty},T_F}:\mathsf{Strip}F{P}_F$$ by constructor conversion. These are the two term arguments of the constructor-abstraction case, and therefore $$q_{\mathrm{t}\mathrm{a}\mathrm{b}\mathrm{s}}=\mathit{tabs}[P_F]{\mathsf{strip}}_{F,\mathsf{Ty},T_F}(\mathrm{\Lambda }Z::\mathsf{Ty}.q_{\mathrm{a}\mathrm{b}\mathrm{s}}):F{P}_F.$$

The source operator has universal type represented by $P_F$, whereas the whole instance has arrow type represented by $R_F=F{P}_F\to F{P}_F$. Hence the type-application interface first receives the operator index $P_F$ and its child $q_{\mathrm{t}\mathrm{a}\mathrm{b}\mathrm{s}}:F{P}_F$. It then receives the result index $R_F$ and the instantiation map ${\mathsf{inst}}_{P_F,P_F}:P_F\to F{R}_F$. Therefore $$q_0=\mathit{tapp}[P_F]q_{\mathrm{t}\mathrm{a}\mathrm{b}\mathrm{s}}[R_F]{\mathsf{inst}}_{P_F,P_F}:F{R}_F.$$ Reversing the two indices would require $q_{\mathrm{t}\mathrm{a}\mathrm{b}\mathrm{s}}:F{R}_F$ and is rejected before any reduction is considered.

Put After the recursive child has become $q^{\prime }$, the constructor-application branch is $$(\mathrm{\Lambda }X.\lambda f:X.\mathrm{\Lambda }Y.\lambda g:X\to Y.gf)[P]q^{\prime }[R](\lambda x:P.x[Q]).$$ Keeping the type-beta and term-beta contractions separate gives The induction hypothesis gives $q^{\prime }{⟹}_{\beta }^{\ast }e$ under the constructor variable $u$. The first use of type recovery is $Q{\to }_{\beta }^{\ast }C$; compatible mixed reduction therefore gives $q^{\prime }[Q]{⟹}_{\beta }^{\ast }e[C]$. The second use is $R{\to }_{\beta }^{\ast }A[C/u]$, which converts the branch result type to the source result type. The operator index $P$ already has universal outer form by its definition, so no third recovery step is needed to form $q^{\prime }[Q]$.

The source tree has an application root, a term-abstraction operator, and the closed identity argument. Counting the identity as its type abstraction, term abstraction, and variable body gives six nodes. The fold visits each child before the application case. Each copied variable is replaced by $\mathsf{one}$ in the strengthened size proof; each unary abstraction case applies successor to its child’s count; and the application case returns one plus the two child counts. Thus $$1+(1+1)+(1+(1+1))=6.$$ The outer-constructor fold ignores both recursive results and selects its application result, so it returns $\mathsf{false}$ for the abstraction test. Both answers follow the displayed source tree rather than its beta-normal form.

Under $x:A$, the fundamental lemma gives a prequotation $$F::\mathsf{Ty}\to \mathsf{Ty};x:F{\mathsf{pre}}_F(A),{\mathrm{\Xi }}_F⊢q:F{\mathsf{pre}}_F(B).$$ After substituting $\mathsf{Id}$ and the four unquoting cases, the open claim is $q{⟹}_{\beta }^{\ast }e$ under $x:A$, up to the constructor conversions supplied by type recovery. The variable case is the copied variable. The term-abstraction case contracts $\mathsf{unAbs}$ and applies the induction hypothesis below the binder; the term-application case contracts $\mathsf{unApp}$, then applies the two induction hypotheses. In the type-abstraction case, $\mathsf{unTAbs}$ discards its strip argument and returns the copied type abstraction, after which compatible reduction applies the induction hypothesis below the type binder. In the type-application case, $\mathsf{unTApp}$ applies $\mathsf{inst}$ to the recursively unquoted operator. Expanding $\mathsf{inst}$ yields $q^{\prime }[Q]$, where $Q={\mathsf{pre}}_{\mathsf{Id}}(C)$, and type recovery converts (Q) to the source argument (C). Conversion changes no term, so the same induction hypothesis is reused at the converted result type. What is unavailable is the closure step used in the closed quotation theorem. The term $q$ still has the free variable $x:F{\mathsf{pre}}_F(A)$. Abstracting $F$ and the four cases alone would leave a free variable whose type contains the bound $F$, so it does not produce a term of $\mathsf{Exp}\hat{B}$. The prequotation and its unquotation property remain valid as open judgments.

The term ${\mathsf{junk}}_B$ has the required representation type by the four case interfaces. Its outer $\mathit{tapp}$ child is nevertheless headed by $\mathit{abs}$ at the arrow-normal index $P_F$. In a genuine type-application quotation, that child quotes an operator of universal type, so its first index is the representation of a universal. Constructor normalization and injectivity of outer normal forms separate these shapes. Thus ${\mathsf{junk}}_B$ is well typed but outside the quotation image; no normalization contradiction is needed.

An internal quoter at each fixed index would still not supply the typing equalities required by the diagonal. Write $Q(A):=\mathsf{Exp}\hat{A}$ and suppose, hypothetically, that ${\mathsf{quote}}_A:A\to Q(A)$ is available for each closed $A$. If $u_A:Q(A)\to A$, then typing $(u_{A}x)x$ for $x:Q(A)$ first requires $$A{=}_{\beta }Q(A)\to B$$ for some $B$. If the resulting diagonal term has type $P$, its quotation has type $Q(P)$, while the diagonal term expects $Q(A)$; self-application therefore also requires $Q(P){=}_{\beta }Q(A)$. To use the unquoting equation at that quotation requires $P{=}_{\beta }A$. The hypothetical family of quoters establishes none of these constructor equalities. Thus it does not by itself reinstate the raw diagonal. Strong normalization is used only after the missing equalities are assumed and the forbidden application has thereby been made well typed.