Type Operators, Kinds, and System F-omega

Proof. For weakening, induct on the displayed kinding derivation. In K-Var, the declaration used by the premise is still present after insertion. For K-App, K-Arr, and K-Prod, weaken every premise and reapply the same rule; K-Nat has no premises. In a binder rule, say K-Abs, first choose its bound variable $v$ fresh for the inserted declaration. Its premise has context ${\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2,v::{\kappa }_0$; apply the induction hypothesis at this longer suffix and reapply K-Abs. The K-All and K-Some cases are identical.

For substitution, again induct on the final rule. If K-Var selects $u$, replace that leaf by the given derivation of $B$ and weaken it through ${\mathrm{\Delta }}_2$; if it selects another variable, keep the leaf. For K-App, K-Arr, and K-Prod, apply the induction hypothesis to every premise and rebuild the same rule; K-Nat is unchanged. In a binder rule, choose the displayed binder $v$ distinct from $u$ and fresh for $B$. For example, the K-All premise is $${\mathrm{\Delta }}_1,u::{\kappa }^{\prime },{\mathrm{\Delta }}_2,v::{\kappa }_0⊢A_0::\mathsf{Ty}.$$ The induction hypothesis, with suffix ${\mathrm{\Delta }}_2,v::{\kappa }_0$, gives ${\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2,v::{\kappa }_0⊢A_0[B/u]::\mathsf{Ty}$. Rule K-All concludes with subject $\mathrm{\forall }v::{\kappa }_0.A_0[B/u]$. The binder clause of constructor substitution gives $$\mathrm{\forall }v::{\kappa }_0.A_0[B/u]=(\mathrm{\forall }v::{\kappa }_0.A_0)[B/u].$$ Replacing K-All by K-Abs or K-Some gives the other two binder cases. ◻

Proof. Rule selection is read off the table: the eight rules have subjects of eight distinct outer forms. This does not yet assert that an application’s intermediate domain kind is unique. Uniqueness of the conclusion kind is a structural induction on $A$. For $u$ the context determines $\kappa$, declarations being distinct by KCtx-Ext. For $\mathbb{N}$, arrows, products, and both quantifiers the kind is $\mathsf{Ty}$ in every derivation. For $\lambda u::{\kappa }_1.A_0$, inversion gives $\kappa ={\kappa }_1\to {\kappa }_2$ and ${\kappa }^{\prime }={\kappa }_1\to {\kappa }_2^{\prime }$ with both ${\kappa }_2,{\kappa }_2^{\prime }$ kinds of $A_0$ in $\mathrm{\Delta },u::{\kappa }_1$; the induction hypothesis gives ${\kappa }_2={\kappa }_2^{\prime }$. Note that the domain kind is read off the annotation—this is where Church-style annotation is used, exactly as in lemma 2.19. For $A_1{A}_2$, the inductive hypothesis for $A_1$ equates the two arrow kinds, and injectivity of the kind grammar equates their codomains. For derivation uniqueness, the outer constructor first selects its kinding rule. In the application case it selects K-App; kind uniqueness just proved fixes the intermediate domain kind, and the induction hypotheses uniquely determine the derivations of $\mathrm{\Delta }⊢A_1::{\kappa }_1\to {\kappa }_2$ and $\mathrm{\Delta }⊢A_2::{\kappa }_1$, so the reconstructed K-App node is unique. For a variable, the unique context declaration fixes the leaf; K-Nat is the unique premise-free leaf. Arrow and product nodes have two premise derivations, each fixed by its induction hypothesis. Universal, existential, and abstraction nodes have one body premise under the binder, again fixed by the induction hypothesis. These cases exhaust the rule table. ◻

Proof. Induct on the typing derivation. At T-Var, context formation gives the declared type’s kind. The lambda, pair, and natural cases rebuild K-Arr, K-Prod, or K-Nat from the induction hypotheses. In an application or projection, lemma 7.9 inverts the kinding of the premise’s arrow or product type to obtain the required component. The T-TLam case uses K-All. The T-TApp case uses constructor substitution, lemma 7.8, on the body formation obtained by inverting K-All. Finally, the equality premise of T-Conv already forms its right endpoint at $\mathsf{Ty}$. ◻

Proof. Induction on the derivation of the step. For TR-Beta, the subject is $(\lambda u::{\kappa }_1.A_0)B$. Inversion (lemma 7.9) gives $\mathrm{\Delta }⊢\lambda u::{\kappa }_1.A_0::{\kappa }_1\to \kappa$ and $\mathrm{\Delta }⊢B::{\kappa }_1$, and inverting again, $\mathrm{\Delta },u::{\kappa }_1⊢A_0::\kappa$. Substitution (lemma 7.8) yields $\mathrm{\Delta }⊢A_0[B/u]::\kappa$. Each congruence case applies the inductive hypothesis to the stepped premise of the inverted rule and reapplies the rule. ◻

Proof. Rule induction. Q-Refl and the congruence rules are immediate from their premises and the corresponding kinding rules; Q-Sym and Q-Trans rearrange inductive hypotheses; Q-Beta kinds its left side by K-Abs and K-App and its right side by lemma 7.8. ◻

Proof. Induction on the step. At a redex, inversion gives $\mathrm{\Delta },u::{\kappa }_1⊢A_0::{\kappa }_2$ and $\mathrm{\Delta }⊢B::{\kappa }_1$, exactly the premises of Q-Beta. A congruence step in an argument position uses the inductive hypothesis there, Q-Refl at the unchanged positions, and the matching congruence rule Q-Arr, …, Q-App. The starred form follows by Q-Refl and Q-Trans, using lemma 7.10 to keep each intermediate constructor kinded. ◻

Proof. Finite branching is a structural induction: a step is either TR-Beta at the root, possible in at most one way, or a step in one of finitely many argument positions, each finitely branching by the inductive hypothesis. For the second claim, consider the tree whose root is $A$ and whose children of any node are its one-step reducts; it is finitely branching, and every branch is finite because $A\in \mathrm{SN}$. If the branch lengths were unbounded, we could choose at the root a child whose subtree has unbounded branch lengths (some child must, as there are finitely many), and repeat, producing an infinite branch—a contradiction. So branch lengths are bounded, and $\nu (A)$ is their maximum; a reduct’s subtree is a subtree of $A$’s, giving the strict decrease. ◻

Proof. The outer simultaneous induction is on $\kappa$ and proves (CR1)–(CR3) together. In the arrow-kind (CR3) case a second induction on the natural number $\nu (B)$ controls reductions in the argument. No third induction is implicit.

Base kind. (CR1) is the definition. (CR2): a suffix of an infinite reduction from $A^{\prime }$ would extend to one from $A$. (CR3): any infinite sequence from $A$ has a first step, landing in some reduct, which is in $\mathrm{SN}$ by hypothesis; contradiction. (Neutrality is not needed at the base kind.)

Arrow kind ${\kappa }_1\to {\kappa }_2$. (CR1): let $A\in {\mathrm{Red}}_{{\kappa }_1\to {\kappa }_2}$ and pick a variable $u$; by the inductive (CR3) at ${\kappa }_1$, $u\in {\mathrm{Red}}_{{\kappa }_1}$, so $Au\in {\mathrm{Red}}_{{\kappa }_2}\subseteq \mathrm{SN}$ by the inductive (CR1). An infinite reduction from $A$ would, under the application congruence, give one from $Au$; so $A\in \mathrm{SN}$. (CR2): for $B\in {\mathrm{Red}}_{{\kappa }_1}$ we have $AB\in {\mathrm{Red}}_{{\kappa }_2}$ and $AB{⟶}_{\beta }{A}^{\prime }B$, so $A^{\prime }B\in {\mathrm{Red}}_{{\kappa }_2}$ by the inductive (CR2). (CR3): let $A$ be neutral with all reducts in ${\mathrm{Red}}_{{\kappa }_1\to {\kappa }_2}$, and let $B\in {\mathrm{Red}}_{{\kappa }_1}$; then $B\in \mathrm{SN}$ by the inductive (CR1), and we show $AB\in {\mathrm{Red}}_{{\kappa }_2}$ by a side induction on $\nu (B)$. The constructor $AB$ is neutral, so by the inductive (CR3) at ${\kappa }_2$ it suffices that all its one-step reducts are in ${\mathrm{Red}}_{{\kappa }_2}$. A reduct is either $A^{\prime }B$ with $A{⟶}_{\beta }{A}^{\prime }$—then $A^{\prime }\in {\mathrm{Red}}_{{\kappa }_1\to {\kappa }_2}$ by hypothesis, so $A^{\prime }B\in {\mathrm{Red}}_{{\kappa }_2}$—or $A{B}^{\prime }$ with $B{⟶}_{\beta }{B}^{\prime }$—then $B^{\prime }\in {\mathrm{Red}}_{{\kappa }_1}$ by the inductive (CR2) and , so the side induction applies—or a root $\beta$-step, impossible since $A$ is neutral, hence not an abstraction. ◻

Proof. (1) Structural induction on $A$ over representatives whose binders avoid $u,v$ and the free variables of $B,C$. For $A=v$: both sides are $B[C/u]$. For $A=u$: the left side is $C$, the right side is $C[B[C/u]/v]=C$ since $v$ is not free in $C$. Other variables give themselves on both sides, and every composite form distributes both substitutions to its arguments, where the inductive hypothesis applies.

(2) Induction on the step. For TR-Beta: Congruence steps substitute in an argument position and use the inductive hypothesis under the same congruence rule.

(3) Structural induction on $A$. At $A=u$ use the single step $C{⟶}_{\beta }{C}^{\prime }$; another variable takes no steps. Application, arrow, and product concatenate the induction-hypothesis sequences in their argument positions through the corresponding congruence rules. At $\diamond v::\kappa .A_0$, for $\diamond \in \{\lambda ,\mathrm{\forall },\mathrm{\exists }\}$, first freshen $v$ away from $u,C,C^{\prime }$, apply the induction hypothesis to $A_0$, and lift its sequence under the binder congruence.

(4) Structural induction on $A$, choosing every binder fresh for $\theta ,B,u$. At $A=u$, both sides are $B$. At another variable $v$, freshness ensures that substituting $u$ into $\theta (v)$ leaves it unchanged. For an arrow $A_1\to A_2$, apply the two induction hypotheses and rebuild the arrow. For $\mathrm{\forall }v::\kappa .A_0$, choose $v$ fresh for $\theta ,B,u$, apply the body hypothesis, and reattach the binder. Product and existential formers are the corresponding binary and binder cases. ◻

Proof. Fix $B\in {\mathrm{Red}}_{{\kappa }_1}$; we must show $(\lambda u::{\kappa }_1.A)B\in {\mathrm{Red}}_{{\kappa }_2}$. Variables are reducible by lemma 7.16; taking the variable $u$ itself for $B$ in the hypothesis gives $A=A[u/u]\in {\mathrm{Red}}_{{\kappa }_2}$, so $A\in \mathrm{SN}$ by (CR1), and $B\in \mathrm{SN}$ likewise. We argue by complete induction on $\nu (A)+\nu (B)$, generalized over both $A$ and $B$ and over the hypothesis that $A[B_0/u]\in {\mathrm{Red}}_{{\kappa }_2}$ for every $B_0\in {\mathrm{Red}}_{{\kappa }_1}$. Thus the induction hypothesis remains available after replacing $A$ by a reduct $A^{\prime }$ or $B$ by a reduct $B^{\prime }$. The application is neutral, so by (CR3) it suffices that each one-step reduct lies in ${\mathrm{Red}}_{{\kappa }_2}$. The reducts are:

• $A[B/u]$, in ${\mathrm{Red}}_{{\kappa }_2}$ by hypothesis;

• $(\lambda u::{\kappa }_1.A^{\prime })B$ with $A{⟶}_{\beta }{A}^{\prime }$: for every $B_0\in {\mathrm{Red}}_{{\kappa }_1}$, $A[B_0/u]{⟶}_{\beta }{A}^{\prime }[B_0/u]$ by lemma 7.17(2), so $A^{\prime }[B_0/u]\in {\mathrm{Red}}_{{\kappa }_2}$ by (CR2); since , the inductive hypothesis applies;

• $(\lambda u::{\kappa }_1.A)B^{\prime }$ with $B{⟶}_{\beta }{B}^{\prime }$: then $B^{\prime }\in {\mathrm{Red}}_{{\kappa }_1}$ by (CR2) and , so the inductive hypothesis applies.

By (CR3), $(\lambda u::{\kappa }_1.A)B\in {\mathrm{Red}}_{{\kappa }_2}$, and as $B$ was arbitrary, $\lambda u::{\kappa }_1.A\in {\mathrm{Red}}_{{\kappa }_1\to {\kappa }_2}$. ◻