mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Compare commits
2 commits
031df0312d
...
8caee3929a
| Author | SHA1 | Date | |
|---|---|---|---|
8caee3929a
|
|||
|
cc0cb9cd18
|
8 changed files with 371 additions and 145 deletions
|
|
@ -176,10 +176,10 @@ open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼
|
|||
|
||||
|
||||
module DelayMonad where
|
||||
Delayₛ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
|
||||
Delayₛ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } }
|
||||
Delayₛ∼ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
|
||||
Delayₛ∼ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } }
|
||||
Delay≈ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
|
||||
Delay≈ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } }
|
||||
Delay∼ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
|
||||
Delay∼ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } }
|
||||
<_> = _⟨$⟩_
|
||||
open _⟶_ using (cong)
|
||||
|
||||
|
|
@ -220,10 +220,10 @@ module DelayMonad where
|
|||
lift-cong {A} {B} f {later x} {later y} (later≈ x≈y) = later≈ (lift-cong′ {A} {B} f x≈y)
|
||||
force≈ (lift-cong′ {A} {B} f {x} {y} x≈y) = lift-cong f (force≈ x≈y)
|
||||
|
||||
liftFₛ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delayₛ A ⟶ Delayₛ B
|
||||
liftFₛ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delay≈ A ⟶ Delay≈ B
|
||||
liftFₛ {A} {B} f = record { to = liftF < f > ; cong = lift-cong f }
|
||||
|
||||
liftFₛ∼ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delayₛ∼ A ⟶ Delayₛ∼ B
|
||||
liftFₛ∼ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delay∼ A ⟶ Delay∼ B
|
||||
liftFₛ∼ {A} {B} f = record { to = liftF < f > ; cong = ∼-cong }
|
||||
where
|
||||
∼-cong : ∀ {x y} → [ A ][ x ∼ y ] → [ B ][ liftF < f > x ∼ liftF < f > y ]
|
||||
|
|
@ -258,7 +258,7 @@ module DelayMonad where
|
|||
later-eq {A} {x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ a≡b x↓a (now↓ y≡b)
|
||||
later-eq {A} {x} {later y} x≈ly = ≈-trans A later-self x≈ly
|
||||
|
||||
lift-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (liftFₛ (idₛ A)) ≋ (idₛ (Delayₛ A))
|
||||
lift-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (liftFₛ (idₛ A)) ≋ (idₛ (Delay≈ A))
|
||||
lift-id′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} → [ A ][ (liftF id) x ≈′ id x ]
|
||||
lift-id {A} {now x} = ≈-refl A
|
||||
lift-id {A} {later x} = later≈ lift-id′
|
||||
|
|
@ -276,7 +276,7 @@ module DelayMonad where
|
|||
lift-resp-≈ {A} {B} {f} {g} f≋g {later x} = later≈ (lift-resp-≈′ {A} {B} {f} {g} f≋g)
|
||||
force≈ (lift-resp-≈′ {A} {B} {f} {g} f≋g {x}) = lift-resp-≈ {A} {B} {f} {g} f≋g
|
||||
|
||||
ηₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ Delayₛ A
|
||||
ηₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ Delay≈ A
|
||||
ηₛ A = record { to = now ; cong = now-cong }
|
||||
|
||||
η-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (ηₛ B ∘ f) ≋ (liftFₛ f ∘ ηₛ A)
|
||||
|
|
@ -288,35 +288,35 @@ module DelayMonad where
|
|||
μ {A} (now x) = x
|
||||
μ {A} (later x) = later (μ′ {A} x)
|
||||
|
||||
μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} {b : ∣ A ∣} → [ Delayₛ A ][ x ↓ y ] → [ A ][ y ↓ b ] → [ A ][ (μ {A} x) ↓ b ]
|
||||
μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} {b : ∣ A ∣} → [ Delay≈ A ][ x ↓ y ] → [ A ][ y ↓ b ] → [ A ][ (μ {A} x) ↓ b ]
|
||||
μ↓-trans {A} {now x} {y} {b} (now↓ x≡y) y↓b = ≈↓ A (≈-sym A x≡y) y↓b
|
||||
μ↓-trans {A} {later x} {now y} {b} (later↓ x↓y) (now↓ y≡b) = later↓ (μ↓-trans x↓y (now↓ y≡b))
|
||||
μ↓-trans {A} {later x} {later y} {b} (later↓ x↓y) (later↓ y↓b) = later↓ (μ↓-trans (≡↓ (Delayₛ A) (≈-sym A later-self) x↓y) y↓b)
|
||||
μ↓-trans {A} {later x} {later y} {b} (later↓ x↓y) (later↓ y↓b) = later↓ (μ↓-trans (≡↓ (Delay≈ A) (≈-sym A later-self) x↓y) y↓b)
|
||||
|
||||
μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delayₛ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈ y ]
|
||||
μ↓′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delayₛ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈′ y ]
|
||||
μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delay≈ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈ y ]
|
||||
μ↓′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delay≈ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈′ y ]
|
||||
force≈ (μ↓′ {A} {x} {y} x↓y) = μ↓ x↓y
|
||||
μ↓ {A} {now x} {y} (now↓ x≡y) = x≡y
|
||||
μ↓ {A} {later x} {now y} (later↓ x↓y) = ≈-trans A (≈-sym A later-self) (↓≈ (≡-refl A) (μ↓-trans x↓y (now↓ (≡-refl A))) (now↓ (≡-refl A)))
|
||||
μ↓ {A} {later x} {later y} (later↓ x↓y) = later≈ (μ↓′ {A} {force x} {force y} (≡↓ (Delayₛ A) (≈-sym A later-self) x↓y))
|
||||
μ↓ {A} {later x} {later y} (later↓ x↓y) = later≈ (μ↓′ {A} {force x} {force y} (≡↓ (Delay≈ A) (≈-sym A later-self) x↓y))
|
||||
|
||||
μ-cong : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ A ][ x ≈ y ] → [ A ][ μ {A} x ≈ μ {A} y ]
|
||||
μ-cong′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ A ][ x ≈′ y ] → [ A ][ μ {A} x ≈′ μ {A} y ]
|
||||
μ-cong : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delay≈ A ][ x ≈ y ] → [ A ][ μ {A} x ≈ μ {A} y ]
|
||||
μ-cong′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delay≈ A ][ x ≈′ y ] → [ A ][ μ {A} x ≈′ μ {A} y ]
|
||||
μ-cong A {now x} {now y} x≈y = now-inj x≈y
|
||||
μ-cong A {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ≈-trans A (≈-sym A (μ↓ (≡↓ (Delayₛ A) (≈-trans A (≈-sym A a≡b) (≈-sym A x≡a)) y↓b))) later-self
|
||||
μ-cong A {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ≈-trans A (≈-sym A later-self) (μ↓ (≡↓ (Delayₛ A) (≈-trans A a≡b (≈-sym A y≡b)) x↓a))
|
||||
μ-cong A {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (μ-cong′ A (≈→≈′ (Delayₛ A) (↓≈ a≡b x↓a y↓b)))
|
||||
μ-cong A {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ≈-trans A (≈-sym A (μ↓ (≡↓ (Delay≈ A) (≈-trans A (≈-sym A a≡b) (≈-sym A x≡a)) y↓b))) later-self
|
||||
μ-cong A {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ≈-trans A (≈-sym A later-self) (μ↓ (≡↓ (Delay≈ A) (≈-trans A a≡b (≈-sym A y≡b)) x↓a))
|
||||
μ-cong A {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (μ-cong′ A (≈→≈′ (Delay≈ A) (↓≈ a≡b x↓a y↓b)))
|
||||
μ-cong A {later x} {later y} (later≈ x≈y) = later≈ (μ-cong′ A x≈y)
|
||||
force≈ (μ-cong′ A {x} {y} x≈y) = μ-cong A (force≈ x≈y)
|
||||
|
||||
μₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delayₛ (Delayₛ A) ⟶ Delayₛ A
|
||||
μₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delay≈ (Delay≈ A) ⟶ Delay≈ A
|
||||
μₛ A = record { to = μ {A} ; cong = μ-cong A }
|
||||
|
||||
μₛ∼ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delayₛ∼ (Delayₛ∼ A) ⟶ Delayₛ∼ A
|
||||
μₛ∼ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delay∼ (Delay∼ A) ⟶ Delay∼ A
|
||||
μₛ∼ A = record { to = μ {A} ; cong = μ-cong∼ A }
|
||||
where
|
||||
μ-cong∼ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ∼ A ][ x ∼ y ] → [ A ][ μ {A} x ∼ μ {A} y ]
|
||||
μ-cong∼′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ∼ A ][ x ∼′ y ] → [ A ][ μ {A} x ∼′ μ {A} y ]
|
||||
μ-cong∼ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delay∼ A ][ x ∼ y ] → [ A ][ μ {A} x ∼ μ {A} y ]
|
||||
μ-cong∼′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delay∼ A ][ x ∼′ y ] → [ A ][ μ {A} x ∼′ μ {A} y ]
|
||||
force∼ (μ-cong∼′ A {x} {y} x∼y) = μ-cong∼ A (force∼ x∼y)
|
||||
μ-cong∼ A {.(now _)} {.(now _)} (now∼ x∼y) = x∼y
|
||||
μ-cong∼ A {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (μ-cong∼′ A x∼y)
|
||||
|
|
@ -327,13 +327,13 @@ module DelayMonad where
|
|||
μ-natural {A} {B} f {now x} = ≈-refl B
|
||||
μ-natural {A} {B} f {later x} = later≈ (μ-natural′ f {force x})
|
||||
|
||||
μ-assoc' : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼ (μₛ A ∘ μₛ (Delayₛ A)) ⟨$⟩ x ]
|
||||
μ-assoc'′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼′ (μₛ A ∘ μₛ (Delayₛ A)) ⟨$⟩ x ]
|
||||
μ-assoc' : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼ (μₛ A ∘ μₛ (Delay≈ A)) ⟨$⟩ x ]
|
||||
μ-assoc'′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼′ (μₛ A ∘ μₛ (Delay≈ A)) ⟨$⟩ x ]
|
||||
force∼ (μ-assoc'′ {A} {x}) = μ-assoc' {A} {x}
|
||||
μ-assoc' {A} {now x} = ∼-refl A
|
||||
μ-assoc' {A} {later x} = later∼ (μ-assoc'′ {A} {force x})
|
||||
|
||||
μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ (liftFₛ (μₛ A))) ≋ (μₛ A ∘ μₛ (Delayₛ A))
|
||||
μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ (liftFₛ (μₛ A))) ≋ (μₛ A ∘ μₛ (Delay≈ A))
|
||||
μ-assoc {A} {x} = ∼⇒≈ (μ-assoc' {A} {x})
|
||||
|
||||
identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} {y : ∣ A ∣} → [ A ][ x ↓ y ] → [ A ][ ((μₛ A) ⟨$⟩ ((liftFₛ (ηₛ A)) ⟨$⟩ x)) ↓ y ]
|
||||
|
|
@ -346,20 +346,20 @@ module DelayMonad where
|
|||
identityˡ∼ {A} {later x} = later∼ identityˡ∼′
|
||||
force∼ (identityˡ∼′ {A} {x}) = identityˡ∼
|
||||
|
||||
identityˡ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ liftFₛ (ηₛ A)) ≋ idₛ (Delayₛ A)
|
||||
identityˡ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ liftFₛ (ηₛ A)) ≋ idₛ (Delay≈ A)
|
||||
identityˡ′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} → [ A ][ (μₛ A ∘ liftFₛ (ηₛ A)) ⟨$⟩ x ≈′ x ]
|
||||
force≈ (identityˡ′ {A} {x}) = identityˡ
|
||||
identityˡ {A} {now x} = ≈-refl A
|
||||
identityˡ {A} {later x} = later≈ identityˡ′
|
||||
|
||||
identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ ηₛ (Delayₛ A)) ≋ idₛ (Delayₛ A)
|
||||
identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ ηₛ (Delay≈ A)) ≋ idₛ (Delay≈ A)
|
||||
identityʳ {A} {now x} = ≈-refl A
|
||||
identityʳ {A} {later x} = ≈-refl A
|
||||
|
||||
delayMonad : Monad (Setoids c (c ⊔ ℓ))
|
||||
delayMonad = record
|
||||
{ F = record
|
||||
{ F₀ = Delayₛ
|
||||
{ F₀ = Delay≈
|
||||
; F₁ = liftFₛ
|
||||
; identity = lift-id
|
||||
; homomorphism = λ {X} {Y} {Z} {f} {g} → lift-comp {X} {Y} {Z} {f} {g}
|
||||
|
|
@ -433,7 +433,7 @@ module extra {A : Setoid c (c ⊔ ℓ)} where
|
|||
ι (x , zero) = now x
|
||||
ι (x , suc n) = later (ι′ (x , n))
|
||||
|
||||
ιₛ' : (A ×ₛ (ℕ-setoid {c})) ⟶ Delayₛ∼ A
|
||||
ιₛ' : (A ×ₛ (ℕ-setoid {c})) ⟶ Delay∼ A
|
||||
ιₛ' = record { to = ι ; cong = ι-cong }
|
||||
where
|
||||
ι-cong : ∀ {x y} → [ A ×ₛ (ℕ-setoid {c}) ][ x ≡ y ] → [ A ][ ι x ∼ ι y ]
|
||||
|
|
|
|||
|
|
@ -76,8 +76,8 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
helper : [ Y ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
|
||||
helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y
|
||||
|
||||
iter-cong∼ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼ (iter {A} {X} < f > y) ]
|
||||
iter-cong∼′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼′ (iter {A} {X} < f > y) ]
|
||||
iter-cong∼ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delay∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼ (iter {A} {X} < f > y) ]
|
||||
iter-cong∼′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delay∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼′ (iter {A} {X} < f > y) ]
|
||||
force∼ (iter-cong∼′ {A} {X} f {x} {y} x≡y) = iter-cong∼ f x≡y
|
||||
iter-cong∼ {A} {X} f {x} {y} x≡y with < f > x in eqx | < f > y in eqy
|
||||
... | inj₁ a | inj₁ b = inj₁-helper f x≡y eqx eqy
|
||||
|
|
@ -85,8 +85,8 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
|
||||
... | inj₂ a | inj₂ b = later∼ (iter-cong∼′ {A} {X} f (inj₂-helper f x≡y eqx eqy))
|
||||
|
||||
iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈ (iter {A} {X} < f > y) ]
|
||||
iter-cong′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈′ (iter {A} {X} < f > y) ]
|
||||
iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delay≈ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈ (iter {A} {X} < f > y) ]
|
||||
iter-cong′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delay≈ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈′ (iter {A} {X} < f > y) ]
|
||||
force≈ (iter-cong′ {A} {X} f {x} {y} x≡y) = iter-cong f x≡y
|
||||
iter-cong {A} {X} f {x} {y} x≡y with < f > x in eqx | < f > y in eqy
|
||||
... | inj₁ a | inj₁ b = inj₁-helper f x≡y eqx eqy
|
||||
|
|
@ -94,43 +94,43 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
|
||||
... | inj₂ a | inj₂ b = later≈ (iter-cong′ {A} {X} f (inj₂-helper f x≡y eqx eqy))
|
||||
|
||||
iterₛ∼ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ∼ A ⊎ₛ X)) → X ⟶ Delayₛ∼ A
|
||||
iterₛ∼ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delay∼ A ⊎ₛ X)) → X ⟶ Delay∼ A
|
||||
iterₛ∼ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong∼ {A} {X} f }
|
||||
|
||||
iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ A ⊎ₛ X)) → X ⟶ Delayₛ A
|
||||
iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delay≈ A ⊎ₛ X)) → X ⟶ Delay≈ A
|
||||
iterₛ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong {A} {X} f }
|
||||
|
||||
iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {x : ∣ X ∣} → [ A ][ iter {A} {X} < f > x ≈ [ Function.id , iter {A} {X} < f > ] (f ⟨$⟩ x) ]
|
||||
iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {x : ∣ X ∣} → [ A ][ iter {A} {X} < f > x ≈ [ Function.id , iter {A} {X} < f > ] (f ⟨$⟩ x) ]
|
||||
iter-fixpoint {A} {X} {f} {x} with < f > x in eqx
|
||||
... | inj₁ a = ≈-refl A
|
||||
... | inj₂ a = ≈-trans A (≈-sym A later-self) (≈-refl A)
|
||||
|
||||
iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} < f > x ≈ iter {A} {X} < g > y ]
|
||||
iter-resp-≈′ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} < f > x ≈′ iter {A} {X} < g > y ]
|
||||
iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delay≈ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} < f > x ≈ iter {A} {X} < g > y ]
|
||||
iter-resp-≈′ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delay≈ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} < f > x ≈′ iter {A} {X} < g > y ]
|
||||
force≈ (iter-resp-≈′ {A} {X} f g f≋g {x} {y} x≡y) = iter-resp-≈ f g f≋g {x} {y} x≡y
|
||||
iter-resp-≈ {A} {X} f g f≋g {x} {y} x≡y with < f > x in eqa | < g > y in eqb
|
||||
... | inj₁ a | inj₁ b = drop-inj₁ helper
|
||||
where
|
||||
helper : [ Delayₛ A ⊎ₛ X ][ inj₁ a ≡ inj₁ b ]
|
||||
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delayₛ A ⊎ₛ X) (cong f x≡y) f≋g
|
||||
... | inj₁ a | inj₂ b = conflict (Delayₛ A) X helper
|
||||
helper : [ Delay≈ A ⊎ₛ X ][ inj₁ a ≡ inj₁ b ]
|
||||
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delay≈ A ⊎ₛ X) (cong f x≡y) f≋g
|
||||
... | inj₁ a | inj₂ b = conflict (Delay≈ A) X helper
|
||||
where
|
||||
helper : [ Delayₛ A ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
|
||||
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delayₛ A ⊎ₛ X) (cong f x≡y) f≋g
|
||||
... | inj₂ a | inj₁ b = conflict (Delayₛ A) X (≡-sym (Delayₛ A ⊎ₛ X) helper)
|
||||
helper : [ Delay≈ A ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
|
||||
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delay≈ A ⊎ₛ X) (cong f x≡y) f≋g
|
||||
... | inj₂ a | inj₁ b = conflict (Delay≈ A) X (≡-sym (Delay≈ A ⊎ₛ X) helper)
|
||||
where
|
||||
helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₁ b ]
|
||||
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delayₛ A ⊎ₛ X) (cong f x≡y) f≋g
|
||||
helper : [ Delay≈ A ⊎ₛ X ][ inj₂ a ≡ inj₁ b ]
|
||||
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delay≈ A ⊎ₛ X) (cong f x≡y) f≋g
|
||||
... | inj₂ a | inj₂ b = later≈ (iter-resp-≈′ f g f≋g (drop-inj₂ helper))
|
||||
where
|
||||
helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₂ b ]
|
||||
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delayₛ A ⊎ₛ X) (cong f x≡y) f≋g
|
||||
helper : [ Delay≈ A ⊎ₛ X ][ inj₂ a ≡ inj₂ b ]
|
||||
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delay≈ A ⊎ₛ X) (cong f x≡y) f≋g
|
||||
|
||||
iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {g : Y ⟶ (Delayₛ A ⊎ₛ Y)} {h : X ⟶ Y}
|
||||
→ ([ inj₁ₛ ∘ (idₛ (Delayₛ A)) , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h)
|
||||
iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {g : Y ⟶ (Delay≈ A ⊎ₛ Y)} {h : X ⟶ Y}
|
||||
→ ([ inj₁ₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h)
|
||||
→ ∀ {x : ∣ X ∣} {y : ∣ Y ∣} → [ Y ][ y ≡ h ⟨$⟩ x ] → [ A ][ iter {A} {X} < f > x ≈ (iter {A} {Y} < g >) y ]
|
||||
iter-uni′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {g : Y ⟶ (Delayₛ A ⊎ₛ Y)} {h : X ⟶ Y}
|
||||
→ ([ inj₁ₛ ∘ (idₛ (Delayₛ A)) , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h)
|
||||
iter-uni′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {g : Y ⟶ (Delay≈ A ⊎ₛ Y)} {h : X ⟶ Y}
|
||||
→ ([ inj₁ₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h)
|
||||
→ ∀ {x : ∣ X ∣} {y : ∣ Y ∣} → [ Y ][ y ≡ h ⟨$⟩ x ] → [ A ][ iter {A} {X} < f > x ≈′ (iter {A} {Y} < g >) y ]
|
||||
force≈ (iter-uni′ {A} {X} {Y} {f} {g} {h} eq {x} {y} y≡h$x) = iter-uni {A} {X} {Y} {f} {g} {h} eq {x} {y} y≡h$x
|
||||
iter-uni {A} {X} {Y} {f} {g} {h} eq {x} {y} x≡y with f ⟨$⟩ x in eqx | g ⟨$⟩ (h ⟨$⟩ x) in eqy | g ⟨$⟩ y in eqz | eq {x}
|
||||
|
|
@ -140,10 +140,10 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
... | inj₂ a | inj₂ b | inj₂ c | inj₂ req = later≈ (iter-uni′ {f = f} {g = g}{h = h} eq c≡h$a)
|
||||
where
|
||||
c≡h$a : [ Y ][ c ≡ h ⟨$⟩ a ]
|
||||
c≡h$a = ≡-trans Y (drop-inj₂ (≡-trans (Delayₛ A ⊎ₛ Y) (≡-trans (Delayₛ A ⊎ₛ Y) (≡-sym (Delayₛ A ⊎ₛ Y) (≡→≡ {Delayₛ A ⊎ₛ Y} eqz)) (cong g x≡y)) (≡→≡ {Delayₛ A ⊎ₛ Y} eqy))) (≡-sym Y req)
|
||||
c≡h$a = ≡-trans Y (drop-inj₂ (≡-trans (Delay≈ A ⊎ₛ Y) (≡-trans (Delay≈ A ⊎ₛ Y) (≡-sym (Delay≈ A ⊎ₛ Y) (≡→≡ {Delay≈ A ⊎ₛ Y} eqz)) (cong g x≡y)) (≡→≡ {Delay≈ A ⊎ₛ Y} eqy))) (≡-sym Y req)
|
||||
|
||||
iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ (X ⊎ₛ Y)} {x : ∣ X ⊎ₛ Y ∣} → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} < f > , inj₂ ∘f < h > ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f < f > , (inj₂ ∘f < h >) ] x ]
|
||||
iter-folding′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ (X ⊎ₛ Y)} {x : ∣ X ⊎ₛ Y ∣} → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} < f > , inj₂ ∘f < h > ] x ≈′ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f < f > , (inj₂ ∘f < h >) ] x ]
|
||||
iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {h : Y ⟶ (X ⊎ₛ Y)} {x : ∣ X ⊎ₛ Y ∣} → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} < f > , inj₂ ∘f < h > ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f < f > , (inj₂ ∘f < h >) ] x ]
|
||||
iter-folding′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {h : Y ⟶ (X ⊎ₛ Y)} {x : ∣ X ⊎ₛ Y ∣} → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} < f > , inj₂ ∘f < h > ] x ≈′ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f < f > , (inj₂ ∘f < h >) ] x ]
|
||||
force≈ (iter-folding′ {A} {X} {Y} {f} {h} {x}) = iter-folding {A} {X} {Y} {f} {h} {x}
|
||||
iter-folding {A} {X} {Y} {f} {h} {inj₁ x} with f ⟨$⟩ x in eqa
|
||||
... | inj₁ a = ≈-refl A
|
||||
|
|
@ -159,7 +159,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
... | inj₁ a = later≈ (iter-folding′ {A} {X} {Y} {f} {h} {inj₁ a})
|
||||
... | inj₂ a = later≈ (iter-folding′ {A} {X} {Y} {f} {h} {inj₂ a})
|
||||
|
||||
delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (Delayₛ A)
|
||||
delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (Delay≈ A)
|
||||
delay-algebras-on {A} = record
|
||||
{ _# = iterₛ {A}
|
||||
; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f}
|
||||
|
|
@ -169,7 +169,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
}
|
||||
|
||||
delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra
|
||||
delay-algebras A = record { A = Delayₛ A ; algebra = delay-algebras-on {A}}
|
||||
delay-algebras A = record { A = Delay≈ A ; algebra = delay-algebras-on {A}}
|
||||
|
||||
open Elgot-Algebra using (#-Fixpoint; #-Uniformity; #-Compositionality; #-resp-≈; #-Diamond) renaming (A to ⟦_⟧)
|
||||
|
||||
|
|
@ -183,12 +183,12 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
helper₁ (now x) = inj₁ (< f > x)
|
||||
helper₁ (later x) = inj₂ (force x)
|
||||
|
||||
helper₁-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ helper₁ x ≡ helper₁ y ]
|
||||
helper₁-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delay∼ A ][ helper₁ x ≡ helper₁ y ]
|
||||
helper₁-cong (now∼ x≡y) = inj₁ (cong f x≡y)
|
||||
helper₁-cong (later∼ x≡y) = inj₂ (force∼ x≡y)
|
||||
|
||||
-- -- setoid-morphism that preserves strong-bisimilarity
|
||||
helper : (Delayₛ∼ A) ⟶ (⟦ B ⟧ ⊎ₛ Delayₛ∼ A)
|
||||
helper : (Delay∼ A) ⟶ (⟦ B ⟧ ⊎ₛ Delay∼ A)
|
||||
helper = record { to = helper₁ ; cong = helper₁-cong}
|
||||
|
||||
helper#∼-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ][ helper # ⟨$⟩ x ≡ helper # ⟨$⟩ y ]
|
||||
|
|
@ -223,31 +223,31 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
helper₁' (now (x , suc n)) = inj₂ (< liftFₛ∼ outer > (ι {A} (x , n)))
|
||||
helper₁' (later y) = inj₂ (force y)
|
||||
|
||||
helper₁-cong' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ helper₁' x ≡ helper₁' y ]
|
||||
helper₁-cong' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid) ][ helper₁' x ≡ helper₁' y ]
|
||||
helper₁-cong' {now (x , zero)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
|
||||
helper₁-cong' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (cong (liftFₛ∼ outer) (cong ιₛ' (x≡y , ≣-refl)))
|
||||
helper₁-cong' (later∼ x∼y) = inj₂ (force∼ x∼y)
|
||||
|
||||
helper' : (Delayₛ∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
|
||||
helper' : (Delay∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
|
||||
helper' = record { to = helper₁' ; cong = helper₁-cong'}
|
||||
|
||||
helper₁'' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ Delay (∣ A ∣ × ℕ {ℓ})
|
||||
helper₁'' (now (x , _)) = inj₁ (< f > x)
|
||||
helper₁'' (later y) = inj₂ (force y)
|
||||
|
||||
helper₁-cong'' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ helper₁'' x ≡ helper₁'' y ]
|
||||
helper₁-cong'' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid) ][ helper₁'' x ≡ helper₁'' y ]
|
||||
helper₁-cong'' {now (x , _)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
|
||||
helper₁-cong'' (later∼ x∼y) = inj₂ (force∼ x∼y)
|
||||
|
||||
helper'' : (Delayₛ∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
|
||||
helper'' : (Delay∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
|
||||
helper'' = record { to = helper₁'' ; cong = helper₁-cong''}
|
||||
|
||||
-- Needs #-Diamond
|
||||
eq₀ : ∀ {z} → [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper'' # ⟨$⟩ z ]
|
||||
eq₀ {z} = ≡-trans ⟦ B ⟧
|
||||
(#-resp-≈ B {Delayₛ∼ (A ×ₛ ℕ-setoid)} {helper'} step₁)
|
||||
(#-resp-≈ B {Delay∼ (A ×ₛ ℕ-setoid)} {helper'} step₁)
|
||||
(≡-trans ⟦ B ⟧
|
||||
(#-Diamond B {Delayₛ∼ (A ×ₛ ℕ-setoid)} helper''')
|
||||
(#-Diamond B {Delay∼ (A ×ₛ ℕ-setoid)} helper''')
|
||||
(#-resp-≈ B (λ {x} → (step₂ {x}))))
|
||||
where
|
||||
helper₁''' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ (Delay (∣ A ∣ × ℕ {ℓ}) ⊎ Delay (∣ A ∣ × ℕ {ℓ}))
|
||||
|
|
@ -255,45 +255,45 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
helper₁''' (now (x , suc n)) = inj₂ (inj₁ (< liftFₛ∼ outer > (ι {A} (x , n))))
|
||||
helper₁''' (later y) = inj₂ (inj₂ (force y))
|
||||
|
||||
helper₁-cong''' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ (Delayₛ∼ (A ×ₛ ℕ-setoid) ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) ][ helper₁''' x ≡ helper₁''' y ]
|
||||
helper₁-cong''' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ (Delay∼ (A ×ₛ ℕ-setoid) ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid)) ][ helper₁''' x ≡ helper₁''' y ]
|
||||
helper₁-cong''' {now (x , zero)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
|
||||
helper₁-cong''' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (inj₁ (cong (liftFₛ∼ outer) (cong ιₛ' (x≡y , ≣-refl))))
|
||||
helper₁-cong''' (later∼ x∼y) = inj₂ (inj₂ (force∼ x∼y))
|
||||
|
||||
helper''' : (Delayₛ∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ (Delayₛ∼ (A ×ₛ ℕ-setoid) ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)))
|
||||
helper''' : (Delay∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ (Delay∼ (A ×ₛ ℕ-setoid) ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid)))
|
||||
helper''' = record { to = helper₁''' ; cong = helper₁-cong''' }
|
||||
|
||||
step₁ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ helper' ⟨$⟩ x ≡ ([ inj₁ , inj₂ ∘′ [ id , id ] ] ∘′ helper₁''') x ]
|
||||
step₁ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
|
||||
step₁ {now (a , suc n)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
|
||||
step₁ {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
|
||||
step₁ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid) ][ helper' ⟨$⟩ x ≡ ([ inj₁ , inj₂ ∘′ [ id , id ] ] ∘′ helper₁''') x ]
|
||||
step₁ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
|
||||
step₁ {now (a , suc n)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
|
||||
step₁ {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
|
||||
|
||||
step₂ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ ([ inj₁ , [ inj₁ ∘′ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) , idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > , inj₂ ] ] ∘′ helper₁''') x ≡ helper'' ⟨$⟩ x ]
|
||||
step₂ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
|
||||
step₂ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid) ][ ([ inj₁ , [ inj₁ ∘′ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delay∼ (A ×ₛ ℕ-setoid)) , idₛ (Delay∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > , inj₂ ] ] ∘′ helper₁''') x ≡ helper'' ⟨$⟩ x ]
|
||||
step₂ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
|
||||
step₂ {now (x , suc n)} = inj₁ (by-induction n)
|
||||
where
|
||||
by-induction : ∀ n → [ ⟦ B ⟧ ][ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) , idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > (< liftFₛ∼ outer > (ι (x , n))) ≡ f ⟨$⟩ x ]
|
||||
by-induction : ∀ n → [ ⟦ B ⟧ ][ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delay∼ (A ×ₛ ℕ-setoid)) , idₛ (Delay∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > (< liftFₛ∼ outer > (ι (x , n))) ≡ f ⟨$⟩ x ]
|
||||
by-induction zero = #-Fixpoint B
|
||||
by-induction (suc n) = ≡-trans ⟦ B ⟧ (#-Fixpoint B) (by-induction n)
|
||||
step₂ {later y} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))
|
||||
step₂ {later y} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
|
||||
|
||||
eq₁ : ∀ {z} → [ ⟦ B ⟧ ][ helper'' # ⟨$⟩ z ≡ helper # ⟨$⟩ liftF proj₁ z ]
|
||||
eq₁ {z} = #-Uniformity B {f = helper''} {g = helper} {h = liftFₛ∼ proj₁ₛ} by-uni
|
||||
where
|
||||
by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ (liftF proj₁) ] (helper₁'' x) ≡ (< helper > ∘′ liftF proj₁) x ]
|
||||
by-uni {now (a , b)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ A)
|
||||
by-uni {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ A)
|
||||
by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delay∼ A ][ [ inj₁ , inj₂ ∘′ (liftF proj₁) ] (helper₁'' x) ≡ (< helper > ∘′ liftF proj₁) x ]
|
||||
by-uni {now (a , b)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ A)
|
||||
by-uni {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ A)
|
||||
|
||||
eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
|
||||
eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delay∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
|
||||
eq {now (x , n)} {now (y , .n)} (now∼ (x∼y , ≣-refl)) = eq' {n}
|
||||
where
|
||||
eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ]
|
||||
eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delay∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ]
|
||||
eq' {zero} = inj₁ (cong f x∼y)
|
||||
eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delayₛ∼ A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (∼-trans A identityˡ∼ (cong ιₛ' (x∼y , ≣-refl))))
|
||||
eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delay∼ A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (∼-trans A identityˡ∼ (cong ιₛ' (x∼y , ≣-refl))))
|
||||
eq (later∼ x∼y) = inj₂ (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x∼y)))
|
||||
|
||||
eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)]
|
||||
eq₂ = Elgot-Algebra.#-Uniformity B {Delayₛ∼ (A ×ₛ ℕ-setoid {ℓ})} {Delayₛ∼ A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} (λ {x} → eq {x} {x} (∼-refl (A ×ₛ ℕ-setoid)))
|
||||
eq₂ = Elgot-Algebra.#-Uniformity B {Delay∼ (A ×ₛ ℕ-setoid {ℓ})} {Delay∼ A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} (λ {x} → eq {x} {x} (∼-refl (A ×ₛ ℕ-setoid)))
|
||||
|
||||
delay-lift' = record { to = < helper # > ; cong = helper#≈-cong }
|
||||
|
||||
|
|
@ -307,34 +307,34 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
_⟶_.to ‖‖-quote x = x
|
||||
cong (‖‖-quote {X}) ≣-refl = ≡-refl X
|
||||
|
||||
disc-dom : ∀ {X : Setoid ℓ ℓ} → X ⟶ (Delayₛ A ⊎ₛ X) → ‖ X ‖ ⟶ (Delayₛ∼ A ⊎ₛ ‖ X ‖)
|
||||
disc-dom : ∀ {X : Setoid ℓ ℓ} → X ⟶ (Delay≈ A ⊎ₛ X) → ‖ X ‖ ⟶ (Delay∼ A ⊎ₛ ‖ X ‖)
|
||||
_⟶_.to (disc-dom f) x = f ⟨$⟩ x
|
||||
cong (disc-dom {X} f) {x} {y} x≡y rewrite x≡y = ≡-refl (Delayₛ∼ A ⊎ₛ ‖ X ‖)
|
||||
cong (disc-dom {X} f) {x} {y} x≡y rewrite x≡y = ≡-refl (Delay∼ A ⊎ₛ ‖ X ‖)
|
||||
|
||||
iter-g-var : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delayₛ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼ (iterₛ∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ]
|
||||
iter-g-var′ : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delayₛ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼′ (iterₛ∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ]
|
||||
iter-g-var : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delay≈ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼ (iterₛ∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ]
|
||||
iter-g-var′ : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delay≈ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼′ (iterₛ∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ]
|
||||
force∼ (iter-g-var′ {X} g {x}) = iter-g-var {X} g {x}
|
||||
iter-g-var {X} g {x} with g ⟨$⟩ x
|
||||
... | inj₁ a = ∼-refl A
|
||||
... | inj₂ a = later∼ (iter-g-var′ {X} g {a})
|
||||
|
||||
preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delayₛ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
|
||||
preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delay≈ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
|
||||
preserves' {X} {g} {x} = ≡-trans ⟦ B ⟧ step₁ step₂
|
||||
where
|
||||
step₁ : [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ]
|
||||
step₁ = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (helper#∼-cong (iter-g-var g)) (sub-step₁ (disc-dom g) {inj₂ x})) (≡-sym ⟦ B ⟧ (#-Compositionality B {f = helper} {h = disc-dom g}))
|
||||
where
|
||||
sub-step₁ : (g : ‖ X ‖ ⟶ ((Delayₛ∼ A) ⊎ₛ ‖ X ‖)) → ∀ {x} → [ ⟦ B ⟧ ][ ((helper #) ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x
|
||||
sub-step₁ : (g : ‖ X ‖ ⟶ ((Delay∼ A) ⊎ₛ ‖ X ‖)) → ∀ {x} → [ ⟦ B ⟧ ][ ((helper #) ∘ [ idₛ (Delay∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x
|
||||
≡ ([ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ) # ⟨$⟩ x ]
|
||||
sub-step₁ g {u} = ≡-sym ⟦ B ⟧ (#-Uniformity B {h = [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ} (λ {y} → last-step {y}))
|
||||
sub-step₁ g {u} = ≡-sym ⟦ B ⟧ (#-Uniformity B {h = [ idₛ (Delay∼ A) , iterₛ∼ g ]ₛ} (λ {y} → last-step {y}))
|
||||
where
|
||||
last-step : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ (Delayₛ∼ A) ][ [ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ ]ₛ ∘ [ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ ⟨$⟩ x ≡ (helper ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x ]
|
||||
last-step {inj₁ (now a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
|
||||
last-step {inj₁ (later a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
|
||||
last-step : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ (Delay∼ A) ][ [ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delay∼ A) , iterₛ∼ g ]ₛ ]ₛ ∘ [ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ ⟨$⟩ x ≡ (helper ∘ [ idₛ (Delay∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x ]
|
||||
last-step {inj₁ (now a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼ A))
|
||||
last-step {inj₁ (later a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼ A))
|
||||
last-step {inj₂ a} with g ⟨$⟩ a in eqb
|
||||
... | inj₁ (now b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
|
||||
... | inj₁ (later b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
|
||||
... | inj₂ b = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
|
||||
... | inj₁ (now b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼ A))
|
||||
... | inj₁ (later b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼ A))
|
||||
... | inj₂ b = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼ A))
|
||||
step₂ : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
|
||||
step₂ = #-Uniformity B {h = ‖‖-quote} sub-step₂
|
||||
where
|
||||
|
|
@ -359,23 +359,23 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
|||
→ (<< h >> ∘ (ηₛ A)) ≋ f
|
||||
→ << g >> ≋ << h >>
|
||||
*-uniq' {B} f g h eqᵍ eqʰ {x} = ≡-trans ⟦ B ⟧ (cong << g >> iter-id)
|
||||
(≡-trans ⟦ B ⟧ (preserves g {Delayₛ∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x})
|
||||
(≡-trans ⟦ B ⟧ (preserves g {Delay∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x})
|
||||
(≡-trans ⟦ B ⟧ (#-resp-≈ B (λ {x} → helper-eq' {x}) {x})
|
||||
(≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delayₛ∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x}))
|
||||
(≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delay∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x}))
|
||||
(≡-sym ⟦ B ⟧ (cong << h >> iter-id)))))
|
||||
where
|
||||
open Elgot-Algebra B using (_#)
|
||||
D∼⇒D≈ : ∀ {A : Setoid ℓ ℓ} → Delayₛ∼ A ⟶ Delayₛ A
|
||||
D∼⇒D≈ : ∀ {A : Setoid ℓ ℓ} → Delay∼ A ⟶ Delay≈ A
|
||||
D∼⇒D≈ {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq }
|
||||
|
||||
helper-now₁ : (Delay ∣ A ∣) → (Delay ∣ A ∣ ⊎ (Delay ∣ A ∣))
|
||||
helper-now₁ (now x) = inj₁ (now x)
|
||||
helper-now₁ (later x) = inj₂ (force x)
|
||||
helper-now : Delayₛ∼ A ⟶ ((Delayₛ∼ A) ⊎ₛ (Delayₛ∼ A))
|
||||
helper-now : Delay∼ A ⟶ ((Delay∼ A) ⊎ₛ (Delay∼ A))
|
||||
helper-now = record { to = helper-now₁ ; cong = λ { (now∼ eq) → inj₁ (now∼ eq)
|
||||
; (later∼ eq) → inj₂ (force∼ eq) } }
|
||||
|
||||
helper-eq' : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ ([ inj₁ₛ ∘ << g >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x
|
||||
helper-eq' : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delay∼ A ][ ([ inj₁ₛ ∘ << g >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x
|
||||
≡ ([ inj₁ₛ ∘ << h >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
|
||||
helper-eq' {now x} = inj₁ (≡-trans ⟦ B ⟧ eqᵍ (≡-sym ⟦ B ⟧ eqʰ))
|
||||
helper-eq' {later x} = inj₂ (∼-refl A)
|
||||
|
|
|
|||
|
|
@ -172,6 +172,25 @@
|
|||
numpages = {37}
|
||||
}
|
||||
|
||||
@article{setoids,
|
||||
author = {Barthe, Gilles and Capretta, Venanzio and Pons, Olivier},
|
||||
title = {Setoids in type theory},
|
||||
year = {2003},
|
||||
issue_date = {March 2003},
|
||||
publisher = {Cambridge University Press},
|
||||
address = {USA},
|
||||
volume = {13},
|
||||
number = {2},
|
||||
issn = {0956-7968},
|
||||
url = {https://doi.org/10.1017/S0956796802004501},
|
||||
doi = {10.1017/S0956796802004501},
|
||||
abstract = {Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids and assesses their suitability as a basis for developing mathematics. According to whether the equality relation is required to be reflexive or not we have total or partial setoid, respectively. There is only one definition of total setoid, but four different definitions of partial setoid, depending on four different notions of setoid function. We prove that one approach to partial setoids in unsuitable, and that the other approaches can be divided in two classes of equivalence. One class contains definitions of partial setoids that are equivalent to total setoids; the other class contains an inherently different definition, that has been useful in the modeling of type systems. We also provide some elements of discussion on the merits of each approach from the viewpoint of formalizing mathematics. In particular, we exhibit a difficulty with the common definition of subsetoids in the partial setoid approach.},
|
||||
journal = {J. Funct. Program.},
|
||||
month = {mar},
|
||||
pages = {261–293},
|
||||
numpages = {33}
|
||||
}
|
||||
|
||||
@article{sol-thm,
|
||||
author = {Aczel, Peter and Ad\'{a}mek, Jir\'{\i} and Milius, Stefan and Velebil, Jir\'{\i}},
|
||||
title = {Infinite trees and completely iterative theories: a coalgebraic view},
|
||||
|
|
|
|||
|
|
@ -108,8 +108,18 @@
|
|||
%\usepackage{fontspec}
|
||||
%\setmonofont{Noto Sans Mono}
|
||||
|
||||
\newcommand{\obj}[1]{\ensuremath{\vert \mathcal{#1} \vert}}
|
||||
\newcommand{\elgotobj}[1]{\ensuremath{\vert \mathit{Elgot}(\mathcal{#1}) \vert}}
|
||||
% category C
|
||||
\newcommand*{\C}{\ensuremath{\mathcal{C}}}
|
||||
% objects of category
|
||||
\newcommand*{\obj}[1]{\ensuremath{\vert #1 \vert}}
|
||||
% category of elgot algebras on #1
|
||||
\newcommand*{\elgotalgs}[1]{\ensuremath{\mathit{ElgotAlgs}(#1)}}
|
||||
% category of monads on #1
|
||||
\newcommand*{\monads}[1]{\ensuremath{\mathit{Monads}(#1)}}
|
||||
% category of pre-Elgot monads on #1
|
||||
\newcommand*{\preelgot}[1]{\ensuremath{\mathit{PreElgot}(#1)}}
|
||||
\newcommand*{\setoids}{\ensuremath{\mathit{Setoids}}}
|
||||
|
||||
\begin{document}
|
||||
\pagestyle{plain}
|
||||
\input{src/titlepage}%
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
|
||||
We assume familiarity with basic categorical notions, in particular: categories, functors, functor algebras and natural transformations, as well as special objects like (co-)products, terminal and initial objects and special morphisms like isos, epis and monos.
|
||||
In this chapter we will introduce notation that will be used throughout the thesis and also introduce some notions that are crucial to this thesis in more detail.
|
||||
We write $\obj{C}$ for the objects of a category $\mathcal{C}$, $id_X$ for the identity morphism on $X$, $(-) \circ (-)$ for the composition of morphisms and $\mathcal{C}(X,Y)$ for the set of morphisms between $X$ and $Y$.
|
||||
We write $\obj{C}$ for the objects of a category $\C$, $id_X$ for the identity morphism on $X$, $(-) \circ (-)$ for the composition of morphisms and $\C(X,Y)$ for the set of morphisms between $X$ and $Y$.
|
||||
We will also sometimes omit indices of the identity and of natural transformations in favor of readability.
|
||||
|
||||
\section{Distributive and Cartesian Closed Categories}
|
||||
|
|
@ -36,7 +36,7 @@ Categories with finite products (i.e. binary products and a terminal object) are
|
|||
|
||||
\begin{definition}[Distributive Category]
|
||||
\label{def:distributive}
|
||||
A cartesian and cocartesian category $\mathcal{C}$ is called distributive if the canonical (left) distributivity morphism morphism $dstl^{-1}$ is an iso:
|
||||
A cartesian and cocartesian category $\C$ is called distributive if the canonical (left) distributivity morphism morphism $dstl^{-1}$ is an iso:
|
||||
% https://q.uiver.app/#q=WzAsMixbMCwwLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzMsMCwiWCBcXHRpbWVzIChZICsgWikiXSxbMCwxLCJkc3RsXnstMX0gOj0ge1xcbGJyYWNrIGlkIFxcdGltZXMgaV8xICwgaWQgXFx0aW1lcyBpXzIgXFxyYnJhY2t9IiwwLHsiY3VydmUiOi0zfV0sWzEsMCwiZHN0bCIsMCx7ImN1cnZlIjotM31dXQ==
|
||||
\[\begin{tikzcd}
|
||||
{X \times Y + X \times Z} &&& {X \times (Y + Z)}
|
||||
|
|
@ -94,7 +94,7 @@ Categories with finite products (i.e. binary products and a terminal object) are
|
|||
\end{proof}
|
||||
|
||||
\begin{definition}[Exponential Object]
|
||||
Let $\mathcal{C}$ be a cartesian category and $X , Y \in \vert \mathcal{C} \vert$.
|
||||
Let $\C$ be a cartesian category and $X , Y \in \vert \C \vert$.
|
||||
An object $X^Y$ is called an exponential object (of $X$ and $Y$) if there exists an evaluation morphism $eval : X^Y \times Y \rightarrow X$ and for any $f : X \times Y \rightarrow Z$ there exists a morphism $curry\; f : X \rightarrow Z^Y$ that is unique with respect to the following diagram:
|
||||
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJaIFxcdGltZXMgWSJdLFsyLDAsIlheWSBcXHRpbWVzIFkiXSxbMiwyLCJYIl0sWzEsMiwiZXZhbCJdLFswLDEsImN1cnJ5XFw7ZiBcXHRpbWVzIGlkIl0sWzAsMiwiZiIsMl1d
|
||||
\[\begin{tikzcd}
|
||||
|
|
@ -107,29 +107,54 @@ Categories with finite products (i.e. binary products and a terminal object) are
|
|||
\end{tikzcd}\]
|
||||
\end{definition}
|
||||
|
||||
A cartesian closed category is a cartesian category $\mathcal{C}$ that also has an exponential object $X^Y$ for any $X, Y \in \mathcal{C}$.
|
||||
A cartesian closed category is a cartesian category $\C$ that also has an exponential object $X^Y$ for any $X, Y \in \C$.
|
||||
The internal logic of cartesian closed categories is the simply typed $\lambda$-calculus, which makes them a suitable target for interpreting programming languages. But in this thesis we will not assume a cartesian closed category as to be more general.
|
||||
|
||||
\section{Stable Natural Numbers Object}
|
||||
|
||||
\unsure[inline]{Introduce NNO? Actually not needed!}
|
||||
|
||||
\section{Monads}
|
||||
Monads are widely known among programmers as a way of modelling effects in pure languages and are also central to this thesis. Let's recall the basic definitions\cite{Lane1971}\cite{moggi}.
|
||||
Monads are widely known among programmers as a way of modelling effects in pure languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
|
||||
|
||||
\begin{definition}[Monad]
|
||||
A monad on a category $\mathcal{C}$ is a triple $(F, \eta, \mu)$, where $F : \mathcal{C} \rightarrow \mathcal{C}$ is an endofunctor and $\eta : Id \rightarrow F, \mu : F^2 \rightarrow F$ are natural transformations, satisfying the following laws:
|
||||
A monad on a category $\C$ is a triple $(F, \eta, \mu)$, where $F : \C \rightarrow \C$ is an endofunctor and $\eta : Id \rightarrow F, \mu : F^2 \rightarrow F$ are natural transformations, satisfying the following laws:
|
||||
\begin{alignat*}{1}
|
||||
&\mu_X \circ \mu_{FX} = \mu_X \circ F\mu_X \tag*{(M1)}\label{M1}\\
|
||||
&\mu_X \circ \eta_{FX} = id_{FX} \tag*{(M2)}\label{M2}\\
|
||||
&\mu_X \circ F\eta_X = id_{FX} \tag*{(M3)}\label{M3}
|
||||
\end{alignat*}
|
||||
\todo[inline]{diagrams}
|
||||
\end{definition}
|
||||
|
||||
Morphisms between monads are natural transformations that respect the monad operations:
|
||||
|
||||
\change[inline]{
|
||||
Maybe remove the definition of Mon(C) and just introduce the category of pre-Elgot monads.
|
||||
}
|
||||
|
||||
\begin{definition}[Monad Morphism]
|
||||
A morphism between two monads $(S, \eta^S, \mu^S)$ and $(T, \eta^T, \mu^T)$ is a natural transformation $\alpha : S \rightarrow T$ between the underlying functors satisfying:
|
||||
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzIsMCwiU1giXSxbMiwxLCJUWCJdLFs0LDAsIlNTWCJdLFs2LDAsIlNUWCJdLFs0LDEsIlNYIl0sWzYsMSwiVFRYIl0sWzUsMiwiVFgiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl1d
|
||||
\[\begin{tikzcd}
|
||||
X && SX && SSX && STX \\
|
||||
&& TX && SX && TTX \\
|
||||
&&&&& TX
|
||||
\arrow["{\eta^S}", from=1-1, to=1-3]
|
||||
\arrow["\alpha", from=1-3, to=2-3]
|
||||
\arrow["{\eta^T}"', from=1-1, to=2-3]
|
||||
\arrow["S\alpha", from=1-5, to=1-7]
|
||||
\arrow["{\mu^S}"', from=1-5, to=2-5]
|
||||
\arrow["\alpha", from=1-7, to=2-7]
|
||||
\arrow["\alpha"', from=2-5, to=3-6]
|
||||
\arrow["{\mu^T}", from=2-7, to=3-6]
|
||||
\end{tikzcd}\]
|
||||
\end{definition}
|
||||
|
||||
\begin{definition}[The Category of Monads]
|
||||
Monads on a category $\C$ together with monad morphisms yield a category that we call $\monads{\C}$. The identity morphism is the identity natural transformation that trivially respects the monad operations and composition of morphisms is composition of natural transformations.
|
||||
\end{definition}
|
||||
|
||||
For programmers a second equivalent definition is more useful:
|
||||
|
||||
\begin{definition}[Kleisli Triple]
|
||||
A kleisli triple on a category $\mathcal{C}$ is a triple $(F, \eta, (-)^*)$, where $F : \obj{C} \rightarrow \obj{C}$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\obj{C}}$ is a family of morphisms and for every morphism $f : X \rightarrow FY$ there exists a morphism $f^* : FX \rightarrow FY$ called the kleisli lifting, where the following laws hold:
|
||||
A kleisli triple on a category $\C$ is a triple $(F, \eta, (-)^*)$, where $F : \obj{C} \rightarrow \obj{C}$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\obj{C}}$ is a family of morphisms and for every morphism $f : X \rightarrow FY$ there exists a morphism $f^* : FX \rightarrow FY$ called the kleisli lifting, where the following laws hold:
|
||||
\begin{alignat*}{1}
|
||||
&\eta_X^* = id_{FX} \tag*{(K1)}\label{K1}\\
|
||||
&\eta_X \circ f^* = f \tag*{(K2)}\label{K2}\\
|
||||
|
|
@ -147,11 +172,11 @@ In functional programming languages like Haskell the Kleisli lifting $(-)^*$ is
|
|||
This results in the following:
|
||||
|
||||
\begin{definition}[Kleisli Category]
|
||||
Given a monad $T$ on a category $\mathcal{C}$, the Kleisli category $\mathcal{C}^T$ is defined as:
|
||||
Given a monad $T$ on a category $\C$, the Kleisli category $\C^T$ is defined as:
|
||||
\begin{itemize}
|
||||
\item $\vert \mathcal{C}^T \vert = \obj{C}$
|
||||
\item $\mathcal{C^T}(X, Y) = \mathcal{C}(X, TY)$
|
||||
\item composition of $f : X \rightarrow TY$ and $g : Y \rightarrow TZ$ is defined as $f \circ_{\mathcal{C}^T} g = f^* \circ_{\mathcal{C}} g$.
|
||||
\item $\vert \C^T \vert = \obj{C}$
|
||||
\item $\mathcal{C^T}(X, Y) = \C(X, TY)$
|
||||
\item composition of $f : X \rightarrow TY$ and $g : Y \rightarrow TZ$ is defined as $f \circ_{\C^T} g = f^* \circ_{\C} g$.
|
||||
\item the identity morphisms are the unit morphisms of $T$, $id_X = \eta_X : X \rightarrow TX$
|
||||
\end{itemize}
|
||||
The laws of categories then follow from the Kleisli triple laws, making this indeed a category.
|
||||
|
|
@ -194,7 +219,7 @@ When modelling partiality with a monad, one would expect the following two progr
|
|||
\end{multicols}
|
||||
where p and q are (partial) computations. This condition can be expressed categorically, but first we need another definition:
|
||||
|
||||
\begin{definition}[Strong Monad] A monad $M$ on a cartesian category $\mathcal{C}$ is called strong if there exists a natural transformation $\tau_{X,Y} : X \times MY \rightarrow M(X \times Y)$, satisfying the following conditions:
|
||||
\begin{definition}[Strong Monad] A monad $M$ on a cartesian category $\C$ is called strong if there exists a natural transformation $\tau_{X,Y} : X \times MY \rightarrow M(X \times Y)$, satisfying the following conditions:
|
||||
\begin{alignat*}{1}
|
||||
&M\pi_2 \circ \tau_{1,X} = \pi_2 \tag*{(S1)}\label{S1}\\
|
||||
&\tau_{X,Y} \circ (id_X \times \eta_Y) = \eta_{X\times Y} \tag*{(S2)}\label{S2}\\
|
||||
|
|
@ -216,7 +241,7 @@ Now we can express the above condition:
|
|||
Free objects are constructions capturing the essence of structures in a minimal way, we will rely on free structures in chapter~\ref{chp:iteration} to define a monad in a general setting. We recall the definition to establish some notation:
|
||||
|
||||
\begin{definition}[Free Object]
|
||||
Let $\mathcal{C}, \mathcal{D}$ be categories and $U : C \rightarrow D$ a forgetful functor (whose construction usually is obvious). A free object on some object $X \in \mathcal{D}$ is an object $FX \in \mathcal{C}$ together with a morphism $\eta : X \rightarrow UFX$ such that the following universal property holds for any $Y \in \obj{C}$ and $f : X \rightarrow UY$:
|
||||
Let $\C, \mathcal{D}$ be categories and $U : C \rightarrow D$ a forgetful functor (whose construction usually is obvious). A free object on some object $X \in \mathcal{D}$ is an object $FX \in \C$ together with a morphism $\eta : X \rightarrow UFX$ such that the following universal property holds for any $Y \in \obj{C}$ and $f : X \rightarrow UY$:
|
||||
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJGWCJdLFswLDEsImYiXSxbMCwyLCJcXGV0YSIsMl0sWzIsMSwiXFxleGlzdHMhXFxsbGJyYWNrZXQgZiBcXHJyYnJhY2tldCIsMl1d
|
||||
\[\begin{tikzcd}
|
||||
X & UY \\
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
\chapter{Partiality Monads}
|
||||
\chapter{Partiality Monads}\label{chp:partiality}
|
||||
Moggi's categorical semantics~\cite{moggi} give us a way to interpret an effectul programming language in a category. For this one needs a (strong) monad $T$ capturing the desired effects, then we can take the elements of $TA$ as denotations for programs of type $A$. The kleisli category of $T$ can be viewed as the category of programs, which gives us a way of composing programs (Kleisli composition).
|
||||
|
||||
For this thesis we will restrict ourselves to monads for modelling partiality, the goal of this chapter is to capture what it means to be a partiality monad and look at two common examples.
|
||||
|
|
@ -355,6 +355,7 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre
|
|||
the last step holds generally for any $f : DX \times DY \rightarrow D(X \times Y)$.
|
||||
\end{proof}
|
||||
|
||||
\change[inline]{wording}
|
||||
We have now seen that $\mathbf{D}$ is strong and commutative, ideally we would want it to be an equational lifting monad, but this is not the case since besides modelling non-termination, the delay monad also captures the execution time. This is a result of the too intensional notion of equality that this monad comes with.
|
||||
|
||||
In chapter~\ref{chp:setoids} we will see how to remedy this, by taking the quotient of the delay monad where execution time is ignored. This will then give us an equational lifting monad in the category of setoids, but Chapman et al.~\cite{quotienting} have found that this does not work generally without assuming some form of the axiom of countable choice (which crucially holds in the category of setoids).
|
||||
|
|
@ -23,39 +23,39 @@ In this chapter we will draw on the inherent connection between recursion and it
|
|||
A morphism between Elgot algebras $h : (A, (-)^{\#_a}) \rightarrow (B, (-)^{\#_a})$ is an iteration preserving morphism $h : A \rightarrow B$ i.e. a morphism satisfying: $h \circ f^{\#_a} = ((h + id) \circ f)^{\#_b}$ for any $f : X \rightarrow A + X$.
|
||||
|
||||
\begin{theorem}
|
||||
Elgot algebras on a category $\mathcal{C}$ and the morphisms between them form a category that we call $\mathit{Elgot}(\mathcal{C})$.
|
||||
Elgot algebras on a category $\C$ and the morphisms between them form a category that we call $\elgotalgs{\C}$.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
The identity morphism $id : (A, (-)^\#) \rightarrow (A, (-)^\#)$ is the identity morphism of $\mathcal{C}$ that is trivially iteration preserving.
|
||||
The identity morphism $id : (A, (-)^\#) \rightarrow (A, (-)^\#)$ is the identity morphism of $\C$ that is trivially iteration preserving.
|
||||
|
||||
Composition of two morphisms $f : (B , (-)^{\#_b}) \rightarrow (C, (-)^{\#_c})$ and $g : (A , (-)^{\#_a}) \rightarrow (B , (-)^{\#_b})$ is the composition of the underlying morphisms, we are left to check that it is iteration preserving, i.e. let $X \in \obj{C}$ and $h : X \rightarrow A + X$:
|
||||
Composition of two morphisms $f : (B , (-)^{\#_b}) \rightarrow (C, (-)^{\#_c})$ and $g : (A , (-)^{\#_a}) \rightarrow (B , (-)^{\#_b})$ is the composition of the underlying morphisms, we are left to check that it is iteration preserving, i.e. let $X \in \obj{\C}$ and $h : X \rightarrow A + X$:
|
||||
\begin{alignat*}{1}
|
||||
&f \circ g \circ h^{\#_a}\\
|
||||
=\;& f \circ ((g + id) \circ h)^{\#_b}\tag*{g iteration preserving}\\
|
||||
=\;&((f \circ g) \circ h)^{\#_c}\tag*{f iteration preserving}
|
||||
\end{alignat*}
|
||||
|
||||
The laws concerning $id$ and composition follow directly since they hold in $\mathcal{C}$.
|
||||
The laws concerning $id$ and composition follow directly since they hold in $\C$.
|
||||
\end{proof}
|
||||
|
||||
We can form products and exponentials of Elgot algebras in a canonical way, for products this is even stronger:
|
||||
|
||||
\begin{lemma}
|
||||
If $\mathcal{C}$ is a cartesian category, so is $\mathit{Elgot}(\mathcal{C})$.
|
||||
If $\C$ is a cartesian category, so is $\elgotalgs{\C}$.
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
Let $1$ be the terminal object of $\mathcal{C}$. Given $f : X \rightarrow 1 + X$ we define the iteration $f^\# =\;! : X \rightarrow 1$ as the unique morphism into the terminal object. The laws of Elgot algebras then follow instantly, i.e. $(1 , !)$ is an Elgot algebra and it is the terminal object in $\mathit{Elgot}(\mathcal{C})$ since $!$ is trivially iteration preserving.
|
||||
Let $1$ be the terminal object of $\C$. Given $f : X \rightarrow 1 + X$ we define the iteration $f^\# =\;! : X \rightarrow 1$ as the unique morphism into the terminal object. The laws of Elgot algebras then follow instantly, i.e. $(1 , !)$ is an Elgot algebra and it is the terminal object in $\elgotalgs{\C}$ since $!$ is trivially iteration preserving.
|
||||
|
||||
Let $(A, (-)^{\#_a}) , (B, (-)^{\#_b}) \in \vert\mathit{Elgot}(\mathcal{C})\vert$ and $A \times B$ be the product in $\mathcal{C}$. Given $f : X \rightarrow (A \times B) + X$ we define the iteration as:
|
||||
Let $(A, (-)^{\#_a}) , (B, (-)^{\#_b}) \in \vert\elgotalgs{\C}\vert$ and $A \times B$ be the product in $\C$. Given $f : X \rightarrow (A \times B) + X$ we define the iteration as:
|
||||
\[f^\# = \langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle : X \rightarrow A \times B\]
|
||||
Then $(A \times B, (-)^\#)$ is indeed an Elgot algebra, the laws follow by the laws of the algebras on A and B.
|
||||
|
||||
The product diagram of $A \times B$ in $\mathcal{C}$ then also holds in $\mathit{Elgot}(\mathcal{C})$, we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism $\langle f , g \rangle$ is iteration preserving for any $f : (Z, (-)^{\#_z}) \rightarrow (X, (-)^{\#_x}), g : (Z, (-)^{\#_z}) \rightarrow (Y, (-)^{\#_y})$, which follows since $f$ and $g$ are iteration preserving.
|
||||
The product diagram of $A \times B$ in $\C$ then also holds in $\elgotalgs{\C}$, we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism $\langle f , g \rangle$ is iteration preserving for any $f : (Z, (-)^{\#_z}) \rightarrow (X, (-)^{\#_x}), g : (Z, (-)^{\#_z}) \rightarrow (Y, (-)^{\#_y})$, which follows since $f$ and $g$ are iteration preserving.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}\label{lem:elgotexp}
|
||||
Given $X \in \obj{C}$ and $(A, (-)^{\#_a}) \in \vert\mathit{Elgot}(\mathcal{C})\vert$. The exponential $X^A$ (if it exists) can be equipped with an Elgot algebra structure.
|
||||
Given $X \in \obj{\C}$ and $(A, (-)^{\#_a}) \in \vert\elgotalgs{\C}\vert$. The exponential $X^A$ (if it exists) can be equipped with an Elgot algebra structure.
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
Take $f^\# = curry (((eval + id) \circ dstr \circ (f \times id))^{\#_a})$ for any $f : Z \rightarrow A^X + Z$.
|
||||
|
|
@ -78,22 +78,45 @@ We can form products and exponentials of Elgot algebras in a canonical way, for
|
|||
\change[inline]{be more concrete with types here}
|
||||
\end{remark}
|
||||
|
||||
Pre-Elgot monads on $\C$ form a category that is a subcategory of $\monads{\C}$.
|
||||
|
||||
\begin{definition}[Category of pre-Elgot monads]
|
||||
Let $\C$ be a category. We define the category $\preelgot{\C}$ where objects are pre-Elgot monads and a morphism between two pre-Elgot monads $(S, \eta^S, \mu^S, (-)^{\#_S})$ and $(T, \eta^T, \mu^T, (-)^{\#_T})$ is a natural transformation $\alpha : S \rightarrow T$ satisfying the following diagrams:
|
||||
% https://q.uiver.app/#q=WzAsMTEsWzAsMCwiWCJdLFsyLDAsIlNYIl0sWzIsMSwiVFgiXSxbMywwLCJTU1giXSxbNSwwLCJTVFgiXSxbMywxLCJTWCJdLFs1LDEsIlRUWCJdLFs0LDIsIlRYIl0sWzYsMCwiWCJdLFs4LDAsIlNBIl0sWzgsMSwiVEEiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl0sWzksMTAsIlxcYWxwaGEiXSxbOCw5LCJoXntcXCNfU30iXSxbOCwxMCwiKChcXGFscGhhICsgaWQpIFxcY2lyYyBmKV57XFwjX1R9IiwyXV0=
|
||||
\[\begin{tikzcd}
|
||||
X && SX & SSX && STX & X && SA \\
|
||||
&& TX & SX && TTX &&& TA \\
|
||||
&&&& TX
|
||||
\arrow["{\eta^S}", from=1-1, to=1-3]
|
||||
\arrow["\alpha", from=1-3, to=2-3]
|
||||
\arrow["{\eta^T}"', from=1-1, to=2-3]
|
||||
\arrow["S\alpha", from=1-4, to=1-6]
|
||||
\arrow["{\mu^S}"', from=1-4, to=2-4]
|
||||
\arrow["\alpha", from=1-6, to=2-6]
|
||||
\arrow["\alpha"', from=2-4, to=3-5]
|
||||
\arrow["{\mu^T}", from=2-6, to=3-5]
|
||||
\arrow["\alpha", from=1-9, to=2-9]
|
||||
\arrow["{h^{\#_S}}", from=1-7, to=1-9]
|
||||
\arrow["{((\alpha + id) \circ h)^{\#_T}}"', from=1-7, to=2-9]
|
||||
\end{tikzcd}\]
|
||||
\end{definition}
|
||||
|
||||
\todo[inline]{Category of (strong) pre-Elgot monads, introduce category of monads in preliminaries}
|
||||
|
||||
\section{The Initial Pre-Elgot Monad}
|
||||
In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial pre-Elgot monad.
|
||||
|
||||
\begin{lemma}
|
||||
If every $X \in \obj{C}$ extends to a free Elgot algebra $KX$ we get a monad $\mathbf{K}$.
|
||||
If every $X \in \obj{\C}$ extends to a free Elgot algebra $KX$ we get a monad $\mathbf{K}$.
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
Existence of all free objects in $\mathit{Elgot}(\mathcal{C})$ yields an adjunction between $\mathcal{C}$ and $\mathit{Elgot}(\mathcal{C})$ that in turn gives us a monad on $\mathcal{C}$.
|
||||
Existence of all free objects in $\elgotalgs{\C}$ yields an adjunction between $\C$ and $\elgotalgs{\C}$ that in turn gives us a monad on $\C$.
|
||||
\end{proof}
|
||||
|
||||
To show that $\mathbf{K}$ is strong we will need a notion of stability:
|
||||
|
||||
\begin{definition}[Right-Stable Free Elgot Algebra]\label{def:rightstablefreeelgot}
|
||||
Let $KY$ be a free Elgot algebra on $Y \in \obj{C}$. We call $KY$ \textit{right-stable} if for every $A \in \mathit{Elgot}(\mathcal{C})$ and $f : X \times Y \rightarrow A$ there exists a unique $f^{\sharp_r} : X \times KY \rightarrow A$ satisfying:
|
||||
Let $KY$ be a free Elgot algebra on $Y \in \obj{\C}$. We call $KY$ \textit{right-stable} if for every $A \in \elgotalgs{\C}$ and $f : X \times Y \rightarrow A$ there exists a unique $f^{\sharp_r} : X \times KY \rightarrow A$ satisfying:
|
||||
\begin{alignat*}{1}
|
||||
&f = f^{\sharp_r} \circ (id \times \eta)\tag*{($\sharp_r 1$)}\label{sharpr1}\\
|
||||
&f^{\sharp_r} \circ (id \times h^\#) = ((f + id) \circ dstl \circ (id \times h))^\#\tag*{($\sharp_r 2$)}\label{sharpr2}
|
||||
|
|
@ -104,7 +127,7 @@ To show that $\mathbf{K}$ is strong we will need a notion of stability:
|
|||
We get the following dual definition:
|
||||
|
||||
\begin{definition}[Left-Stable Free Elgot Algebra]\label{def:leftstablefreeelgot}
|
||||
Let $KY$ be a free Elgot algebra on $Y \in \obj{C}$. We call $KY$ \textit{left-stable} if for every $A \in \mathit{Elgot}(\mathcal{C})$ and $f : Y \times X \rightarrow A$ there exists a unique $f^{\sharp_l} : KY \times X \rightarrow A$ satisfying:
|
||||
Let $KY$ be a free Elgot algebra on $Y \in \obj{\C}$. We call $KY$ \textit{left-stable} if for every $A \in \elgotalgs{\C}$ and $f : Y \times X \rightarrow A$ there exists a unique $f^{\sharp_l} : KY \times X \rightarrow A$ satisfying:
|
||||
\begin{alignat*}{1}
|
||||
&f = f^{\sharp_l} \circ (\eta \times id)\tag*{($\sharp_l 1$)}\label{sharpl1}\\
|
||||
&f^{\sharp_l} \circ (h^\# \times id) = ((f + id) \circ dstr \circ (h \times id))^\#\tag*{($\sharp_l 2$)}\label{sharpl2}
|
||||
|
|
@ -129,15 +152,15 @@ We will usually refer to right-stable free Elgot algebras as just stable Elgot a
|
|||
|
||||
Stability of $KX$ expresses that it somehow behaves like it would in a cartesian closed category, the following theorem should then follow trivially:
|
||||
|
||||
\begin{theorem}
|
||||
\begin{theorem}\label{thm:stability}
|
||||
In a cartesian closed category every free Elgot algebra is stable.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
Let $X \in \obj{C}$ and $((KX, (-)^\#), \llbracket - \rrbracket)$ be a free Elgot algebra on $X$.
|
||||
Let $X \in \obj{\C}$ and $((KX, (-)^\#), \llbracket - \rrbracket)$ be a free Elgot algebra on $X$.
|
||||
|
||||
We will show that $KX$ is left-stable, i.e. given $X \in \obj{C}, A \in \vert\mathit{Elgot}(\mathcal{C})\vert$ and $f : Y \times X \rightarrow A$ we define
|
||||
We will show that $KX$ is left-stable, i.e. given $X \in \obj{\C}, A \in \vert\elgotalgs{\C}\vert$ and $f : Y \times X \rightarrow A$ we define
|
||||
$f^{\sharp_l} := eval \circ (\llbracket curry\;f \rrbracket \times id)$.
|
||||
Note that we are using the universal property of a free object over $\textit{Elgot}(\mathcal{C})$ which when spelled out requires us to show that $A^X$ is an Elgot algebra, for that we reference lemma~\ref{lem:elgotexp}.
|
||||
Note that we are using the universal property of a free object over $\textit{Elgot}(\C)$ which when spelled out requires us to show that $A^X$ is an Elgot algebra, for that we reference lemma~\ref{lem:elgotexp}.
|
||||
\ref{sharpl1} and \ref{sharpl2} then follow by properties of the exponential and of distributive categories, uniqueness is more interesting:
|
||||
Let $g : KY \times X \rightarrow A$ be a morphism satisfying \ref{sharpl1} and \ref{sharpl2}, we need to show that $g = eval \circ (\llbracket curry\;f \rrbracket \times id)$. We use that fact that $curry$ is an injective mapping, i.e. it suffices to show that:
|
||||
\[curry\; g = \llbracket curry\;f \rrbracket = curry (eval \circ (\llbracket curry\;f \rrbracket \times id))\]
|
||||
|
|
@ -149,13 +172,13 @@ For the rest of this chapter we will assume every $KX$ to exist and be stable to
|
|||
Before proving strength, we will introduce a proof principle similar to remark~\ref{rem:coinduction}.
|
||||
|
||||
\begin{remark}[Proof by stability]~\label{rem:proofbystability}
|
||||
Given two morphisms $g, h : X \times KY \rightarrow A$ where $X, Y \in \obj{C}, A \in \elgotobj{C}$ to show that $g = h$ it suffices to find a morphism $f : X \times Y \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpr1} and \ref{sharpr2}.
|
||||
Given two morphisms $g, h : X \times KY \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$ to show that $g = h$ it suffices to find a morphism $f : X \times Y \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpr1} and \ref{sharpr2}.
|
||||
\end{remark}
|
||||
|
||||
Of course there is also a symmetric version of this:
|
||||
|
||||
\begin{remark}[Proof by left-stability]~\label{rem:proofbyleftstability}
|
||||
Given two morphisms $g, h : KY \times X \rightarrow A$ where $X, Y \in \obj{C}, A \in \elgotobj{C}$ to show that $g = h$ it suffices to find a morphism $f : Y \times X \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpl1} and \ref{sharpl2}.
|
||||
Given two morphisms $g, h : KY \times X \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$ to show that $g = h$ it suffices to find a morphism $f : Y \times X \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpl1} and \ref{sharpl2}.
|
||||
\end{remark}
|
||||
|
||||
\begin{theorem}
|
||||
|
|
@ -267,7 +290,7 @@ Of course there is also a symmetric version of this:
|
|||
\end{tikzcd}\]
|
||||
The proofs for \ref{sharpr1} and the proof that $\hat{\tau}^* \circ \tau$ is right iteration preserving are straightforward and can be looked up in the formalization.
|
||||
The proof that $\tau^* \circ \hat{\tau}$ is right iteration preserving is non-trivial, so we will look at it in more detail:
|
||||
Let $Z \in \obj{C}, h : Z \rightarrow KY + Z$ and let us introduce a definition for brevity: $\psi = \tau^* \circ \hat{\tau}$. We now use remark~\ref{rem:proofbyleftstability} to show that $\psi$ is right iteration preserving:
|
||||
Let $Z \in \obj{\C}, h : Z \rightarrow KY + Z$ and let us introduce a definition for brevity: $\psi = \tau^* \circ \hat{\tau}$. We now use remark~\ref{rem:proofbyleftstability} to show that $\psi$ is right iteration preserving:
|
||||
|
||||
% https://q.uiver.app/#q=WzAsNCxbNCwwLCJLWCBcXHRpbWVzIEtZIl0sWzQsMSwiSyhYIFxcdGltZXMgWSkiXSxbMCwxLCJLWCBcXHRpbWVzIFoiXSxbMCwzLCJYIFxcdGltZXMgWiJdLFswLDEsIlxccHNpIl0sWzIsMCwiaWQgXFx0aW1lcyBoXlxcIyJdLFsyLDEsIigoXFxwc2kgKyBpZCkgXFxjaXJjIGRzdGwgXFxjaXJjIChpZCBcXHRpbWVzIGgpKV5cXCMiLDJdLFszLDIsIlxcZXRhIFxcdGltZXMgaWQiXSxbMywxLCJcXHRhdSBcXGNpcmMgKGlkIFxcdGltZXMgaF5cXCMpIiwyXV0=
|
||||
\[\begin{tikzcd}
|
||||
|
|
|
|||
|
|
@ -1,11 +1,159 @@
|
|||
\chapter{A Case Study on Setoids}\label{chp:setoids}
|
||||
|
||||
\todo[inline]{Introduce category of setoids}
|
||||
In chapter~\ref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality but it also respects computation time. One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified. In this chapter we will use the quotients-as-setoid approach, i.e. we will work in the category of setoids and show that the quotiented delay monad is the initial pre-Elgot monad in this category.
|
||||
|
||||
\todo[inline]{introduce delay monad in agda (coinductive types)}
|
||||
Let us introduce the category that we are working in:
|
||||
|
||||
\todo[inline]{quotient of delay}
|
||||
\section{Setoids in Type Theory}
|
||||
|
||||
\todo[inline]{proof: delay is monad}
|
||||
\begin{definition}[Setoid]
|
||||
A setoid is a tuple $(A, \hat{=})$ where $A$ (usually called the \textit{carrier}) is a type and $\hat{=}$ an equivalence relation on the inhabitants of $A$.
|
||||
\end{definition}
|
||||
|
||||
\todo[inline]{proof: delay is free elgot}
|
||||
Morphisms between setoids are functions that respect the equivalence relation:
|
||||
|
||||
\begin{definition}[Setoid Morphism]
|
||||
A morphism between two setoids $(A , =^A)$ and $(B , =^B)$ is a function $f : A \rightarrow B$ such that $x =^A y$ implies $fx =^B fy$ for any $x, y : A$.
|
||||
\end{definition}
|
||||
|
||||
Setoids and setoid morphisms form a category that we call $\setoids$.
|
||||
|
||||
\improvement[inline]{Text is not good}
|
||||
\todo[inline]{sketch the proof that setoids is CCC and cocartesian}
|
||||
|
||||
|
||||
\section{Quotienting the Delay Monad}
|
||||
% TODO merge this into introduction
|
||||
% Chapman et al. have already proven that quotienting the delay datatype by weak bisimilarity using the quotients-as-setoids approach yields a monad~\cite{quotienting}, we will build upon their results and show that this quotient is indeed an instance of our monad $\mathbf{K}$.
|
||||
% Historically proof assistants like Agda and Coq have been offering multiple ways of defining coinductive types, nowadays the manuals of both Agda and Coq advise users to use coinductive records instead of defining coinductive types by constructors, we will heed this advice.
|
||||
% Since the delay monad is usually defined by the constructors $now$ and $later$
|
||||
|
||||
Originally the delay monad has been introduced as a coinductive datatype with two constructors, in pseudo Agda-like code this would look something like:
|
||||
\begin{minted}{agda}
|
||||
codata (A : Set) : Set where
|
||||
now : A → Delay A
|
||||
later : Delay A → Delay A
|
||||
\end{minted}
|
||||
|
||||
This style is sometimes called \textit{positively coinductive} and is nowadays advised against in the manuals of both Agda and Coq\todo{cite}. Instead one is advised to use coinductive records, we will heed this advice and use the following representation of the delay monad in Agda:
|
||||
|
||||
\todo[inline]{cite https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html somehow}
|
||||
|
||||
\begin{minted}{agda}
|
||||
mutual
|
||||
data Delay (A : Set) : Set where
|
||||
now : A → Delay A
|
||||
later : Delay′ A → Delay A
|
||||
record Delay′ (A : Set) : Set where
|
||||
coinductive
|
||||
field force : Delay A
|
||||
\end{minted}
|
||||
|
||||
Here \Verb{Delay} is defined as a inductive datatype where the coinductive part of the original definition (i.e. the coinductive occurence of the delay type in the \Verb{later} constructor) references a coinductive record \Verb{Delay'} which consists of only one field that forces a coinductive value to an inductive one.
|
||||
|
||||
For the sake of readability we will introduce other concepts only by inference rules instead of Agda code, for the delay monad this looks like:
|
||||
|
||||
\[
|
||||
\inferrule*{x : A}{now\; x : Delay \;A} \hskip 1cm
|
||||
\inferrule*{x : Delay' \;A}{later \;x : Delay\; A} \hskip 1cm
|
||||
\mprset{fraction={===}}\inferrule*{x : Delay' \;A}{force \;x : Delay \;A}
|
||||
\]
|
||||
|
||||
We will now introduce two notions of equality on inhabitants of the delay type, given a setoid $(A, =^A)$ we call the equivalence received by lifting $=^A$ to $Delay\;A$ \textit{strong bisimilarity}, the definition is as follows:
|
||||
|
||||
\[
|
||||
\inferrule*{eq : x =^A y}{now \;eq : x \sim y} \hskip 1cm
|
||||
\inferrule*{eq : force \;x \sim' force\; y}{later\;eq : later\; x \sim later\; y} \hskip 1cm
|
||||
\mprset{fraction={===}}\inferrule*{eq : x \sim' y}{force\; eq : x \sim y}
|
||||
\]
|
||||
|
||||
\begin{lemma}
|
||||
$(Delay\;A, \sim)$ is a setoid.
|
||||
\end{lemma}
|
||||
|
||||
In $(Delay\;A, \sim)$ computations that evaluate to the same result but in a different amount of time are not equal. We will now quotient this type by weak bisimilarity, i.e. we will identify all computations that terminate with the same result. Let us first consider what it means for a computation to evaluate to some result:
|
||||
|
||||
\[
|
||||
\inferrule*{eq : x =^A y}{now\; eq : now\;x \downarrow y} \hskip 1cm
|
||||
\inferrule*{d : force\;x \downarrow c}{later\;d : later\;x \downarrow c }
|
||||
\]
|
||||
|
||||
Now we can relate two computations \textit{iff} they evaluate to the same result:
|
||||
\[
|
||||
\inferrule*{eq : a =^A b \\ xa : x \downarrow a \\ yb : y \downarrow b}{\downarrow\approx \; eq \; xa \; yb : x \approx y} \hskip 1cm
|
||||
\inferrule*{eq : force \;x \approx' force \;y}{later\;eq : later \;x \approx later \;y} \hskip 1cm
|
||||
\mprset{fraction={===}}\inferrule*{eq : x \approx' y}{force\;eq : x \approx y}
|
||||
\]
|
||||
|
||||
\begin{lemma}
|
||||
$(Delay\;A, \approx)$ is a setoid.
|
||||
\end{lemma}
|
||||
|
||||
\begin{theorem}
|
||||
$(Delay\;A, \approx)$ is a monad.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
The monad unit is the constructor \Verb{now} and monad multiplication can be defined as follows:
|
||||
|
||||
\begin{minted}{agda}
|
||||
μ : Delay (Delay X) → Delay X
|
||||
μ' : Delay' (Delay X) → Delay' X
|
||||
μ (now x) = x
|
||||
μ (later x) = later (μ' x)
|
||||
force (μ' x) = μ (force x)
|
||||
\end{minted}
|
||||
|
||||
The monad laws have already been proven in~\cite{quotienting} and in our own formalization so we will not reiterate the proofs here.
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}
|
||||
$(Delay\;A , \approx)$ is an instance of $\mathbf{K}$ in the category $\setoids$.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
We need to show that for every setoid $(A, =^A)$ the resulting setoid $(Delay\;A, \approx)$ can be extended to a stable free Elgot algebra.
|
||||
Stability follows automatically by theorem~\ref{thm:stability} and the fact that $\setoids$ is cartesian closed, so it suffices to define a free elgot Algebra on $(Delay\;A, \approx)$.
|
||||
|
||||
Let $(X , =^X) \in \obj{\setoids}$ and $f : X \rightarrow Delay\; A + X$ be a setoid morphism, we define $f^\# : X \rightarrow Delay\;A$ pointwise:
|
||||
\[
|
||||
f^\# (x) :=
|
||||
\begin{cases}
|
||||
a & \text{if } f\;x = i_1 (a)\\
|
||||
later\;(f^{\#'} a) & \text{if } f\;x = i_2 (a)
|
||||
\end{cases}
|
||||
\]
|
||||
where $f^{\#'} : X \rightarrow Delay'\;A$ is defined corecursively by:
|
||||
\[
|
||||
force (f^{\#'}(x)) = f^\#(x)
|
||||
\]
|
||||
|
||||
Let us first show that $f^\#$ is a setoid morphism, i.e. given $x, y : X$ with $x =^X y$, we need to show that $f^\#(x) = f^\#(y)$. Since $f$ is a setoid morphism we know that $f(x) =^+ f(y)$ in the coproduct setoid $(Delay\;A + X, =^+)$. We proceed by case distinction on $f(x)$:
|
||||
|
||||
\begin{itemize}
|
||||
\item Case $f(x) = i_1 (a)$:
|
||||
\[f^\# (x) = a = f^\#(y)\]
|
||||
|
||||
\item Case $f(x) = i_2 (a)$:
|
||||
\[f^\# (x) = later (f^{\#'}(a)) = f^\# (y)\]
|
||||
\end{itemize}
|
||||
|
||||
Now we check the iteration laws:
|
||||
|
||||
\change[inline]{change the equivalence sign of coproducts}
|
||||
|
||||
\begin{itemize}
|
||||
\item \textbf{Fixpoint}: We need to show that $f^\# (x) \approx ([ id , f^\# ] \circ f)(x)$:
|
||||
|
||||
\begin{itemize}
|
||||
\item Case $f(x) =^+ i_1 (a)$:
|
||||
\[ f^\#(x) \approx a \approx [ id , f^\# ] (i_1 (a)) = ([ id , f^\# ] \circ f) (x) \]
|
||||
\item Case $f(x) =^+ i_2 (a)$:
|
||||
\[ f^\#(x) \approx later (f^{\#'}(a)) \overset{(*)}{\approx} f^\#(a) \approx [ id , f^\# ] (i_2 (a)) \approx ([ id , f^\# ] \circ f) (x)\]
|
||||
\end{itemize}
|
||||
where $(*)$ follows from a general fact: any $z : Delay'\;A$ satisfies $force\;z \approx later\;z$.
|
||||
\item \textbf{Uniformity}: Let $(Y , =^Y) \in \setoids$ and $g : Y \rightarrow Delay\; A + Y, h : X \rightarrow Y$ be setoid morphisms with $(id + h) \circ f = g \circ h$.
|
||||
\item \textbf{Folding}:
|
||||
\end{itemize}
|
||||
|
||||
|
||||
|
||||
\end{proof}
|
||||
|
|
|
|||
Loading…
Reference in a new issue