Skip to content

Commit b4edd11

Browse files
jmougeotjmougeot
committed
Domain Theory propreties
1 parent a7355ba commit b4edd11

File tree

4 files changed

+309
-208
lines changed

4 files changed

+309
-208
lines changed

‎src/Relation/Binary/Domain/Bundles.agda

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Bundles for domain theory
5+
------------------------------------------------------------------------
6+
7+
module Relation.Binary.Domain.Bundles where
8+
9+
open import Relation.Binary.Bundles using (Poset)
10+
open import Relation.Binary.Core using (Rel)
11+
open import Level using (Level; _⊔_; suc; Lift; lift; lower)
12+
open import Function using (_∘_; id)
13+
open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
14+
open import Relation.Unary using (Pred)
15+
open import Relation.Binary.PropositionalEquality using (_≡_; subst; cong)
16+
open import Relation.Binary.Reasoning.PartialOrder
17+
open import Relation.Binary.Structures
18+
open import Data.Bool using (Bool; true; false; if_then_else_)
19+
open import Relation.Binary.Morphism.Structures
20+
open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
21+
open import Data.Nat.Properties using (≤-trans)
22+
23+
open import Relation.Binary.Domain.Structures
24+
open import Relation.Binary.Domain.Definitions
25+
26+
private variable
27+
o ℓ e o' ℓ' e' ℓ₂ : Level
28+
Ix A B : Set o
29+
module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
30+
open Poset P
31+
32+
record Lub {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
33+
constructor mkLub
34+
field
35+
lub : Carrier
36+
is-upperbound : ∀ i → s i ≤ lub
37+
is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
38+
39+
record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
40+
field
41+
poset : Poset c ℓ₁ ℓ₂
42+
DcpoStr : IsDCPO poset
43+
44+
open Poset poset public
45+
open IsDCPO DcpoStr public
46+
47+
module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
48+
49+
private
50+
module P = Poset P
51+
module Q = Poset Q
52+
53+
-- record ScottContinuous : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
54+
-- field
55+
-- Function : (f : P.Carrier → Q.Carrier)
56+
-- Scottfunciton : IsScottContinuous f
57+

‎src/Relation/Binary/Domain/Definitions.agda

Lines changed: 4 additions & 208 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
------------------------------------------------------------------------
22
-- The Agda standard library
33
--
4-
-- Defintions for domain theory
4+
-- Definitions for domain theory
55
------------------------------------------------------------------------
66

77
module Relation.Binary.Domain.Definitions where
@@ -14,15 +14,14 @@ open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
1414
open import Relation.Unary using (Pred)
1515
open import Relation.Binary.PropositionalEquality using (_≡_; subst; cong)
1616
open import Relation.Binary.Reasoning.PartialOrder
17-
open import Relation.Binary.Structures
18-
open import Data.Bool using (Bool; true; false; if_then_else_)
1917
open import Relation.Binary.Morphism.Structures
2018
open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
2119
open import Data.Nat.Properties using (≤-trans)
2220

2321
private variable
24-
o ℓ e o' ℓ' e' ℓ₂ : Level
22+
c o ℓ e o' ℓ' e' ℓ₂ : Level
2523
Ix A B : Set o
24+
P : Poset c ℓ e
2625

2726
module _ where
2827
IsMonotone : (P : Poset o ℓ e) → (Q : Poset o' ℓ' e') → (f : Poset.Carrier P → Poset.Carrier Q) → Set (o ⊔ ℓ ⊔ e ⊔ ℓ' ⊔ e')
@@ -33,207 +32,4 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
3332

3433
IsSemidirectedFamily : ∀ {Ix : Set c} → (s : Ix → Carrier) → Set _
3534
IsSemidirectedFamily s = ∀ i j → ∃[ k ] (s i ≤ s k × s j ≤ s k)
36-
37-
record IsDirectedFamily {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
38-
no-eta-equality
39-
field
40-
elt : Ix
41-
SemiDirected : IsSemidirectedFamily s
42-
43-
record IsLub {Ix : Set c} (s : Ix → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
44-
field
45-
is-upperbound : ∀ i → s i ≤ lub
46-
is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
47-
48-
record Lub {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
49-
constructor mkLub
50-
field
51-
lub : Carrier
52-
is-upperbound : ∀ i → s i ≤ lub
53-
is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
54-
55-
record IsDCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
56-
field
57-
⋁ : ∀ {Ix : Set c}
58-
→ (s : Ix → Carrier)
59-
→ IsDirectedFamily s
60-
→ Carrier
61-
⋁-isLub : ∀ {Ix : Set c}
62-
→ (s : Ix → Carrier)
63-
→ (dir : IsDirectedFamily s)
64-
→ IsLub s (⋁ s dir)
65-
66-
module _ {Ix : Set c} {s : Ix → Carrier} {dir : IsDirectedFamily s} where
67-
open IsLub (⋁-isLub s dir)
68-
renaming (is-upperbound to ⋁-≤; is-least to ⋁-least)
69-
public
70-
71-
record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
72-
field
73-
poset : Poset c ℓ₁ ℓ₂
74-
DcpoStr : IsDCPO poset
75-
76-
open Poset poset public
77-
open IsDCPO DcpoStr public
78-
79-
module _ {c ℓ₁ ℓ₂} (D : DCPO c ℓ₁ ℓ₂) where
80-
private
81-
module D = DCPO D
82-
83-
uniqueLub : ∀ {Ix} {s : Ix → D.Carrier}
84-
→ (x y : D.Carrier) → IsLub D.poset s x → IsLub D.poset s y
85-
→ x D.≈ y
86-
uniqueLub x y x-lub y-lub = D.antisym
87-
(IsLub.is-least x-lub y (IsLub.is-upperbound y-lub))
88-
(IsLub.is-least y-lub x (IsLub.is-upperbound x-lub))
89-
90-
is-lub-cong : ∀ {Ix} {s : Ix → D.Carrier}
91-
→ (x y : D.Carrier)
92-
→ x D.≈ y
93-
→ IsLub D.poset s x → IsLub D.poset s y
94-
is-lub-cong x y x≈y x-lub = record
95-
{ is-upperbound = λ i → D.trans (IsLub.is-upperbound x-lub i) (D.reflexive x≈y)
96-
; is-least = λ z ub → D.trans (D.reflexive (D.Eq.sym x≈y)) (IsLub.is-least x-lub z (λ i → D.trans (ub i) (D.reflexive D.Eq.refl)))
97-
}
98-
99-
100-
module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
101-
102-
private
103-
module P = Poset P
104-
module Q = Poset Q
105-
106-
record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
107-
field
108-
PreserveLub : ∀ {Ix : Set c} {s : Ix → P.Carrier}
109-
→ (dir : IsDirectedFamily P s)
110-
→ (lub : P.Carrier)
111-
→ IsLub P s lub
112-
→ IsLub Q (f ∘ s) (f lub)
113-
PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y
114-
115-
dcpo+scott→monotone : (P-dcpo : IsDCPO P)
116-
→ (f : P.Carrier → Q.Carrier)
117-
→ (scott : IsScottContinuous f)
118-
→ IsMonotone P Q f
119-
dcpo+scott→monotone P-dcpo f scott = record
120-
{ cong = λ {x} {y} x≈y → IsScottContinuous.PreserveEquality scott x≈y
121-
; mono = λ {x} {y} x≤y → mono-proof x y x≤y
122-
}
123-
where
124-
mono-proof : ∀ x y → x P.≤ y → f x Q.≤ f y
125-
mono-proof x y x≤y = IsLub.is-upperbound fs-lub (lift true)
126-
where
127-
s : Lift c Bool → P.Carrier
128-
s (lift b) = if b then x else y
129-
130-
sx≤sfalse : ∀ b → s b P.≤ s (lift false)
131-
sx≤sfalse (lift true) = x≤y
132-
sx≤sfalse (lift false) = P.refl
133-
134-
s-directed : IsDirectedFamily P s
135-
s-directed = record
136-
{ elt = lift true
137-
; SemiDirected = λ i j → (lift false , sx≤sfalse i , sx≤sfalse j)
138-
}
139-
140-
s-lub : IsLub P s y
141-
s-lub = record
142-
{ is-upperbound = sx≤sfalse
143-
; is-least = λ z proof → proof (lift false)
144-
}
145-
146-
fs-lub : IsLub Q (f ∘ s) (f y)
147-
fs-lub = IsScottContinuous.PreserveLub scott s-directed y s-lub
148-
149-
150-
monotone∘directed : ∀ {Ix : Set c} {s : Ix → P.Carrier}
151-
→ (f : P.Carrier → Q.Carrier)
152-
→ IsMonotone P Q f
153-
→ IsDirectedFamily P s
154-
→ IsDirectedFamily Q (f ∘ s)
155-
monotone∘directed f ismonotone dir = record
156-
{ elt = IsDirectedFamily.elt dir
157-
; SemiDirected = λ i j →
158-
let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.SemiDirected dir i j
159-
in k , IsOrderHomomorphism.mono ismonotone s[i]≤s[k] , IsOrderHomomorphism.mono ismonotone s[j]≤s[k]
160-
}
161-
162-
module _ where
163-
164-
ScottId : ∀ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} → IsScottContinuous {P = P} {Q = P} id
165-
ScottId = record
166-
{ PreserveLub = λ dir lub z → z
167-
; PreserveEquality = λ z → z }
168-
169-
scott-∘ : ∀ {c ℓ₁ ℓ₂} {P Q R : Poset c ℓ₁ ℓ₂}
170-
→ (f : Poset.Carrier R → Poset.Carrier Q) (g : Poset.Carrier P → Poset.Carrier R)
171-
→ IsScottContinuous {P = R} {Q = Q} f → IsScottContinuous {P = P} {Q = R} g
172-
→ IsMonotone R Q f → IsMonotone P R g
173-
→ IsScottContinuous {P = P} {Q = Q} (f ∘ g)
174-
scott-∘ f g scottf scottg monof monog = record
175-
{ PreserveLub = λ dir lub z → f.PreserveLub
176-
(monotone∘directed g monog dir)
177-
(g lub)
178-
(g.PreserveLub dir lub z)
179-
; PreserveEquality = λ {x} {y} z →
180-
f.PreserveEquality (g.PreserveEquality z)
181-
}
182-
where
183-
module f = IsScottContinuous scottf
184-
module g = IsScottContinuous scottg
185-
186-
module _ {c ℓ₁ ℓ₂} (D : DCPO c ℓ₁ ℓ₂) (let module D = DCPO D) where
187-
open DCPO D
188-
189-
open import Relation.Binary.Reasoning.PartialOrder poset public
190-
191-
⋃-pointwise : ∀ {Ix} {s s' : Ix → Carrier}
192-
→ {fam : IsDirectedFamily poset s} {fam' : IsDirectedFamily poset s'}
193-
→ (∀ ix → s ix ≤ s' ix)
194-
→ ⋁ s fam ≤ ⋁ s' fam'
195-
⋃-pointwise {s = s} {s'} {fam} {fam'} p =
196-
⋁-least (⋁ s' fam') λ i → trans (p i) (⋁-≤ i)
197-
198-
module Scott
199-
{c ℓ₁ ℓ₂}
200-
{D E : DCPO c ℓ₁ ℓ₂}
201-
(let module D = DCPO D)
202-
(let module E = DCPO E)
203-
(f : D.Carrier → E.Carrier)
204-
(isScott : IsScottContinuous {P = D.poset} {Q = E.poset} f)
205-
(mono : IsMonotone D.poset E.poset f) where
206-
207-
open DCPO D
208-
open DCPO E
209-
210-
pres-⋁
211-
: ∀ {Ix} (s : Ix → D.Carrier) → (dir : IsDirectedFamily D.poset s)
212-
→ f (D.⋁ s dir) E.≈ E.⋁ (f ∘ s) (monotone∘directed f mono dir)
213-
pres-⋁ s dir = E.antisym
214-
(IsLub.is-least
215-
(IsScottContinuous.PreserveLub isScott dir (D.⋁ s dir) (D.⋁-isLub s dir))
216-
(E.⋁ (f ∘ s) (monotone∘directed f mono dir))
217-
E.⋁-≤
218-
)
219-
(IsLub.is-least
220-
(E.⋁-isLub (f ∘ s) (monotone∘directed f mono dir))
221-
(f (D.⋁ s dir))
222-
(λ i → IsOrderHomomorphism.mono mono (D.⋁-≤ i))
223-
)
224-
225-
226-
227-
module _ {c ℓ₁ ℓ₂} (D E : DCPO c ℓ₁ ℓ₂) where
228-
private
229-
module D = DCPO D
230-
module E = DCPO E
231-
232-
to-scott : (f : D.Carrier → E.Carrier) → IsMonotone D.poset E.poset f
233-
→ (∀ {Ix} (s : Ix → D.Carrier) (dir : IsDirectedFamily D.poset s) →
234-
IsLub E.poset (f ∘ s) (f (D.⋁ s dir))) → IsScottContinuous {P = D.poset} {Q = E.poset} f
235-
to-scott f mono pres-⋁ = record
236-
{ PreserveLub = λ dir lub x → is-lub-cong E (f (D.⋁ _ dir)) (f lub)
237-
(IsOrderHomomorphism.cong mono (uniqueLub D (D.⋁ _ dir) lub (D.⋁-isLub _ dir) x))
238-
(pres-⋁ _ dir)
239-
; PreserveEquality = IsOrderHomomorphism.cong mono }
35+

‎src/Relation/Binary/Domain/Structures.agda

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Structures for domain theory
5+
------------------------------------------------------------------------
6+
7+
module Relation.Binary.Domain.Structures where
8+
9+
open import Relation.Binary.Bundles using (Poset)
10+
open import Relation.Binary.Core using (Rel)
11+
open import Level using (Level; _⊔_; suc; Lift; lift; lower)
12+
open import Function using (_∘_; id)
13+
open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
14+
open import Relation.Unary using (Pred)
15+
open import Relation.Binary.PropositionalEquality using (_≡_; subst; cong)
16+
open import Relation.Binary.Reasoning.PartialOrder
17+
open import Relation.Binary.Structures
18+
open import Data.Bool using (Bool; true; false; if_then_else_)
19+
open import Relation.Binary.Morphism.Structures
20+
open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
21+
open import Data.Nat.Properties using (≤-trans)
22+
open import Relation.Binary.Domain.Definitions
23+
24+
private variable
25+
o ℓ e o' ℓ' e' ℓ₂ : Level
26+
Ix A B : Set o
27+
28+
module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
29+
open Poset P
30+
31+
record IsDirectedFamily {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
32+
no-eta-equality
33+
field
34+
elt : Ix
35+
SemiDirected : IsSemidirectedFamily P s
36+
37+
record IsLub {Ix : Set c} (s : Ix → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
38+
field
39+
is-upperbound : ∀ i → s i ≤ lub
40+
is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
41+
42+
record IsDCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
43+
field
44+
⋁ : ∀ {Ix : Set c}
45+
→ (s : Ix → Carrier)
46+
→ IsDirectedFamily s
47+
→ Carrier
48+
⋁-isLub : ∀ {Ix : Set c}
49+
→ (s : Ix → Carrier)
50+
→ (dir : IsDirectedFamily s)
51+
→ IsLub s (⋁ s dir)
52+
53+
module _ {Ix : Set c} {s : Ix → Carrier} {dir : IsDirectedFamily s} where
54+
open IsLub (⋁-isLub s dir)
55+
renaming (is-upperbound to ⋁-≤; is-least to ⋁-least)
56+
public
57+
58+
module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
59+
60+
private
61+
module P = Poset P
62+
module Q = Poset Q
63+
64+
record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
65+
field
66+
PreserveLub : ∀ {Ix : Set c} {s : Ix → P.Carrier}
67+
→ (dir : IsDirectedFamily P s)
68+
→ (lub : P.Carrier)
69+
→ IsLub P s lub
70+
→ IsLub Q (f ∘ s) (f lub)
71+
PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y

0 commit comments

Comments
 (0)