open import Cat.Functor.Subcategory
open import Cat.Displayed.Total
open import Cat.Prelude

open import Data.Maybe.Base

open import Order.Diagram.Fixpoint
open import Order.Diagram.Bottom
open import Order.Diagram.Lub
open import Order.Base
open import Order.DCPO

import Cat.Reasoning

import Data.Nat as Nat

module Order.DCPO.Pointed where

private variable
o β : Level
Ix : Type o


# 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.

module _ {o β} (D : DCPO o β) where
open DCPO D
open Lub


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 (lub (Ξ» ()) (Ξ» ())))


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 # (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 # y β€ y β β n β fβΏβ₯ n β€ y
fβΏβ₯β€fix y p (lift zero) = Β‘
fβΏβ₯β€fix y p (lift (suc n)) =
f # (fβΏ n bot)   β€β¨ f.monotone (fβΏβ₯β€fix y p (lift n)) β©β€
f # y            β€β¨ p β©β€
y                β€β

least-fix : β (y : Ob) β f # 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 # (β fβΏβ₯ fβΏβ₯-dir) β€ β fβΏβ₯ fβΏβ₯-dir
roll =
f # (β fβΏβ₯ _)        =β¨ f.pres-β fβΏβ₯ fβΏβ₯-dir β©=
β (apply 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 # (β fβΏβ₯ fβΏβ₯-dir)
unroll = least-fix (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 (β€-refl' y-fix)  ## Strictly Scott-continuous mapsπ A Scott-continuous map is strictly continuous if it preserves bottoms. module _ {o β} {D E : DCPO o β} where private module D = DCPO D module E = DCPO E   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 (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 (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 (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} {β} Pointed-DCPOsβͺDCPOs : Functor (Pointed-DCPOs o β) (DCPOs o β) Pointed-DCPOsβͺDCPOs = Forget-subcat Pointed-DCPOsβͺSets : Functor (Pointed-DCPOs o β) (Sets o) Pointed-DCPOsβͺSets = DCPOsβͺSets Fβ Pointed-DCPOsβͺDCPOs  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 (Ξ» x β absurd (Β¬i x))) (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 (Ξ» 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 (f # x)
pres-bottoms = Subcat-hom.witness f

pres-β₯ : f # D.bottom β‘ E.bottom
pres-β₯ = bottom-unique E.poset (pres-bottoms D.bottom D.bottomβ€x) E.bottomβ€x

: β {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 (apply f β s)) (f # 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 (f # x)
pres-adjoin-lub {s = s} {x = x} sdir x-lub .is-lub.least y le =
is-lub.least
(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 (apply f β s) (f # x)
pres-semidirected-lub s sdir x x-lub =

pres-β-prop
: β {Ix} (s : Ix β D.Ob) (p q : is-prop Ix)
β f # (D.β-prop s p) β‘ E.β-prop (apply f β s) q
pres-β-prop s p q =
lub-unique
(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 β f # y β‘ E.bottom β f # x β‘ E.bottom
bottom-bounded {x = x} {y = y} p y-bot =
E.β€-antisym
(f # x    E.β€β¨ monotone p β©E.β€
f # 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


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.β.has-lub _ _) (D.β-semi-lub s (dir .semidirected))) β©E.=
f (D.β-semi s (dir .semidirected)) E.β€β¨ pres-β-semi _ _ .is-lub.least 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 (Ξ» x β absurd (x .Lift.lower)) (Ξ» ())) y (Ξ» ()) β©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 _ (Ξ» x β absurd (x .Lift.lower)) x (lift-is-lub (is-bottomβis-lub D.poset {f = Ξ» ()} x-bot)))
y (Ξ» ()))