module Order.DCPO.Pointed where

Pointed DCPOs🔗

A DCPO is pointed if it has a least element ⊥\bot. 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 ⊥→D\bot \to D, 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 DD has a bottom element ⊥\bot, then we can extend any semidirected family I→DI \to D to a directed family Maybe(I)→D\mathrm{Maybe}(I) \to D by sending nothing to the bottom element.

  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, ss 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 DD be a pointed DCPO. Every Scott continuous function f:D→Df : D \to D 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 N→D\mathbb{N} \to D that maps nn to fn(⊥)f^n(\bot).

    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 yy such that fy≤yf y \le y, ⋃(fn(⊥))≤y\bigcup (f^{n}(\bot)) \le y. 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 ⋃(fn(⊥))\bigcup (f^{n}(\bot)) is actuall a fixpoint. First, the forward direction: ⋃(fn(⊥))≤f(⋃(fn(⊥)))\bigcup (f^{n}(\bot)) \le f (\bigcup (f^{n}(\bot))). This follows directly from Scott-continuity of ff.

    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 f(f(⋃(fn(⊥))))≤f(⋃(fn(⊥)))f (f (\bigcup (f^{n}(\bot)))) \le f (\bigcup (f^{n}(\bot))). We can then apply monotonicity of ff, 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-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 DD 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 DD.

  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 _)

We also provide a handful of ways of constructing strictly Scott-continuous maps. First, we note that if ff is monotonic and preserves the chosen least upper bound of semidirected families, then ff 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 ff is monotonic, preserves chosen least upper bounds of directed families, and preserves chosen bottoms, then ff 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 ff preserves arbitrary least upper bounds of semidirected families, then ff 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))