Sized Copattern Recursion and Mixed Induction–Coinduction
Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.
A stream processor reads finitely many elements from an input stream before it writes one element to the output stream, and then continues. Its states form the type 𝖲𝖯≅𝜈𝑋.𝜇𝑌.((𝐴→𝑌)+(𝐵×𝑋)), a least fixed point nested inside a greatest one: the inner 𝜇 bounds the number of reads between two writes, and the outer 𝜈 allows infinitely many writes. The program that runs a processor on a stream is 𝗋𝗎𝗇(𝗀𝖾𝗍𝑓)(𝑣,𝑣𝑠)=𝗋𝗎𝗇(𝑓𝑣)𝑣𝑠,𝗋𝗎𝗇(𝗉𝗎𝗍(𝑤,𝑠𝑝))𝑣𝑠=(𝑤,𝗋𝗎𝗇𝑠𝑝𝑣𝑠). Both checkers of chapter 33, chapter 124 reject it, and for opposite reasons.
A structural-recursion checker looks for an argument that decreases at every recursive call. In the second clause the call 𝗋𝗎𝗇𝑠𝑝𝑣𝑠 occurs under the pair constructor and its first argument 𝑠𝑝 is not a subterm of 𝗉𝗎𝗍(𝑤,𝑠𝑝) in any order that also decreases in the first clause, where the first argument passes from 𝗀𝖾𝗍𝑓 to 𝑓𝑣: the two clauses decrease at different components, and neither component decreases at both.
A guarded-corecursion checker looks for every recursive call to occur directly under a constructor of the coinductive result type. In the second clause it does, since 𝗋𝗎𝗇𝑠𝑝𝑣𝑠 sits under a pair. In the first clause it does not: the call 𝗋𝗎𝗇(𝑓𝑣)𝑣𝑠 is the whole right-hand side and produces no output before recurring.
The two rejections point at the same missing datum. The first clause terminates because a finite quantity — the number of remaining reads — decreases; the second is productive because a coinductive observation is emitted. A checker that inspects the position of a call sees neither. This chapter presents a calculus in which both quantities are indices in the type, so that the two clauses are typed by a single rule with a lexicographic measure.
Fix a countable set of size variables𝑖,𝑗,…. A size expression is 𝑎,𝑏::=𝑖+𝑛∣∞+𝑛(𝑛∈ℕ), where the offset 𝑛 is omitted when it is 0. An extended size expression is 𝑎+::=𝑎∣𝑛, and a measure is a finite tuple 𝑚::=⋅∣𝑎+,𝑚 of extended size expressions. A size context is Ψ::=⋅∣Ψ,𝑖:𝜋(<𝑎), a finite map from size variables to a polarity𝜋 and a bound 𝑎. We write ≤𝑎 for <(𝑎+1), and 𝗌𝗂𝗓𝖾 for ≤∞, and abbreviate 𝑖:∘(<𝑎) to 𝑖<𝑎.
The clause (∞+𝑛)↑=∞ is what makes ∞ a fixed point of the successor and is used at every place where a construction at size ∞ must be closed under the introduction rule; lemma 165.10 makes that use explicit.
A valuation𝜂 is a finite map from size variables to natural numbers; 𝜂satisfiesΨ when 𝜂(𝑖)<𝜂(𝑎) for every (𝑖<𝑎)∈Ψ. We write Ψ⊢∃Ψ′ when every valuation satisfying Ψ extends to one satisfying Ψ,Ψ′.
The context 𝑖≤∞,𝑗<𝑖 is consistent: take 𝜂(𝑖)=1, 𝜂(𝑗)=0. But 𝑖≤∞⊢∃(𝑗<𝑖) fails, because the valuation 𝜂(𝑖)=0 satisfies 𝑖≤∞ and no value of 𝑗 satisfies 𝑗<0. The judgment of definition 165.3 is therefore strictly stronger than consistency of the concatenation, and definition 165.14 will require it of every clause.
★☆☆ Decide each of the following in the context 𝑖≤∞,𝑗<𝑖, giving a derivation or naming the rule that fails: 𝑗<𝑖; 𝑗+1≤𝑖; 𝑖<∞; 𝑖+2<∞+1; |𝑖,𝑗+1|<|𝑖,∞+1|; and |𝑖,0|<|𝑖,𝑗|.
Simple kinds are 𝜄::=∗∣𝑜∣𝜄→𝜄′, where ∗ classifies proper types and 𝑜 classifies size expressions. Kinds refine them with size bounds and variance: 𝜅::=∗∣<𝑎∣𝜋𝜅→𝜅′,𝜋::=∘∣+∣−∣⊤. The variances are ordered ∘≤𝜋≤⊤ and composed by ⊤𝜋=⊤,∘𝜋=∘(𝜋≠⊤),+𝜋=𝜋,−−=+, with composition commutative. A type variable context is Δ::=⋅∣Δ,𝑋:𝜋𝜅, and 𝜋Δ multiplies every declared variance by 𝜋.
Read 𝜋 as what is known about the direction in which a constructor moves its argument: + covariant, − contravariant, ⊤ constant, and ∘ nothing known. The order is by information content, so ∘ is the least informative and is the default.
𝐾::=𝑎∣𝑋∣𝟏∣×∣→∣∀𝜅∣∃𝜅𝐹,𝐺,𝐴,𝐵::=𝐾∣𝜆𝑋:𝜄.𝐹∣𝐹𝐺∣𝜇𝑎𝑆∣𝜈𝑎𝑅𝑆::=⟨𝑐1:𝐹1;…;𝑐𝑛:𝐹𝑛⟩𝑅::={𝑑1:𝐹1;…;𝑑𝑛:𝐹𝑛} A variant row𝑆 maps constructor labels to type constructors and a record row𝑅 maps destructor labels to type constructors; both are abstracted over the recursive occurrence, so that a stream is written 𝜈𝑎{𝗁𝖾𝖺𝖽:𝜆𝑋.𝐴;𝗍𝖺𝗂𝗅:𝜆𝑋.𝑋} rather than 𝜈𝑎𝑋.{𝗁𝖾𝖺𝖽:𝐴;𝗍𝖺𝗂𝗅:𝑋}. We write 𝐴×𝐵 and 𝐴→𝐵 for the two binary formers, ∀𝑋:𝜅.𝐴 for ∀𝜅(𝜆𝑋.𝐴), and ∀𝑖<𝑎.𝐴 for ∀<𝑎(𝜆𝑖:𝑜.𝐴).
A measured type is ̂𝐴::=∀Δ.𝑚⇒𝐴 and a constrained type is ⌈𝐴⌉::=∀Ψ.𝑐⇒𝐴 with 𝑐::=𝑚<𝑚′. A constrained type is not a type: a variable of constrained type may be used only when applied to size arguments satisfying the constraint.
Write Δ⊢𝐹≤𝜋𝐹′ for the 𝜋-directed comparison of type constructors, with ≤+ ordinary subtyping, ≤− its converse, ≤⊤ equality and ≤∘ the total relation. The clauses that concern sizes are Δ⊢𝑎≤𝑏Δ⊢𝜇𝑎𝑆≤+𝜇𝑏𝑆,Δ⊢𝑎≤𝑏Δ⊢𝜈𝑏𝑅≤+𝜈𝑎𝑅, so an inductive type is covariant and a coinductive type is contravariant in its size index.
Let 𝐴 be a type with Δ⊢𝑎≤𝑏. If 𝜇𝑎𝑆≤+𝜇𝑏𝑆 failed, the constructor rule of definition 165.9 would not type 𝖼𝑎𝑡 at 𝜇𝑏𝑆 for 𝑎≤𝑏; and if 𝜈𝑏𝑅≤+𝜈𝑎𝑅 failed, the destructor rule would not allow a 𝑏-deep observation of an 𝑎-deep object for 𝑎≤𝑏.
Proof of Lemma 165.8 — The two size variances are forced
Proof. For the first, 𝖼𝑎𝑡:𝜇𝑎↑𝑆 by definition 165.9, and typing it at 𝜇𝑏↑𝑆 requires 𝜇𝑎↑𝑆≤𝜇𝑏↑𝑆, which is the displayed clause with 𝑎↑≤𝑏↑ from 𝑎≤𝑏. For the second, an object of 𝜈𝑏𝑅 admits observations at every 𝑗<𝑏↑ by definition 165.9; a use of it at 𝜈𝑎𝑅 demands observations only at 𝑗<𝑎↑, and 𝑎≤𝑏 makes that a subset. ◻
Both rules move one step: a constructor at size 𝑎 packages a value at some strictly smaller size, and a destructor at size 𝑎 delivers a value at any strictly smaller size. The asymmetry between the existential in Mu-I and the universal in Nu-E is the difference between building and observing.
Proof. By definition 165.1, ∞↑=∞. For the constructor, ∞<∞↑ fails, but ∞<∞+1=∞↑ holds after bound normalization, so the witness 𝑗:=∞ satisfies the premise of Mu-I and ∃𝑗<∞↑.𝑆𝑐(𝜇𝑗𝑆) is inhabited by the pair ∞𝑡. For the destructor, instantiate the universal of Nu-E at 𝑗:=∞, again using ∞<∞↑. ◻
𝑟,𝑠,𝑡::=𝑢∣𝑣∣𝜆.⃗𝐷term𝑣::=()∣(𝑡1,𝑡2)∣𝑐𝑡∣𝐺𝑡introduction𝑢::=𝑥∣𝑓∣𝑟𝑒applicativeterm𝑒::=𝑡∣𝐺∣.𝑑elimination𝑝::=𝑥∣()∣(𝑝1,𝑝2)∣𝑐𝑝∣𝑋𝑝pattern𝑞::=𝑝∣𝑋∣.𝑑copattern𝐷::={⃗𝑞→𝑡}clause⃗𝐷::={𝐷1;…;𝐷𝑛}clauses An object 𝜆.⃗𝐷 subsumes abstraction and record formation: 𝜆.{𝑥→𝑡} is 𝜆𝑥.𝑡, and 𝜆.{.𝖿𝗌𝗍→𝑡1;.𝗌𝗇𝖽→𝑡2} is a lazy pair.
Matching 𝑡/𝑝&𝜏;𝜎 of a term against a pattern, and ⃗𝑒/⃗𝑞&𝜏;𝜎 of an elimination spine against a copattern spine, produce a type substitution 𝜏 and a term substitution 𝜎; the clauses are the evident ones, with 𝑡/𝑥&⋅;𝑡/𝑥 at a variable pattern and .𝑑/.𝑑&⋅;⋅ at a projection copattern. Weak head contraction is ⃗𝑒/⃗𝑞𝑘&𝜏;𝜎𝜆.{⃗𝑞→𝑡}⃗𝑒⃗𝑒′⇝0𝑡𝑘𝜏𝜎⃗𝑒′,(𝑓:𝐴=⃗𝐷)∈Σ𝜆.⃗𝐷⃗𝑒⇝0𝑡′𝑓⃗𝑒⇝0𝑡′, and ⟶ is the compatible closure of ⇝0 over all subterms, including the bodies of clauses. Clauses may overlap and need not cover; an unmatched spine leaves the term stuck.
Two features of definition 165.12 are used throughout the normalization proof and are worth naming now. A whole copattern spine is matched at once, so a partially applied object such as 𝜆.{𝑥𝑦→𝑡}𝑠 is stuck but may become unstuck when a further argument arrives. And a function symbol unfolds to its clauses without any guard, so the termination argument cannot rely on a syntactic restriction on unfolding.
A declaration is 𝑓:̂𝐴=⃗𝐷 with ̂𝐴 a measured type; a mutual block is 𝗆𝗎𝗍𝗎𝖺𝗅𝑚⃗̂𝛿, a sequence of declarations sharing a lexicographic measure of length 𝑚; a program is a sequence of blocks followed by an applicative entry point.
where pattern spine typing Δ;Γ∣𝐴⊢Δ0⃗𝑞⇒𝐶 eliminates 𝐴 along ⃗𝑞, binding the type variables and pattern variables of ⃗𝑞 in Δ and Γ, and its two clauses for the sized formers are Δ;Γ∣∀𝑗<𝑎↑.𝑅𝑑(𝜈𝑗𝑅)⊢Δ0⃗𝑞⇒𝐶Δ;Γ∣𝜈𝑎𝑅⊢Δ0.𝑑⃗𝑞⇒𝐶,Δ;Γ⊢Δ0𝑝⇐∃𝑗<𝑎↑.𝑆𝑐(𝜇𝑗𝑆)Δ;Γ⊢Δ0𝑐𝑝⇐𝜇𝑎𝑆.
Let ̂𝐴=∀Δ.𝑚⇒𝐴 be the measured type of 𝑓 in a mutual block. While checking the clauses of 𝑓 in a context where Δ’s variables are in scope, each recursive occurrence of any 𝑔 of the block, with measured type ∀Δ𝑔.𝑚𝑔⇒𝐴𝑔, is given the constrained typê𝐴𝑔<𝑚:=∀Δ′𝑔.𝑚′𝑔<𝑚⇒𝐴′𝑔, where Δ′𝑔,𝑚′𝑔,𝐴′𝑔 rename the variables of Δ𝑔 apart. A variable of constrained type must be applied to size arguments ⃗𝑎 satisfying both Δ′𝑔 and the condition 𝑚′𝑔[⃗𝑎]<𝑚 before it can be used.
The condition 𝑚′𝑔<𝑚 is the entire termination discipline of the calculus. It is checked once per recursive occurrence, by comparing two measures in the size order of definition 165.2; no inspection of the position of the occurrence takes place.
The inner type is used at size ∞ inside the outer one: an arbitrary finite number of reads is allowed between two writes, and the outer size counts writes. Definition 165.9 then gives the derived rules, for 𝑏<𝑎↑: 𝑓:𝐴→𝖲𝖯𝑏𝜇𝑋𝗀𝖾𝗍𝑏𝑓:𝖲𝖯𝑎𝜇𝑋,𝑤:𝐵𝑠𝑝:𝑋𝗉𝗎𝗍𝑏(𝑤,𝑠𝑝):𝖲𝖯𝑎𝜇𝑋,𝑠𝑝:𝖲𝖯𝑎𝜈𝑠𝑝.𝗈𝗎𝗍𝑏:𝖲𝖯∞𝜇𝖲𝖯𝑏𝜈. For streams, define 𝗁𝖽𝑖𝑠:=𝗉𝗋1(𝑠.𝖿𝗈𝗋𝖼𝖾𝑖):∀𝑖.𝖲𝗍𝗋𝑖+1𝐴→𝐴,𝗍𝗅𝑖𝑠:=𝗉𝗋2(𝑠.𝖿𝗈𝗋𝖼𝖾𝑖):∀𝑖.𝖲𝗍𝗋𝑖+1𝐴→𝖲𝗍𝗋𝑖𝐴, whose instances at ∞ have types 𝖲𝗍𝗋∞𝐴→𝐴 and 𝖲𝗍𝗋∞𝐴→𝖲𝗍𝗋∞𝐴 by lemma 165.10.
The two declarations of construction 165.17 form a mutual block with lexicographic measure of length two, and every recursive occurrence satisfies the condition of definition 165.15.
Proof of Proposition 165.18 — The block type-checks
Proof. There are three recursive occurrences; we check each against definition 165.15, displaying the two measures being compared.
𝗋𝗎𝗇𝜇 calls 𝗋𝗎𝗇𝜇. The clause matches the pattern 𝗀𝖾𝗍𝑗′𝑓 against 𝖲𝖯𝑗𝜇(…), so by the second clause of definition 165.14 the pattern binds 𝑗′<𝑗↑, that is 𝑗′≤𝑗; and 𝑓 has type 𝐴→𝖲𝖯𝑗′𝜇(𝖲𝖯𝑖𝜈). The call is at |𝑖,𝑗′+1| and the condition is |𝑖,𝑗′+1|<|𝑖,𝑗+1|, which holds because the first components agree and 𝑗′<𝑗; the pattern in fact binds 𝑗′<𝑗↑, and the constrained type of the recursive occurrence requires the strict inequality, so the clause is accepted exactly when the matched size is strictly smaller.
𝗋𝗎𝗇𝜇 calls 𝗋𝗎𝗇𝜈. The condition is |𝑖,0|<|𝑖,𝑗+1|, which holds because the first components agree and 0<𝑗+1.
𝗋𝗎𝗇𝜈 calls 𝗋𝗎𝗇𝜇. The copattern .𝖿𝗈𝗋𝖼𝖾𝑖′ eliminates 𝖲𝗍𝗋𝑖𝐵 and by definition 165.14 binds 𝑖′<𝑖↑; the call is at |𝑖′,∞+1| and the condition is |𝑖′,∞+1|<|𝑖,0|, which holds because 𝑖′<𝑖 in the first component, so the second components are not compared.
Well-typedness of the right-hand sides is then read off the derived rules above: in the first clause 𝑓(𝗁𝖽∞𝑣𝑠) has type 𝖲𝖯𝑗′𝜇(𝖲𝖯𝑖𝜈) and 𝗍𝗅∞𝑣𝑠 has type 𝖲𝗍𝗋∞𝐴; in the second, 𝑤:𝐵 and 𝗋𝗎𝗇𝜈𝑖𝑠𝑝𝑣𝑠:𝖲𝗍𝗋𝑖𝐵, so the pair has the required type 𝐵×𝖲𝗍𝗋𝑖𝐵; in the third, 𝑠𝑝.𝗈𝗎𝗍𝑖′:𝖲𝖯∞𝜇𝖲𝖯𝑖′𝜈 and the result type after the copattern is 𝐵×𝖲𝗍𝗋𝑖′𝐵, which is what 𝗋𝗎𝗇𝜇𝑖′∞ delivers. ◻
Let 𝐴=𝐵=ℕ, let 𝑣𝑠 be a stream with 𝗁𝖽∞𝑣𝑠=𝟢, and let 𝑠𝑝0:=𝜆.{.𝗈𝗎𝗍𝑘→𝗀𝖾𝗍∞(𝜆𝑣.𝗉𝗎𝗍∞(𝑣,𝑠𝑝0))}. Then 𝑠𝑝0:𝖲𝖯∞𝜈, and the first forced observation of 𝗋𝗎𝗇𝜈∞𝑠𝑝0𝑣𝑠 reduces as follows. (𝗋𝗎𝗇𝜈∞𝑠𝑝0𝑣𝑠).𝖿𝗈𝗋𝖼𝖾∞⇝0𝗋𝗎𝗇𝜇∞∞(𝑠𝑝0.𝗈𝗎𝗍∞)𝑣𝑠⟶𝗋𝗎𝗇𝜇∞∞(𝗀𝖾𝗍∞(𝜆𝑣.𝗉𝗎𝗍∞(𝑣,𝑠𝑝0)))𝑣𝑠⇝0𝗋𝗎𝗇𝜇∞∞(𝗉𝗎𝗍∞(𝟢,𝑠𝑝0))(𝗍𝗅∞𝑣𝑠)⇝0(𝟢,𝗋𝗎𝗇𝜈∞𝑠𝑝0(𝗍𝗅∞𝑣𝑠)). Three contractions produce one output element, and the residual is again a 𝗋𝗎𝗇𝜈 call, at the same outer size ∞ and on the tail of the input. The measure that fell was the inner one, ∞+1 to 0, at the second contraction; the outer measure did not fall, and by lemma 165.10 it does not have to at ∞.
★★☆ Exchange the two components of the measures in construction 165.17, giving 𝗋𝗎𝗇𝜇 the measure |𝑗+1,𝑖| and 𝗋𝗎𝗇𝜈 the measure |0,𝑖|. Check each of the three conditions of proposition 165.18 again and identify the one that now fails, naming the clause of definition 165.2 that would be needed.
The normalization proof interprets a type as a set of strongly normalizing terms. Two features of definition 165.12 force a modification of Girard’s usual conditions. Clauses may overlap, so reduction is not deterministic and not confluent; and a function symbol unfolds to its clauses, so a semantic type must contain a symbol whenever it contains the object it unfolds to.
Write SN for the set of strongly normalizing terms, Intro for the introduction terms of definition 165.11, and 𝑟⟶ for the set of one-step reducts of 𝑟. An applicative term 𝑢 is terminally stuck when 𝑢⃗𝑒 is not a redex for any elimination spine ⃗𝑒. A term 𝑟 is neutral, written 𝑟∈Ne, when it is a redex or terminally stuck. Write 𝑟⊳⃗𝑟 when 𝑟simulates the terms ⃗𝑟, meaning that every contraction of 𝑟 is a contraction of some 𝑟𝑘: this holds for 𝜆.⃗𝐷⊳𝜆.𝐷1,…,𝜆.𝐷𝑛 and for 𝑓⊳𝜆.⃗𝐷 when (𝑓:𝐴=⃗𝐷)∈Σ.
The restriction to terminally stuck terms is needed. The partial application 𝜆.{𝑥𝑦→𝑥𝑥}𝛿 with 𝛿:=𝜆.{𝑥→𝑥𝑥} is stuck and in normal form, but supplying one further argument makes it reduce to 𝛿𝛿, which diverges. If it counted as neutral, condition CR3 below would place it in every candidate, including semantic function types, and the interpretation would contain a divergent term.
A set A of terms is a reducibility candidate, A∈CR, when
CR1
A⊆SN;
CR2
𝑡∈A implies (𝑡⟶)⊆A;
CR3
𝑡∈Ne and (𝑡⟶)⊆A imply 𝑡∈A;
CR4
𝑡∉Intro, (𝑡⟶)⊆A and 𝑡⊳⃗𝑡 with ⃗𝑡∈A imply 𝑡∈A.
For A⊆SN closed under reduction, write ――A for the least candidate containing A, generated inductively by the three clauses “𝑡∈A”, “𝑡 is neutral with all reducts in ――A” and “𝑡 is not an introduction, all its reducts are in ――A, and it simulates terms of ――A”.
Proof of Lemma 165.22 — Multi-clause objects and symbols
Proof. For the first claim, argue by induction on ⃗𝐷∈SN. Since 𝜆.⃗𝐷⊳𝜆.𝐷1,…,𝜆.𝐷𝑛, condition CR4 applies once we show that every reduct of 𝜆.⃗𝐷 lies in A. A contraction 𝜆.⃗𝐷⇝0𝑡 is a contraction 𝜆.𝐷𝑘⇝0𝑡 for some 𝑘 by definition 165.12, and 𝜆.𝐷𝑘∈A gives 𝑡∈A by CR2. Otherwise the reduction is inside a body, so the reduct is 𝜆.⃗𝐷′ with ⃗𝐷⟶⃗𝐷′, and the induction hypothesis applies.
For the second claim, 𝑓∉Intro and 𝑓⊳𝜆.⃗𝐷 by definition 165.20, and every reduct of 𝑓 is a reduct of 𝜆.⃗𝐷, hence in A by CR2. Apply CR4. ◻
For candidates A,B, an index set K, a family F∈K→CR and a proposition 𝑃, set A→B:={𝑟∈SN∣∀𝑠∈A.𝑟𝑠∈B},∀KF:={𝑟∈SN∣∀G∈K.𝑟𝐺∈F(G)},𝟏:={()},A1×A2:=――――――――――――――{(𝑡1,𝑡2)∣𝑡1∈A1,𝑡2∈A2},∃KF:=―――――――――――――{𝐺𝑡∣∃G∈K.𝑡∈F(G)},𝑃⇒A:={𝑟∣𝑟∈Aif𝑃}. The conditional 𝑃⇒A is a candidate only when 𝑃 holds; otherwise it is the set of all expressions, which is why constrained types are not types.
Proof of Lemma 165.24 — The function space is a candidate
Proof.CR1: for 𝑟∈A→B and a variable 𝑥∈A we get 𝑟𝑥∈B⊆SN, hence 𝑟∈SN.
CR2: if 𝑟⟶𝑟′ and 𝑠∈A then 𝑟𝑠⟶𝑟′𝑠, and 𝑟𝑠∈B gives 𝑟′𝑠∈B by CR2 for B.
CR3: let 𝑟∈Ne with all reducts in A→B, and let 𝑠∈A. Then 𝑟𝑠∈Ne by definition 165.20, so by CR3 for B it suffices to place every reduct of 𝑟𝑠 in B; argue by induction on 𝑟,𝑠∈SN. Because 𝑟 is neutral, a reduct is 𝑟′𝑠 or 𝑟𝑠′, and each is handled by the induction hypothesis.
CR4: let 𝑟∉Intro with all reducts in A→B and 𝑟⊳⃗𝑟 with ⃗𝑟∈A→B, and let 𝑠∈A. Then 𝑟𝑠∉Intro and 𝑟𝑠⊳𝑟1𝑠,…,𝑟𝑛𝑠∈B, so CR4 for B applies once every reduct of 𝑟𝑠 is in B. By induction on 𝑟,𝑠∈SN: the cases 𝑟′𝑠 and 𝑟𝑠′ are the induction hypothesis; a contraction 𝑟𝑠⇝0𝑡 is a contraction 𝑟𝑘𝑠⇝0𝑡 for some 𝑘, and 𝑟𝑘𝑠∈B gives 𝑡∈B by CR2. ◻
Let S map constructor labels and R destructor labels to operators on candidates. For an ordinal 𝛼 define 𝜇𝛼S:=――――――――――――――――――{𝑐𝑡∣𝑐∈dom(S),𝑡∈∃𝛽<𝛼S𝑐(𝜇𝛽S)},𝜈𝛼R:={𝑟∈SN∣∀𝑑∈dom(R).𝑟.𝑑∈∀𝛽<𝛼R𝑑(𝜈𝛽R)}. This is inflationary iteration for 𝜇 and deflationary iteration for 𝜈: no monotonicity of S or R is needed for the chains ∅=𝜇0S⊆𝜇1S⊆⋯,SN=𝜈0R⊇𝜈1R⊇⋯ to be monotone and antitone respectively. Both chains are subsets of the countable set of expressions, so both become stationary; write ∞ for an ordinal at which every such chain of the calculus is stationary, and 𝛼↑:=∞+1 for 𝛼≥∞ and 𝛼↑:=𝛼 otherwise.
Proof of Lemma 165.26 — Pre- and post-fixed points
Proof. For the first, 𝜇∞+1S=𝜇∞S by stationarity, and 𝑐𝑡∈𝜇∞+1S is the definition. For the second, 𝑟∈𝜈∞+1R=𝜈∞R, and the definition at ∞+1 is the displayed statement. Neither direction uses monotonicity of S or R. ◻
Proof. For 𝜇 it suffices to prove the inclusion from left to right, that is that 𝜇∞S is a post-fixed point. By definition 165.25, 𝜇∞S=―――――――――――――――――――⋃𝛽<∞{𝑐𝑏𝑡∣𝑐∈dom(S),𝑡∈S𝑐(𝜇𝛽S)}, and 𝜇𝛽S⊆𝜇∞S, so monotonicity of S𝑐 and of the closure operator give the inclusion.
For 𝜈 it suffices to prove that 𝜈∞R is a pre-fixed point: if 𝑟.𝑑𝑏∈R𝑑(𝜈∞R) for every 𝑑 and 𝑏, then 𝑟.𝑑𝑏∈R𝑑(𝜈𝛽R) for every 𝛽<∞ by monotonicity of R𝑑 together with 𝜈∞R⊆𝜈𝛽R, which is the definition of 𝑟∈𝜈∞R. ◻
Lemma 165.27 is the exact place where variance is load-bearing. The hypothesis is monotonicity of every row component, and the kinding discipline of definition 165.5 is what guarantees it: a row component declared at variance + denotes a monotone operator, and definition 165.7 then makes the size index of 𝜇 covariant and of 𝜈 contravariant. Without the hypothesis, lemma 165.26 still holds in the two displayed directions and no more.
Strong normalization
Proof structure. The obstruction is that a function symbol unfolds without a guard, so nothing syntactic bounds the number of unfoldings. The construction that overcomes it is the measured type: a symbol is admitted into its semantic type only relative to an ordinal tuple, and its recursive occurrences are admitted only at strictly smaller tuples. Three statements carry the argument. Theorem 165.29 interprets each typing rule, with the symbol’s type read off the signature. Theorem 165.30 discharges a mutual block by lexicographic induction on the measure. Corollary 165.31 assembles them; the desired conclusion, that the entry point is strongly normalizing, appears there.
Let [[𝜄]] interpret simple kinds by [[∗]]:=CR, [[𝑜]]:=O the set of ordinals below ∞+𝜔, and [[𝜄→𝜄′]]:=[[𝜄]]→[[𝜄′]]; let [[𝜅]] refine it by requiring the declared monotonicity behaviour for each variance and the bound for each <𝑎. For a type variable context Δ write D:=[[Δ]] for the set of valuations 𝜌, and for a typing context Γ write E(𝜌):=[[Γ]]𝜌 for the set of substitutions 𝜎 sending each 𝑥:𝐴 to an element of [[𝐴]]𝜌. Write D;E⊢𝑡∈C for: for all 𝜌∈D and 𝜎∈E(𝜌), 𝑡𝜎∈C(𝜌). Write Sound(Σ) when every declaration (𝑓:𝐴=⃗𝐷)∈Σ satisfies 𝑓∈[[𝐴]].
Proof of Theorem 165.29 — Soundness of expression typing
Proof. Simultaneously by induction on the typing derivation. We display one case per mechanism; the remaining cases are the same computation with the corresponding clause of definition 165.23 in place of the one shown, and are listed at the end.
Function symbol. The rule is Δ;Γ⊢𝑓⇒Σ(𝑓), and the conclusion is 𝑓∈[[Σ(𝑓)]], which is the hypothesis Sound(Σ).
Application. From Δ;Γ⊢𝑟⇒𝐴→𝐵 and Δ;Γ⊢𝑠⇐𝐴, the induction hypotheses give 𝑟𝜎∈[[𝐴]]𝜌→[[𝐵]]𝜌 and 𝑠𝜎∈[[𝐴]]𝜌, so (𝑟𝑠)𝜎∈[[𝐵]]𝜌 by definition 165.23.
Constructor. From Δ;Γ⊢𝑡⇐∃𝑗<𝑎↑.𝑆𝑐(𝜇𝑗𝑆) the induction hypothesis gives 𝑡𝜎∈∃𝛽<[[𝑎]]↑𝜌S𝑐(𝜇𝛽S), and definition 165.25 then places 𝑐𝑡𝜎 in 𝜇[[𝑎]]𝜌S. When [[𝑎]]𝜌≥∞ this is lemma 165.26(1).
Destructor. From Δ;Γ⊢𝑟⇒𝜈𝑎𝑅 the induction hypothesis gives 𝑟𝜎∈𝜈[[𝑎]]𝜌R, and definition 165.25 gives 𝑟𝜎.𝑑∈∀𝛽<[[𝑎]]𝜌R𝑑(𝜈𝛽R); lemma 165.26(2) covers [[𝑎]]𝜌=∞.
Clause. The rule is Clause of definition 165.14. Its first premise is discharged by soundness of pattern spine typing: whenever an elimination spine ⃗𝑒 matches ⃗𝑞 with substitutions 𝜏;𝜎 and the components of ⃗𝑒 lie in the semantic types assigned by the spine judgment, the resulting 𝜏,𝜎 lie in the semantic contexts D′,E′. Its second premise, Δ⊢∃Δ′ of definition 165.3, guarantees that D′ is nonempty over every 𝜌∈D, so the third premise may be instantiated. The induction hypothesis for the body then places 𝑡𝜏𝜎 in C′.
Object. From Δ;Γ⊢⃗𝐷⇐𝐴, the previous case gives 𝜆.𝐷𝑘𝜎∈[[𝐴]]𝜌 for each 𝑘, and lemma 165.22(1) gives 𝜆.⃗𝐷𝜎∈[[𝐴]]𝜌.
Remaining cases. Variables, the unit, pairs, type application, type abstraction, existential introduction, subsumption and type ascription are the computation displayed in the application case with the corresponding clause of definition 165.23; subsumption in addition uses that Δ⊢𝐴≤𝐶 implies [[𝐴]]𝜌⊆[[𝐶]]𝜌, which is proved by induction on the subtyping derivation, with the two size clauses of definition 165.7 discharged by the monotonicity and antitonicity recorded in definition 165.25. The case of a variable of constrained type uses that 𝑃⇒A is A when 𝑃 holds, and the rule requires exactly that the size arguments make the condition hold. ◻
Proof of Theorem 165.30 — Soundness of block typing
Proof.Single declaration. For 𝗅𝖾𝗍𝑓:𝐴=⃗𝐷, put A:=[[𝐴]]. Theorem 165.29(3) gives 𝜆.⃗𝐷∈A, and 𝑓⊳𝜆.⃗𝐷 gives 𝑓∈A by lemma 165.22(2).
Mutual block. Let the block have 𝑛 declarations ̂𝛿𝑘=(𝑓𝑘:̂𝐴𝑘=⃗𝐷𝑘) with ̂𝐴𝑘=∀Ψ𝑘.𝑚𝑘⇒𝐴𝑘 and a measure of length 𝑚. Write Sound⃗𝛼(⃗̂𝛿⇒̂𝛿𝑘) for the statement that ̂𝛿𝑘 is semantically sound at the ordinal tuple ⃗𝛼 provided every 𝑓𝑙 of the block inhabits [[̂𝐴𝑙]]<⃗𝛼, the semantic type restricted to tuples strictly below ⃗𝛼.
Argue by lexicographic induction on ⃗𝛼 in the set O𝑚 of 𝑚-tuples of ordinals. Fix ⃗𝛼 and 𝑘 and show Sound⃗𝛼(̂𝛿𝑘). The induction hypothesis gives Sound⃗𝛽(⃗̂𝛿) for every ⃗𝛽<⃗𝛼. To apply Sound⃗𝛼(⃗̂𝛿⇒̂𝛿𝑘), it must be shown that 𝑓𝑙∈[[̂𝐴𝑙]]<⃗𝛼 for every 𝑙; so let 𝜌∈[[Ψ𝑙]] with [[𝑚𝑙]]𝜌<⃗𝛼, let ⃗𝑏 instantiate Ψ𝑙, and show 𝑓𝑙⃗𝑏∈[[𝐴𝑙]]𝜌. This is the induction hypothesis at ⃗𝛽:=[[𝑚𝑙]]𝜌, which is strictly below ⃗𝛼 by assumption.
The statement Sound⃗𝛼(⃗̂𝛿⇒̂𝛿𝑘) itself is theorem 165.29(3) applied in the signature extended with the constrained types of definition 165.15: each recursive occurrence of 𝑓𝑙 has type ̂𝐴𝑙<𝑚𝑘, and the typing rule for a variable of constrained type forces the size arguments to satisfy 𝑚′𝑙<𝑚𝑘, which is exactly the hypothesis just discharged.
Finally, 𝑓𝑘⊳𝜆.⃗𝐷𝑘 and lemma 165.22(2) put 𝑓𝑘 into its semantic type. ◻
Proof. The first claim is theorem 165.30 applied to each block in turn. For the second, the entry point 𝑡 is typed in the resulting signature, so theorem 165.29 places it in [[𝐶]] for its type 𝐶, and [[𝐶]] is a candidate, hence contained in SN by CR1. ◻
Proof of Corollary 165.32 — Termination and productivity of the stream processor
Proof. The first claim is corollary 165.31 applied to the entry point 𝗋𝗎𝗇𝜇𝑎𝑏𝑠𝑝𝑣𝑠, using proposition 165.18 for well-typedness of the block.
For the second, iterate. The term (𝗋𝗎𝗇𝜈∞𝑠𝑝𝑣𝑠).𝖿𝗈𝗋𝖼𝖾∞ has type 𝐵×𝖲𝗍𝗋∞𝐵 by definition 165.16, and is strongly normalizing by the first claim, so it has a normal form; that normal form is in a semantic product type, hence by definition 165.23 it is a pair or a neutral term. It is not neutral: by proposition 165.18 the clause of 𝗋𝗎𝗇𝜈 matches the copattern .𝖿𝗈𝗋𝖼𝖾∞, so the term is a redex and reduces, and the reduct is 𝗋𝗎𝗇𝜇∞∞(𝑠𝑝.𝗈𝗎𝗍∞) applied to 𝑣𝑠, whose clauses match a 𝗀𝖾𝗍 or a 𝗉𝗎𝗍. Repeating on the second component of the pair gives the observation at 𝑘+1. ◻
Corollary 165.32(2) is the productivity statement that the two checkers of the opening could not supply. It is a consequence of strong normalization together with the typing of construction 165.17; no separate productivity argument is made.
Mendler’s scheme replaces the size index by a type variable that stands for the recursive occurrence and is abstract in the body. Its recursor for an inductive type has the form 𝖬𝖱𝖾𝖼:∏𝑋:∗((𝑋→𝐶)→𝑆(𝑋)→𝐶)→𝜇𝑆→𝐶, in which the recursive call is the argument 𝑋→𝐶 and 𝑋 is bound in the step, so the body cannot inspect the recursive occurrence. The two disciplines differ on what they can express.
Mendler’s scheme has no index, so it cannot state a lexicographic measure; the two clauses of (165.2) decrease at different components and cannot be presented as one Mendler step.
The counterexample separating them is a program whose recursive argument decreases only after a coinductive observation: 𝗋𝗎𝗇𝜈 calls 𝗋𝗎𝗇𝜇 at |𝑖′,∞+1|, larger in the second component than the caller’s |𝑖,0|, and admissible only because 𝑖′<𝑖. No Mendler step types that call, since 𝗋𝗎𝗇𝜈’s abstract variable would have to be instantiated at the larger second component.
A guarded calculus indexes the recursive occurrence by a modality rather than a size, and its fixed-point rule requires the recursion variable to have a modal type. The comparison is a comparison of rules, not a transfer of theorems.
A guarded fixed-point rule types a recursive occurrence whose type is ▹𝐴 and admits any number of them; definition 165.15 types a recursive occurrence whose measure has fallen and admits any type.
A guarded calculus makes the first clause of (165.2) untypable: the call 𝗋𝗎𝗇(𝑓𝑣)𝑣𝑠 produces no observation, so its result type carries no ▹. The sized calculus types it because the inner size fell.
Conversely, a guarded calculus types a definition whose recursive occurrence is passed to an arbitrary function of ▹-type, with no index to decrease. Nothing above types such a definition without first assigning a size to the function’s argument.
No theorem of either route is a premise of any statement in this chapter.
The calculus of section 165.1–section 165.3 has size expressions 𝑖+𝑛 and ∞+𝑛 only. There is no type of sizes, no quantifier ranging over a large collection of sizes, and no rule that commutes such a quantifier with a type former. Consequently nothing above constructs an initial algebra or a final coalgebra as an object of the calculus: lemma 165.27 is a statement about semantic candidates, in the metatheory.
No consistency theorem is proved. Corollary 165.31 is strong normalization of typed programs; it does not say that the type system is a logic, and there is no realizability model of a large size type here. The size annotations are erasable: they occur only at the type level, and corollary 165.31 concerns terms after erasure.
Coverage is not required. Definition 165.12 allows overlapping and incomplete clause sets, and definition 165.21 was framed with CR4 and the terminally-stuck restriction precisely so that the normalization proof survives their absence. A coverage checker would be a separate development.
★★★Lemma 165.24 verified the four conditions for A→B. Verify them for the other formers.
Show that A1×A2 and ∃KF of definition 165.23 are candidates, saying at each step why the closure operator is needed and why it adds no introduction term.
Show that ∀KF is a candidate, and explain why the clause 𝑟∈SN cannot be dropped there although it can be dropped from A→B.
Show that 𝜇𝛼S and 𝜈𝛼R are candidates for every 𝛼, and identify the one place where 𝜈0R=SN is used.
★★★ A breadth-first labelling of an infinite binary tree consumes a stream of label streams and returns a tree together with the remaining streams. Set 𝖲𝖲𝑖:=𝖲𝗍𝗋𝑖(𝖲𝗍𝗋∞𝑉),𝖳𝗋𝖾𝖾𝑖:=𝜈𝑖{𝗅𝖺𝖻𝖾𝗅:𝜆𝑋.𝑉;𝗅𝖾𝖿𝗍:𝜆𝑋.𝑋;𝗋𝗂𝗀𝗁𝗍:𝜆𝑋.𝑋},𝖱𝖾𝗌𝗎𝗅𝗍𝑖:=𝜈∞{𝗍𝗋𝖾𝖾:𝜆𝑋.𝖳𝗋𝖾𝖾𝑖;𝗋𝖾𝗌𝗍:𝜆𝑋.𝖲𝖲𝑖}.
Explain why 𝖱𝖾𝗌𝗎𝗅𝗍𝑖 is a lazy product rather than a genuinely coinductive type, and why a record is needed rather than a pair.
Write the five clauses of a function 𝖻𝖿𝗌:∀𝑖.|𝑖|⇒𝖲𝖲𝑖→𝖱𝖾𝗌𝗎𝗅𝗍𝑖, one for each of the five components of the informal equation 𝖻𝖿𝗌(𝖼𝗈𝗇𝗌(𝖼𝗈𝗇𝗌𝑣𝑣𝑠)𝑣𝑠𝑠)=(𝗇𝗈𝖽𝖾𝑣𝑙𝑟,𝖼𝗈𝗇𝗌𝑣𝑠𝑣𝑠𝑠″).
Check the measure condition of definition 165.15 at each recursive occurrence, displaying the two measures compared.
State what corollary 165.31 gives for this program and what it does not: in particular, say why it does not by itself establish that the labelling is the intended one.
★★☆Definition 165.20 admits only terminally stuck applicative terms as neutral.
Let 𝛿:=𝜆.{𝑥→𝑥𝑥} and 𝑟:=𝜆.{𝑥𝑦→𝑥𝑥}𝛿. Show that 𝑟 is in normal form, that 𝑟𝛿 is not strongly normalizing, and hence that admitting 𝑟 as neutral would violate CR1 for A→B.
Show that a variable is terminally stuck, and that terminally stuck terms are closed under application to an arbitrary elimination.
Identify the step of lemma 165.24 that uses the second fact, and say what would go wrong without it.
★★★Practical project.sized-copattern-checker Implement, in Kappa, a checker for the mutual-block discipline of definition 165.15 and an evaluator for definition 165.12, and run them on the programs of this chapter.
Calculus to implement. The size expressions, measures and comparison of definition 165.1, definition 165.2; the sized formers 𝜇𝑎𝑆 and 𝜈𝑎𝑅 of definition 165.9 with rows; terms, copatterns and clauses of definition 165.11; copattern matching and reduction of definition 165.12; and the clause and pattern-spine typing of definition 165.14 restricted to the fragment used by construction 165.17. Copattern matching must be implemented as a single match of the whole spine, and the evaluator must leave a partially applied object stuck rather than reducing it.
Invariant. Every recursive occurrence must be checked against the constrained type of definition 165.15, and the check must consist of one lexicographic comparison in the order of definition 165.2; the checker must never inspect the position of the occurrence. The evaluator must maintain, for every reduction step it performs, that the step is a contraction of a matched clause or a congruence, and it must count contractions so that a bounded run reports either a normal form or the bound.
Concrete result. For a program, a report giving the accept or reject verdict for each recursive occurrence, with the two measures compared, and for a named entry point the sequence of contractions up to a bound, with the normal form when reached.
Acceptance test. The block of construction 165.17 must be accepted, with the three comparisons printed exactly as in proposition 165.18. The measure-swapped variant of exercise 165.3 must be rejected, naming the offending occurrence. The reduction of example 165.19 must be reproduced contraction by contraction, and the three-contraction count must match. The processor that never writes, from exercise 165.2, must be rejected. Finally, the term 𝜆.{𝑥𝑦→𝑥𝑥}𝛿 of exercise 165.6 must be reported as stuck but not normal in the sense of the checker, and the same term applied to 𝛿 must exhaust the contraction bound. Produce three mutations that still run — compare measures componentwise instead of lexicographically, allow a non-strict comparison, and match copatterns one at a time — and confirm that each accepts a program the unchanged checker rejects. State explicitly that the program illustrates corollary 165.31 on finitely many inputs and does not prove it.