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

open import Data.Bool

open import Order.Diagram.Lub
open import Order.Base

import Cat.Reasoning

import Order.Reasoning as Poset

module Order.DCPO where

private variable
o β β' : Level
Ix A B : Type o


# Directed-Complete Partial Ordersπ

Let $(P, \le)$ be a partial order. A family of elements $f : I \to P$ is a semi-directed family if for every $i, j$, there merely exists some $k$ such $f i \le f k$ and $f j \le f k$. A semidirected family $f : I \to P$ is a directed family when $I$ 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, \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.

module _ {o β} {P : Poset o β} where
open Poset P
open is-dcpo

  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, \le)$ and $(Q, \sqsubseteq)$ be a pair of posets. A monotone map $f : P \to Q$ is called Scott-continuous when it preserves all directed lubs. module _ {P Q : Poset o β} where private module P = Poset P module Q = Poset Q open is-directed-family open Total-hom   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, \le)$ is a DCPO, then any function $f : 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 : P$ with $x \le y$. The family $s : \mathrm{Bool} \to P$ that sends $\mathrm{true}$ to $x$ and $\mathrm{false}$ to $y$ is directed: $\mathrm{Bool}$ is inhabited, and $\mathrm{false}$ is a least upper bound for arbitrary values of the family. Since $f$ preserves lubs, we have $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 \to Q$ is an arbitrary monotone map, and $s : I \to P$ is a directed family, then $fs : 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)  module _ where open Total-hom  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)  module DCPOs {o β : Level} = Cat.Reasoning (DCPOs o β) DCPO : (o β : Level) β Type _ DCPO o β = DCPOs.Ob {o} {β} Forget-DCPO : β {o β} β Functor (DCPOs o β) (Sets o) Forget-DCPO = ΟαΆ _ Fβ Forget-subcat  # 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))  module _ {o β} {D E : DCPO o β} where private module D = DCPO D module E = DCPO E open is-directed-family open Total-hom scott-path : β {f g : DCPOs.Hom D E} β (β x β Scott.hom f x β‘ Scott.hom g x) β f β‘ g scott-path p = Subcat-hom-path$
total-hom-path _ (funext p) \$
is-propβpathp (Ξ» i β is-monotone-is-prop (Ξ» x β p x i) D.poset-on E.poset-on) _ _


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 $f$ 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