module Order.DCPO.Pointed where
Pointed DCPOsπ
A DCPO is pointed if it has a least element . This is a property of a DCPO, as bottom elements are unique.
is-pointed-dcpo : DCPO o β β Type _ is-pointed-dcpo D = Bottom (DCPO.poset D) is-pointed-dcpo-is-prop : β (D : DCPO o β) β is-prop (is-pointed-dcpo D) is-pointed-dcpo-is-prop D = Bottom-is-prop (DCPO.poset D)
A DCPO is pointed if and only if it has least upper bounds of all semidirected families.
The forward direction is straightforward: bottom elements are equivalent to least upper bounds of the empty family , and this family is trivially semidirected.
semidirected-lubβpointed : (β {Ix : Type o} (s : Ix β Ob) β is-semidirected-family poset s β Lub poset s) β is-pointed-dcpo D semidirected-lubβpointed lub = LubβBottom poset (lower-lub poset (lub (absurd β Lift.lower) (absurd β Lift.lower)))
Conversely, if
has a bottom element
,
then we can extend any semidirected family
to a directed family
by sending nothing
to the bottom element.
module _ {o β} (D : DCPO o β) (pointed : is-pointed-dcpo D) where open DCPO D open Bottom pointed open is-directed-family open is-lub
extend-bottom : (Ix β Ob) β Maybe Ix β Ob extend-bottom s nothing = bot extend-bottom s (just i) = s i extend-bottom-directed : (s : Ix β Ob) β is-semidirected-family poset s β is-directed-family poset (extend-bottom s) extend-bottom-directed s semidir .elt = inc nothing extend-bottom-directed s semidir .semidirected (just i) (just j) = do (k , iβ€k , jβ€k) β semidir i j pure (just k , iβ€k , jβ€k) extend-bottom-directed s semidir .semidirected (just x) nothing = pure (just x , β€-refl , Β‘) extend-bottom-directed s semidir .semidirected nothing (just y) = pure (just y , Β‘ , β€-refl) extend-bottom-directed s semidir .semidirected nothing nothing = pure (nothing , β€-refl , β€-refl)
Furthermore, has a least upper bound only if the extended family does.
lubβextend-bottom-lub : β {s : Ix β Ob} {x : Ob} β is-lub poset s x β is-lub poset (extend-bottom s) x lubβextend-bottom-lub {s = s} {x = x} x-lub .famβ€lub (just i) = x-lub .famβ€lub i lubβextend-bottom-lub {s = s} {x = x} x-lub .famβ€lub nothing = Β‘ lubβextend-bottom-lub {s = s} {x = x} x-lub .least y le = x-lub .least y (le β just) extend-bottom-lubβlub : β {s : Ix β Ob} {x : Ob} β is-lub poset (extend-bottom s) x β is-lub poset s x extend-bottom-lubβlub x-lub .famβ€lub i = x-lub .famβ€lub (just i) extend-bottom-lubβlub x-lub .least y le = x-lub .least y Ξ» where nothing β Β‘ (just i) β le i
If we put this all together, we see that any semidirected family has a least upper bound in a pointed DCPO.
pointedβsemidirected-lub : is-pointed-dcpo D β β {Ix : Type o} (s : Ix β Ob) β is-semidirected-family poset s β Lub poset s pointedβsemidirected-lub pointed {Ix = Ix} s semidir .Lub.lub = β (extend-bottom s) (extend-bottom-directed s semidir) pointedβsemidirected-lub pointed {Ix = Ix} s semidir .Lub.has-lub = extend-bottom-lubβlub (β.has-lub _ _)
Fixpointsπ
Let be a pointed DCPO. Every Scott continuous function has a least fixed point.
module _ {o β} {D : DCPO o β} where open DCPO D pointedβleast-fixpoint : is-pointed-dcpo D β (f : DCPOs.Hom D D) β Least-fixpoint poset (Scott.mono f) pointedβleast-fixpoint pointed f = f-fix where open Bottom pointed module f = Scott f
We begin by constructing a directed family that maps to .
fβΏ : Nat β Ob β Ob fβΏ zero x = x fβΏ (suc n) x = f.hom (fβΏ n x) fβΏ-mono : β {i j} β i Nat.β€ j β fβΏ i bot β€ fβΏ j bot fβΏ-mono Nat.0β€x = Β‘ fβΏ-mono (Nat.sβ€s p) = f.monotone _ _ (fβΏ-mono p) fβΏβ₯ : Lift o Nat β Ob fβΏβ₯ (lift n) = fβΏ n bot fβΏβ₯-dir : is-directed-family poset fβΏβ₯ fβΏβ₯-dir .is-directed-family.elt = inc (lift zero) fβΏβ₯-dir .is-directed-family.semidirected (lift i) (lift j) = inc (lift (Nat.max i j) , fβΏ-mono (Nat.max-β€l i j) , fβΏ-mono (Nat.max-β€r i j))
The least upper bound of this sequence shall be our least fixpoint. We begin by proving a slightly stronger variation of the universal property; namely for any such that , . This follows from som quick induction.
fβΏβ₯β€fix : β (y : Ob) β f.hom y β€ y β β n β fβΏβ₯ n β€ y fβΏβ₯β€fix y p (lift zero) = Β‘ fβΏβ₯β€fix y p (lift (suc n)) = f.hom (fβΏ n bot) β€β¨ f.monotone _ _ (fβΏβ₯β€fix y p (lift n)) β©β€ f.hom y β€β¨ p β©β€ y β€β least-fix : β (y : Ob) β f.hom y β€ y β β fβΏβ₯ fβΏβ₯-dir β€ y least-fix y p = β.least _ _ _ (fβΏβ₯β€fix y p)
Now, letβs show that is actuall a fixpoint. First, the forward direction: . This follows directly from Scott-continuity of .
roll : f.hom (β fβΏβ₯ fβΏβ₯-dir) β€ β fβΏβ₯ fβΏβ₯-dir roll = Scott.hom f (β fβΏβ₯ _) =β¨ f.pres-β fβΏβ₯ fβΏβ₯-dir β©= β (Scott.hom f β fβΏβ₯) _ β€β¨ β.least _ _ _ (Ξ» (lift n) β β.famβ€lub _ _ (lift (suc n))) β©β€ β fβΏβ₯ _ β€β
To show the converse, we use universal property we proved earlier to re-arrange the goal to . We can then apply monotonicity of , and then use the forward direction to finish off the proof.
unroll : β fβΏβ₯ fβΏβ₯-dir β€ f.hom (β fβΏβ₯ fβΏβ₯-dir) unroll = least-fix (Scott.hom f (β fβΏβ₯ fβΏβ₯-dir)) $ f.monotone _ _ roll
All that remains is to package up the data.
f-fix : Least-fixpoint poset f.mono f-fix .Least-fixpoint.fixpoint = β fβΏβ₯ fβΏβ₯-dir f-fix .Least-fixpoint.has-least-fixpoint .is-least-fixpoint.fixed = β€-antisym roll unroll f-fix .Least-fixpoint.has-least-fixpoint .is-least-fixpoint.least y y-fix = least-fix y (pathββ€ y-fix)
Strictly Scott-continuous mapsπ
A Scott-continuous map is strictly continuous if it preserves bottoms.
is-strictly-scott-continuous : (f : DCPOs.Hom D E) β Type _ is-strictly-scott-continuous f = β (x : D.Ob) β is-bottom D.poset x β is-bottom E.poset (Scott.hom f x)
is-strictly-scott-is-prop : (f : DCPOs.Hom D E) β is-prop (is-strictly-scott-continuous f) is-strictly-scott-is-prop f = Ξ -is-hlevelΒ² 1 Ξ» x _ β is-bottom-is-prop E.poset (Scott.hom f x)
Strictly Scott-continuous functions are closed under identities and composites.
strict-scott-id : β {D : DCPO o β} β is-strictly-scott-continuous (DCPOs.id {x = D}) strict-scott-id x x-bot = x-bot strict-scott-β : β {D E F : DCPO o β} β (f : DCPOs.Hom E F) (g : DCPOs.Hom D E) β is-strictly-scott-continuous f β is-strictly-scott-continuous g β is-strictly-scott-continuous (f DCPOs.β g) strict-scott-β f g f-strict g-strict x x-bot = f-strict (Scott.hom g x) (g-strict x x-bot)
Pointed DCPOs and strictly Scott-continuous functions form a subcategory of the category of DCPOs.
Pointed-DCPOs-subcat : β o β β Subcat (DCPOs o β) (o β β) (o β β) Pointed-DCPOs-subcat o β .Subcat.is-ob = is-pointed-dcpo Pointed-DCPOs-subcat o β .Subcat.is-hom f _ _ = is-strictly-scott-continuous f Pointed-DCPOs-subcat o β .Subcat.is-hom-prop f _ _ = is-strictly-scott-is-prop f Pointed-DCPOs-subcat o β .Subcat.is-hom-id {D} _ = strict-scott-id {D = D} Pointed-DCPOs-subcat o β .Subcat.is-hom-β {f = f} {g = g} f-strict g-strict = strict-scott-β f g f-strict g-strict Pointed-DCPOs : β o β β Precategory (lsuc (o β β)) (lsuc o β β) Pointed-DCPOs o β = Subcategory (Pointed-DCPOs-subcat o β) Pointed-DCPOs-is-category : is-category (Pointed-DCPOs o β) Pointed-DCPOs-is-category = subcat-is-category DCPOs-is-category is-pointed-dcpo-is-prop
Reasoning with Pointed DCPOsπ
The following module re-exports facts about pointed DCPOs, and also proves a bunch of useful lemma.s
module Pointed-DCPOs {o β : Level} = Cat.Reasoning (Pointed-DCPOs o β) Pointed-dcpo : β o β β Type _ Pointed-dcpo o β = Pointed-DCPOs.Ob {o} {β} Forget-Pointed-dcpo : Functor (Pointed-DCPOs o β) (Sets o) Forget-Pointed-dcpo = Forget-DCPO Fβ Forget-subcat
module Pointed-dcpo {o β} (D : Pointed-dcpo o β) where
These proofs are all quite straightforward, so we omit them.
open is-directed-family dcpo : DCPO o β dcpo = D .fst has-pointed : is-pointed-dcpo dcpo has-pointed = D .snd open DCPO dcpo public bottom : Ob bottom = Bottom.bot (D .snd) bottomβ€x : β x β bottom β€ x bottomβ€x = Bottom.has-bottom (D .snd) adjoin : β {Ix : Type o} β (Ix β Ob) β Maybe Ix β Ob adjoin = extend-bottom dcpo has-pointed adjoin-directed : β (s : Ix β Ob) β is-semidirected-family poset s β is-directed-family poset (adjoin s) adjoin-directed = extend-bottom-directed dcpo has-pointed lubβadjoin-lub : β {s : Ix β Ob} {x : Ob} β is-lub poset s x β is-lub poset (adjoin s) x lubβadjoin-lub = lubβextend-bottom-lub dcpo has-pointed adjoin-lubβlub : β {s : Ix β Ob} {x : Ob} β is-lub poset (adjoin s) x β is-lub poset s x adjoin-lubβlub = extend-bottom-lubβlub dcpo has-pointed -- We put these behind 'opaque' to prevent blow ups in goals. opaque β-semi : (s : Ix β Ob) β is-semidirected-family poset s β Ob β-semi s semidir = β (adjoin s) (adjoin-directed s semidir) β-semi-lub : β (s : Ix β Ob) (dir : is-semidirected-family poset s) β is-lub poset s (β-semi s dir) β-semi-lub s dir = adjoin-lubβlub (β.has-lub (adjoin s) (adjoin-directed s dir)) β-semi-le : β (s : Ix β Ob) (dir : is-semidirected-family poset s) β β i β s i β€ β-semi s dir β-semi-le s dir = is-lub.famβ€lub (β-semi-lub s dir) β-semi-least : β (s : Ix β Ob) (dir : is-semidirected-family poset s) β β x β (β i β s i β€ x) β β-semi s dir β€ x β-semi-least s dir x le = is-lub.least (β-semi-lub s dir) x le β-semi-pointwise : β {Ix} {s s' : Ix β Ob} β {fam : is-semidirected-family poset s} {fam' : is-semidirected-family poset s'} β (β ix β s ix β€ s' ix) β β-semi s fam β€ β-semi s' fam' β-semi-pointwise le = β-pointwise Ξ» where (just i) β le i nothing β bottomβ€x _
However, we do call attention to one extremely useful fact: if is a pointed DCPO, then it has least upper bounds of families indexed by propositions.
opaque β-prop : β {Ix : Type o} β (Ix β Ob) β is-prop Ix β Ob β-prop s ix-prop = β-semi s (prop-indexedβsemidirected poset s ix-prop) β-prop-le : β (s : Ix β Ob) (p : is-prop Ix) β β i β s i β€ β-prop s p β-prop-le s p i = β-semi-le _ _ i β-prop-least : β (s : Ix β Ob) (p : is-prop Ix) β β x β (β i β s i β€ x) β β-prop s p β€ x β-prop-least s p = β-semi-least _ _ β-prop-lub : β (s : Ix β Ob) (p : is-prop Ix) β is-lub poset s (β-prop s p) β-prop-lub s p = β-semi-lub _ _
This allows us to reflect the truth value of a proposition into .
opaque β-prop-false : β (s : Ix β Ob) (p : is-prop Ix) β Β¬ Ix β β-prop s p β‘ bottom β-prop-false s p Β¬i = β€-antisym (β-prop-least s p bottom (absurd β Β¬i)) (bottomβ€x _) β-prop-true : β (s : Ix β Ob) (p : is-prop Ix) β (i : Ix) β β-prop s p β‘ s i β-prop-true s p i = sym $ lub-of-const-fam poset (Ξ» i j β ap s (p i j)) (β-prop-lub s p) i
We define a similar module for strictly Scott-continuous maps.
module Strict-scott {D E : Pointed-dcpo o β} (f : Pointed-DCPOs.Hom D E) where
These proofs are all quite straightforward, so we omit them.
private module D = Pointed-dcpo D module E = Pointed-dcpo E scott : DCPOs.Hom D.dcpo E.dcpo scott = Subcat-hom.hom f open Scott scott public opaque pres-bottoms : β x β is-bottom D.poset x β is-bottom E.poset (hom x) pres-bottoms = Subcat-hom.witness f pres-β₯ : hom D.bottom β‘ E.bottom pres-β₯ = bottom-unique E.poset (pres-bottoms D.bottom D.bottomβ€x) E.bottomβ€x pres-adjoin-lub : β {s : Ix β D.Ob} {x : D.Ob} β is-semidirected-family D.poset s β is-lub D.poset (D.adjoin s) x β is-lub E.poset (E.adjoin (hom β s)) (hom x) pres-adjoin-lub {s = s} {x = x} sdir x-lub .is-lub.famβ€lub (just i) = monotone _ _ (is-lub.famβ€lub x-lub (just i)) pres-adjoin-lub {s = s} {x = x} sdir x-lub .is-lub.famβ€lub nothing = E.bottomβ€x (hom x) pres-adjoin-lub {s = s} {x = x} sdir x-lub .is-lub.least y le = is-lub.least (pres-directed-lub (D.adjoin s) (D.adjoin-directed s sdir) x x-lub) y Ξ» where (just i) β le (just i) nothing β pres-bottoms _ D.bottomβ€x y pres-semidirected-lub : β {Ix} (s : Ix β D.Ob) β is-semidirected-family D.poset s β β x β is-lub D.poset s x β is-lub E.poset (hom β s) (hom x) pres-semidirected-lub s sdir x x-lub = E.adjoin-lubβlub (pres-adjoin-lub sdir (D.lubβadjoin-lub x-lub)) pres-β-prop : β {Ix} (s : Ix β D.Ob) (p q : is-prop Ix) β hom (D.β-prop s p) β‘ E.β-prop (hom β s) q pres-β-prop s p q = lub-unique E.poset (pres-semidirected-lub _ (prop-indexedβsemidirected D.poset s p) (D.β-prop s p) (D.β-prop-lub s p)) (E.β-prop-lub _ _) bottom-bounded : β {x y} β x D.β€ y β hom y β‘ E.bottom β hom x β‘ E.bottom bottom-bounded {x = x} {y = y} p y-bot = E.β€-antisym (hom x E.β€β¨ monotone _ _ p β©E.β€ hom y E.=β¨ y-bot β©E.= E.bottom E.β€β) (E.bottomβ€x _)
module _ {o β} {D E : Pointed-dcpo o β} where private module D = Pointed-dcpo D module E = Pointed-dcpo E open Total-hom open is-directed-family strict-scott-path : β {f g : Pointed-DCPOs.Hom D E} β (β x β Strict-scott.hom f x β‘ Strict-scott.hom g x) β f β‘ g strict-scott-path p = Subcat-hom-path (scott-path p)
We also provide a handful of ways of constructing strictly Scott-continuous maps. First, we note that if is monotonic and preserves the chosen least upper bound of semidirected families, then is strictly Scott-continuous.
to-strict-scott-β-semi : (f : D.Ob β E.Ob) β (β x y β x D.β€ y β f x E.β€ f y) β (β {Ix} (s : Ix β D.Ob) β (dir : is-semidirected-family D.poset s) β is-lub E.poset (f β s) (f (D.β-semi s dir))) β Pointed-DCPOs.Hom D E to-strict-scott-β-semi f monotone pres-β-semi = sub-hom (to-scott f monotone pres-β) pres-bot where pres-β : β {Ix} (s : Ix β D.Ob) β (dir : is-directed-family D.poset s) β is-lub E.poset (f β s) (f (D.β s dir)) pres-β s dir .is-lub.famβ€lub i = monotone _ _ $ D.β.famβ€lub _ _ i pres-β s dir .is-lub.least y le = f (D.β s dir) E.=β¨ ap f (lub-unique D.poset (D.β.has-lub _ _) (D.β-semi-lub s (dir .semidirected))) β©E.= f (D.β-semi s (dir .semidirected)) E.β€β¨ is-lub.least (pres-β-semi _ _) y le β©E.β€ y E.β€β pres-bot : β x β is-bottom D.poset x β is-bottom E.poset (f x) pres-bot x x-bot y = f x E.β€β¨ monotone _ _ (x-bot _) β©E.β€ f (D.β-semi _ _) E.β€β¨ is-lub.least (pres-β-semi (absurd β Lift.lower) (absurd β Lift.lower)) y (absurd β Lift.lower) β©E.β€ y E.β€β
Next, if is monotonic, preserves chosen least upper bounds of directed families, and preserves chosen bottoms, then is strictly Scott-continuous.
to-strict-scott-bottom : (f : D.Ob β E.Ob) β (β x y β x D.β€ y β f x E.β€ f y) β (β {Ix} (s : Ix β D.Ob) β (dir : is-directed-family D.poset s) β is-lub E.poset (f β s) (f (D.β s dir))) β is-bottom E.poset (f D.bottom) β Pointed-DCPOs.Hom D E to-strict-scott-bottom f monotone pres-β pres-bot = sub-hom (to-scott f monotone pres-β) Ξ» x x-bot y β f x E.β€β¨ monotone _ _ (x-bot _) β©E.β€ f D.bottom E.β€β¨ pres-bot y β©E.β€ y E.β€β
Finally, if preserves arbitrary least upper bounds of semidirected families, then must be monotonic, and thus strictly Scott-continuous.
to-strict-scott-semidirected : (f : D.Ob β E.Ob) β (β {Ix} (s : Ix β D.Ob) β (dir : is-semidirected-family D.poset s) β β x β is-lub D.poset s x β is-lub E.poset (f β s) (f x)) β Pointed-DCPOs.Hom D E to-strict-scott-semidirected f pres = sub-hom (to-scott-directed f (Ξ» s dir x lub β pres s (is-directed-family.semidirected dir) x lub)) (Ξ» x x-bot y β is-lub.least (pres _ (absurd β Lift.lower) x (lift-is-lub D.poset (is-bottomβis-lub D.poset x-bot))) y (absurd β Lift.lower))