mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
sync
This commit is contained in:
parent
4d24b1d0e5
commit
fd7b498554
2 changed files with 40 additions and 11 deletions
|
@ -65,6 +65,9 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
|
||||||
|
|
||||||
open StrongBisimilarity renaming (_∼_ to [_][_∼_])
|
open StrongBisimilarity renaming (_∼_ to [_][_∼_])
|
||||||
|
|
||||||
|
_⊥ₛ' : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
|
||||||
|
_⊥ₛ' A = record { Carrier = ∣ A ∣ ⊥ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } }
|
||||||
|
|
||||||
module WeakBisimilarity (A : Setoid c (c ⊔ ℓ)) where
|
module WeakBisimilarity (A : Setoid c (c ⊔ ℓ)) where
|
||||||
data _↓_ : ∣ A ∣ ⊥ → ∣ A ∣ → Set (c ⊔ ℓ) where
|
data _↓_ : ∣ A ∣ ⊥ → ∣ A ∣ → Set (c ⊔ ℓ) where
|
||||||
now↓ : ∀ {x y} (x≡y : [ A ][ x ≡ y ]) → now x ↓ y
|
now↓ : ∀ {x y} (x≡y : [ A ][ x ≡ y ]) → now x ↓ y
|
||||||
|
@ -251,4 +254,21 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
|
||||||
; identityˡ = identityˡ
|
; identityˡ = identityˡ
|
||||||
; identityʳ = identityʳ
|
; identityʳ = identityʳ
|
||||||
}
|
}
|
||||||
|
|
||||||
|
strongMonad : Monad (Setoids c (c ⊔ ℓ))
|
||||||
|
strongMonad = record
|
||||||
|
{ F = record
|
||||||
|
{ F₀ = _⊥ₛ'
|
||||||
|
; F₁ = λ {A} {B} f → record { _⟨$⟩_ = liftF (f ._⟨$⟩_) ; cong = {! !} }
|
||||||
|
; identity = {! !}
|
||||||
|
; homomorphism = {! !}
|
||||||
|
; F-resp-≈ = {! !}
|
||||||
|
}
|
||||||
|
; η = {! !}
|
||||||
|
; μ = {! !}
|
||||||
|
; assoc = {! !}
|
||||||
|
; sym-assoc = {! !}
|
||||||
|
; identityˡ = {! !}
|
||||||
|
; identityʳ = {! !}
|
||||||
|
}
|
||||||
```
|
```
|
|
@ -10,7 +10,7 @@ open import Function.Equality as SΠ renaming (id to idₛ)
|
||||||
open import Codata.Musical.Notation
|
open import Codata.Musical.Notation
|
||||||
open import Function using (_∘′_) renaming (_∘_ to _∘f_)
|
open import Function using (_∘′_) renaming (_∘_ to _∘f_)
|
||||||
import Relation.Binary.PropositionalEquality as Eq
|
import Relation.Binary.PropositionalEquality as Eq
|
||||||
open Eq using (_≡_) renaming (sym to ≣-sym)
|
open Eq using (_≡_) renaming (sym to ≣-sym; refl to ≣-refl; trans to ≣-trans)
|
||||||
open import FreeObject
|
open import FreeObject
|
||||||
open import Categories.FreeObjects.Free
|
open import Categories.FreeObjects.Free
|
||||||
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
|
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
|
||||||
|
@ -75,6 +75,13 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
||||||
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
|
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
|
||||||
... | inj₂ a | inj₂ b = ≈-sym A (later-eq (later≈ (♯ iter-cong f (≡-sym X (inj₂-helper f x≡y eqx eqy)))))
|
... | inj₂ a | inj₂ b = ≈-sym A (later-eq (later≈ (♯ iter-cong f (≡-sym X (inj₂-helper f x≡y eqx eqy)))))
|
||||||
|
|
||||||
|
iter-fixpoint' : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (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 = ∼-sym A {! !} -- ≈-sym A (later-eq (later≈ (♯ iter-cong f (≡-sym X (inj₂-helper f x≡y eqx eqy)))))
|
||||||
|
|
||||||
iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (A ⊥ₛ ⊎ₛ X)) → X ⟶ A ⊥ₛ
|
iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (A ⊥ₛ ⊎ₛ X)) → X ⟶ A ⊥ₛ
|
||||||
iterₛ {A} {X} f = record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f }
|
iterₛ {A} {X} f = record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f }
|
||||||
|
|
||||||
|
@ -216,21 +223,23 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
|
||||||
out-cong {later x} {now y} x≡y = {! !}
|
out-cong {later x} {now y} x≡y = {! !}
|
||||||
out-cong {later x} {later y} x≡y = {! !}
|
out-cong {later x} {later y} x≡y = {! !}
|
||||||
|
|
||||||
|
set-setoid : ∀ {c} → Set c → Setoid c c
|
||||||
|
set-setoid A = record { Carrier = A ; _≈_ = _≡_ ; isEquivalence = record { refl = ≣-refl ; sym = ≣-sym ; trans = ≣-trans } }
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
|
delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
|
||||||
delay-lift {A} {B} f = record { h = (B Elgot-Algebra.#) helper ; preserves = {! !} }
|
delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = ((B Elgot-Algebra.#) helper) ._⟨$⟩_ ; cong = λ {x} {y} x≈y → ? } ; preserves = {! !} }
|
||||||
where
|
where
|
||||||
-- this definition of helper₁ corresponds to `(f + id) ∘ out`, but using the representation of _⊥ as a positive coinductive type
|
-- (f + id) ∘ out, this is just on sets
|
||||||
helper₁ : ∣ A ∣ ⊥ → ∣ ⟦ B ⟧ ∣ ⊎ ∣ A ∣ ⊥
|
helper₁ : ∣ A ∣ ⊥ → ∣ ⟦ B ⟧ ∣ ⊎ ∣ A ∣ ⊥
|
||||||
helper₁ (now x) = inj₁ (< f > x)
|
helper₁ (now x) = inj₁ (< f > x)
|
||||||
helper₁ (later x) = inj₂ (♭ x)
|
helper₁ (later x) = inj₂ (♭ x)
|
||||||
helper₁-cong : ∀ {x y : ∣ A ∣ ⊥} → [ A ][ x ≈ y ] → [ ⟦ B ⟧ ⊎ₛ A ⊥ₛ ][ helper₁ x ≡ helper₁ y ]
|
-- setoid-morphism that preserves strong-bisimilarity
|
||||||
helper₁-cong {now x} {now y} x≈y = {! !} -- yes
|
helper : A ⊥ₛ' ⟶ ⟦ B ⟧ ⊎ₛ A ⊥ₛ'
|
||||||
helper₁-cong {now x} {later y} x≈y = {! !} -- problematic, need to show inj₁ (f x) ≈ inj₂ y, which is contradictory, while the assumption now x ≈ later y is not contradictory.
|
helper = record { _⟨$⟩_ = helper₁ ; cong = {! !} }
|
||||||
helper₁-cong {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = {! !}
|
-- helper' :
|
||||||
helper₁-cong {later x} {later y} (later≈ x≈y) = {! !} -- cong inj₂ₛ (♭ x≈y)
|
-- is-cong :
|
||||||
helper₁-cong {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = {! !} --cong inj₂ₛ (↓≈ a≡b x↓a y↓b)
|
|
||||||
helper : A ⊥ₛ ⟶ ⟦ B ⟧ ⊎ₛ A ⊥ₛ
|
|
||||||
helper = record { _⟨$⟩_ = helper₁ ; cong = helper₁-cong }
|
|
||||||
|
|
||||||
freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
|
freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
|
||||||
freeAlgebra A = record
|
freeAlgebra A = record
|
||||||
|
|
Loading…
Reference in a new issue