Instantly share code, notes, and snippets.

# jcreedcmu/fixpoint.txt

Last active March 19, 2024 21:28
Show Gist options
• Save jcreedcmu/f193d0f8718d5920ef3f1a1623627e3d to your computer and use it in GitHub Desktop.
lil fixpoint lemma
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 Suppose ℂ is a ω-cocomplete category: it has colimits of any diagram that is a functor ω → ℂ. Suppose ℂ has an initial object ⊥. Suppose F is a functor ℂ → ℂ that preserves all ω-colimits. Let U : ω → ℂ be the diagram ! F! F² ⊥ → F(⊥) → F²(⊥) → ⋯ Lemma: If we have a map m : FA → A, then we can construct a map colim U → A. Proof: By the UMP of the colimit, it suffices to find fₙ that make ⊥ → F(⊥) → F²(⊥) → ⋯ f₀↓ f₁↓ f₂↓ A === A ===== A ===== ⋯ commute. Check that the inductive definition f₀ = ! fₙ₊₁ = m ∘ F(fₙ) works. ∎ (iirc this ought to be first bit of demonstrating that colim U is the carrier of the initial F-algebra) Corollary: Suppose we have a functor S : ω → ℂ and a map ϕ : colim (F ∘ S) → (colim S). Then there exists a map (colim U) → (colim S) Proof: Since F preserve colimits, we can transform ϕ into a map F(colim S) → (colim S) Apply lemma with A := colim S. Bringing this down to earth: Claim: If fₙ : P → P are monotone ω-continuous maps from an ω-CPO to itself, and aᵢ is a fair scheduling of the naturals, then supₜ (⋃ₙ fₙ)ᵗ (⊥) ≤ supₜ (f_{aₜ} ∘ ⋯ f_{a₀}) (⊥) Proof: Let ℂ be P. Let F be ⋃ₙ fₙ. Let S(t) = (f_{aₜ} ∘ ⋯ f_{a₀}) (⊥) Then the thing we're trying to do is obtain a morphism (colim U) → (colim S). U is "running all the rules concurrently, repeatedly" S is "running all the rules chaotically, but fairly" F preserves ω-colimits because fₙ are ω-continuous. The remaining proof obligation is ϕ. We must show colim (F ∘ S) → (colim S) so it suffices to use the UMP of the colimit on the left and show ∀n. F(S(n)) ≤ supₜ (f_{aₜ} ∘ ⋯ f_{a₀}) (⊥) i.e. ∀s. F((f_{aₛ} ∘ ⋯ f_{a₀})(t)) ≤ supₜ (f_{aₜ} ∘ ⋯ f_{a₀}) (⊥) i.e. all we need is ∀s,n. fₙ((f_{aₛ} ∘ ⋯ f_{a₀})(t)) ≤ supₜ (f_{aₜ} ∘ ⋯ f_{a₀}) (⊥) But this is just seeing that, if we're at stage s, and we hit our result with fₙ, there is *some* future stage t that exceeds fₙ applied to step s. This follows from fairness. ∎