Chapter 85Core route

Coinduction, Copatterns, and Bisimulation

A finite list can be inspected until a constructor closes it. A stream has no last constructor to reach. Its correctness question is instead finite: after any requested number of tail observations, can the next head be produced? A definition that answers every such request is productive: every finite sequence of tail observations can be followed by a head observation that returns an element.

Streams are given by observations

Fix $A : U_{i}$ . The signature $T_{co}$ extends $T_{0}$ by one coinductive record and a guarded corecursor.

Definition 85.1 — The guarded stream fragment ¶

A stream over $A$ is an element of $Stream (A)$ . It is observed by two destructors: $head$ returns the next element and $tail$ returns the stream after that element.

Γ ⊢ A : U_{i}

Γ ⊢ Stream (A) : U_{i}

Stream-form

Γ ⊢ s : Stream (A)

Γ ⊢ head (s) : A

Head

Γ ⊢ s : Stream (A)

Γ ⊢ tail (s) : Stream (A)

Tail

For a state type $S : U_{j}$ , an output $h : S \to A$ , a transition $t : S \to S$ , and an initial state $x : S$ , the guarded corecursor has type

Γ ⊢ S : U_{j}

Γ ⊢ h : S \to A

Γ ⊢ t : S \to S

Γ ⊢ x : S

Γ ⊢ {corec}_{A} (S, h, t, x) : Stream (A)

Stream-corec

with judgmental observation equations $\begin{aligned} (C o r e c - h e a d) & head ({corec}_{A} (S, h, t, x)) & \equiv h (x), \\ (C o r e c - t a i l) & tail ({corec}_{A} (S, h, t, x)) & \equiv {corec}_{A} (S, h, t, t (x)) . \end{aligned}$ The recursive stream occurs only on the right of a tail observation. This placement is the guarded-call invariant of this fragment.

Referenced from 3 locations

Coinduction, Copatterns, and Bisimulation

The rules do not add a constructor $A \to Stream (A) \to Stream (A)$ . Such a constructor would invite dependent pattern matching on coinductive data and a restricted unfolding rule for recursively defined coinductive values. The destructor presentation makes the two equations that compute into the primitive interface.

Definition 85.2 — Finite stream observations ¶

Define $nth : N \to Stream (A) \to A$ by structural recursion on its natural-number argument: $nth (0, s) : = head (s), nth (suc (n), s) : = nth (n, tail (s)) .$ The observation depth of $nth (n, s)$ is $n$ : it requests $n$ tails and then one head.

Referenced from 3 locations

Coinduction, Copatterns, and Bisimulation

Theorem 85.3 — Productivity of guarded corecursion ¶

For $S, h, t, x$ as in definition 85.1 and every $n : N$ , ${Id}_{A} (nth (n, {corec}_{A} (S, h, t, x)), h (t^{n} (x)))$ is inhabited, where $t^{0} (x) : = x$ and $t^{suc (n)} (x) : = t^{n} (t (x))$ . Hence every finite observation of a guarded corecursive stream is identified with an application of $h$ at a finite state iterate.

Referenced from 4 locations

Coinduction, Copatterns, and Bisimulation

Proof of Theorem 85.3 — Productivity of guarded corecursion

Proof. Induct on $n$ with the state $x : S$ quantified in the motive. At zero, the required identification is reflexivity after the judgmental calculation $nth (0, {corec}_{A} (S, h, t, x)) \overset{d e f i n i t i o n 85.2}{\equiv} head ({corec}_{A} (S, h, t, x)) \overset{(C o r e c - h e a d)}{\equiv} h (x) .$ For a successor, instantiate the induction hypothesis at $t (x)$ : $\begin{aligned} nth (suc (n), {corec}_{A} (S, h, t, x)) & \overset{d e f i n i t i o n 85.2}{\equiv} nth (n, tail ({corec}_{A} (S, h, t, x))) \\ \overset{(C o r e c - t a i l)}{\equiv} nth (n, {corec}_{A} (S, h, t, t (x))) \\ \overset{IH (t (x))}{=} h (t^{n} (t (x))) \\ \overset{i t e r a t e d e f i n i t i o n}{\equiv} h (t^{suc (n)} (x)) . \end{aligned}$ The middle relation is the identification obtained from the induction hypothesis. Each closed numeral instance is judgmental by repeated use of (Corec-tail) followed by (Corec-head); the theorem for a neutral $n$ is propositional because structural recursion on $n$ is stuck. ◻

Remark 85.4 — Guardedness is sufficient, not complete ¶

The equation $s = tail (s)$ is not an instance of Stream-corec: no output function produces a head before the recursive transition. More subtle productive programs may also fail to have the corecursor form when productivity depends on the behavior of a higher-order argument. Thus this fragment proves productivity for terms generated by its rule; it does not describe every productive stream program.

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

Stream programs are state machines

The corecursor first becomes concrete at small state types.

Construction 85.5 — Iteration and stream map ¶

For $x : A$ and $f : A \to A$ , define $iterate (f, x) : = {corec}_{A} (A, λ a . a, f, x) .$ Equations (Corec-head) and (Corec-tail) give $head (iterate (f, x)) \equiv x, tail (iterate (f, x)) \equiv iterate (f, f (x)) .$ For $g : A \to B$ and $s : Stream (A)$ , define $map (g, s) : = {corec}_{B} (Stream (A), λ u . g (head (u)), tail, s) .$ It computes by observation: $\begin{aligned} (M a p - h e a d) & head (map (g, s)) & \equiv g (head (s)), \\ (M a p - t a i l) & tail (map (g, s)) & \equiv map (g, tail (s)) . \end{aligned}$

Referenced from 3 locations

Coinduction, Copatterns, and Bisimulation

Construction 85.6 — Zip and Fibonacci states ¶

For $f : A \to B \to C$ , $s : Stream (A)$ , and $t : Stream (B)$ , use the state $Stream (A) \times Stream (B)$ to define $\begin{aligned} zipWith (f, s, t) : = {corec}_{C} ( & Stream (A) \times Stream (B), \\ λ (u, v) . f (head (u)) (head (v)), \\ λ (u, v) . (tail (u), tail (v)), (s, t)) . \end{aligned}$ Its two reusable computation equations are $\begin{aligned} (Z i p - h e a d) & head (zipWith (f, s, t)) & \equiv f (head (s)) (head (t)), \\ (Z i p - t a i l) & tail (zipWith (f, s, t)) & \equiv zipWith (f, tail (s), tail (t)) . \end{aligned}$

Define the Fibonacci stream by the state transition $(a, b) \mapsto (b, a + b)$ : $fibs : = {corec}_{N} (N \times N, λ (a, b) . a, λ (a, b) . (b, a + b), (0, 1)) .$ The first five observations are $\begin{aligned} nth (0, fibs) & \equiv 0, & nth (1, fibs) & \equiv 1, & nth (2, fibs) & \equiv 1, \\ nth (3, fibs) & \equiv 2, & nth (4, fibs) & \equiv 3. \end{aligned}$ Each equality is a judgmental closed calculation. Apply (Corec-tail) repeatedly to the numeral depth. Finish with (Corec-head).

Referenced from 3 locations

Coinduction, Copatterns, and Bisimulation

The propositional theorem theorem 85.3 packages the same calculation uniformly for a variable depth.

Lemma 85.7 — Successor iterate swap ¶

For $S : U_{j}$ , $t : S \to S$ , $x : S$ , and $n : N$ , ${Id}_{S} (t^{suc (n)} (x), t (t^{n} (x)))$ is inhabited.

Referenced from 3 locations

Coinduction, Copatterns, and Bisimulation

Proof of Lemma 85.7 — Successor iterate swap

Proof. Induct on $n$ while quantifying over $x$ . At zero both endpoints reduce to $t (x)$ . At $suc (n)$ , the iterate definition and the induction hypothesis at $t (x)$ give $t^{suc (suc (n))} (x) \equiv t^{suc (n)} (t (x)) \overset{IH (t (x))}{=} t (t^{n} (t (x))) \equiv t (t^{suc (n)} (x)) .$ ◻

Proposition 85.8 — Fibonacci recurrence ¶

For every $n : N$ , the following identity type is inhabited: ${Id}_{N} (nth (n + 2, fibs), nth (n, fibs) + nth (n + 1, fibs)) .$

Referenced from 3 locations

Coinduction, Copatterns, and Bisimulation

Proof of Proposition 85.8 — Fibonacci recurrence

Proof. Let $(a_{n}, b_{n})$ be the $n$ th iterate of $(a, b) \mapsto (b, a + b)$ at $(0, 1)$ . By theorem 85.3, $nth (n, fibs) = a_{n}$ . By lemma 85.7, applying the transition to $(a_{n}, b_{n})$ gives $a_{n + 1} = b_{n}$ . The same facts give $a_{n + 2} \overset{l e m m a 85.7}{=} b_{n + 1} \overset{t r a n s i t i o n e q u a t i o n}{=} a_{n} + b_{n} \overset{a_{n + 1} = b_{n}}{=} a_{n} + a_{n + 1} .$ Substitution of the three observation equations yields the result. This argument holds for arbitrary $n$ ; it is not an extrapolation from the five closed observations above. ◻

Exercise 85.1 ¶

★☆☆ Use Boolean state and negation to define the alternating stream $tt, ff, tt, \dots$ . Calculate observations at depths zero through four and identify the state iterate used by each calculation.

Referenced from 3 locations

Copatterns compile observations

A pattern describes how an input was constructed. A copattern describes how a result will be observed. For streams, the primitive copatterns are $head (◻)$ and $tail (◻)$ , where $◻$ marks the defined result.

Definition 85.9 — Guarded stream copattern definition ¶

A unary stream definition by copatterns has the form $head (F (x)) = h (x), tail (F (x)) = F (t (x)),$ where $x : S$ , $h : S \to A$ , and $t : S \to S$ . It is complete because it gives one clause for each stream destructor. Its compilation is $F (x) : = {corec}_{A} (S, h, t, x) .$ The two source clauses become the two judgmental equations (Corec-head) and (Corec-tail). A unary clause system is accepted by the guarded copattern fragment if and only if it contains both displayed clauses for some $S, h, t$ and compiles to this corecursor term. Thus “accepted” names this syntactic class rather than an unstated checking judgment.

Referenced from 4 locations

For example, the two equations for $map$ in construction 85.5 are a copattern definition. Compilation chooses the input stream itself as state. The right side of the tail clause is a guarded recursive call because a tail observation has been matched before the call is demanded.

Exercise 85.2 ¶

★★☆ Give copattern clauses for $zipWith (f, s, t)$ and compile them to the corecursor using the pair state from construction 85.6. Derive both clauses from the compiled term. Then delete the tail clause and state exactly which observation is uncovered.

Referenced from 3 locations

Bisimulation proves equality of observations

Ordinary induction on a stream cannot begin because there is no stream constructor on which to split. A first attempt can instead induct on finite observation depth. Fix $s : Stream (A)$ and try to prove $\begin{matrix} (F a i l e d - d e p t h - i n d u c t i o n) & P (n) : = {Id}_{A} (nth (n, map (λ x . x, s)), nth (n, s)) . \end{matrix}$ The zero case reduces to reflexivity. In the successor case, the two tail equations reduce the goal to ${Id}_{A} (nth (n, map (λ x . x, tail (s))), nth (n, tail (s))) .$ This is not $P (n)$ : the fixed stream $s$ has changed to $tail (s)$ . One repair quantifies over every stream. The reusable repair records instead a relation whose evidence gives equal heads and another piece of evidence after taking tails. Those two obligations determine bisimulation.

Definition 85.10 — Observational stream equality ¶

Streams $s, t : Stream (A)$ are observationally equal, written $s \approx_{A} t$ , when $s \approx_{A} t : = \prod_{n : N} {Id}_{A} (nth (n, s), nth (n, t)) .$ This is an internal family of identifications. It does not add a judgmental equation $s \equiv t$ and therefore does not make a stuck destructor compute.

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

A nested copattern, also called a deep copattern, places a finite composite of destructors around the defined result. The customary deep-copattern presentation of Fibonacci consists of $\begin{aligned} head (fibs) & = 0, \\ head (tail (fibs)) & = 1, \\ tail (tail (fibs)) \approx_{N} zipWith (+, fibs, tail (fibs)) . \end{aligned}$ The first two clauses are judgmental closed instances of the state-machine equations. The third is only observational; it is proved in corollary 85.17 and is not a primitive unfolding equation. Deep copattern notation therefore does not enlarge definitional equality.

Remark 85.11 — No stream uniqueness rule ¶

The signature $T_{co}$ has no uniqueness or eta rule saying that a stream is equal to the corecursor determined by its observations. In this fragment, a proof of $s \approx_{A} t$ therefore does not yield an inhabitant of ${Id}_{Stream (A)} (s, t)$ . A stream-extensionality principle can close that gap. An observational type theory extended with a stream clause defined by all finite head-and-tail observations can also close it. Neither extension is a rule of $T_{co}$ .

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

Definition 85.12 — Stream bisimulation ¶

A relation $B : Stream (A) \to Stream (A) \to U_{k}$ is a stream bisimulation when it is equipped with functions $\begin{aligned} {bisimHead}_{B} & : \prod_{s : Stream (A)} \prod_{t : Stream (A)} B (s, t) \to {Id}_{A} (head (s), head (t)), \\ {bisimTail}_{B} & : \prod_{s : Stream (A)} \prod_{t : Stream (A)} B (s, t) \to B (tail (s), tail (t)) . \end{aligned}$ The first component matches the immediate observations. The second returns the same relation after one tail observation.

Referenced from 5 locations

Theorem 85.13 — Stream coinduction ¶

Let $B$ be a stream bisimulation. For all $s, t : Stream (A)$ and $q : B (s, t)$ , $s \approx_{A} t$ .

Referenced from 4 locations

Coinduction, Copatterns, and Bisimulation

Proof of Theorem 85.13 — Stream coinduction

Proof. We must construct an identification at every depth $n$ . Induct on $n$ while quantifying over $s, t$ , and $q : B (s, t)$ . At zero, $nth (0, s) \equiv head (s) and nth (0, t) \equiv head (t),$ so ${bisimHead}_{B} (s, t, q)$ has the required type. At $suc (n)$ , the tail component gives $q^{'} : = {bisimTail}_{B} (s, t, q) : B (tail (s), tail (t))$ . The induction hypothesis at $q^{'}$ gives $nth (n, tail (s)) =_{A} nth (n, tail (t)),$ which converts along the two successor equations of definition 85.2 to the required identification at depth $suc (n)$ . ◻

Remark 85.14 — Why the bisimulation hypotheses are exact ¶

Deleting the head clause allows a relation between streams with different first elements. Deleting closure under tail allows a relation that matches only the first element. Each deletion therefore invalidates the corresponding case of the proof of theorem 85.13.

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

Exercise 85.3 ¶

★☆☆ Let $s, t : Stream (A)$ and let $B (s, t)$ mean only that $head (s) = head (t)$ . Give two streams related by $B$ whose depth-one observations differ. Identify the missing premise of definition 85.12.

Referenced from 3 locations

Theorem 85.15 — Map fusion ¶

For $g : A \to B$ , $f : B \to C$ , and $s : Stream (A)$ , $map (f, map (g, s)) \approx_{C} map (λ x . f (g (x)), s) .$

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

Proof of Theorem 85.15 — Map fusion

Proof. Define the relation by the dependent sum $\begin{aligned} L (r) & : = map (f, map (g, r)), \\ R (r) & : = map (λ x . f (g (x)), r), \\ B (u, v) & : = \sum_{r : Stream (A)} ({Id}_{Stream (C)} (u, L (r)) \times {Id}_{Stream (C)} (v, R (r))) . \end{aligned}$ The original pair belongs to $B$ with witness $s$ . For a pair witnessed by $r$ , eliminate the two displayed identities. It remains to treat the canonical representatives $u \equiv map (f, map (g, r))$ and $v \equiv map (λ x . f (g (x)), r)$ . Their heads calculate as $\begin{aligned} head (u) & \overset{(M a p - h e a d)}{\equiv} f (head (map (g, r))) \\ \overset{(M a p - h e a d)}{\equiv} f (g (head (r))) \\ \overset{(M a p - h e a d)}{\equiv} head (v) . \end{aligned}$ Their tails satisfy $\begin{aligned} tail (u) & \overset{(M a p - t a i l)}{\equiv} map (f, map (g, tail (r))), \\ tail (v) & \overset{(M a p - t a i l)}{\equiv} map (λ x . f (g (x)), tail (r)) . \end{aligned}$ Thus the tail pair belongs to $B$ with witness $tail (r)$ and two reflexivity identifications after the displayed computations. Transporting back along the eliminated identities gives the required head and tail data for the original $u, v$ . The relation is a bisimulation, and theorem 85.13 gives the result. ◻

Exercise 85.4 ¶

★★☆ Let $s, t : Stream (A)$ . Assume $f : A \to A \to A$ and $c : \prod_{x : A} \prod_{y : A} {Id}_{A} (f (x) (y), f (y) (x)) .$ Put $u : = zipWith (f, s, t), v : = zipWith (f, t, s) .$ Construct a bisimulation proving $u \approx_{A} v$ . State the tail witness and use $c$ only in the head component.

Referenced from 3 locations

Lemma 85.16 — Zip observations ¶

For $f : A \to B \to C$ , $s : Stream (A)$ , $t : Stream (B)$ , and $n : N$ , the identity type ${Id}_{C} (nth (n, zipWith (f, s, t)), f (nth (n, s)) (nth (n, t)))$ is inhabited.

Referenced from 3 locations

Coinduction, Copatterns, and Bisimulation

Proof of Lemma 85.16 — Zip observations

Proof. Induct on $n$ while quantifying over $s$ and $t$ . At zero, $\begin{aligned} nth (0, zipWith (f, s, t)) & \overset{d e f i n i t i o n 85.2}{\equiv} head (zipWith (f, s, t)) \\ \overset{(Z i p - h e a d)}{\equiv} f (head (s)) (head (t)) \\ \overset{d e f i n i t i o n 85.2}{\equiv} f (nth (0, s)) (nth (0, t)) . \end{aligned}$ At $suc (n)$ , the calculation is $\begin{aligned} nth (suc (n), zipWith (f, s, t)) & \overset{d e f i n i t i o n 85.2}{\equiv} nth (n, tail (zipWith (f, s, t))) \\ \overset{(Z i p - t a i l)}{\equiv} nth (n, zipWith (f, tail (s), tail (t))) \\ \overset{IH (tail (s), tail (t))}{=} f (nth (n, tail (s))) (nth (n, tail (t))) \\ \overset{d e f i n i t i o n 85.2}{\equiv} f (nth (suc (n), s)) (nth (suc (n), t)) . \end{aligned}$ ◻

Corollary 85.17 — The feedback equation for Fibonacci ¶

The Fibonacci stream satisfies $tail (tail (fibs)) \approx_{N} zipWith (+, fibs, tail (fibs)) .$

Referenced from 3 locations

Coinduction, Copatterns, and Bisimulation

Proof of Corollary 85.17 — The feedback equation for Fibonacci

Proof. By lemma 85.16, specializing to addition, $fibs$ , and $tail (fibs)$ identifies the right observation at depth $n$ with $nth (n, fibs) + nth (n + 1, fibs)$ . The left observation is $nth (n + 2, fibs)$ , and proposition 85.8 gives the final identity for every neutral $n$ . ◻

The selected coinductive-record schema

Streams have one observable field and one successor field. The same proof works for finitely many fields.

Definition 85.18 — The T_ co record schema ¶

Fix observation types $O_{1}, \dots, O_{m}$ . Fix also $r$ recursive successor fields. The schema generates a coinductive record $C$ with destructors $\begin{aligned} o_{i} & : C \to O_{i} & (1 \leq i \leq m), \\ d_{j} & : C \to C & (1 \leq j \leq r) . \end{aligned}$ Given a state $S$ , outputs $h_{i} : S \to O_{i}$ , transitions $t_{j} : S \to S$ , and $x : S$ , its corecursor satisfies $\begin{aligned} o_{i} ({corec}_{C} (S, \bar{h}, \bar{t}, x)) & \equiv h_{i} (x), \\ d_{j} ({corec}_{C} (S, \bar{h}, \bar{t}, x)) & \equiv {corec}_{C} (S, \bar{h}, \bar{t}, t_{j} (x)) . \end{aligned}$ Every recursive occurrence is the complete result of a recursive destructor. Dependent observation types, nested recursive fields, mixed inductive–coinductive declarations, and higher-order guards are not in this schema.

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

Theorem 85.19 — Finite-observation productivity for the schema ¶

For $k : N$ , indices $1 \leq j_{1}, \dots, j_{k} \leq r$ , and $1 \leq i \leq m$ , abbreviate $c_{x} : = {corec}_{C} (S, \bar{h}, \bar{t}, x)$ . Then $\begin{aligned} o_{i} (d_{j_{k}} (\dots d_{j_{1}} (c_{x}) \dots)) \\ \equiv h_{i} (t_{j_{k}} (\dots t_{j_{1}} (x) \dots)) . \end{aligned}$ For $k \equiv 0$ , both finite composites are empty and the equation reads $o_{i} (c_{x}) \equiv h_{i} (x) .$

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

Proof of Theorem 85.19 — Finite-observation productivity for the schema

Proof. Induct on $k$ . The empty word reduces by the $o_{i}$ equation. In a nonempty word, the destructor adjacent to the corecursor is $d_{j_{1}}$ ; its equation replaces the state $x$ by $t_{j_{1}} (x)$ . Apply the induction hypothesis to the remaining word $j_{2}, \dots, j_{k}$ at that state. A finite index list is empty or has this first entry, so these are all cases. ◻

Remark 85.20 — Structural coinduction is a separate calculus ¶

Downen and Ariola’s contextual signature has terms $v$ , coterms $e$ , values $V$ , covalues $E$ , commands $⟨ v ∣ e ⟩$ , types generated in part by $N$ , $Stream (A)$ , and $A \to B$ , and three equality judgments under $Γ ∣ Δ$ : command equality, value equality $v = v^{'} : A$ , and consumer equality $e = e^{'} \div A$ . Here $e \div A$ means that the coterm $e$ consumes a value of type $A$ . Its cut congruence is the named rule

Γ ∣ Δ ⊢ v = v^{'} : A

Γ ∣ Δ ⊢ e = e^{'} \div A

Γ ∣ Δ ⊢ ⟨ v ∣ e ⟩ = ⟨ v^{'} ∣ e^{'} ⟩

Cut

A productive command property $Ψ (α)$ has base form $⟨ V ∣ α ⟩ = ⟨ V^{'} ∣ α ⟩$ , with $α$ absent from $V, V^{'}$ , and is closed under the stream rule

Γ, β \div A ∣ Δ ⊢ Ψ [head β / α]

Γ, α \div Stream (A) ∣ Δ, Ψ (α) ⊢ Ψ [tail α / α]

Γ, α \div Stream (A) ∣ Δ ⊢ Ψ (α)

ωStream

For a concrete instance, let $u_{0}, u_{1} : Stream (N)$ have the contextual equations $head (u_{i}) = 0, tail (u_{i}) = u_{i} (i \in {0, 1}),$ and put $Ψ (α) : = ⟨ u_{0} ∣ α ⟩ = ⟨ u_{1} ∣ α ⟩$ . The head premise of $ω Stream$ contracts to $⟨ 0 ∣ β ⟩ = ⟨ 0 ∣ β ⟩$ . The tail premise contracts back to $Ψ (α)$ and is discharged by the displayed hypothesis in that premise. Thus the rule derives $Ψ (α)$ from one immediate value equality and one guarded reuse.

The head premise of $ω Stream$ performs the same role as ${bisimHead}_{B}$ , and its tail premise performs the same role as ${bisimTail}_{B}$ . The contextual rule phrases those obligations as command equality under a reusable hypothesis; definition 85.12 phrases them as destructor observations of a relation witness. Their Theorem 5.21 proves semantic soundness of the extensional logic for both call-by-value and call-by-name. Theorem 5.23 concludes, separately, that derivable command, value, and covalue equalities imply their corresponding observational equivalences. The stronger strategy-specific logics use the separate soundness statement of Theorem 5.28. None of these results proves a guarded-corecursor or copattern-coverage theorem for $T_{co}$ .

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

Bounded sized approximants

Fix $Size : U_{i}$ and a relation $<_{s}$ . The optional signature $T_{size}$ describes observations bounded by a supplied descending size chain. Its rules do not postulate a distinguished size with arbitrarily many available tails, so they describe sized approximants rather than asserting an infinite-stream object.

Definition 85.21 — Sized approximant formation and observations ¶

For $A : U_{j}$ and $α : Size$ ,

Γ ⊢ A : U_{j}

Γ ⊢ α : Size

Γ ⊢ {Stream}^{α} (A) : U_{j}

Sized-Stream-form

Γ ⊢ s : {Stream}^{α} (A)

Γ ⊢ {head}^{α} (s) : A

Sized-head

Γ ⊢ r : β <_{s} α

Γ ⊢ s : {Stream}^{α} (A)

Γ ⊢ {tail}^{α, β} (r, s) : {Stream}^{β} (A)

Sized-tail

Observation equality is judgmental in $T_{size}$ ; no coercion or equality between approximants at different sizes is silently inserted.

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

Definition 85.22 — Sized approximant builder ¶

Let $S : Size \to U_{k}$ . Given $h : \prod_{α : Size} S (α) \to A, t : \prod_{α : Size} \prod_{β : Size} β <_{s} α \to S (α) \to S (β),$ the corecursor rule is

Γ ⊢ x : S (α)

Γ ⊢ {corec}_{A}^{α} (S, h, t, x) : {Stream}^{α} (A)

Sized-corec

It is governed by $\begin{aligned} (S i z e d - c o r e c - h e a d) & {head}^{α} ({corec}_{A}^{α} (S, h, t, x)) & \equiv h (α, x), \\ (S i z e d - c o r e c - t a i l) & {tail}^{α, β} (r, {corec}_{A}^{α} (S, h, t, x)) & \equiv {corec}_{A}^{β} (S, h, t, t (α, β, r, x)) . \end{aligned}$ The only recursively produced approximant in the second equation is indexed by $r : β <_{s} α$ , which is its decrease certificate. Deleting $r$ would define a different, unsupported signature, while adding a distinguished infinity size or size-weakening operation would require additional rules not present here.

Referenced from 3 locations

Construction 85.23 — Map on sized approximants ¶

For $f : A \to B$ and $s : {Stream}^{α} (A)$ , take $S (γ) : = {Stream}^{γ} (A)$ , $h (γ, u) : = f ({head}^{γ} (u))$ , and $t (γ, δ, r, u) : = {tail}^{γ, δ} (r, u)$ . Then ${map}^{α} (f, s) : = {corec}_{B}^{α} (S, h, t, s) : {Stream}^{α} (B) .$ The two corecursor equations calculate to $\begin{aligned} {head}^{α} ({map}^{α} (f, s)) & \equiv f ({head}^{α} (s)), \\ {tail}^{α, β} (r, {map}^{α} (f, s)) & \equiv {map}^{β} (f, {tail}^{α, β} (r, s)) . \end{aligned}$ Thus map is constructed from the displayed corecursor rather than postulated as a second recursive operation.

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

Theorem 85.24 — Bounded observation calculation ¶

Let $α_{n} <_{s} \dots <_{s} α_{1} <_{s} α_{0}$ be witnessed by $r_{q} : α_{q + 1} <_{s} α_{q}$ . Starting at $x_{0} : S (α_{0})$ , define $x_{q + 1} : = t (α_{q}, α_{q + 1}, r_{q}, x_{q})$ . Applying the corresponding $n$ tails and then ${head}^{α_{n}}$ to ${corec}_{A}^{α_{0}} (S, h, t, x_{0})$ reduces judgmentally to $h (α_{n}, x_{n})$ .

Referenced from 2 locations

Coinduction, Copatterns, and Bisimulation

Proof of Theorem 85.24 — Bounded observation calculation

Proof. Induct on the length of the displayed chain. At zero, the calculation is ${head}^{α_{0}} ({corec}_{A}^{α_{0}} (S, h, t, x_{0})) \overset{(S i z e d - c o r e c - h e a d)}{\equiv} h (α_{0}, x_{0}) .$ A successor chain first uses (Sized-corec-tail). The resulting term is ${corec}_{A}^{α_{1}} (S, h, t, x_{1}) .$ The induction hypothesis applies to its shorter tail. The calculation covers exactly the observations backed by the displayed finite chain. If $<_{s}$ is well founded, accessibility rules out any one infinite sequence of successive tail observations. It does not impose a uniform finite bound on the depths reachable from a fixed size: at an $ω$ -like size, every finite depth may be reachable along its own finite chain. No infinite-stream productivity conclusion follows from the bounded calculation alone. ◻

For finite sizes $\hat{0} <_{s} \hat{1} <_{s} \hat{2} <_{s} \hat{3}$ , let $S (γ) : = N$ , $h (γ, x) : = x$ , and $t (γ, δ, r, x) : = x + x$ . Construct $s : = {corec}_{N}^{\hat{3}} (S, h, t, 2) : {Stream}^{\hat{3}} (N) .$ Its successive heads along the displayed descent are $2, 4, 8, 16$ . At the first depth, the map calculation is $\begin{aligned} {head}^{\hat{3}} ({map}^{\hat{3}} (suc, s)) & \overset{c o n s t r u c t i o n 85.23}{\equiv} suc ({head}^{\hat{3}} (s)) \\ \overset{(S i z e d - c o r e c - h e a d)}{\equiv} suc (2) \overset{natural-number computation}{\equiv} 3. \end{aligned}$ One, two, and three applications of (Sized-corec-tail) give the corresponding mapped heads $5$ , $9$ , and $17$ . This is a mathematical sized approximant calculation, not an infinite stream and not a theorem about every implementation named “sized types.”

Abel and Pientka’s calculus combines size quantification, variance, copatterns, and a reducibility interpretation at its published signature; the bounded fragment above deliberately includes neither its infinity size nor its size-weakening structure. Experimental Agda sized-type features have also admitted consistency bugs; no implementation theorem is inferred from the mathematical display above.

Suggested first pass.

None of these problems is a prerequisite. Begin with exercise 85.5, then complete exercise 85.8.

Exercise 85.5 ¶

★★☆ Let $s : Stream (A)$ . Define a bisimulation and prove $map (λ x . x, s) \approx_{A} s$ . Write the head calculation and the exact witness relating the tails.

Referenced from 4 locations

Exercise 85.6 ¶

★★★ Specify a stream of triangular numbers first by a pair-state corecursor and then by complete head/tail copattern clauses. Compile the clauses, calculate the first six observations, and prove that the two definitions are observationally equal.

Referenced from 3 locations

Exercise 85.7 ¶

★★☆ Use the accepted clause system $head (zeros) \equiv 0$ and $tail (zeros) \equiv zeros$ . Let $nats : = iterate (suc, 0)$ , so that $head (nats) \equiv 0$ . First prove by induction that $nth (n, map (g, s))$ is identified with $g (nth (n, s))$ . Use that lemma to prove $tail (nats) \approx_{N} map (suc, nats) and {Id}_{N} (nth (n, nats), n) .$ Explain why replacing the observational equality by $\equiv$ would not give the unary state-update clause required by definition 85.9; do not claim that the guarded fragment is complete.

Referenced from 3 locations

Exercise 85.8 ¶

★★★ Practical project.guarded-stream-observer Implement in Kappa the state-machine corecursor through a finite observer rather than by constructing an infinite host value. Maintain the invariant that a request of depth $n$ performs exactly $n$ state transitions before applying the output function. On the Fibonacci state machine, print the observations at depths $0$ through $9$ ; the exact output must be 0,1,1,2,3,5,8,13,21,34. A mutated transition $(a, b) \mapsto (a, a + b)$ must fail the acceptance test by printing 0,0 in the first two positions. Report both traces.

Referenced from 5 locations

Sources. The destructor and copattern presentation follows Abel, Pientka, Thibodeau, and Setzer, especially its stream and Fibonacci examples [APTS13]. The sized boundary follows Abel and Pientka’s journal development [AP16]. The contextual comparison is restricted to the exact soundness results of Downen and Ariola [DA25].