Definitons of domain theory

Author: jmougeot

CHANGELOG.md

@@ -123,6 +123,10 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
+* Added a new domain theory section to the library under `Relation.Binary.Domain.*`:
+  - Introduced new modules and bundles for domain theory, including `DCPO`, `Lub`, and `ScottContinuous`.
+  - All files for domain theory are now available in `src/Relation/Binary/Domain/`.
+
 Additions to existing modules
 -----------------------------
 

src/Relation/Binary/Domain.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Order-theoretic Domains
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain where
+
+------------------------------------------------------------------------
+-- Re-export various components of the Domain hierarchy
+
+open import Relation.Binary.Domain.Definitions public
+open import Relation.Binary.Domain.Structures public
+open import Relation.Binary.Domain.Bundles public

src/Relation/Binary/Domain/Bundles.agda

@@ -0,0 +1,53 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bundles for domain theory
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Bundles where
+
+open import Level using (Level; _⊔_; suc)
+open import Relation.Binary.Bundles using (Poset)
+open import Relation.Binary.Domain.Structures
+open import Relation.Binary.Domain.Definitions
+
+private
+  variable
+    o ℓ e o' ℓ' e' ℓ₂ : Level
+    Ix A B : Set o
+
+------------------------------------------------------------------------
+-- DCPOs
+------------------------------------------------------------------------
+
+record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  field
+    poset   : Poset c ℓ₁ ℓ₂
+    DcpoStr : IsDCPO poset
+
+  open Poset poset public
+  open IsDCPO DcpoStr public
+
+------------------------------------------------------------------------
+-- Scott-continuous functions
+------------------------------------------------------------------------
+
+record ScottContinuous {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} :
+  Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  field
+    f             : Poset.Carrier P → Poset.Carrier Q
+    Scottfunction : IsScottContinuous {P = P} {Q = Q} f
+
+------------------------------------------------------------------------
+-- Lubs
+------------------------------------------------------------------------
+
+record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Ix : Set c} (s : Ix → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+  private
+    module P = Poset P
+  field
+    lub           : P.Carrier
+    is-upperbound : ∀ i → P._≤_ (s i) lub
+    is-least      : ∀ y → (∀ i → P._≤_ (s i) y) → P._≤_ lub y

src/Relation/Binary/Domain/Definitions.agda

@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions for domain theory
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Definitions where
+
+open import Data.Product using (∃-syntax; _×_; _,_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Bundles using (Poset)
+open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
+
+private
+  variable
+    c o ℓ e o' ℓ' e' ℓ₁ ℓ₂ : Level
+    Ix A B : Set o
+    P : Poset c ℓ e
+
+------------------------------------------------------------------------
+-- Directed families
+------------------------------------------------------------------------
+
+IsSemidirectedFamily : (P : Poset c ℓ₁ ℓ₂) → ∀ {Ix : Set c} → (s : Ix → Poset.Carrier P) → Set _
+IsSemidirectedFamily P {Ix} s = ∀ i j → ∃[ k ] (Poset._≤_ P (s i) (s k) × Poset._≤_ P (s j) (s k))
+

src/Relation/Binary/Domain/Structures.agda

@@ -0,0 +1,66 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Structures for domain theory
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Structures where
+
+open import Data.Product using (_×_; _,_)
+open import Data.Nat.Properties using (≤-trans)
+open import Function using (_∘_)
+open import Level using (Level; _⊔_; suc)
+open import Relation.Binary.Bundles using (Poset)
+open import Relation.Binary.Domain.Definitions
+open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
+
+private variable
+  o ℓ e o' ℓ' e' ℓ₂ : Level
+  Ix A B : Set o
+
+module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
+  open Poset P
+
+  record IsDirectedFamily {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+    no-eta-equality
+    field
+      elt : Ix
+      SemiDirected : IsSemidirectedFamily P s
+
+  record IsLub {Ix : Set c} (s : Ix → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      is-upperbound : ∀ i → s i ≤ lub
+      is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
+
+  record IsDCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+    field
+      ⋁ : ∀ {Ix : Set c}
+        → (s : Ix → Carrier)
+        → IsDirectedFamily s
+        → Carrier
+      ⋁-isLub : ∀ {Ix : Set c}
+        → (s : Ix → Carrier)
+        → (dir : IsDirectedFamily s)
+        → IsLub s (⋁ s dir)
+
+    module _ {Ix : Set c} {s : Ix → Carrier} {dir : IsDirectedFamily s} where
+      open IsLub (⋁-isLub s dir)
+        renaming (is-upperbound to ⋁-≤; is-least to ⋁-least)
+        public
+
+module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
+
+  private
+    module P = Poset P
+    module Q = Poset Q
+
+  record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+    field
+      PreserveLub : ∀ {Ix : Set c} {s : Ix → P.Carrier}
+        → (dir : IsDirectedFamily P s)
+        → (lub : P.Carrier)
+        → IsLub P s lub
+        → IsLub Q (f ∘ s) (f lub)
+      PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y