Chapter 94Optional

Subject-Dependent Self Types

Prerequisites. Direct starred prerequisites: Chapter 37. No later core chapter depends on this route.

Dependent intersection can add a view $B (t)$ to a subject $t$ whose left-hand type is already known. It cannot define one type $T$ whose membership condition says, for every $t : T$ , that a predicate holds of $t$ itself. The Church encoding of naturals exposes the missing dependency. Its iterator provides $n : \forall C : U_{0} . (C \to C) \to C \to C,$ but induction needs a motive $C : Nat \to U_{0}$ and the conclusion $C (n)$ , where the subject $n$ occurs in its own assigned type.

System S

Convention 94.1 — The frozen System S ¶

System S is Fu and Stump’s Curry-style extension of the Calculus of Constructions. Its terms are untyped lambda terms with globally defined closed constants. Its types add implicit products $\forall x : A . B$ , type-level term abstraction and application, and the subject-dependent self type $ι x . T$ . A global closure may contain a singly recursive type definition $X \mapsto T$ , but every occurrence of $X$ in $T$ is positive or lies in an erased position. Term definitions are nonrecursive and closed. The metatheorems below apply to this exact signature, not to an unrestricted recursive type equation.

Referenced from 3 locations

Subject-Dependent Self Types

An implicit product classifies a term without adding a lambda. Its binder is erased both at introduction and elimination. The rules are

Γ ⊢ A type

Γ, x : A ⊢ B type

Γ ⊢ \forall x : A . B type

S–F

Γ, x : A ⊢ t : B

x \notin FV (t)

Γ ⊢ t : \forall x : A . B

S–I

Γ ⊢ t : \forall x : A . B

Γ ⊢ u : A

Γ ⊢ t : B [u / x]

S–E

Γ, x : A ⊢ t : B

x \notin FV (t)

erase (t) = erase (t)

S–β

The last rule records the computation: implicit abstraction and instantiation perform type substitution but no term reduction.

Definition 94.2 — Subject-dependent self ¶

The type $ι x . T$ binds the term variable $x$ in $T$ . Formation, generation, instantiation, and their erasure equation are

Γ, x : ι x . T ⊢ T type

Γ ⊢ ι x . T type

S-Self-F

Γ ⊢ t : T [t / x]

Γ ⊢ ι x . T type

Γ ⊢ t : ι x . T

S-Self-Gen

Γ ⊢ t : ι x . T

Γ ⊢ t : T [t / x]

S-Self-Inst

Γ ⊢ t : ι x . T

erase (selfGen (t)) = erase (t) = erase (selfInst (t))

S-Self-Erase

The terms in the source conclusions are all the same Curry term $t$ ; $selfGen$ and $selfInst$ above name typing steps, not runtime constructors. The rules are inverse changes of type annotation, not a judgmental equation $ι x . T \equiv T [t / x]$ valid for arbitrary $t$ .

Referenced from 2 locations

Subject-Dependent Self Types

Let $z : ι x . T$ be neutral. Rule S-Self-Inst changes its type to $T [z / x]$ , but no reduction occurs. This is the stuck case: the self rule reveals a dependent view of $z$ without revealing the head constructor of $z$ .

Exercise 94.1 ¶

★☆☆ Starting from $t : T [t / x]$ , apply S-Self-Gen and then S-Self-Inst. Write the type after each step and compute the erasure. Explain why the calculation does not prove $ι x . T \equiv T [u / x]$ for an unrelated $u$ .

Referenced from 3 locations

The closure restriction does work

The tempting recursive equation $Bad : = Bad \to N$ places $Bad$ to the left of an arrow. If it were admitted equi-recursively, the untyped self-application $δ : = λ x . x x$ could receive type $Bad \to N$ and $δ δ$ would reproduce itself. This would contradict strong normalization.

Definition 94.3 — Positive recursive closure ¶

For the strong-normalization theorem, a closure entry $X \mapsto T$ satisfies $Pos (X, T)$ when every non-erased occurrence of $X$ is positive. The polarity calculation is ${pol}_{p} (A \to B) = {pol}_{\neg p} (A) \land {pol}_{p} (B),$ and products preserve polarity in their bodies. Occurrences in kinds and in the domain annotation of an implicit product are erased by the target translation and impose no recursive target equation. Mutual recursive type definitions and open recursive right-hand sides are excluded from the frozen closure.

Referenced from 2 locations

Subject-Dependent Self Types

For $Bad \mapsto Bad \to N$ , the occurrence is negative and the closure is rejected. For the Church natural closure below, the recursive occurrences in motive annotations and implicit domains are erased, while the remaining target equation is positive.

Induction from self instantiation

Define a closed recursive type closure $μ_{N}$ by $\begin{aligned} Nat & \mapsto ι x . \forall C : Nat \to U_{0} . (\forall n : Nat . C (n) \to C (S (n))) \to C (0) \to C (x), \\ 0 & \mapsto λ s . λ z . z, \\ S & \mapsto λ n . λ s . λ z . s (n s z) . \end{aligned}$ The binders over $C$ and $n$ are implicit. Their erasure gives the ordinary Church type $(C \to C) \to C \to C$ .

Lemma 94.4 — Constructor typing ¶

Under $μ_{N}$ , $0 : Nat, S : Nat \to Nat .$

Referenced from 3 locations

Subject-Dependent Self Types

Proof of Lemma 94.4 — Constructor typing

Proof. For zero, fix $C$ , a step $s$ , and a base $z : C (0)$ . The term $λ s . λ z . z$ has the instantiated body type ending in $C (λ s . λ z . z)$ because this term is definitionally the Church zero. Rule S-Self-Gen gives the self type $Nat$ .

For successor, assume $n : Nat$ . By S-Self-Inst, $n : \forall C : Nat \to U_{0} . (\forall k : Nat . C (k) \to C (S (k))) \to C (0) \to C (n) .$ Thus $n s z : C (n)$ and $s n (n s z) : C (S (n))$ . Abstraction gives the body required for $S (n)$ , and S-Self-Gen gives $S (n) : Nat$ . ◻

Theorem 94.5 — Derived natural-number induction ¶

The Curry term $ind : = λ s . λ z . λ n . n s z$ has type $\forall C : Nat \to U_{0} . (\forall n : Nat . C (n) \to C (S (n))) \to C (0) \to \prod_{n : Nat} C (n) .$

Referenced from 2 locations

Subject-Dependent Self Types

Proof of Theorem 94.5 — Derived natural-number induction

Proof. Fix $C$ , $s$ , $z$ , and $n : Nat$ . Rule S-Self-Inst gives exactly the implicit product displayed in the first paragraph of lemma 94.4. Three eliminations yield $n s z : C (n) .$ Abstraction over $n$ , $z$ , and $s$ , followed by the implicit introduction for $C$ , gives the stated type. The type of the final result mentions the function argument $n$ because self instantiation substituted that same subject for $x$ . ◻

The constructor computations occur after erasure: $\begin{aligned} ind s z 0 & \overset{β}{⟶} z, \\ ind s z (S n) & \overset{β}{⟶^{*}} s n (n s z) . \end{aligned}$ For a neutral $n$ , $n s z$ remains stuck even though its type is $C (n)$ .

Exercise 94.2 ¶

★★☆ Fix $A : U_{0}$ . Work in context $n : Nat$ with the indexed closure $\begin{aligned} Vec (A, n) \mapsto & ι v . \forall C : (\prod_{k : Nat} Vec (A, k) \to U_{0}) . \\ C (0, vnil) \to \\ (\forall k : Nat . \forall a : A . \forall x s : Vec (A, k) . C (k, x s) \to \\ C (S (k), vcons (k, a, x s))) \to C (n, v) . \end{aligned}$ Give fully typed Church terms for $vnil$ and $vcons$ under this closure. Then derive the exact result type $\prod_{n : Nat} \prod_{v : Vec (A, n)} C (n, v)$ of the induction term, including the nil and cons premises displayed above and the final self-instantiation step.

Referenced from 3 locations

Metatheory at the frozen signature

Lemma 94.6 — System S substitution ¶

If $Γ, x : A, Δ ⊢ t : T$ and $Γ ⊢ u : A$ , then $Γ, Δ [u / x] ⊢ t [u / x] : T [u / x]$ .

Referenced from 2 locations

Subject-Dependent Self Types

Proof of Lemma 94.6 — System S substitution

Proof. Induct on the typing derivation. The implicit-product cases choose their bound variable outside $FV (u) \cup FV (Γ) \cup FV (Δ)$ and apply the induction hypothesis under that binder. In the S-Self-Gen case, the induction hypothesis gives $t [u / x] : T [t / y] [u / x]$ . Choose the self binder $y$ outside $FV (u)$ . Capture avoidance gives $T [t / y] [u / x] = T [u / x] [t [u / x] / y],$ which is the premise of S-Self-Gen for $ι y . T [u / x]$ . The S-Self-Inst case uses the same equation in the opposite direction. Closure entries are closed, so substitution does not alter their right-hand sides. ◻

Theorem 94.7 — Confluence and preservation ¶

In a well-formed System S closure, beta reduction on terms and types is confluent. If $Γ ⊢ t : T$ and $t ⟶_{β} t^{'}$ , then $Γ ⊢ t^{'} : T$ .

Referenced from 2 locations

Subject-Dependent Self Types

Proof of Theorem 94.7 — Confluence and preservation

Proof. This is an exact import for the signature of convention 94.1. Fu and Stump prove confluence of beta reduction as Lemma 1 on page 12. Their self-conversion relation and $ι$ -elimination theorem are Definition 15 and Theorem 6 on pages 11–12. Definitions 17–20 and Lemmas 3–7 on page 13 define the term- and type-morphing substitutions and prove product compatibility as Theorem 7. Theorem 8 on that page then has the signature $Γ ⊢ t : T, Γ ⊢ t ⟶_{β} t^{'}, Γ wf ⟹ Γ ⊢ t^{'} : T .$ These imported results give the two clauses of the theorem; no theorem is transferred to mutual, open, or nonpositive closure entries [FS14]. ◻

Theorem 94.8 — Strong normalization of System S ¶

If $Γ wf$ and $Γ ⊢ t : T$ in the frozen System S signature, then $t$ is strongly normalizing for beta reduction.

Referenced from 2 locations

Subject-Dependent Self Types

Proof of Theorem 94.8 — Strong normalization of System S

Proof. Import the exact erasure and reducibility development of Fu and Stump. On page 10, Definitions 8–11 give the target $F_{ω}$ signature with positive definitions and the kind, type, and context erasures; Theorem 4 proves that a well-formed System S derivation maps to that target. On page 11, Definitions 12–14 give the reducibility candidates, the least-fixed-point environment for positive recursive definitions, and the logical relation. Theorem 5 states that if $Γ ⊢ t : T$ and $Γ wf$ , then the unchanged Curry term belongs to the candidate interpreting the erased $T$ . The sentence immediately following Theorem 5 combines it with Theorem 4 to conclude strong normalization. Those results have exactly the closure and positivity hypotheses frozen here, so they establish the displayed statement [FS14]. ◻

If the positivity hypothesis is removed, $Bad$ above and $δ δ$ invalidate the fixed-point interpretation and the conclusion. If mutual recursion or open closure right-hand sides are added, the displayed translation no longer proves the theorem; a separate target metatheory would be required.

Four distinct self binders

System	self binder occurs in	enabling rule	erasure
dependent intersection	second view $B (x)$	same-subject introduction	one existing term
System S	the assigned type $T (x)$	self generation/instantiation	unchanged term
OO $Self$	method result types	class/matching rules	object value
DOT	recursive object type	recursive introduction/path selection	allocated object

An identity self-loop instead has a path variable $p : x =_{A} x$ and an identity eliminator. System S has neither endpoints nor path elimination. Its normalization proof depends on the positive recursive closure and on erasure, not on a groupoid law.

Suggested first pass.

Begin with exercise 94.3, then complete exercise 94.5.

Exercise 94.3 ¶

★★☆ Write the complete typing derivation of $ind s z n : C (n)$ . Circle the occurrence of $n$ introduced by S-Self-Inst. Replace $C (n)$ by a constant motive and identify the ordinary Church iterator obtained after erasure.

Referenced from 4 locations

Exercise 94.4 ¶

★★☆ Compute the polarity of the recursive variable in $1 + X \times X$ , $X \to N$ , and $(X \to N) \to N$ . For each result, state whether the frozen closure admits it. For the rejected case, show the failed reducibility-candidate monotonicity inclusion.

Referenced from 3 locations

Exercise 94.5 ¶

★★★ Practical project.system-s-self-positivity-checker Implement in Kappa a finite polarity checker for products and arrows, together with a finite same-subject check for self generation and instantiation. Maintain two invariants: both self rules preserve the subject’s erased tag, and every accepted recursive occurrence is positive. Accept $X \times X$ and $(X \to 1) \to 1$ , reject $X \to 1$ , and reject a self-instantiation whose displayed subject differs from the substituted subject. Removing the arrow-domain polarity flip must make the test fail.

Referenced from 5 locations

Sources. The System S syntax and rules are on pages 5–7 of Fu and Stump’s extended version; the Church-natural derivation is on pages 7–8. The erasure to $F_{ω}$ with positive definitions begins on pages 9–11, the confluence and morph analyses on pages 11–13, and preservation and consistency on pages 13–14. The source proves strong normalization only for its restricted closure discipline. No public System S checker or mechanized metatheory was available, so the Kappa project tests the printed side conditions rather than claiming to mechanize the theorem [FS14].