Martin Escardo, Tom de Jong, 16 & 22 Feb 2023 In this module Various.Pataraia-Taylor we implement a predicative version of Pataraia's fixed point theorem: Every monotone endomap of a dcpo (directed complete poset) with a least element has a least fixed point. The original impredicative version is implemented in the module Various.Pataraia. Pataraia [1] was the first to give a constructive proof of this in topos logic. A version of his proof is published in [2] by Escardo, with Pataraia's permission. Pataraia himself didn't publish the result. An earlier, less general, theorem was proved by Coquand [6] for *bounded complete* dcpos, with an easier proof. See the module Various.Pataraia for an implementation of the impredicative proof given [2]. Pataraia's proof has two steps, the first of which is directly predicative and coded in the module lemma₂·₁ in the file Various.Pataraia. The second step (theorem-₂·₂ in the file Various.Pataraia) is impredicative, because it considers the intersection of all subsets of the dcpo that contain the least element, are closed under the monotone map, and are closed under directed suprema. This is impredicative in the sense that it requires propositional resizing axioms so that we can form this intersection. We instead consider a direct, explicit, elegant, predicative construction of this subset, due to Paul Taylor [3], in our alternative second step here, coded in the module `Taylor` below. This version of the theorem probably deserves to be called the Pataraia-Taylor fixed-point theorem, not only because the proof involves a new ingredient, but also because it holds in a more general predicative setting (here MLTT with function extensionality and existence of propositional truncations). There is a catch, though. In a predicative setting, there is no non-trivial dcpo to apply the theorem [4]. More precisely, dcpos are parametrized by three universes (𝓤,𝓥,𝓦) where the carrier lives in 𝓤, the truth values of the order relation live in 𝓥, and the index types for directed families live in 𝓦. In practice, for instance for the Scott model of PCF, or Scott's D∞-model of the untyped lambda-calculus, the parameter is of the form (𝓤⁺,𝓤,𝓤), and we refer to such dcpos as "large, locally small, small directed-complete", and if the parameter is (𝓤,𝓤,𝓤), we could refer to the dcpo as "small and small directed-complete". The Pataraia-Taylor fixed point theorem presented here applies to small, small directed-complete dcpos, and the trouble is that there are no non-trivial examples of such dcpos in our predicative world [4]. The only way to produce nontrivial such dcpos to apply the theorem is to assume propositional resizing axioms (which e.g. the UniMath project [5] does). [1] Dito Pataraia. A constructive proof of Tarski’s fixed-point theorem for dcpo’s. Presented at the 65th Peripatetic Seminar on Sheaves and Logic, Aarhus, Denmark, November 1997. [2] Martin Escardo. Joins in the frame of nuclei. Applied Categorical Structures 11: 117–124, 2003. https://doi.org/10.1023/A:1023555514029 [3] Paul Taylor. Two recent talks at Birmingham. Slides and papers available at https://paultaylor.eu/ordinals/ https://web.archive.org/web/20240222103315/https://paultaylor.eu/ordinals/ (22 Feb 2024 snapshot) [4] Tom de Jong. Domain theory in constructive and predicative univalent foundations. PhD thesis at the University of Birmingham, UK, 2023. https://arxiv.org/abs/2301.12405 [5] Vladimir Voevodky, Benedikt Ahrens, Dan Grayson and others. Unimath --- a computer-checked library of univalent mathematics. https://unimath.github.io/UniMath/ https://doi.org/10.5281/zenodo.8427604 [6] Thierry Coquand. A topos theoretic fix point theorem. Unpublished manuscript, June 1995. https://web.archive.org/web/20110822085930/https://www.cse.chalmers.se/~coquand/fix.pdf \begin{code} {-# OPTIONS --safe --without-K #-} open import MLTT.Spartan open import UF.FunExt open import UF.PropTrunc \end{code} We assume that propositional truncations exist, that function extensionality holds, and work in a fixed universe 𝓤. \begin{code} module Various.Pataraia-Taylor (pt : propositional-truncations-exist) (fe : Fun-Ext) (𝓤 : Universe) where open PropositionalTruncation pt open import DomainTheory.Basics.Dcpo pt fe 𝓤 open import DomainTheory.Basics.Miscelanea pt fe 𝓤 open import UF.Sets open import UF.Sets-Properties open import UF.Subsingletons open import UF.Subsingletons-FunExt open import Various.Pataraia pt fe 𝓤 \end{code} We prove the following theorem, which says that every monotone endomap of a dcpo with a least element has a least fixed point. As discussed above, dcpos require three universes to be fully specified. For the formulation of the theorem, we need the three universes to be the same, namely 𝓤. (Notice that we mention 𝓤 only twice in the statement of the theorem. This is because when we opened the domain theory modules above, we already passed the universe 𝓤 once as a parameter.) \begin{code} Theorem : (𝓓 : DCPO {𝓤} {𝓤}) → has-bottom 𝓓 → (f : ⟨ 𝓓 ⟩ → ⟨ 𝓓 ⟩) → is-monotone 𝓓 𝓓 f → Σ x ꞉ ⟨ 𝓓 ⟩ , (f x ＝ x) × ((y : ⟨ 𝓓 ⟩) → f y ＝ y → x ⊑⟨ 𝓓 ⟩ y) \end{code} Before proving this theorem, we first need to prove a number of lemmas, in two modules, lemma₂·₁ in Various.Pataraia, and `taylor` here. The second part of Pataraia's proof (theorem₂·₂ of the module Various.Pataraia) considers the intersection of all subsets of 𝓓 that have ⊥ as a member, are closed under f, and are closed under directed suprema. This is impredicative in the sense that it requires propositional resizing axioms to compute the intersection. We instead consider the subset of 𝓓 consisting of the elements that satisfy Taylor's condition (TC) below, which is defined predicatively. \begin{code} module Taylor (𝓓 : DCPO {𝓤} {𝓤}) ((⊥ , ⊥-is-least) : has-bottom 𝓓) (f : ⟨ 𝓓 ⟩ → ⟨ 𝓓 ⟩) (fm : is-monotone 𝓓 𝓓 f) where private D = ⟨ 𝓓 ⟩ _⊑_ = underlying-order 𝓓 TC : D → 𝓤 ̇ TC x = (x ⊑ f x) × ((u : D) → f u ⊑ u → x ⊑ u) TC₁ : (x : D) → TC x → x ⊑ f x TC₁ x = pr₁ TC₂ : (x : D) → TC x → (u : D) → f u ⊑ u → x ⊑ u TC₂ x = pr₂ TC-is-prop-valued : (x : D) → is-prop (TC x) TC-is-prop-valued x = ×-is-prop (prop-valuedness 𝓓 _ _) (Π₂-is-prop fe λ _ _ → prop-valuedness 𝓓 _ _) TC-is-closed-under-directed-sups : is-closed-under-directed-sups 𝓓 TC TC-is-closed-under-directed-sups {A} α δ TC-preservation = c₁ , c₂ where TC-preservation₁ : (a : A) → α a ⊑ f (α a) TC-preservation₁ a = TC₁ (α a) (TC-preservation a) TC-preservation₂ : (a : A) (u : D) → f u ⊑ u → α a ⊑ u TC-preservation₂ a = TC₂ (α a) (TC-preservation a) I : (a : A) → α a ⊑ f (∐ 𝓓 δ) I a = α a ⊑⟨ 𝓓 ⟩[ TC-preservation₁ a ] f (α a) ⊑⟨ 𝓓 ⟩[ fm (α a) (∐ 𝓓 δ) (∐-is-upperbound 𝓓 δ a) ] f (∐ 𝓓 δ) ∎⟨ 𝓓 ⟩ c₁ : ∐ 𝓓 δ ⊑ f (∐ 𝓓 δ) c₁ = ∐-is-lowerbound-of-upperbounds 𝓓 δ (f (∐ 𝓓 δ)) I c₂ : (u : D) → f u ⊑ u → ∐ 𝓓 δ ⊑ u c₂ u l = ∐-is-lowerbound-of-upperbounds 𝓓 δ u II where II : (a : A) → α a ⊑ u II a = TC-preservation₂ a u l TC-holds-at-⊥ : TC ⊥ TC-holds-at-⊥ = ⊥-is-least (f ⊥) , (λ (u : D) _ → ⊥-is-least u) \end{code} Now the rest of Taylor is essentially the original one by Pataraia. We apply lemma₂·₁ of the module Various.Pataraia to the subdcpo 𝓔 of 𝓓 consisting of the elements that satisfy Taylor's condition. \begin{code} 𝓔 : DCPO 𝓔 = subdcpo 𝓓 TC TC-is-prop-valued TC-is-closed-under-directed-sups private E = ⟨ 𝓔 ⟩ _≤_ : E → E → 𝓤 ̇ s ≤ t = s ⊑⟨ 𝓔 ⟩ t NB-E : E ＝ (Σ x ꞉ D , TC x) NB-E = by-definition NB-≤ : (x x' : D) (c : TC x) (c' : TC x') → ((x , c) ≤ (x' , c')) ＝ (x ⊑ x') NB-≤ x x' c c' = by-definition ι : E → D ι (x , c) = x τ : (t : E) → TC (ι t) τ (x , c) = c ⊥𝓔 : E ⊥𝓔 = ⊥ , TC-holds-at-⊥ \end{code} The monotone function f : D → D restricts to a monotone inflationary function 𝓯 : E → E. \begin{code} 𝓯 : E → E 𝓯 (x , c₁ , c₂) = f x , fm x (f x) c₁ , (λ u (l : f u ⊑ u) → f x ⊑⟨ 𝓓 ⟩[ fm x u (c₂ u l) ] f u ⊑⟨ 𝓓 ⟩[ l ] u ∎⟨ 𝓓 ⟩) 𝓯-is-monotone : (s t : E) → s ≤ t → 𝓯 s ≤ 𝓯 t 𝓯-is-monotone (x , _) (y , _) = fm x y 𝓯-is-inflationary : (t : E) → t ≤ 𝓯 t 𝓯-is-inflationary (x , c₁ , c₂) = c₁ TC-𝓯 : (s : E) → TC (f (ι s)) TC-𝓯 s = pr₂ (𝓯 s) \end{code} So now we can apply lemma₂·₁ proved in Various.Pataraia. \begin{code} open lemma₂·₁ 𝓔 𝕗 : MI 𝕗 = (𝓯 , 𝓯-is-monotone , 𝓯-is-inflationary) t₀ : E t₀ = γ ⊥𝓔 t₀-is-fp : 𝓯 t₀ ＝ t₀ t₀-is-fp = γ-is-fixed-point 𝕗 ⊥𝓔 x₀ : D x₀ = ι t₀ x₀-is-fp : f x₀ ＝ x₀ x₀-is-fp = ap ι t₀-is-fp \end{code} x₀ is the least pre-fixed point. \begin{code} x₀-is-lpfp : (x : D) → f x ⊑ x → x₀ ⊑ x x₀-is-lpfp = TC₂ x₀ (τ t₀) \end{code} And so it is the least fixed point. \begin{code} x₀-is-lfp : (x : D) → f x ＝ x → x₀ ⊑ x x₀-is-lfp x p = x₀-is-lpfp x (＝-to-⊑ 𝓓 p) \end{code} This concludes the proof of the theorem. \begin{code} Theorem 𝓓 hb f fm = x₀ , x₀-is-fp , x₀-is-lfp where open Taylor 𝓓 hb f fm \end{code} This theorem can be strengthened as follows, which says that any endofunctor f has an initial algebra, when the dcpo is viewed as a category. \begin{code} initial-algebra : (𝓓 : DCPO {𝓤} {𝓤}) → has-bottom 𝓓 → (f : ⟨ 𝓓 ⟩ → ⟨ 𝓓 ⟩) → is-monotone 𝓓 𝓓 f → Σ x ꞉ ⟨ 𝓓 ⟩ , (f x ＝ x) × ((y : ⟨ 𝓓 ⟩) → f y ⊑⟨ 𝓓 ⟩ y → x ⊑⟨ 𝓓 ⟩ y) initial-algebra 𝓓 hb f fm = x₀ , x₀-is-fp , x₀-is-lpfp where open Taylor 𝓓 hb f fm \end{code} NB. We could have formulated and proved this more categorically as (𝓓 : DCPO {𝓤} {𝓤}) → has-bottom 𝓓 → (f : ⟨ 𝓓 ⟩ → ⟨ 𝓓 ⟩) → is-monotone 𝓓 𝓓 f → Σ x ꞉ ⟨ 𝓓 ⟩ , (f x ⊑⟨ 𝓓 ⟩ x) × ((y : ⟨ 𝓓 ⟩) → f y ⊑⟨ 𝓓 ⟩ y → x ⊑⟨ 𝓓 ⟩ y) and then conclude that actually f x ＝ x by Lambek's Lemma. But we already know that the initial algebra is a fixed point in our case, and so there is no point in doing this. For later reference we repackage the theorem as follows: \begin{code} module _ (𝓓 : DCPO {𝓤} {𝓤}) ((⊥ , ⊥-is-least) : has-bottom 𝓓) (f : ⟨ 𝓓 ⟩ → ⟨ 𝓓 ⟩) (fm : is-monotone 𝓓 𝓓 f) where lfp : ⟨ 𝓓 ⟩ lfp = pr₁ (Theorem 𝓓 (⊥ , ⊥-is-least) f fm) lfp-is-fixed-point : f lfp ＝ lfp lfp-is-fixed-point = pr₁ (pr₂ (Theorem 𝓓 (⊥ , ⊥-is-least) f fm)) lfp-is-least : (y : ⟨ 𝓓 ⟩) → f y ＝ y → lfp ⊑⟨ 𝓓 ⟩ y lfp-is-least = pr₂ (pr₂ (Theorem 𝓓 (⊥ , ⊥-is-least) f fm)) \end{code} Added 22 February 2024. It follows directly from Pataraia's original proof [2] that if P is a property that holds for ⊥, is closed under directed suprema, and is closed under f, then P holds for the least fixed point of f. We refer to this as the fixed-point induction principle. Although this principle doesn't follow directly from the above argument, we can prove it as follows, using the above module Taylor again. \begin{code} lfp-induction : (P : ⟨ 𝓓 ⟩ → 𝓤 ̇ ) → ((x : ⟨ 𝓓 ⟩) → is-prop (P x)) → P ⊥ → is-closed-under-directed-sups 𝓓 P → ((x : ⟨ 𝓓 ⟩) → P x → P (f x)) → P lfp module fixed-point-induction (P : ⟨ 𝓓 ⟩ → 𝓤 ̇ ) (P-is-prop-valued : (x : ⟨ 𝓓 ⟩) → is-prop (P x)) (P-holds-at-⊥ : P ⊥) (P-is-closed-under-directed-sups : is-closed-under-directed-sups 𝓓 P) (P-is-closed-under-f : (x : ⟨ 𝓓 ⟩) → P x → P (f x)) where private D = ⟨ 𝓓 ⟩ _⊑_ = underlying-order 𝓓 open Taylor 𝓓 (⊥ , ⊥-is-least) f fm using (TC ; TC₂ ; TC-𝓯 ; TC-is-prop-valued ; TC-is-closed-under-directed-sups ; TC-holds-at-⊥) renaming (𝓯 to 𝓯') TC' : D → 𝓤 ̇ TC' x = TC x × P x TC'-⊆-TC : (x : ⟨ 𝓓 ⟩) → TC' x → TC x TC'-⊆-TC x = pr₁ TC'-⊆-P : (x : ⟨ 𝓓 ⟩) → TC' x → P x TC'-⊆-P x = pr₂ TC'-is-prop-valued : (x : D) → is-prop (TC' x) TC'-is-prop-valued x = ×-is-prop (TC-is-prop-valued x) (P-is-prop-valued x) TC'-is-closed-under-directed-sups : is-closed-under-directed-sups 𝓓 TC' TC'-is-closed-under-directed-sups α δ TC'-preservation = c₁ , c₂ where c₁ : TC (∐ 𝓓 δ) c₁ = TC-is-closed-under-directed-sups α δ (λ a → TC'-⊆-TC (α a) (TC'-preservation a)) c₂ : P (∐ 𝓓 δ) c₂ = P-is-closed-under-directed-sups α δ (λ a → TC'-⊆-P (α a) (TC'-preservation a)) 𝓔 : DCPO 𝓔 = subdcpo 𝓓 TC' TC'-is-prop-valued TC'-is-closed-under-directed-sups private E = ⟨ 𝓔 ⟩ _≤_ : E → E → 𝓤 ̇ s ≤ t = s ⊑⟨ 𝓔 ⟩ t ι : E → D ι (x , c) = x τ' : (t : E) → TC' (ι t) τ' (x , c) = c τ : (t : E) → TC (ι t) τ t = TC'-⊆-TC (ι t) (τ' t) ⊥𝓔 : E ⊥𝓔 = ⊥ , TC-holds-at-⊥ , P-holds-at-⊥ 𝓯 : E → E 𝓯 (x , tc , p) = f x , TC-𝓯 (x , tc) , P-is-closed-under-f x p 𝓯-is-monotone : (s t : E) → s ≤ t → 𝓯 s ≤ 𝓯 t 𝓯-is-monotone (x , _) (y , _) = fm x y 𝓯-is-inflationary : (t : E) → t ≤ 𝓯 t 𝓯-is-inflationary (x , (c₁ , c₂) , _) = c₁ open lemma₂·₁ 𝓔 𝕗 : MI 𝕗 = (𝓯 , 𝓯-is-monotone , 𝓯-is-inflationary) t₀ : E t₀ = γ ⊥𝓔 t₀-is-fp : 𝓯 t₀ ＝ t₀ t₀-is-fp = γ-is-fixed-point 𝕗 ⊥𝓔 x₀ : D x₀ = ι t₀ x₀-is-fp : f x₀ ＝ x₀ x₀-is-fp = ap ι t₀-is-fp x₀-is-lpfp : (x : D) → f x ⊑ x → x₀ ⊑ x x₀-is-lpfp = TC₂ x₀ (τ t₀) x₀-is-lfp : (x : D) → f x ＝ x → x₀ ⊑ x x₀-is-lfp x p = x₀-is-lpfp x (＝-to-⊑ 𝓓 p) x₀-satisfies-P : P x₀ x₀-satisfies-P = TC'-⊆-P (ι t₀) (τ' t₀) \end{code} Now we are ready to prove the least fixed point induction theorem. \begin{code} lfp-induction P P-is-prop-valued P-holds-at-⊥ P-is-closed-under-directed-sups P-is-closed-under-f = transport P e x₀-satisfies-P where open fixed-point-induction P P-is-prop-valued P-holds-at-⊥ P-is-closed-under-directed-sups P-is-closed-under-f e : x₀ ＝ lfp e = antisymmetry 𝓓 x₀ lfp (x₀-is-lfp lfp lfp-is-fixed-point) (lfp-is-least x₀ x₀-is-fp) \end{code}