Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.
Two definitions that ought to be admissible are rejected by the guardedness conditions of chapter 33, chapter 124.
The first is a stream. Let 𝗆𝖺𝗉 send a function and a stream of naturals to the stream of its values, and consider 𝗇𝖺𝗍𝗌:=0::𝗆𝖺𝗉𝗌𝗎𝖼𝗇𝖺𝗍𝗌. Every finite prefix of 𝗇𝖺𝗍𝗌 is determined: the first element is 0, and the (𝑘+1)st is the successor of the 𝑘th. A syntactic guardedness check nevertheless rejects (162.1), because the recursive occurrence is an argument of 𝗆𝖺𝗉 rather than an immediate argument of the constructor (::). The check inspects the position of the recursive call and cannot inspect what 𝗆𝖺𝗉 does with it.
The second is a type. Solve 𝐷≅(𝐷→ℕ). No inductive or coinductive definition produces 𝐷: the variable occurs negatively, so (162.2) is not the initial algebra or the final coalgebra of a functor. A positivity check rejects it for that reason.
Both rejections come from a check on where a recursive occurrence sits. This chapter replaces that check by a type former. Write ▹𝐴 for the type of elements of 𝐴 that are available one step later. Then (162.1) becomes a definition whose recursive occurrence has type ▹𝖲𝗍𝗋 rather than 𝖲𝗍𝗋, and (162.2) becomes 𝐷≅(▹𝐷→ℕ), which has a unique solution, negative occurrence and all. The chapter’s task is to give the rules for ▹, to interpret them, and to prove that the resulting programs deliver every finite observation.
The ambient theory is extensional Martin-Löf type theory: contexts, the judgments Γ𝖼𝗍𝗑, Γ⊢𝐴𝗍𝗒𝗉𝖾, Γ⊢𝑡:𝐴, Γ⊢𝐴≡𝐵𝗍𝗒𝗉𝖾 and Γ⊢𝑡≡𝑢:𝐴; dependent products and sums; the natural numbers ℕ with 𝟢 and 𝗌𝗎𝖼; identity types 𝖨𝖽𝐴(𝑡,𝑢) with equality reflection, so that an inhabitant of 𝖨𝖽𝐴(𝑡,𝑢) gives Γ⊢𝑡≡𝑢:𝐴; and Tarski universes U with decoding 𝖤𝗅(−). Every rule of that theory remains available; this chapter states only what is added.
The first attempt at the delta is the following pair of rules, which say that ▹ is an applicative functor: data available now is available later, and a function available later can be applied to an argument available later. Γ⊢𝑡:𝐴Γ⊢𝗇𝖾𝗑𝗍𝑡:▹𝐴Γ⊢𝑓:▹(𝐴→𝐵)Γ⊢𝑡:▹𝐴Γ⊢𝑓⊛𝑡:▹𝐵 These two rules suffice while types do not depend on terms. They fail as soon as they do. Suppose Γ⊢𝑓:▹(∏𝑥:𝐴𝐵) and Γ⊢𝑡:▹𝐴. What is the type of 𝑓⊛𝑡? If 𝑡 were 𝗇𝖾𝗑𝗍𝑢, the answer would be ▹(𝐵[𝑢/𝑥]). For an arbitrary 𝑡 there is no such 𝑢 to substitute, and (162.3) cannot be stated.
The situation is not hypothetical. Let 𝐴 be a type of guarded streams and let 𝐵 be a predicate on streams. A proof by guarded recursion has an induction hypothesis of type ▹(∏𝑥:𝐴𝐵), and it must be applied to the tail of a stream, whose type is ▹𝐴. The type of the result must mention the tail, which is available only later.
The repair is to keep the substitution and delay it.
The raw syntax of convention 162.1 is extended by 𝐴,𝐵::=⋯∣▹𝜉.𝐴,𝑡,𝑢::=⋯∣𝗇𝖾𝗑𝗍𝜉.𝑡∣̂▹𝑡,𝜉::=⋅∣𝜉[𝑥←𝑡]. A delayed substitution𝜉 is a list of assignments of terms of ▹-types to variables; the judgment Γ⊢𝜉:Γ′ says that 𝜉 assigns, to each variable of the telescope Γ′, a term available one step later. In ▹𝜉.𝐴 and 𝗇𝖾𝗑𝗍𝜉.𝑡 the variables assigned by 𝜉 are bound in 𝐴 and in 𝑡 respectively. We write ▹𝐴 for ▹⋅.𝐴 and 𝗇𝖾𝗑𝗍𝑡 for 𝗇𝖾𝗑𝗍⋅.𝑡.
The following equations are added to the judgmental equality of convention 162.1. In Later-Weak and Next-Weak the type 𝐴 and the term 𝑢 are well formed in a context without 𝑥; in Later-Exch and Next-Exch the type of 𝑥 does not mention 𝑦 and the type of 𝑦 does not mention 𝑥. ▹𝜉[𝑥←𝑡].𝐴≡▹𝜉.𝐴𝐿𝑎𝑡𝑒𝑟−𝑊𝑒𝑎𝑘▹𝜉[𝑥←𝑡,𝑦←𝑢]𝜉′.𝐴≡▹𝜉[𝑦←𝑢,𝑥←𝑡]𝜉′.𝐴𝐿𝑎𝑡𝑒𝑟−𝐸𝑥𝑐ℎ▹𝜉[𝑥←𝗇𝖾𝗑𝗍𝜉.𝑡].𝐴≡▹𝜉.𝐴[𝑡/𝑥]𝐿𝑎𝑡𝑒𝑟−𝐹𝑜𝑟𝑐𝑒𝖤𝗅(̂▹(𝗇𝖾𝗑𝗍𝜉.𝑡))≡▹𝜉.𝖤𝗅(𝑡)𝐿𝑎𝑡𝑒𝑟−𝐸𝑙𝖨𝖽▹𝜉.𝐴(𝗇𝖾𝗑𝗍𝜉.𝑡,𝗇𝖾𝗑𝗍𝜉.𝑠)≡▹𝜉.𝖨𝖽𝐴(𝑡,𝑠)𝐿𝑎𝑡𝑒𝑟−𝐼𝑑𝗇𝖾𝗑𝗍𝜉[𝑥←𝑡].𝑢≡𝗇𝖾𝗑𝗍𝜉.𝑢𝑁𝑒𝑥𝑡−𝑊𝑒𝑎𝑘𝗇𝖾𝗑𝗍𝜉[𝑥←𝑡].𝑥≡𝑡𝑁𝑒𝑥𝑡−𝑉𝑎𝑟𝗇𝖾𝗑𝗍𝜉[𝑥←𝑡,𝑦←𝑢]𝜉′.𝑣≡𝗇𝖾𝗑𝗍𝜉[𝑦←𝑢,𝑥←𝑡]𝜉′.𝑣𝑁𝑒𝑥𝑡−𝐸𝑥𝑐ℎ𝗇𝖾𝗑𝗍𝜉[𝑥←𝗇𝖾𝗑𝗍𝜉.𝑡].𝑢≡𝗇𝖾𝗑𝗍𝜉.𝑢[𝑡/𝑥]𝑁𝑒𝑥𝑡−𝐹𝑜𝑟𝑐𝑒𝖿𝗂𝗑𝑥.𝑡≡𝑡[𝗇𝖾𝗑𝗍(𝖿𝗂𝗑𝑥.𝑡)/𝑥]𝐹𝑖𝑥−𝑈𝑛𝑓𝑜𝑙𝑑
Define 𝑓⊛𝑡:=𝗇𝖾𝗑𝗍[𝑔←𝑓,𝑥←𝑡].𝑔𝑥. Then the rule Γ⊢𝑓:▹𝜉.∏𝑥:𝐴𝐵Γ⊢𝑡:▹𝜉.𝐴Γ⊢𝑓⊛𝑡:▹𝜉[𝑥←𝑡].𝐵 is derivable, and the two applicative-functor laws (𝗇𝖾𝗑𝗍𝜉.𝑓)⊛(𝗇𝖾𝗑𝗍𝜉.𝑡)≡𝗇𝖾𝗑𝗍𝜉.(𝑓𝑡),(𝗇𝖾𝗑𝗍𝜉.𝜆𝑥.𝑥)⊛𝑡≡𝑡 hold.
Proof of Proposition 162.4 — Dependent application
Proof. For the typing rule, extend 𝜉 twice. From Γ⊢𝑓:▹𝜉.∏𝑥:𝐴𝐵 and DS-Cons we obtain Γ⊢𝜉[𝑔←𝑓]:Γ′,𝑔:∏𝑥:𝐴𝐵; from Γ⊢𝑡:▹𝜉.𝐴 and Later-Weak we obtain Γ⊢𝑡:▹𝜉[𝑔←𝑓].𝐴, so DS-Cons applies again and gives Γ⊢𝜉[𝑔←𝑓,𝑥←𝑡]:Γ′,𝑔:∏𝑥:𝐴𝐵,𝑥:𝐴. In that extended telescope 𝑔𝑥:𝐵, so Later-I types 𝗇𝖾𝗑𝗍[𝑔←𝑓,𝑥←𝑡].𝑔𝑥 at ▹𝜉[𝑔←𝑓,𝑥←𝑡].𝐵. The variable 𝑔 does not occur in 𝐵, so Later-Weak and Later-Exch remove it, leaving ▹𝜉[𝑥←𝑡].𝐵.
For the first law, (𝗇𝖾𝗑𝗍𝜉.𝑓)⊛(𝗇𝖾𝗑𝗍𝜉.𝑡)𝑑𝑒𝑓.≡𝗇𝖾𝗑𝗍[𝑔←𝗇𝖾𝗑𝗍𝜉.𝑓,𝑥←𝗇𝖾𝗑𝗍𝜉.𝑡].𝑔𝑥𝑁𝑒𝑥𝑡−𝐹𝑜𝑟𝑐𝑒≡𝗇𝖾𝗑𝗍𝜉.(𝑓𝑡), the last step applying Next-Force twice, once for each assignment.
For the second law, (𝗇𝖾𝗑𝗍𝜉.𝜆𝑥.𝑥)⊛𝑡𝑑𝑒𝑓.≡𝗇𝖾𝗑𝗍[𝑔←𝗇𝖾𝗑𝗍𝜉.𝜆𝑥.𝑥,𝑦←𝑡].𝑔𝑦𝑁𝑒𝑥𝑡−𝐹𝑜𝑟𝑐𝑒≡𝗇𝖾𝗑𝗍[𝑦←𝑡].𝑦𝑁𝑒𝑥𝑡−𝑉𝑎𝑟≡𝑡. ◻
★☆☆ Derive the non-dependent rule Γ⊢𝑓:▹𝜉.(𝐴→𝐵)Γ⊢𝑡:▹𝜉.𝐴Γ⊢𝑓⊛𝑡:▹𝜉.𝐵 from proposition 162.4, naming the equation of definition 162.3 that removes the extra assignment. Then show that ▹ is not a monad by attempting to derive a term of type ▹▹𝐴→▹𝐴 and identifying the rule that would be needed.
A term formed by Fix is defined by guarded recursion. When the type 𝐴 is a proposition, the same rule reads Γ,𝑥:▹𝐴⊢𝑡:𝐴Γ⊢𝖿𝗂𝗑𝑥.𝑡:𝐴, and is called Löb induction: to prove 𝐴 it suffices to prove 𝐴 from the assumption that 𝐴 holds one step later.
Löb induction is not a valid principle of ordinary logic. Taking 𝐴 to be the false proposition and ▹𝐴 to be 𝐴 would prove falsity; what prevents that is exactly that ▹𝐴 is not 𝐴. The next lemma is the precise form of the difference, and it is proved in the model in section 162.3.
The statement is deliberately about the interpretation and not about the calculus: Fix-Unfold makes 𝖿𝗂𝗑𝑥.𝑡a fixed point, and uniqueness is a semantic fact that theorem 162.14 supplies.
Let Γ⊢̂𝐴:U be a code with 𝐴:=𝖤𝗅(̂𝐴). Define the code ̂𝖲𝗍𝗋𝐴:=𝖿𝗂𝗑𝑋.̂𝐴̂×̂▹𝑋,𝖲𝗍𝗋𝐴:=𝖤𝗅(̂𝖲𝗍𝗋𝐴), where ̂× is the code of the product type. The guarded stream type𝖲𝗍𝗋𝐴 satisfies 𝖲𝗍𝗋𝐴≡𝐴×▹𝖲𝗍𝗋𝐴, and we write 𝗁𝖽:=𝗉𝗋1,𝗍𝗅:=𝗉𝗋2,𝖼𝗈𝗇𝗌:=𝜆𝑎.𝜆𝑎𝑠.(𝑎,𝑎𝑠):𝐴→▹𝖲𝗍𝗋𝐴→𝖲𝗍𝗋𝐴.
Derivation of the displayed equation. Unfolding the fixed point and decoding, 𝖲𝗍𝗋𝐴𝑑𝑒𝑓.≡𝖤𝗅(̂𝖲𝗍𝗋𝐴)𝐹𝑖𝑥−𝑈𝑛𝑓𝑜𝑙𝑑≡𝖤𝗅(̂𝐴̂×̂▹(𝗇𝖾𝗑𝗍̂𝖲𝗍𝗋𝐴))𝐿𝑎𝑡𝑒𝑟−𝐸𝑙≡𝐴×▹𝖤𝗅(̂𝖲𝗍𝗋𝐴)𝑑𝑒𝑓.≡𝐴×▹𝖲𝗍𝗋𝐴, where the third step uses Later-El with the empty delayed substitution and the decoding of ̂× as a product. ◻
Define, for 𝐴:=ℕ, 𝗆𝖺𝗉:=𝖿𝗂𝗑𝜑.𝜆𝑓.𝜆𝑠.𝖼𝗈𝗇𝗌(𝑓(𝗁𝖽𝑠))(𝜑⊛𝗇𝖾𝗑𝗍𝑓⊛𝗍𝗅𝑠):(ℕ→ℕ)→𝖲𝗍𝗋ℕ→𝖲𝗍𝗋ℕ,𝗇𝖺𝗍𝗌:=𝖿𝗂𝗑𝑥.𝖼𝗈𝗇𝗌𝟢((𝗇𝖾𝗑𝗍(𝗆𝖺𝗉𝗌𝗎𝖼))⊛𝑥):𝖲𝗍𝗋ℕ. In 𝗇𝖺𝗍𝗌 the recursion variable 𝑥 has type ▹𝖲𝗍𝗋ℕ, and the only operation applied to it is ⊛, which by proposition 162.4 returns a term of ▹-type again. The definition is therefore typed by Fix exactly because the recursive occurrence stays under ▹. The syntactic check that rejected (162.1) inspected the position of the recursive occurrence; Fix inspects its type.
★★☆ Define 𝗓𝗂𝗉𝖶𝗂𝗍𝗁:(ℕ→ℕ→ℕ)→𝖲𝗍𝗋ℕ→𝖲𝗍𝗋ℕ→𝖲𝗍𝗋ℕ by guarded recursion, giving the type of every subterm containing the recursion variable. Then attempt to define the function that deletes every second element of a stream, with type 𝖲𝗍𝗋ℕ→𝖲𝗍𝗋ℕ, and identify the exact judgment that cannot be derived. State which type the second element of the output would have to be read from.
Exercise 162.2 exhibits the boundary of the single-modality calculus: a function whose 𝑛th output uses the (2𝑛)th input cannot be typed, because 𝗍𝗅 moves one step later each time it is applied and nothing brings the result back. Section 162.5 adds the operation that does.
Let 𝜔 be the poset 1≤2≤3≤⋯ of positive integers. The topos of trees is the presheaf category S:=[𝜔op,𝐒𝐞𝐭]. Concretely, an object 𝑋 is a family of sets 𝑋1,𝑋2,… together with restriction maps𝑟𝑋𝑛:𝑋𝑛+1⟶𝑋𝑛 for 𝑛≥1, and a map 𝑓:𝑋⇒𝑌 is a family 𝑓𝑛:𝑋𝑛⟶𝑌𝑛 with 𝑟𝑌𝑛∘𝑓𝑛+1=𝑓𝑛∘𝑟𝑋𝑛.
Read 𝑋𝑛 as the information about an element of 𝑋 that is available after 𝑛 steps, and 𝑟𝑋𝑛 as forgetting the last step. A global element of 𝑋, that is a map 1⇒𝑋, is a compatible family 𝑥𝑛∈𝑋𝑛 with 𝑟𝑋𝑛(𝑥𝑛+1)=𝑥𝑛.
Define ▸:S→S by (▸𝑋)1:={∗},(▸𝑋)𝑛+1:=𝑋𝑛,𝑟▸𝑋1:=!,𝑟▸𝑋𝑛+1:=𝑟𝑋𝑛, with (▸𝑓)1:=id and (▸𝑓)𝑛+1:=𝑓𝑛. Define next𝑋:𝑋⇒▸𝑋 by (next𝑋)1:=! and (next𝑋)𝑛+1:=𝑟𝑋𝑛.
Proof of Lemma 162.11 — Preservation of finite limits
Proof. Finite limits in S are computed levelwise. At level 1 the value of ▸ is the one-point set, which is the limit of any finite diagram of one-point sets; at level 𝑛+1 the value is the level-𝑛 value of the argument, and the limit at level 𝑛 is preserved because the identity function preserves it. Naturality of next at level 1 holds because the codomain is a one-point set, and at level 𝑛+1 it is the naturality square of 𝑓 at level 𝑛. ◻
There is no natural transformation ▸▸⇒▸. Such a transformation would supply, at level 2, a function (▸▸𝑋)2=(▸𝑋)1={∗}⟶(▸𝑋)2=𝑋1 natural in 𝑋, hence a global element of 𝑋1 uniform in 𝑋; taking 𝑋 with 𝑋1=∅ makes that impossible. This is the semantic reason that exercise 162.1 has no term of type ▹▹𝐴→▹𝐴.
Let 𝑔:▸𝑋⇒𝑋. There is exactly one global element 𝑥:1⇒𝑋 with 𝑥=𝑔∘next𝑋∘𝑥, namely 𝑥1:=𝑔1(∗),𝑥𝑛+1:=𝑔𝑛+1(𝑥𝑛). Consequently every contractive endomorphism of 𝑋 has exactly one fixed point.
Proof of Theorem 162.14 — Unique guarded fixed points
Proof.The family is a global element. The displayed clauses are typed: (▸𝑋)1={∗} and (▸𝑋)𝑛+1=𝑋𝑛, so 𝑔1(∗)∈𝑋1 and 𝑔𝑛+1(𝑥𝑛)∈𝑋𝑛+1. Compatibility is proved by induction on 𝑛. For 𝑛=1, naturality of 𝑔 at level 1 gives 𝑟𝑋1∘𝑔2=𝑔1∘𝑟▸𝑋1=𝑔1∘!, hence 𝑟𝑋1(𝑥2)𝑑𝑒𝑓.=𝑟𝑋1(𝑔2(𝑥1))𝑛𝑎𝑡.=𝑔1(∗)𝑑𝑒𝑓.=𝑥1. For 𝑛≥2, naturality gives 𝑟𝑋𝑛∘𝑔𝑛+1=𝑔𝑛∘𝑟𝑋𝑛−1, hence 𝑟𝑋𝑛(𝑥𝑛+1)𝑑𝑒𝑓.=𝑟𝑋𝑛(𝑔𝑛+1(𝑥𝑛))𝑛𝑎𝑡.=𝑔𝑛(𝑟𝑋𝑛−1(𝑥𝑛))𝐼𝐻=𝑔𝑛(𝑥𝑛−1)𝑑𝑒𝑓.=𝑥𝑛.
It is a fixed point.(next𝑋∘𝑥)1=∗ and (next𝑋∘𝑥)𝑛+1=𝑟𝑋𝑛(𝑥𝑛+1)=𝑥𝑛, so (𝑔∘next𝑋∘𝑥)1=𝑔1(∗)=𝑥1 and (𝑔∘next𝑋∘𝑥)𝑛+1=𝑔𝑛+1(𝑥𝑛)=𝑥𝑛+1.
Uniqueness. Let 𝑦 be a global element with 𝑦=𝑔∘next𝑋∘𝑦. Then 𝑦1=𝑔1(∗)=𝑥1, and if 𝑦𝑛=𝑥𝑛 then 𝑦𝑛+1=𝑔𝑛+1(𝑟𝑋𝑛(𝑦𝑛+1))=𝑔𝑛+1(𝑦𝑛)=𝑔𝑛+1(𝑥𝑛)=𝑥𝑛+1. By induction 𝑦=𝑥.
For the consequence, a contractive 𝑓:𝑋⇒𝑋 with witness 𝑔 satisfies 𝑓∘𝑥=𝑔∘next𝑋∘𝑥 for every 𝑥, so the fixed points of 𝑓 are exactly the solutions of the displayed equation. ◻
A context Γ is interpreted as an object [[Γ]] of S. A type Γ⊢𝐴𝗍𝗒𝗉𝖾 is interpreted as a family [[𝐴]] assigning to every 𝑛≥1 and every 𝛾∈[[Γ]]𝑛 a set [[𝐴]]𝑛(𝛾), together with restriction maps 𝑟𝐴𝑛(𝛾):[[𝐴]]𝑛+1(𝛾)⟶[[𝐴]]𝑛(𝑟[[Γ]]𝑛(𝛾)). A term Γ⊢𝑡:𝐴 is interpreted as a family of elements [[𝑡]]𝑛(𝛾)∈[[𝐴]]𝑛(𝛾) commuting with restriction. Context extension is [[Γ,𝑥:𝐴]]𝑛:={(𝛾,𝑎)∣𝛾∈[[Γ]]𝑛,𝑎∈[[𝐴]]𝑛(𝛾)}. The new clauses are [[▹𝐴]]1(𝛾):={∗},[[▹𝐴]]𝑛+1(𝛾):=[[𝐴]]𝑛(𝑟𝑛(𝛾)),[[▹[𝑥←𝑡].𝐵]]1(𝛾):={∗},[[▹[𝑥←𝑡].𝐵]]𝑛+1(𝛾):=[[𝐵]]𝑛(𝑟𝑛(𝛾),[[𝑡]]𝑛+1(𝛾)),[[𝗇𝖾𝗑𝗍𝑢]]1(𝛾):=∗,[[𝗇𝖾𝗑𝗍𝑢]]𝑛+1(𝛾):=[[𝑢]]𝑛(𝑟𝑛(𝛾)),[[𝗇𝖾𝗑𝗍[𝑥←𝑡].𝑢]]1(𝛾):=∗,[[𝗇𝖾𝗑𝗍[𝑥←𝑡].𝑢]]𝑛+1(𝛾):=[[𝑢]]𝑛(𝑟𝑛(𝛾),[[𝑡]]𝑛+1(𝛾)), and a longer delayed substitution is interpreted by iterating the second and fourth clauses from left to right. A term 𝖿𝗂𝗑𝑥.𝑡 formed by Fix in the empty context is interpreted as the unique fixed point of theorem 162.14 for the map 𝑔:▸[[𝐴]]⇒[[𝐴]] with 𝑔1(∗):=[[𝑡]]1(∗) and 𝑔𝑛+1(𝑎):=[[𝑡]]𝑛+1(𝑎).
The second clause is the whole content of the delayed substitution: at stage 𝑛+1 the argument 𝑡is available, with value [[𝑡]]𝑛+1(𝛾)∈[[𝐴]]𝑛(𝑟𝑛𝛾), and the type 𝐵 is reindexed along it. The delay in the syntax is the shift of index in the model.
Proof. The rules DS-Emp, DS-Cons, Later-F and Later-I hold because each displayed clause of definition 162.15 is defined exactly when its premises are, and Fix holds by theorem 162.14. Each equation is checked at level 1, where both sides are the one-point set or the element ∗, and at level 𝑛+1. We display the level-(𝑛+1) computation for each; throughout, 𝛾 ranges over [[Γ]]𝑛+1 and 𝑟𝑛 abbreviates 𝑟[[Γ]]𝑛.
Later-Weak. If 𝑥 does not occur in 𝐴, then [[𝐴]]𝑛(𝑟𝑛𝛾,𝑎) does not depend on 𝑎, so [[▹[𝑥←𝑡].𝐴]]𝑛+1(𝛾)𝑑𝑒𝑓.=[[𝐴]]𝑛(𝑟𝑛𝛾,[[𝑡]]𝑛+1(𝛾))𝑥∉𝐴=[[𝐴]]𝑛(𝑟𝑛𝛾)𝑑𝑒𝑓.=[[▹𝐴]]𝑛+1(𝛾).
Later-Force. Substituting a 𝗇𝖾𝗑𝗍 recovers an ordinary substitution: [[▹[𝑥←𝗇𝖾𝗑𝗍𝑡].𝐴]]𝑛+1(𝛾)𝑑𝑒𝑓.=[[𝐴]]𝑛(𝑟𝑛𝛾,[[𝗇𝖾𝗑𝗍𝑡]]𝑛+1(𝛾))𝑑𝑒𝑓.=[[𝐴]]𝑛(𝑟𝑛𝛾,[[𝑡]]𝑛(𝑟𝑛𝛾))𝑠𝑢𝑏𝑠𝑡.=[[▹(𝐴[𝑡/𝑥])]]𝑛+1(𝛾).
Later-Exch. The two clauses for 𝑥 and 𝑦 evaluate [[𝑡]]𝑛+1(𝛾) and [[𝑢]]𝑛+1(𝛾) at the same index 𝑛+1, and neither type mentions the other variable, so the resulting reindexing of [[𝐴]]𝑛 is the same pair in either order.
Later-Id. Interpret the extensional identity type by setting [[𝖨𝖽𝐴(𝑡,𝑠)]]𝑛(𝛾) to {∗} when [[𝑡]]𝑛(𝛾)=[[𝑠]]𝑛(𝛾), and to ∅ otherwise. Then [[𝖨𝖽▹𝐴(𝗇𝖾𝗑𝗍𝑡,𝗇𝖾𝗑𝗍𝑠)]]𝑛+1(𝛾)isinhabited⟺[[𝑡]]𝑛(𝑟𝑛𝛾)=[[𝑠]]𝑛(𝑟𝑛𝛾)⟺[[▹𝖨𝖽𝐴(𝑡,𝑠)]]𝑛+1(𝛾)isinhabited, and at level 1 both sides are {∗}, because [[𝗇𝖾𝗑𝗍𝑡]]1(𝛾)=∗=[[𝗇𝖾𝗑𝗍𝑠]]1(𝛾).
Next-Weak and Next-Exch. As in Later-Weak and Later-Exch, with the term clause of definition 162.15 in place of the type clause.
Next-Var. At level 𝑛+1, [[𝗇𝖾𝗑𝗍[𝑥←𝑡].𝑥]]𝑛+1(𝛾) is the value assigned to 𝑥, namely [[𝑡]]𝑛+1(𝛾). At level 1 both sides lie in the one-point set [[▹𝐴]]1(𝛾).
Next-Force. As in Later-Force, with 𝑢 in place of 𝐴.
Fix-Unfold. By theorem 162.14 the interpretation 𝑥 of 𝖿𝗂𝗑𝑥.𝑡 satisfies 𝑥=𝑔∘next∘𝑥, and 𝑔∘next∘𝑥 is by construction the interpretation of 𝑡[𝗇𝖾𝗑𝗍(𝖿𝗂𝗑𝑥.𝑡)/𝑥]. ◻
Proposition 162.6 now follows: the uniqueness clause of theorem 162.14 identifies any two global elements satisfying the unfolding equation.
Theorem 162.16 omits Later-Code and Later-El, which concern the universe. Interpreting them requires a semantic universe in S closed under ▸ and equipped with a code for it, and in the multi-clock calculus of section 162.5 the universes must in addition be indexed by clock contexts. That construction is carried out by Bizjak and Møgelberg, Denotational semantics for guarded dependent type theory, §7, where the universes are built so that inclusions of clock contexts give inclusions of universes commuting with the type operations on the nose [BM20]. It is not reproved here. In the remainder of this chapter the guarded stream type is interpreted directly by theorem 162.18, so no universe is needed for the productivity theorem.
Let Δ(ℕ) be the constant object with Δ(ℕ)𝑛=ℕ and identity restrictions. There is exactly one object 𝑋 of S, up to isomorphism, with 𝑋≅Δ(ℕ)×▸𝑋, and it is given by 𝑋𝑛=ℕ𝑛,𝑟𝑋𝑛(𝑎1,…,𝑎𝑛+1)=(𝑎1,…,𝑎𝑛).
Proof of Theorem 162.18 — The guarded stream object
Proof.The displayed object is a solution. Compute both sides levelwise: (Δ(ℕ)×▸𝑋)1=ℕ×{∗}=ℕ=𝑋1,(Δ(ℕ)×▸𝑋)𝑛+1=ℕ×𝑋𝑛=ℕ𝑛+1=𝑋𝑛+1. Under these identifications the restriction map of the right-hand side sends (𝑎1,(𝑎2,…,𝑎𝑛+1)) to (𝑎1,𝑟▸𝑋𝑛(𝑎2,…,𝑎𝑛+1))=(𝑎1,(𝑎2,…,𝑎𝑛)), which is the displayed 𝑟𝑋𝑛.
Uniqueness. Let 𝑌 satisfy 𝑌≅Δ(ℕ)×▸𝑌 with isomorphism 𝑖. At level 1 the right-hand side is ℕ×{∗}, so 𝑖1 is a bijection 𝑌1→ℕ=𝑋1. Suppose 𝑖 induces a bijection 𝑌𝑛→𝑋𝑛. At level 𝑛+1 the right-hand side is ℕ×𝑌𝑛, so 𝑖𝑛+1 composed with id×(thebijection𝑌𝑛→𝑋𝑛) is a bijection 𝑌𝑛+1→ℕ×𝑋𝑛=𝑋𝑛+1. These bijections commute with the restriction maps because 𝑖 does, so 𝑌≅𝑋 in S. ◻
Let 𝑡 be a closed term with ⋅⊢𝑡:𝖲𝗍𝗋ℕ, interpreted as a global element [[𝑡]] of the object 𝑋 of theorem 162.18. For 𝑘≥1 the 𝑘th observation of 𝑡 is obs𝑘(𝑡):=the𝑘thcoordinateof[[𝑡]]𝑛∈ℕ𝑛,forany𝑛≥𝑘.
Proof of Proposition 162.20 — The observation is well defined
Proof.[[𝑡]] is a global element, so 𝑟𝑋𝑛([[𝑡]]𝑛+1)=[[𝑡]]𝑛; by theorem 162.18 that restriction deletes the last coordinate and leaves the first 𝑛 unchanged. Hence for 𝑘≤𝑛 the 𝑘th coordinate of [[𝑡]]𝑛+1 equals the 𝑘th coordinate of [[𝑡]]𝑛, and the claim follows by induction on 𝑛−𝑘. ◻
Proof of Theorem 162.21 — Productivity of finite observations
Proof. By theorem 162.16 the interpretation of a closed term of type 𝖲𝗍𝗋ℕ is a global element of the object 𝑋 of theorem 162.18, so [[𝑡]]𝑘 is an element of ℕ𝑘 and its 𝑘th coordinate is a natural number; proposition 162.20 shows that no other choice of 𝑛 changes it. Judgmentally equal terms have equal interpretations, again by theorem 162.16, hence equal coordinates. ◻
Theorem 162.21 is the exact repair of the failure recorded at (162.1): the definition is now accepted, and every finite observation of it is a determinate number. The following calculation exhibits those numbers.
Write 𝑚:=[[𝗆𝖺𝗉𝗌𝗎𝖼]] for the interpretation of the function of example 162.8. We claim 𝑚𝑛(𝑎1,…,𝑎𝑛)=(𝑎1+1,…,𝑎𝑛+1). By Fix-Unfold, 𝗆𝖺𝗉𝗌𝗎𝖼𝑠≡𝖼𝗈𝗇𝗌(𝗌𝗎𝖼(𝗁𝖽𝑠))((𝗇𝖾𝗑𝗍(𝗆𝖺𝗉𝗌𝗎𝖼))⊛𝗍𝗅𝑠). At level 1 the second component lies in the one-point set, so 𝑚1(𝑎1)=(𝑎1+1). At level 𝑛+1, the clause for ⊛ in definition 162.15 evaluates 𝗇𝖾𝗑𝗍(𝗆𝖺𝗉𝗌𝗎𝖼) at index 𝑛, so 𝑚𝑛+1(𝑎1,…,𝑎𝑛+1)𝐹𝑖𝑥−𝑈𝑛𝑓𝑜𝑙𝑑=(𝑎1+1,𝑚𝑛(𝑎2,…,𝑎𝑛+1))𝐼𝐻=(𝑎1+1,…,𝑎𝑛+1+1). Now let 𝑥:=[[𝗇𝖺𝗍𝗌]]. By definition 162.15 the witness 𝑔 for 𝗇𝖺𝗍𝗌 satisfies 𝑔1(∗)=(𝟢) and 𝑔𝑛+1(𝑤)=(𝟢,𝑚𝑛(𝑤)), so theorem 162.14 gives 𝑥1=(0),𝑥2=(0,𝑚1(0))=(0,1),𝑥3=(0,𝑚2(0,1))=(0,1,2), and by induction 𝑥𝑛=(0,1,…,𝑛−1). Hence obs𝑘(𝗇𝖺𝗍𝗌)=𝑘−1.
The equation (162.2) rejected at the opening becomes solvable once the occurrence is guarded. Define 𝐹:S→S by 𝐹(𝑌):=(▸𝑌→Δ(ℕ)). Then 𝐷1={∗}→ℕ=ℕ,𝐷𝑛+1=(maps𝐷𝑛⟶ℕatlevel𝑛+1), and the same levelwise induction as in theorem 162.18 shows that 𝐷≅𝐹(𝐷) has a solution determined at each level by the previous one. The variable occurs negatively, and the solution exists because ▸ lowers the level at which the occurrence is read.
★★☆ Compute obs𝑘 for the following closed terms of type 𝖲𝗍𝗋ℕ, in each case by exhibiting the witness 𝑔 of theorem 162.14 and the first three levels of the fixed point: 𝗈𝗇𝖾𝗌:=𝖿𝗂𝗑𝑥.𝖼𝗈𝗇𝗌(𝗌𝗎𝖼𝟢)𝑥,𝖺𝗅𝗍:=𝖿𝗂𝗑𝑥.𝖼𝗈𝗇𝗌𝟢((𝗇𝖾𝗑𝗍(𝜆𝑠.𝖼𝗈𝗇𝗌(𝗌𝗎𝖼𝟢)(𝗇𝖾𝗑𝗍𝑠)))⊛𝑥). State for each whether the value of obs𝑘 depends on 𝑘, and name the level of the model at which that dependence first appears.
Exercise 162.2 asks for a function whose 𝑛th output is read from the 2𝑛th input. Each application of 𝗍𝗅 moves one step later, and the calculus of section 162.1 has no operation moving back. The addition that supplies one is a second binder: quantification over the dimension along which ▹ delays.
Fix a countable set of clock variables and one clock constant 𝜅0. A clock contextΔ is a finite set of clock variables, and ⊢Δ𝜅 says that 𝜅 is a member of Δ or is 𝜅0. Every judgment of convention 162.1 and definition 162.2 is annotated with a clock context, written Γ⊢Δ, and the modality of definition 162.2 is written ▹𝜅, one for each clock 𝜅 with ⊢Δ𝜅. All judgments are closed under clock weakening and clock substitution. The added formers are
Γ⊢𝐴𝗍𝗒𝗉𝖾inΔ,𝜅𝜅∉Δ
Γ⊢∀𝜅.𝐴𝗍𝗒𝗉𝖾inΔ
All-F
Γ⊢Δ,𝜅𝑡:𝐴𝜅∉Δ
Γ⊢ΔΛ𝜅.𝑡:∀𝜅.𝐴
All-I
Γ⊢Δ𝑡:∀𝜅.𝐴⊢Δ𝜅′
Γ⊢Δ𝑡[𝜅′]:𝐴[𝜅′/𝜅]
All-E
Γ⊢Δ,𝜅𝑡:▹𝜅𝐴𝜅∉Δ
Γ⊢Δ𝗉𝗋𝖾𝗏𝜅.𝑡:∀𝜅.𝐴
Prev
with the equations (Λ𝜅.𝑡)[𝜅′]≡𝑡[𝜅′/𝜅]𝐴𝑙𝑙−𝛽Λ𝜅.𝑡[𝜅]≡𝑡𝐴𝑙𝑙−𝜂𝑡[𝜅′]≡𝑡[𝜅″]𝐶𝑙𝑜𝑐𝑘−𝐼𝑟𝑟𝗉𝗋𝖾𝗏𝜅.𝗇𝖾𝗑𝗍𝜅𝑡≡Λ𝜅.𝑡𝑃𝑟𝑒𝑣−𝛽𝗇𝖾𝗑𝗍𝜅((𝗉𝗋𝖾𝗏𝜅.𝑡)[𝜅])≡𝑡𝑃𝑟𝑒𝑣−𝜂 where All-𝜂 requires 𝜅∉Δ, and Clock-Irr requires Γ⊢Δ𝑡:∀𝜅.𝐴 with 𝜅 not free in 𝐴, and ⊢Δ𝜅′, ⊢Δ𝜅″.
Clock-Irr is the clock irrelevance equation: when the type does not mention the clock, the value of a clock-quantified term does not depend on which clock it is instantiated at. It is the equation that turns a guarded type into a genuinely coinductive one, and it is the hardest of the five to model.
Proof of Lemma 162.25 — Clock quantification is trivial on clock-free types
Proof. For one composite, 𝑓(𝑔𝑥)𝛽≡(Λ𝜅.𝑥)[𝜅0]𝐴𝑙𝑙−𝛽≡𝑥. For the other, let Γ⊢𝑦:∀𝜅.𝐴. Then 𝑔(𝑓𝑦)𝛽≡Λ𝜅.𝑦[𝜅0]𝐶𝑙𝑜𝑐𝑘−𝐼𝑟𝑟≡Λ𝜅.𝑦[𝜅]𝐴𝑙𝑙−𝜂≡𝑦, the middle step instantiating Clock-Irr at 𝜅′=𝜅0 and 𝜅″=𝜅, which is legal because 𝜅 is not free in 𝐴. ◻
The clock constant 𝜅0 is used in an essential way in lemma 162.25: without it, the term 𝑓 has nothing to instantiate at.
Let 𝜅 be a fresh clock and let 𝖲𝗍𝗋𝜅ℕ be the guarded stream type of definition 162.7 formed with ▹𝜅. Define 𝖲𝗍𝗋∞ℕ:=∀𝜅.𝖲𝗍𝗋𝜅ℕ,𝗁𝖽∞:=𝜆𝑥𝑠.𝗁𝖽𝜅0(𝑥𝑠[𝜅0]):𝖲𝗍𝗋∞ℕ→ℕ,𝗍𝗅∞:=𝜆𝑥𝑠.𝗉𝗋𝖾𝗏𝜅.𝗍𝗅𝜅(𝑥𝑠[𝜅]):𝖲𝗍𝗋∞ℕ→𝖲𝗍𝗋∞ℕ,𝖼𝗈𝗇𝗌∞:=𝜆𝑥.𝜆𝑥𝑠.Λ𝜅.𝖼𝗈𝗇𝗌𝜅𝑥(𝗇𝖾𝗑𝗍𝜅(𝑥𝑠[𝜅])):ℕ→𝖲𝗍𝗋∞ℕ→𝖲𝗍𝗋∞ℕ.
The tail is the operation that was missing. Applying 𝗍𝗅𝜅 inside the scope of Λ𝜅 produces a term of type ▹𝜅𝖲𝗍𝗋𝜅ℕ, and Prev converts a ▹𝜅 under a clock binder into a ∀𝜅, removing the delay.
Define 𝖾𝗈𝜅:=𝖿𝗂𝗑𝜅𝜑.𝜆𝑥𝑠.𝖼𝗈𝗇𝗌𝜅(𝗁𝖽∞𝑥𝑠)(𝜑⊛𝜅𝗇𝖾𝗑𝗍𝜅(𝗍𝗅∞(𝗍𝗅∞𝑥𝑠))):𝖲𝗍𝗋∞ℕ→𝖲𝗍𝗋𝜅ℕ, and 𝖾𝗈:=𝜆𝑥𝑠.Λ𝜅.𝖾𝗈𝜅𝑥𝑠 of type 𝖲𝗍𝗋∞ℕ→𝖲𝗍𝗋∞ℕ. The recursion variable 𝜑 still has a ▹𝜅-type, so Fix applies; what has changed is that the argument 𝑥𝑠 has the coinductive type, so 𝗍𝗅∞ may be applied to it twice with no delay incurred. The typing of 𝖾𝗈𝜅 fails if 𝖲𝗍𝗋∞ℕ is replaced by 𝖲𝗍𝗋𝜅ℕ, because 𝗍𝗅𝜅 then returns a ▹𝜅-type and the second application has no argument of the right type.
Proof of Theorem 162.28 — Bisimulation for guarded streams
Proof. By theorem 162.18 the interpretations are global elements of the object with 𝑋𝑛=ℕ𝑛, so [[𝑠]]𝑛 and [[𝑡]]𝑛 are 𝑛-tuples. By definition 162.19 the 𝑘th coordinate of [[𝑠]]𝑛 is obs𝑘(𝑠) for every 𝑘≤𝑛, and likewise for 𝑡. Two 𝑛-tuples with the same coordinates are equal, so [[𝑠]]𝑛=[[𝑡]]𝑛 for every 𝑛. ◻
Chapter 33 defines the type of streams as the carrier of the final coalgebra of 𝑌↦ℕ×𝑌 and derives corecursion from finality. The two constructions differ in what they take as primitive.
Finality gives a unique map into the carrier from every coalgebra; the productivity of a definition is then the requirement that it be presented as a coalgebra, and a definition such as (162.1) must be rewritten to expose one.
Theorem 162.14 gives a unique fixed point for every map out of ▸𝑋; productivity is then the requirement that the recursive occurrence carry a ▹, which example 162.8 shows is satisfied by (162.1) as written.
The guarded type 𝖲𝗍𝗋𝜅ℕ is not the final coalgebra: by theorem 162.18 its stage-𝑛 elements are 𝑛-tuples, whereas the final coalgebra has infinite sequences as elements. The type that recovers the final coalgebra is ∀𝜅.𝖲𝗍𝗋𝜅ℕ, and it does so only because Clock-Irr is available. That identification is Møgelberg’s theorem for the set-based semantics and is not proved here.
The results of section 162.3–section 162.4 are proved for the single-clock calculus of definition 162.2, definition 162.3 without universes. Four further systems appear in the literature, each with its own rule table, and their theorems are stated here at those signatures.
The multi-clock model. Bizjak and Møgelberg give a denotational model of guarded dependent type theory with the clock rules of definition 162.24. Their model is built from covariant presheaves over a category of time objects, with clock quantification interpreted by a presheaf of clocks. The point requiring work is Clock-Irr: to validate it, types must be interpreted as presheaves internally right orthogonal to the object of clocks, which for dependent types is a lifting condition with uniqueness of lifts. Because Hofmann–Streicher universes in that model do not satisfy the condition, the universes must be indexed by clock contexts [BM20]. This supplies the two rules omitted from theorem 162.16, at their signature and not at the one of definition 162.15.
Clocked type theory. Bahr, Grathwohl and Møgelberg replace the term former 𝗇𝖾𝗑𝗍𝜅 by tick variables and obtain a reduction semantics. For that calculus they prove subject reduction, confluence, and strong normalization of well-typed terms and types; decidability of the equational theory follows from the last two, since normal forms are unique and computable. They further prove canonicity in the form: if ⊢Δ𝑡:ℕ then 𝑡 reduces to 𝗌𝗎𝖼𝑛𝟢 for some 𝑛, where 𝑡 may contain free clock variables; and productivity in the form: if 𝑡 is a closed term of the coinductive stream type and 𝑛 is a closed term of ℕ, then 𝗇𝗍𝗁𝑛𝑡 reduces to a numeral. Their translation from guarded dependent type theory into clocked type theory preserves equality. None of these is a theorem about the calculus of definition 162.2, whose equality is not presented by a reduction relation at all.
Guarded computational type theory. Sterling and Harper give an operational account with a clock intersection connective in place of clock quantification, enjoying clock irrelevance, and with a predicative hierarchy of universes that is not indexed by clock contexts. For that theory they prove canonicity at the Boolean type: every closed expression of type 𝖻𝗈𝗈𝗅 is equal to one of the two constants; consistency follows [SH18]. Its definitional equality is a computational one in the sense of chapter 36 and is not the judgmental equality of definition 162.3.
Guarded cubical type theory. Combining ▹ with a cubical interval is a further system with its own rule table. Nothing in section 162.1–section 162.5 makes the univalence axiom available: the model of definition 162.9 interprets the identity type extensionally, and no path structure has been introduced. The combination is not used in this chapter.
★★★Theorem 162.16 verifies the equations of definition 162.3 at levels 1 and 𝑛+1. Carry out the two verifications that the proof compressed.
Write, in full and as a function of 𝑛 and 𝛾, the interpretation of a delayed substitution 𝜉=[𝑥1←𝑡1,…,𝑥𝑚←𝑡𝑚] of length 𝑚, and prove by induction on 𝑚 that [[▹𝜉.𝐴]] is a well-formed type in the sense of definition 162.15.
Verify Later-Exch and Next-Exch for 𝑚=2 by displaying both reindexings, and state the exact hypothesis on the types of 𝑥 and 𝑦 that makes them equal.
Give a pair of assignments for which the exchange hypothesis fails and the two sides of Later-Exch denote different types.
★★★ A guarded covector is a stream of a length given by a guarded conatural. Define the guarded conaturals by 𝖢𝗈𝖭𝜅:=𝖿𝗂𝗑𝜅𝑋.̂𝟏̂+̂▹𝜅𝑋 and the covector family by guarded recursion over 𝖢𝗈𝖭𝜅.
Give the two clauses of the family and derive the type isomorphisms 𝖢𝗈𝖵𝖾𝖼0≅𝟏 and 𝖢𝗈𝖵𝖾𝖼(𝗌𝗎𝖼𝖼𝑛)≅ℕ×▹𝜅𝖢𝗈𝖵𝖾𝖼𝑛.
Type the tail function on covectors, showing where the second isomorphism is used.
Type the map function on covectors, and mark the one place where a delayed substitution of length two is unavoidable. State what the type of the recursive call would be if only the applicative rule (162.3) were available.
★★☆Proposition 162.6 was obtained from the model. Investigate whether it can be obtained from the calculus.
Assume 𝑢 satisfies 𝑢≡𝑡[𝗇𝖾𝗑𝗍𝑢/𝑥] and attempt to derive 𝑢≡𝖿𝗂𝗑𝑥.𝑡 using only definition 162.3. Identify the step that would require an induction principle for ▹.
Using Later-Id, formulate the statement 𝖨𝖽𝐴(𝑢,𝖿𝗂𝗑𝑥.𝑡) as the conclusion of a Löb induction, and write the term of type ▹𝖨𝖽𝐴(𝑢,𝖿𝗂𝗑𝑥.𝑡)→𝖨𝖽𝐴(𝑢,𝖿𝗂𝗑𝑥.𝑡) that the induction requires.
State the extra equation on 𝑡 under which that term exists, and check it for 𝑡:=𝖼𝗈𝗇𝗌𝟢𝑥.
★★★Practical project.guarded-observation-evaluator Implement, in Kappa, a finite-level evaluator for the single-clock guarded calculus, and use it to compute the observations of definition 162.19.
Calculus to implement. The syntax of definition 162.2, restricted to the fragment needed for streams: ℕ with 𝟢 and 𝗌𝗎𝖼, products with both projections, function types with abstraction and application, ▹ with 𝗇𝖾𝗑𝗍 and ⊛, and 𝖿𝗂𝗑. Represent terms with de Bruijn indices and implement capture-avoiding substitution. Evaluate a term at a stage 𝑛 by the clauses of definition 162.15: a value at stage 𝑛 is a finite tree, a ▹-value at stage 𝑛+1 is a value at stage 𝑛, and a ▹-value at stage 1 carries no information.
Invariant. Evaluation at stage 𝑛 must never inspect a ▹-value beyond stage 𝑛−1, and the restriction map must satisfy 𝑟𝑛(eval𝑛+1(𝑡))=eval𝑛(𝑡) for every closed term 𝑡 of the fragment. The program must check this equation for every evaluated term and report a failure when it does not hold; that check is the executable form of proposition 162.20.
Concrete result. A function taking a closed term of stream type and a bound 𝑁, and returning the list obs1,…,obs𝑁.
Acceptance test. Run the program on the named inputs of example 162.8, exercise 162.3 with 𝑁=6. The outputs must be exactly 𝗇𝖺𝗍𝗌↦[0,1,2,3,4,5],𝗈𝗇𝖾𝗌↦[1,1,1,1,1,1],𝗆𝖺𝗉𝗌𝗎𝖼𝗇𝖺𝗍𝗌↦[1,2,3,4,5,6],𝗓𝗂𝗉𝖶𝗂𝗍𝗁(+)𝗇𝖺𝗍𝗌𝗇𝖺𝗍𝗌↦[0,2,4,6,8,10]. The program must also reject the term 𝖿𝗂𝗑𝑥.𝖼𝗈𝗇𝗌(𝗁𝖽𝑥)(𝗍𝗅𝑥), in which the recursion variable is used at type 𝖲𝗍𝗋ℕ rather than ▹𝖲𝗍𝗋ℕ, and must report the offending occurrence. Produce three mutations that still run — delete the stage shift in the clause for 𝗇𝖾𝗑𝗍, evaluate ⊛ at stage 𝑛 instead of 𝑛−1, and drop the restriction check — and confirm that each makes at least one named case fail. State explicitly that the program illustrates theorem 162.21 for finitely many programs and finitely many stages, and does not prove it.