ch:type-operators: ch:type-operators

In the context $$c::\mathsf{Ty}\to \mathsf{Ty},d::\mathsf{Ty}\to \mathsf{Ty},a::\mathsf{Ty},$$ write this context as $\mathrm{\Delta }$. Every leaf and rule instance is Now apply K-Abs three times. The complete judgment ladder is The last line discharges the binders in the same order in which they occur in the definition of $\mathsf{Comp}$.

Compatible constructor reduction gives The last constructor contains no constructor application whose head is a lambda, so it is normal.

Choose $v\ne u$ fresh; it is also fresh for $B=\mathbb{N}\times \mathbb{N}$. Before substitution, the relevant premise is $u::\mathsf{Ty},v::\mathsf{Ty}⊢u\to v::\mathsf{Ty}$. After applying lemma 7.8, the complete rebuilt tree is $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{v::\mathsf{Ty}⊢\mathbb{N}::\mathsf{Ty}}}\mathrm{K}-\mathrm{Nat}\\ {\displaystyle \frac{\phantom{X}}{v::\mathsf{Ty}⊢\mathbb{N}::\mathsf{Ty}}}\mathrm{K}-\mathrm{Nat}\end{array}}{v::\mathsf{Ty}⊢\mathbb{N}\times \mathbb{N}::\mathsf{Ty}}}\mathrm{K}-\mathrm{Prod}\\ {\displaystyle \frac{v::\mathsf{Ty}\in v::\mathsf{Ty}}{v::\mathsf{Ty}⊢v::\mathsf{Ty}}}\mathrm{K}-\mathrm{Var}\end{array}}{v::\mathsf{Ty}⊢(\mathbb{N}\times \mathbb{N})\to v::\mathsf{Ty}}}\mathrm{K}-\mathrm{Arr}}{\cdot ⊢\mathrm{\forall }v::\mathsf{Ty}.(\mathbb{N}\times \mathbb{N})\to v::\mathsf{Ty}}\mathrm{K}-\mathrm{All}.$$ The subject is exactly $(\mathrm{\forall }v::\mathsf{Ty}.u\to v)[(\mathbb{N}\times \mathbb{N})/u]$; freshness prevents capture at the quantifier.

Let $A$ be neutral with every reduct in ${\mathrm{Red}}_{{\kappa }_1\to {\kappa }_2}$, and let $B\in {\mathrm{Red}}_{{\kappa }_1}$. By (CR1) at ${\kappa }_1$, $B\in \mathrm{SN}$; induct on its reduction height $\nu (B)$. Every step from the neutral application $AB$ has one of two forms: $$AB{⟶}_{\beta }{A}^{\prime }B\text{or}AB{⟶}_{\beta }A{B}^{\prime }.$$ In the first case the hypothesis on $A$ gives $A^{\prime }\in {\mathrm{Red}}_{{\kappa }_1\to {\kappa }_2}$, hence $A^{\prime }B\in {\mathrm{Red}}_{{\kappa }_2}$. In the second, (CR2) gives $B^{\prime }\in {\mathrm{Red}}_{{\kappa }_1}$ and , so the side induction gives the result. A root beta step would require $A$ to be an abstraction, contradicting neutrality. Thus (CR3) at ${\kappa }_2$ yields $AB\in {\mathrm{Red}}_{{\kappa }_2}$.

The root contraction and the argument contraction are $$(\lambda u::\kappa .A_0)B_0{⟶}_{\beta }{A}_0[B_0/u],(\lambda u::\kappa .A_0)B_0{⟶}_{\beta }(\lambda u::\kappa .A_0)B_0^{\prime }.$$ Take $A_0[B_0^{\prime }/u]$ as the common reduct. The right branch reaches it by one TR-Beta step. The left branch reaches it by lemma 7.17(3), which transports $B_0{⟶}_{\beta }{B}_0^{\prime }$ through every occurrence of $u$ in $A_0$, using zero or more compatible steps.

Write paths from the root with $L$ for the left child of an application and $ϵ$ for the root. The deterministic run is Kind annotations on the two constructor binders are those in the exercise and are unchanged by the calculation. The comparison constructor $\mathbb{N}\times \mathbb{N}$ has no redex, so both inputs normalize to alpha-identical forms. By corollary 7.26, their constructor equality holds.

In the unannotated rule, the kind assigned to the bound constructor is a choice made by the derivation rather than syntax. Choosing $u::\mathsf{Ty}$ gives $$\frac{{\displaystyle \frac{u::\mathsf{Ty}\in u::\mathsf{Ty}}{u::\mathsf{Ty}⊢u::\mathsf{Ty}}}\mathrm{K}-\mathrm{Var}}{\cdot ⊢\lambda u.u::\mathsf{Ty}\to \mathsf{Ty}}\mathrm{K}-\mathrm{Abs}.$$ Choosing instead $u::\mathsf{Ty}\to \mathsf{Ty}$ gives the distinct tree $$\frac{{\displaystyle \frac{u::\mathsf{Ty}\to \mathsf{Ty}\in u::\mathsf{Ty}\to \mathsf{Ty}}{u::\mathsf{Ty}\to \mathsf{Ty}⊢u::\mathsf{Ty}\to \mathsf{Ty}}}\mathrm{K}-\mathrm{Var}}{\cdot ⊢\lambda u.u::(\mathsf{Ty}\to \mathsf{Ty})\to (\mathsf{Ty}\to \mathsf{Ty})}\mathrm{K}-\mathrm{Abs}.$$ The subjects of the two conclusions are literally the same unannotated constructor. Their kinds differ, so the Church-style uniqueness proof fails exactly where it formerly read the domain kind from the abstraction annotation.

The failure occurs immediately in candidate condition CR1. If the base candidate at $\mathsf{Ty}$ contains raw constructors having merely one terminating reduction sequence, membership no longer implies strong normalization. Thus the first reducibility-candidate obligation already fails; the fundamental lemma has no valid base candidate to use.

The arrow candidate also exposes the defect through CR3. Its neutral expansion argument reasons about every one-step reduct and uses a subsidiary induction whose measure is supplied by strong normalization. Existence of one terminating branch gives neither the universal premise nor a bound on the other compatible branches.

Let $$\mathrm{\Omega }=(\lambda u::\mathsf{Ty}.uu)(\lambda u::\mathsf{Ty}.uu).$$ The displayed raw constructor is $$(\lambda x::\mathsf{Ty}.\mathbb{N})\mathrm{\Omega }.$$ Reducing the outer redex first yields $\mathbb{N}$, so it has a terminating path. Compatible reduction may instead reduce inside the argument: $\mathrm{\Omega }\to \mathrm{\Omega }$. Repeating that step produces an infinite path beneath the unchanged outer application. Weak normalization therefore does not control all compatible-reduction paths.

The example is deliberately ill-kinded: the self-application in $\mathrm{\Omega }$ cannot be assigned a kind in $F_{\omega }$. This does not make the diagnostic circular. Reducibility is first defined as a predicate on raw constructors; the fundamental lemma later proves that well-kinded constructors inhabit the appropriate candidates. A proposed base predicate must satisfy the candidate conditions on the raw terms to which its definition applies, before kinding selects the terms used by the theorem.

Normalize beneath the two universal binders. The left side becomes $$\mathrm{\forall }a::\mathsf{Ty}.\mathrm{\forall }b::\mathsf{Ty}.(a\to b)\to ((a\times a)\times (a\times a))\to ((b\times b)\times (b\times b)),$$ whereas the right side becomes $$\mathrm{\forall }a::\mathsf{Ty}.\mathrm{\forall }b::\mathsf{Ty}.(a\to b)\to (a\times a)\to (b\times b).$$ Both are normal. Their next domains after $(a\to b)$ have distinct product trees, so they are not alpha-equal. By the common-normal-form decision theorem, the proposed constructor equality does not hold.