Skip to content

Commit 8142340

Browse files
jmougeotjmougeot
committed
module scott
1 parent ee5d9c1 commit 8142340

File tree

1 file changed

+87
-46
lines changed

1 file changed

+87
-46
lines changed

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

Lines changed: 87 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -33,17 +33,43 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
3333
elt : Ix
3434
SemiDirected : IsSemidirectedFamily s
3535

36+
record IsLub {Ix : Set c} (s : Ix → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
37+
field
38+
is-upperbound : ∀ i → s i ≤ lub
39+
is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
40+
41+
record Lub {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
42+
constructor mkLub
43+
field
44+
lub : Carrier
45+
is-upperbound : ∀ i → s i ≤ lub
46+
is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y
47+
3648
record IsDCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
3749
field
38-
HasDirectedLub : ∀ {Ix : Set c} {s : Ix → Carrier}
50+
⋁ : ∀ {Ix : Set c}
51+
→ (s : Ix → Carrier)
3952
→ IsDirectedFamily s
40-
→ ∃[ lub ] ((∀ i → s i ≤ lub) × ∀ y → (∀ i → s i ≤ y) → lub ≤ y)
53+
→ Carrier
54+
⋁-isLub : ∀ {Ix : Set c}
55+
→ (s : Ix → Carrier)
56+
→ (dir : IsDirectedFamily s)
57+
→ IsLub s (⋁ s dir)
58+
59+
module _ {Ix : Set c} {s : Ix → Carrier} {dir : IsDirectedFamily s} where
60+
open IsLub (⋁-isLub s dir)
61+
renaming (is-upperbound to ⋁-≤; is-least to ⋁-least)
62+
public
63+
4164

4265
record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
4366
field
4467
poset : Poset c ℓ₁ ℓ₂
4568
DcpoStr : IsDCPO poset
4669

70+
open Poset poset public
71+
open IsDCPO DcpoStr public
72+
4773
module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
4874

4975
private
@@ -54,8 +80,9 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ
5480
field
5581
PreserveLub : ∀ {Ix : Set c} {s : Ix → P.Carrier}
5682
→ (dir-s : IsDirectedFamily P s)
57-
→ ∀ lub → ((∀ i → s i P.≤ lub) × ∀ y → (∀ i → s i P.≤ y) → lub P.≤ y)
58-
→ ((∀ i → f (s i) Q.≤ f lub) × ∀ y → (∀ i → f (s i) Q.≤ y) → f lub Q.≤ y)
83+
→ (lub : P.Carrier)
84+
→ IsLub P s lub
85+
→ IsLub Q (f ∘ s) (f lub)
5986
PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y
6087

6188
dcpo+scott→monotone : (P-dcpo : IsDCPO P)
@@ -68,7 +95,7 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ
6895
}
6996
where
7097
mono-proof : ∀ x y → x P.≤ y → f x Q.≤ f y
71-
mono-proof x y x≤y = proj₁ fs-lub (lift true)
98+
mono-proof x y x≤y = IsLub.is-upperbound fs-lub (lift true)
7299
where
73100
s : Lift c Bool → P.Carrier
74101
s (lift b) = if b then x else y
@@ -82,12 +109,16 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ
82109
{ elt = lift true
83110
; SemiDirected = λ i j → (lift false , sx≤sfalse i , sx≤sfalse j)
84111
}
112+
113+
s-lub : IsLub P s y
114+
s-lub = record
115+
{ is-upperbound = sx≤sfalse
116+
; is-least = λ z proof → proof (lift false)
117+
}
118+
119+
fs-lub : IsLub Q (f ∘ s) (f y)
120+
fs-lub = IsScottContinuous.PreserveLub scott s-directed y s-lub
85121

86-
s-lub : P.Carrier × ((∀ i → s i P.≤ y) × (∀ z → (∀ i → s i P.≤ z) → y P.≤ z))
87-
s-lub = y , (sx≤sfalse , λ z lt → lt (lift false))
88-
89-
fs-lub = IsScottContinuous.PreserveLub scott
90-
s-directed y (sx≤sfalse , λ z lt → lt (lift false))
91122

92123
monotone∘directed : ∀ {Ix : Set c} {s : Ix → P.Carrier}
93124
→ (f : P.Carrier → Q.Carrier)
@@ -114,51 +145,61 @@ module _ where
114145
→ IsMonotone R Q f → IsMonotone P R g
115146
→ IsScottContinuous {P = P} {Q = Q} (f ∘ g)
116147
scott-∘ f g scottf scottg monotonef monotoneg = record
117-
{ PreserveLub = λ dir-s lub z → IsScottContinuous.PreserveLub scottf
118-
(monotone∘directed g monotoneg dir-s)
119-
(g lub) ( IsScottContinuous.PreserveLub scottg dir-s lub z)
120-
; PreserveEquality = λ {x} {y} z → IsScottContinuous.PreserveEquality scottf
121-
(IsScottContinuous.PreserveEquality scottg z)
148+
{ PreserveLub = λ dir-s lub z → f.PreserveLub
149+
(monotone∘directed g monotoneg dir-s)
150+
(g lub)
151+
(g.PreserveLub dir-s lub z)
152+
; PreserveEquality = λ {x} {y} z →
153+
f.PreserveEquality (g.PreserveEquality z)
122154
}
155+
where
156+
module f = IsScottContinuous scottf
157+
module g = IsScottContinuous scottg
123158

124-
-- Module for the DCPO record
125-
module _ {c ℓ₁ ℓ₂} (D : DCPO c ℓ₁ ℓ₂) where
126-
open DCPO D public
159+
module _ {c ℓ₁ ℓ₂} (D : DCPO c ℓ₁ ℓ₂) (let module D = DCPO D) where
160+
open DCPO D
127161

128-
posetD : Poset c ℓ₁ ℓ₂
129-
posetD = poset
130-
131-
open Poset posetD
132-
open import Relation.Binary.Reasoning.PartialOrder posetD public
133-
134-
dcpoD : IsDCPO posetD
135-
dcpoD = DcpoStr
136-
137-
⋃ : ∀ {Ix : Set c} (s : Ix → Carrier) → (dir : IsDirectedFamily posetD s) → Carrier
138-
⋃ s dir = proj₁ (IsDCPO.HasDirectedLub dcpoD dir)
139-
140-
module ⋃ {Ix : Set c} (s : Ix → Carrier) (dir : IsDirectedFamily posetD s) where
141-
fam≤lub : ∀ ix → s ix ≤ ⋃ s dir
142-
fam≤lub ix = proj₁ (proj₂ (IsDCPO.HasDirectedLub dcpoD dir)) ix
143-
144-
least : ∀ ub → (∀ ix → s ix ≤ ub) → ⋃ s dir ≤ ub
145-
least ub p = proj₂ (proj₂ (IsDCPO.HasDirectedLub dcpoD dir)) ub p
162+
open import Relation.Binary.Reasoning.PartialOrder poset public
146163

147164
⋃-pointwise : ∀ {Ix} {s s' : Ix → Carrier}
148-
→ {fam : IsDirectedFamily posetD s} {fam' : IsDirectedFamily posetD s'}
165+
→ {fam : IsDirectedFamily poset s} {fam' : IsDirectedFamily poset s'}
149166
→ (∀ ix → s ix ≤ s' ix)
150-
→ ⋃ s fam ≤ ⋃ s' fam'
151-
⋃-pointwise {s = s} {s'} {fam} {fam'} p = ⋃.least s fam (⋃ s' fam') λ ix →
152-
trans (p ix) (⋃.fam≤lub s' fam' ix)
153-
154-
module Scott {c} {ℓ₁} {ℓ₂} {D E : DCPO c ℓ₁ ℓ₂}
155-
(f : Poset.Carrier (DCPO.poset D) → Poset.Carrier (DCPO.poset E))
156-
(mono : IsMonotone (DCPO.poset D) (DCPO.poset E) f) where``
167+
→ ⋁ s fam ≤ ⋁ s' fam'
168+
⋃-pointwise {s = s} {s'} {fam} {fam'} p =
169+
⋁-least (⋁ s' fam') λ i → trans (p i) (⋁-≤ i)
170+
171+
module Scott
172+
{c ℓ₁ ℓ₂}
173+
{D E : DCPO c ℓ₁ ℓ₂}
174+
(let module D = DCPO D)
175+
(let module E = DCPO E)
176+
(f : D.Carrier → E.Carrier)
177+
(mono : IsMonotone D.poset E.poset f) where
178+
179+
res-directed-lub : ∀ {Ix} (s : Ix → D.Carrier)
180+
→ IsDirectedFamily D.poset s
181+
→ ∀ x → IsLub D.poset s x
182+
→ IsLub E.poset (f ∘ s) (f x)
183+
res-directed-lub s dir x lub = {! !}
184+
185+
directed : ∀ {Ix} {s : Ix → D.Carrier} → IsDirectedFamily D.poset s → IsDirectedFamily E.poset (f ∘ s)
186+
directed = monotone∘directed f mono
187+
188+
pres-⋃
189+
: ∀ {Ix} (s : Ix → D.Carrier) → (dir : IsDirectedFamily D.poset s)
190+
→ f (D.⋁ s dir) ≡ E.⋁ (f ∘ s) (monotone∘directed f mono dir)
191+
pres-⋃ s dir = {! !}
157192

193+
module _ {c ℓ₁ ℓ₂} (D E : DCPO c ℓ₁ ℓ₂) where
158194
private
159195
module D = DCPO D
160196
module E = DCPO E
161197

162-
pres-directed-lub : ∀ {Ix} (s : Ix → Carrier) → is-directed-family D.poset s
163-
→ ∀ x → is-lub (D .fst) s x → is-lub (E .fst) (apply f ⊙ s) (f · x)
198+
to-scott : (f : D.Carrier → E.Carrier) → IsMonotone D.poset E.poset f
199+
→ (∀ {Ix} (s : Ix → D.Carrier) (dir : IsDirectedFamily D.poset s) →
200+
IsLub E.poset (f ∘ s) (f (D.⋁ s dir))) → IsScottContinuous {P = D.poset} {Q = E.poset} f
201+
to-scott f monotone pres-⋃ = {! !}
164202

203+
-- res-lub : ∀ {Ix} (s : Ix → D.Carrier) → (dir : is-directed-family D.poset s)
204+
-- → ∀ x → is-lub D.poset s x → is-lub E.poset (f ⊙ s) (f x)
205+
-- pres-lub s dir x x-lub .is-lub.fam≤lub i = ?

0 commit comments

Comments
 (0)