From 8e6e1d01cd110302e5860049305881cb6cbaaf84 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 8 Jan 2024 12:57:33 +0100 Subject: [PATCH] minor and add sergeys suggestion --- agda/src/Monad/Instance/K/Instance/D.lagda.md | 69 ++++++++++++++++++- agda/src/Monad/Instance/Setoids/K'.lagda.md | 35 +++++++++- 2 files changed, 100 insertions(+), 4 deletions(-) diff --git a/agda/src/Monad/Instance/K/Instance/D.lagda.md b/agda/src/Monad/Instance/K/Instance/D.lagda.md index 4b9aee6..4d77415 100644 --- a/agda/src/Monad/Instance/K/Instance/D.lagda.md +++ b/agda/src/Monad/Instance/K/Instance/D.lagda.md @@ -1,7 +1,7 @@ ```agda {-# OPTIONS --allow-unsolved-metas --guardedness #-} -open import Level +open import Level renaming (zero to ℓ-zero; suc to ℓ-suc) open import Function.Equality as SΠ renaming (id to idₛ) open import Relation.Binary open import Data.Sum using (_⊎_; inj₁; inj₂) @@ -12,6 +12,8 @@ open import Function using (id) open import Categories.Monad open import Categories.Category.Instance.Setoids open import Categories.NaturalTransformation hiding (id) +open import Data.Product +open import Data.Nat using (ℕ; suc; zero) module Monad.Instance.K.Instance.D {c ℓ} where @@ -173,7 +175,20 @@ module Bisimilarity (A : Setoid c (c ⊔ ℓ)) where force≈ (≈′-trans x≈′y y≈′z) = ≈-trans (force≈ x≈′y) (force≈ y≈′z) -open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_]) + mutual + data _≲_ : Delay ∣ A ∣ → Delay ∣ A ∣ → Set (c ⊔ ℓ) where + ↓≲ : ∀ {y a} (y↓a : y ↓ a) → now a ≲ y + later≲ : ∀ {x y} (x≈y : force x ≲′ force y) → later x ≲ later y + + record _≲′_ (x y : Delay ∣ A ∣) : Set (c ⊔ ℓ) where + coinductive + + field + force≲ : x ≲ y + + open _≲′_ public + +open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_]; _≲_ to [_][_≲_]; _≲′_ to [_][_≲′_]) module DelayMonad where @@ -351,4 +366,54 @@ module DelayMonad where ; identityˡ = identityˡ ; identityʳ = identityʳ } + +module extra {A : Setoid c (c ⊔ ℓ)} where + ≲→≈ : {x y : Delay ∣ A ∣} → [ A ][ x ≲ y ] → [ A ][ x ≈ y ] + ≲→≈′ : {x y : Delay ∣ A ∣} → [ A ][ x ≲′ y ] → [ A ][ x ≈′ y ] + + ≲→≈ (↓≲ y↓a) = ↓≈ (≡-refl A) (now↓ (≡-refl A)) y↓a + ≲→≈ (later≲ x≈y) = later≈ (≲→≈′ x≈y) + + force≈ (≲→≈′ x≲′y) = ≲→≈ (force≲ x≲′y) + + race : Delay ∣ A ∣ → Delay ∣ A ∣ → Delay ∣ A ∣ + race′ : Delay′ ∣ A ∣ → Delay′ ∣ A ∣ → Delay′ ∣ A ∣ + + race (now a) _ = now a + race (later x) (now a) = now a + race (later x) (later y) = later (race′ x y) + + force (race′ x y) = race (force x) (force y) + + ≈→≲₀ : ∀ {x y a b} (x↓a : [ A ][ x ↓ a ]) (y↓b : [ A ][ y ↓ b ]) (a≡b : [ A ][ a ≡ b ]) → [ A ][ race x y ≲ y ] + ≈→≲₀ (now↓ x≡a) y↓b a≡b = ↓≲ (≡↓ A (≡-sym A (≡-trans A x≡a a≡b)) y↓b) + ≈→≲₀ (later↓ x↓a) (now↓ x≡y) a≡b = ↓≲ (now↓ (≡-refl A)) + ≈→≲₀ (later↓ x↓a) (later↓ y↓b) a≡b = later≲ (record { force≲ = ≈→≲₀ x↓a y↓b a≡b }) + + ≈→≲ : {x y : Delay ∣ A ∣} → [ A ][ x ≈ y ] → [ A ][ race x y ≲ y ] + ≈′→≲′ : {x y : Delay ∣ A ∣} → [ A ][ x ≈′ y ] → [ A ][ race x y ≲′ y ] + + ≈→≲ (↓≈ a≡b x↓a y↓b) = ≈→≲₀ x↓a y↓b a≡b + ≈→≲ (later≈ x≈y) = later≲ (≈′→≲′ x≈y) + + force≲ (≈′→≲′ x≈′y) = ≈→≲ (force≈ x≈′y) + + delta₀ : {x : Delay ∣ A ∣} {a : ∣ A ∣} → (x↓a : [ A ][ x ↓ a ]) → ℕ + delta₀ {x} (now↓ x≡y) = zero + delta₀ (later↓ x↓a) = suc (delta₀ x↓a) + + delta : {x y : Delay ∣ A ∣} → [ A ][ x ≲ y ] → Delay (∣ A ∣ × ℕ) + delta′ : {x y : Delay ∣ A ∣} → [ A ][ x ≲′ y ] → Delay′ (∣ A ∣ × ℕ) + + delta (↓≲ {x}{a} x↓a) = now (a , delta₀ x↓a) + delta (later≲ x≲′y) = later (delta′ x≲′y) + + force (delta′ x≲′y) = delta (force≲ x≲′y) + + ι : ∣ A ∣ × ℕ → Delay ∣ A ∣ + ι′ : ∣ A ∣ × ℕ → Delay′ ∣ A ∣ + force (ι′ p) = ι p + ι (x , zero) = now x + ι (x , suc n) = later (ι′ (x , n)) + ``` diff --git a/agda/src/Monad/Instance/Setoids/K'.lagda.md b/agda/src/Monad/Instance/Setoids/K'.lagda.md index dfa0395..e3bab10 100644 --- a/agda/src/Monad/Instance/Setoids/K'.lagda.md +++ b/agda/src/Monad/Instance/Setoids/K'.lagda.md @@ -14,6 +14,7 @@ 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 () +open import Data.Product.Relation.Binary.Pointwise.NonDependent ``` --> @@ -176,7 +177,13 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where helper₁ (later x) = inj₂ (force x) -- -- setoid-morphism that preserves strong-bisimilarity helper : Delayₛ' A ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ' A - helper = record { _⟨$⟩_ = helper₁ ; cong = {! !} } + helper = record { _⟨$⟩_ = helper₁ ; cong = strong-cong } + where + strong-cong : ∀ {x y : Delay ∣ A ∣} → [ A ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ helper₁ x ≡ helper₁ y ] + strong-cong {.(now _)} {.(now _)} (now∼ x≡y) = cong (inj₁ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong f x≡y) + strong-cong {.(later _)} {.(later _)} (later∼ x∼y) = cong (inj₂ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (force∼ x∼y) + + <<_>> = Elgot-Algebra-Morphism.h freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A freeAlgebra A = record @@ -184,6 +191,30 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where ; η = ηₛ A ; _* = delay-lift ; *-lift = λ {B} f {x} {y} x≡y → ≡-trans ⟦ B ⟧ (Elgot-Algebra.#-Fixpoint B (now∼ x≡y)) (≡-refl ⟦ B ⟧) - ; *-uniq = λ {B} f g eq {x} {y} x≡y → {! !} -- TODO pattern match x and y + ; *-uniq = λ {B} f g eq {x} {y} x≡y → *-uniq' {B} f g eq {x} {y} x≡y } + where + *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x y : Delay ∣ A ∣} → [ A ][ x ≈ y ] → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift f >>) ⟨$⟩ y) + *-uniq' {B} f g eq {now x} {now y} x≡y = ≡-trans ⟦ B ⟧ (eq {x} {y} (now-inj x≡y)) (≡-refl ⟦ B ⟧) + *-uniq' {B} f g eq {now x} {later y} x≡y = {! !} + *-uniq' {B} f g eq {later x} {now y} x≡y = {! !} + *-uniq' {B} f g eq {later x} {later y} x≡y = {! !} + + + + -- TODO stability might be proven more general, since Setoids is CCC (whatever is easier) + + delay-stability : ∀ (Y : Setoid ℓ ℓ) (X : Setoid ℓ ℓ) (B : Elgot-Algebra) (f : X ×ₛ Y ⟶ ⟦ B ⟧) → X ×ₛ Delayₛ Y ⟶ ⟦ B ⟧ + delay-stability Y X B f = {! !} + + isStableFreeElgotAlgebra : ∀ (A : Setoid ℓ ℓ) → IsStableFreeElgotAlgebra (freeAlgebra A) + isStableFreeElgotAlgebra A = record + { [_,_]♯ = λ {X} B f → delay-stability A X B f + ; ♯-law = {! !} + ; ♯-preserving = {! !} + ; ♯-unique = {! !} + } + + delayK : MonadK + delayK = record { freealgebras = freeAlgebra ; stable = isStableFreeElgotAlgebra } ``` \ No newline at end of file