module Order.DCPO where

Directed-Complete Partial Orders🔗

Let (P,≤)(P, \le) be a partial order. A family of elements f:I→Pf : I \to P is a semi-directed family if for every i,ji, j, there merely exists some kk such fi≤fkf i \le f k and fj≤fkf j \le f k. A semidirected family f:I→Pf : I \to P is a directed family when II is merely inhabited.

module _ {o ℓ} (P : Poset o ℓ) where
  open Poset P

  is-semidirected-family : ∀ {Ix : Type o} → (Ix → Ob) → Type _
  is-semidirected-family {Ix = Ix} f = ∀ i j → ∃[ k ∈ Ix ] (f i ≤ f k × f j ≤ f k)

  record is-directed-family {Ix : Type o} (f : Ix → Ob) : Type (o ⊔ ℓ) where
    no-eta-equality
    field
      elt : ∥ Ix ∥
      semidirected : is-semidirected-family f

Note that any family whose indexing type is a proposition is automatically semi-directed:

  prop-indexed→semidirected
    : ∀ {Ix : Type o} → (s : Ix → Ob) → is-prop Ix
    → is-semidirected-family s
  prop-indexed→semidirected s prop i j =
    inc (i , ≤-refl , path→≤ (ap s (prop j i)))

The poset (P,≤)(P, \le) is a directed-complete partial order, or DCPO, if it has least upper bounds of all directed families.

  record is-dcpo : Type (lsuc o ⊔ ℓ) where
    no-eta-equality
    field
      directed-lubs
        : ∀ {Ix : Type o} (f : Ix → Ob) → is-directed-family f → Lub P f

    module ⋃ {Ix : Type o} (f : Ix → Ob) (dir : is-directed-family f) =
      Lub (directed-lubs f dir)

    open ⋃ using () renaming (lub to ⋃; fam≤lub to fam≤⋃; least to ⋃-least) public

Since least upper bounds are unique when they exist, being a DCPO is a property of a poset, and not structure on that poset.

  is-dcpo-is-prop : is-prop (is-dcpo P)
  is-dcpo-is-prop = Iso→is-hlevel 1 eqv $
    Π-is-hlevel′ 1 λ _ →
    Π-is-hlevel² 1 λ _ _ → Lub-is-prop P
    where unquoteDecl eqv = declare-record-iso eqv (quote is-dcpo)

Scott-continuous functions🔗

Let (P,≤)(P, \le) and (Q,⊑)(Q, \sqsubseteq) be a pair of posets. A monotone map f:P→Qf : P \to Q is called Scott-continuous when it preserves all directed lubs.

  is-scott-continuous : (f : Posets.Hom P Q) → Type _
  is-scott-continuous f =
    ∀ {Ix} (s : Ix → P.Ob) (fam : is-directed-family P s)
    → ∀ x → is-lub P s x → is-lub Q (f .hom ⊙ s) (f .hom x)

  is-scott-continuous-is-prop
    : ∀ (f : Posets.Hom P Q) → is-prop (is-scott-continuous f)
  is-scott-continuous-is-prop _ =
    Π-is-hlevel′ 1 λ _ → Π-is-hlevel³ 1 λ _ _ _  → Π-is-hlevel 1 λ _ →
    is-lub-is-prop Q

If (P,≤)(P, \le) is a DCPO, then any function f:P→Qf : P \to Q which preserves directed lubs is automatically a monotone map, and, consequently, Scott-continuous.

To see this, suppose we’re given x,y:Px, y : P with x≤yx \le y. The family s:Bool→Ps : \mathrm{Bool} \to P that sends true\mathrm{true} to xx and false\mathrm{false} to yy is directed: Bool\mathrm{Bool} is inhabited, and false\mathrm{false} is a least upper bound for arbitrary values of the family. Since ff preserves lubs, we have

f(x)≤(⊔f(s))=f(⊔s)=f(y) f(x) \le (\sqcup f(s)) = f(\sqcup s) = f(y)

  opaque
    dcpo+scott→monotone
      : is-dcpo P
      → (f : P.Ob → Q.Ob)
      → (∀ {Ix} (s : Ix → Poset.Ob P) (fam : is-directed-family P s)
         → ∀ x → is-lub P s x → is-lub Q (f ⊙ s) (f x))
      → is-monotone f (P .snd) (Q .snd)
    dcpo+scott→monotone is-dcpo f scott x y p =
      is-lub.fam≤lub fs-lub (lift true)
      where

        s : Lift _ Bool → P.Ob
        s (lift b) = if b then x else y

        sx≤sfalse : ∀ b → s b P.≤ s (lift false)
        sx≤sfalse (lift true) = p
        sx≤sfalse (lift false) = P.≤-refl

        s-directed : is-directed-family P s
        s-directed .elt =
          inc (lift true)
        s-directed .semidirected i j =
          inc (lift false , sx≤sfalse _ , sx≤sfalse _)

        s-lub : is-lub P s y
        s-lub .is-lub.fam≤lub = sx≤sfalse
        s-lub .is-lub.least z lt = lt (lift false)

        fs-lub : is-lub Q (f ⊙ s) (f y)
        fs-lub = scott s s-directed y s-lub

Moreover, if f:P→Qf : P \to Q is an arbitrary monotone map, and s:I→Ps : I \to P is a directed family, then fs:I→Qfs : I \to Q is still a directed family.

  monotone∘directed
    : ∀ {Ix : Type o}
    → {s : Ix → P.Ob}
    → (f : Posets.Hom P Q)
    → is-directed-family P s
    → is-directed-family Q (f .hom ⊙ s)
  monotone∘directed f dir .elt = dir .elt
  monotone∘directed f dir .is-directed-family.semidirected i j =
    ∥-∥-map (Σ-map₂ (×-map (f .preserves _ _) (f .preserves _ _)))
      (dir .semidirected i j)

The identity function is Scott-continuous.

  scott-id
    : ∀ {P : Poset o ℓ}
    → is-scott-continuous (Posets.id {x = P})
  scott-id s fam x lub = lub

Scott-continuous functions are closed under composition.

  scott-∘
    : ∀ {P Q R : Poset o ℓ}
    → (f : Posets.Hom Q R) (g : Posets.Hom P Q)
    → is-scott-continuous f → is-scott-continuous g
    → is-scott-continuous (f Posets.∘ g)
  scott-∘ f g f-scott g-scott s dir x lub =
    f-scott (g .hom ⊙ s)
      (monotone∘directed g dir)
      (g .hom x)
      (g-scott s dir x lub)

The category of DCPOs🔗

DCPOs form a subcategory of the category of posets. Furthermore, since being a DCPO is a property, identity of DCPOs is determined by identity of their underlying posets: thus, the category of DCPOs is univalent.

DCPOs-subcat : ∀ (o ℓ : Level) → Subcat (Posets o ℓ) (lsuc o ⊔ ℓ) (lsuc o ⊔ ℓ)
DCPOs-subcat o ℓ .Subcat.is-ob = is-dcpo
DCPOs-subcat o ℓ .Subcat.is-hom f _ _ = is-scott-continuous f
DCPOs-subcat o ℓ .Subcat.is-hom-prop f _ _ = is-scott-continuous-is-prop f
DCPOs-subcat o ℓ .Subcat.is-hom-id _ = scott-id
DCPOs-subcat o ℓ .Subcat.is-hom-∘ {f = f} {g = g} = scott-∘ f g

DCPOs : ∀ (o ℓ : Level) → Precategory (lsuc (o ⊔ ℓ)) (lsuc o ⊔ ℓ)
DCPOs o ℓ = Subcategory (DCPOs-subcat o ℓ)

DCPOs-is-category : ∀ {o ℓ} → is-category (DCPOs o ℓ)
DCPOs-is-category = subcat-is-category Posets-is-category (λ _ → is-dcpo-is-prop)

Reasoning with DCPOs🔗

The following pair of modules re-exports facts about the underlying posets (resp. monotone maps) of DCPOs (resp. Scott-continuous functions). They also prove a plethora of small lemmas that are useful in formalisation but not for informal reading.

These proofs are all quite straightforward, so we omit them.
module DCPO {o ℓ} (D : DCPO o ℓ) where
  poset : Poset o ℓ
  poset = D .fst

  set : Set o
  set = D .fst .fst

  open Poset poset public

  poset-on : Poset-on ℓ Ob
  poset-on = D .fst .snd

  has-dcpo : is-dcpo poset
  has-dcpo = D .snd

  open is-dcpo has-dcpo public

  ⋃-pointwise
    : ∀ {Ix} {s s' : Ix → Ob}
    → {fam : is-directed-family poset s} {fam' : is-directed-family poset s'}
    → (∀ ix → s ix ≤ s' ix)
    → ⋃ s fam ≤ ⋃ s' fam'
  ⋃-pointwise p = ⋃.least _ _ (⋃ _ _) λ ix →
    ≤-trans (p ix) (⋃.fam≤lub _ _ ix)

module Scott {o ℓ} {D E : DCPO o ℓ} (f : DCPOs.Hom D E) where
  private
    module D = DCPO D
    module E = DCPO E

  mono : Posets.Hom D.poset E.poset
  mono = Subcat-hom.hom f

  hom : D.Ob → E.Ob
  hom x = Total-hom.hom mono x

  monotone : ∀ x y → x D.≤ y → hom x E.≤ hom y
  monotone = Total-hom.preserves mono

  opaque
    pres-directed-lub
      : ∀ {Ix} (s : Ix → D.Ob) → is-directed-family D.poset s
      → ∀ x → is-lub D.poset s x → is-lub E.poset (hom ⊙ s) (hom x)
    pres-directed-lub = Subcat-hom.witness f

    directed
      : ∀ {Ix} {s : Ix → D.Ob} → is-directed-family D.poset s
      → is-directed-family E.poset (hom ⊙ s)
    directed dir = monotone∘directed (Subcat-hom.hom f) dir

    pres-⋃
      : ∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
      → hom (D.⋃ s dir) ≡ E.⋃ (hom ⊙ s) (directed dir)
    pres-⋃ s dir =
      E.≤-antisym
        (is-lub.least (pres-directed-lub s dir (D.⋃ s dir) (D.⋃.has-lub s dir))
          (E.⋃ (hom ⊙ s) (directed dir))
          (E.⋃.fam≤lub (hom ⊙ s) (directed dir)))
        (E.⋃.least (hom ⊙ s) (directed dir) (hom (D.⋃ s dir)) λ i →
          monotone (s i) (D.⋃ s dir) (D.⋃.fam≤lub s dir i))

We also provide a couple methods for constructing Scott-continuous maps. First, we note that if a function is monotonic and commutes with some chosen assignment of least upper bounds, then it is Scott-continuous.

  to-scott
    : (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)))
    → DCPOs.Hom D E
  to-scott f monotone pres-⋃ =
    sub-hom (total-hom f monotone) pres-lub where
      pres-lub
        : ∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
        → ∀ x → is-lub D.poset s x → is-lub E.poset (f ⊙ s) (f x)
      pres-lub s dir x x-lub .is-lub.fam≤lub i =
        monotone _ _ (is-lub.fam≤lub x-lub i)
      pres-lub s dir x x-lub .is-lub.least y le =
        f x              E.≤⟨ monotone _ _ (is-lub.least x-lub _ (D.⋃.fam≤lub s dir)) ⟩E.≤
        f (D.⋃ s dir)    E.=⟨ lub-unique E.poset (pres-⋃ s dir) (E.⋃.has-lub (f ⊙ s) (monotone∘directed (total-hom f monotone) dir)) ⟩E.=
        E.⋃ (f ⊙ s) _    E.≤⟨ E.⋃.least _ _ y le ⟩E.≤
        y                E.≤∎

Furthermore, if ff preserves arbitrary least upper bounds, then it is monotone, and thus Scott-continuous.

  to-scott-directed
    : (f : D.Ob → E.Ob)
    → (∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
       → ∀ x → is-lub D.poset s x → is-lub E.poset (f ⊙ s) (f x))
    → DCPOs.Hom D E
  to-scott-directed f pres =
    sub-hom (total-hom f (dcpo+scott→monotone D.has-dcpo f pres)) pres