mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
progress
This commit is contained in:
parent
32c479a027
commit
f93083706b
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 197 additions and 0 deletions
|
|
@ -179,6 +179,8 @@ 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 } }
|
||||
<_> = Π._⟨$⟩_
|
||||
|
||||
∼⇒≈ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ A ∣} → [ A ][ x ∼ y ] → [ A ][ x ≈ y ]
|
||||
|
|
|
|||
195
agda/src/Monad/Instance/Setoids/K'.lagda.md
Normal file
195
agda/src/Monad/Instance/Setoids/K'.lagda.md
Normal file
|
|
@ -0,0 +1,195 @@
|
|||
<!--
|
||||
```agda
|
||||
{-# OPTIONS --allow-unsolved-metas --guardedness #-}
|
||||
open import Level
|
||||
open import Relation.Binary
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
|
||||
open import Data.Sum.Function.Setoid
|
||||
open import Data.Sum.Relation.Binary.Pointwise
|
||||
open import Function.Equality as SΠ renaming (id to idₛ)
|
||||
open import Function using (_∘′_) renaming (_∘_ to _∘f_)
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_) renaming (sym to ≣-sym; refl to ≣-refl; trans to ≣-trans)
|
||||
open import FreeObject
|
||||
open import Categories.FreeObjects.Free
|
||||
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
|
||||
open import Categories.Category.Instance.Properties.Setoids.Choice using ()
|
||||
```
|
||||
-->
|
||||
|
||||
# The delay monad on the category of setoids is an instance of K
|
||||
|
||||
```agda
|
||||
module Monad.Instance.Setoids.K' {ℓ : Level} where
|
||||
open import Monad.Instance.K.Instance.D {ℓ} {ℓ}
|
||||
open import Category.Ambient.Setoids
|
||||
open import Monad.Instance.K (setoidAmbient {ℓ})
|
||||
open import Algebra.Elgot (setoidAmbient {ℓ})
|
||||
open import Algebra.Elgot.Free (setoidAmbient {ℓ})
|
||||
open import Category.Construction.ElgotAlgebras (setoidAmbient {ℓ})
|
||||
open import Monad.PreElgot (setoidAmbient {ℓ})
|
||||
open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_])
|
||||
open DelayMonad
|
||||
open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_])
|
||||
open eq using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
|
||||
|
||||
iter : ∀ {A X : Setoid ℓ ℓ} → (∣ X ∣ → (Delay ∣ A ∣ ⊎ ∣ X ∣)) → ∣ X ∣ → Delay ∣ A ∣
|
||||
iter′ : ∀ {A X : Setoid ℓ ℓ} → (∣ X ∣ → (Delay ∣ A ∣ ⊎ ∣ X ∣)) → ∣ X ∣ → Delay′ ∣ A ∣
|
||||
force (iter′ {A} {X} f x) = iter {A} {X} f x
|
||||
iter {A} {X} f x with f x
|
||||
... | inj₁ a = a
|
||||
... | inj₂ b = later (iter′ {A} {X} f x)
|
||||
|
||||
conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''}
|
||||
{x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≡ inj₂ y ] → Z
|
||||
conflict X Y ()
|
||||
|
||||
inj₁-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a b : ∣ Y ∣} → [ X ][ x ≡ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₁ b → [ Y ][ a ≡ b ]
|
||||
inj₁-helper {X} {Y} f {x} {y} {a} {b} x≡y fi₁ fi₂ = drop-inj₁ {x = a} {y = b} helper
|
||||
where
|
||||
helper : [ Y ⊎ₛ X ][ inj₁ a ≡ inj₁ b ]
|
||||
helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y
|
||||
|
||||
inj₂-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a b : ∣ X ∣} → [ X ][ x ≡ y ] → f ⟨$⟩ x ≡ inj₂ a → f ⟨$⟩ y ≡ inj₂ b → [ X ][ a ≡ b ]
|
||||
inj₂-helper {X} {Y} f {x} {y} {a} {b} x≡y fi₁ fi₂ = drop-inj₂ {x = a} {y = b} helper
|
||||
where
|
||||
helper : [ Y ⊎ₛ X ][ inj₂ a ≡ inj₂ b ]
|
||||
helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y
|
||||
|
||||
absurd-helper : ∀ {ℓ'} {X Y : Setoid ℓ ℓ} {A : Set ℓ'} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a : ∣ Y ∣} {b : ∣ X ∣} → [ X ][ x ≡ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₂ b → A
|
||||
absurd-helper {ℓ'} {X} {Y} {A} f {x} {y} {a} {b} x≡y fi₁ fi₂ = conflict Y X helper
|
||||
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) ]
|
||||
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
|
||||
... | inj₁ a | inj₂ b = absurd-helper f x≡y eqx eqy
|
||||
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
|
||||
... | inj₂ a | inj₂ b = later≈ (iter-cong′ f x≡y)
|
||||
|
||||
iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ A ⊎ₛ X)) → X ⟶ Delayₛ A
|
||||
iterₛ {A} {X} f = record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f }
|
||||
|
||||
iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈ [ Function.id , iter {A} {X} (f ._⟨$⟩_) ] ((f ._⟨$⟩_) y) ]
|
||||
iter-fixpoint {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
|
||||
... | inj₁ a | inj₂ b = absurd-helper f x≡y eqx eqy
|
||||
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
|
||||
... | inj₂ a | inj₂ b = ≈-trans A (≈-sym A later-self) (iter-cong f {! !})
|
||||
|
||||
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
|
||||
iter-resp-≈ {A} {X} f g f≋g {x} {y} x≡y with (f ._⟨$⟩_) x in eqx | (g ._⟨$⟩_) y in eqy
|
||||
... | inj₁ a | inj₁ b = drop-inj₁ helper
|
||||
where
|
||||
helper : [ Delayₛ A ⊎ₛ X ][ inj₁ a ≡ inj₁ b ]
|
||||
helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y
|
||||
... | inj₁ a | inj₂ b = conflict (Delayₛ A) X helper
|
||||
where
|
||||
helper : [ Delayₛ A ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
|
||||
helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y
|
||||
... | 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 eqy) | (≣-sym eqx) = f≋g x≡y
|
||||
... | inj₂ a | inj₂ b = later≈ (iter-resp-≈′ f g f≋g x≡y)
|
||||
|
||||
|
||||
iter-folding' : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → [ X ⊎ₛ Y ][ 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 ._⟨$⟩_)) ] y ]
|
||||
iter-folding′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → [ X ⊎ₛ Y ][ 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 ._⟨$⟩_)) ] y ]
|
||||
force≈ (iter-folding′ {A} {X} {Y} {f} {h} {x} {y} x≡y) = iter-folding' {A} {X} {Y} {f} {h} x≡y
|
||||
iter-folding' {A} {X} {Y} {f} {h} {inj₁ x} {inj₁ y} ix≡iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy
|
||||
... | inj₁ a | inj₁ b = inj₁-helper f (drop-inj₁ ix≡iy) eqx eqy
|
||||
... | inj₁ a | inj₂ b = absurd-helper f (drop-inj₁ ix≡iy) eqx eqy
|
||||
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X (drop-inj₁ ix≡iy)) eqy eqx
|
||||
... | inj₂ a | inj₂ b = later≈ helper
|
||||
where
|
||||
helper' : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ]
|
||||
helper'' : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ]
|
||||
helper'' b with f ⟨$⟩ b in eqb
|
||||
... | inj₁ c = ≈-refl A
|
||||
... | inj₂ c = later≈ (helper' b)
|
||||
force≈ (helper' b) with f ⟨$⟩ b in eqb
|
||||
... | inj₁ c = ≈-refl A
|
||||
... | inj₂ c = later≈ (helper' b)
|
||||
helper : [ A ][ iter < f > x ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ y) ]
|
||||
force≈ helper = ≈-trans A (iter-cong f (drop-inj₁ ix≡iy)) (helper'' y)
|
||||
|
||||
iter-folding' {A} {X} {Y} {f} {h} {inj₂ x} {inj₂ y} ix≡iy with h ⟨$⟩ x in eqx | h ⟨$⟩ y in eqy
|
||||
... | inj₁ a | inj₁ b = later≈ {! iter-folding′ {A} {X} {Y} {f} {h} {inj₁ a} {inj₁ b} helper !}
|
||||
where
|
||||
helper : [ X ⊎ₛ Y ][ inj₁ a ≡ inj₁ b ]
|
||||
helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
|
||||
... | inj₁ a | inj₂ b = absurd-helper h (drop-inj₂ ix≡iy) eqx eqy
|
||||
... | inj₂ a | inj₁ b = absurd-helper h (≡-sym Y (drop-inj₂ ix≡iy)) eqy eqx
|
||||
... | inj₂ a | inj₂ b = later≈ {! !}
|
||||
where
|
||||
helper' : [ A ][ iter [ inj₁ ∘′ iter < f > , inj₂ ∘′ < h > ] (inj₂ x) ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₂ y) ]
|
||||
force≈ helper' = later≈ {! iter-folding' {A} {X} {Y} {f} {h} {inj₂ a} {inj₂ b} ? !}
|
||||
helper : [ X ⊎ₛ Y ][ inj₂ a ≡ inj₂ b ]
|
||||
helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
|
||||
|
||||
|
||||
iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → [ X ⊎ₛ Y ][ 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 ._⟨$⟩_)) ] y ]
|
||||
iter-folding {A} {X} {Y} {f} {h} {inj₁ x} {inj₁ y} ix≡iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy
|
||||
... | inj₁ a | inj₁ b = inj₁-helper f (drop-inj₁ ix≡iy) eqx eqy
|
||||
... | inj₁ a | inj₂ b = absurd-helper f (drop-inj₁ ix≡iy) eqx eqy
|
||||
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X (drop-inj₁ ix≡iy)) eqy eqx
|
||||
... | inj₂ a | inj₂ b = later≈ {! !} -- later≈ (♯ ≈-trans A (iter-cong f (inj₂-helper f (drop-inj₁ ix≡iy) eqx eqy)) (helper b))
|
||||
where
|
||||
helper : ∀ (b : ∣ X ∣) → [ A ][ iter {A} {X} (f ._⟨$⟩_) b ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ (f ._⟨$⟩_) , inj₂ ∘′ (h ._⟨$⟩_) ] (inj₁ b) ]
|
||||
helper b with f ⟨$⟩ b in eqb
|
||||
... | inj₁ c = ≡-refl (Delayₛ A)
|
||||
... | inj₂ c = later≈ {! !} -- later≈ (♯ helper c)
|
||||
iter-folding {A} {X} {Y} {f} {h} {inj₂ x} {inj₂ y} ix≡iy with h ⟨$⟩ x in eqx | h ⟨$⟩ y in eqy
|
||||
... | inj₁ a | inj₁ b = {! !} -- later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₁ a} {inj₁ b} helper)
|
||||
where
|
||||
helper : [ X ⊎ₛ Y ][ inj₁ a ≡ inj₁ b ]
|
||||
helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
|
||||
... | inj₁ a | inj₂ b = absurd-helper h (drop-inj₂ ix≡iy) eqx eqy
|
||||
... | inj₂ a | inj₁ b = absurd-helper h (≡-sym Y (drop-inj₂ ix≡iy)) eqy eqx
|
||||
... | inj₂ a | inj₂ b = {! !} -- later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₂ a} {inj₂ b} helper)
|
||||
where
|
||||
helper : [ X ⊎ₛ Y ][ inj₂ a ≡ inj₂ b ]
|
||||
helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
|
||||
|
||||
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}
|
||||
; #-Uniformity = {! !} -- λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h}
|
||||
; #-Folding = λ {X} {Y} {f} {h} {x} {y} x≡y → iter-folding {A} {X} {Y} {f} {h} {x} {y} x≡y
|
||||
; #-resp-≈ = λ {X} {f} {g} → iter-resp-≈ {A} {X} f g
|
||||
}
|
||||
|
||||
delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra
|
||||
delay-algebras A = record { A = Delayₛ A ; algebra = delay-algebras-on {A}}
|
||||
|
||||
open Elgot-Algebra using () renaming (A to ⟦_⟧)
|
||||
|
||||
delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
|
||||
delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = ((B Elgot-Algebra.#) helper) ._⟨$⟩_ ; cong = λ {x} {y} x≈y → {! !} } ; preserves = {! !} }
|
||||
where
|
||||
-- (f + id) ∘ out
|
||||
helper₁ : Delay ∣ A ∣ → ∣ ⟦ B ⟧ ∣ ⊎ Delay ∣ A ∣
|
||||
helper₁ (now x) = inj₁ (< f > x)
|
||||
helper₁ (later x) = inj₂ (force x)
|
||||
-- -- setoid-morphism that preserves strong-bisimilarity
|
||||
helper : Delayₛ' A ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ' A
|
||||
helper = record { _⟨$⟩_ = helper₁ ; cong = {! !} }
|
||||
|
||||
freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
|
||||
freeAlgebra A = record
|
||||
{ FX = delay-algebras A
|
||||
; η = ηₛ A
|
||||
; _* = delay-lift
|
||||
; *-lift = {! !}
|
||||
; *-uniq = {! !}
|
||||
}
|
||||
|
||||
```
|
||||
Loading…
Reference in a new issue