🚧 Started working on quotienting the delay monad

This commit is contained in:
Leon Vatthauer 2023-10-03 19:44:08 +02:00
parent e5157c0bc5
commit 0165423fcf
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
3 changed files with 56 additions and 9 deletions

View file

@ -31,3 +31,6 @@ push':
Everything.agda:
git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > Everything.agda
open:
firefox public/index.html

View file

@ -1,6 +1,5 @@
<!--
```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Categories.Category
open import Categories.Monad
@ -22,8 +21,6 @@ module Monad.Instance.Delay {o e} (ambient : Ambient o e) where
open Ambient ambient
```
-- TODO SERGEYS LÖSUNG: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
## Definition
The delay monad is usually defined as a coinductive type with two constructors `now : X → D X` and `later : D X → D X`, e.g. in the [agda-stdlib](https://agda.github.io/agda-stdlib/Effect.Monad.Partiality.html#1523)
@ -418,6 +415,7 @@ Next we will show that the delay monad is strong, by giving a natural transforma
(idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
τ _ ∘ (idC ⁂ extend idC) ∎
where
-- diagram: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
square : out ∘ extend (τ (X , Y)) ∘ τ _ ≈ [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
square = begin
out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩

View file

@ -1,5 +1,6 @@
<!--
```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Categories.Functor
@ -12,16 +13,61 @@ open import Categories.Monad.Relative renaming (Monad to RMonad)
```agda
module Monad.Instance.Delay.Quotienting {o e} (ambient : Ambient o e) where
open Ambient ambient
open import Categories.Diagram.Coequalizer C
open import Monad.Instance.Delay ambient
module _ (D : DelayM) where
open DelayM D
open Functor functor using () renaming (F₁ to D₁)
open RMonad kleisli
module _ {X : Obj} (coeq : Coequalizer (extend (ι {X})) (D₁ π₁)) where
-- TODO
```
# Quotienting the delay monad by weak bisimilarity
The coinductive definition of the delay monad yields a 'wrong' kind of equality called *strong bisimilarity*, which differentiates between computations with different execution times, instead we want two computations to be equal, when they both terminate with the same result (or don't terminate at all).
This is called *weak bisimilarity*. The ideas is then to quotient the delay monad with this 'right' kind of equality and show that the result $\tilde{D}$ is again a (strong) monad.
In category theory existence of **coequalizers** corresponds to qoutienting, so we will express the quotiented delay monad via the following coequalizer:
<!-- https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMiwwLCJEWCJdLFs0LDAsIlxcdGlsZGV7RH1YIl0sWzEsMiwiXFxyaG9fWCJdLFswLDEsIkQgXFxwaV8xIiwyLHsib2Zmc2V0IjoxfV0sWzAsMSwiXFxpb3RhXioiLDAseyJvZmZzZXQiOi0xfV1d -->
<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMiwwLCJEWCJdLFs0LDAsIlxcdGlsZGV7RH1YIl0sWzEsMiwiXFxyaG9fWCJdLFswLDEsIkQgXFxwaV8xIiwyLHsib2Zmc2V0IjoxfV0sWzAsMSwiXFxpb3RhXioiLDAseyJvZmZzZXQiOi0xfV1d&embed" width="765" height="176" style="border-radius: 8px; border: none;"></iframe>
## Preliminaries
Existence of the coequalizer doesn't suffice, we will need some conditions having to do with preservation of the coequalizer, so let's first define what it means for a coequalizer to be preserved by an endofunctor:
```agda
preserves : ∀ {X Y} {f g : X ⇒ Y} → Endofunctor C → Coequalizer f g → Set (o ⊔ ⊔ e)
preserves {X} {Y} {f} {g} F coeq = Coequalizer (Functor.₁ F f) (Functor.₁ F g)
```
We will now show that the following conditions are equivalent:
1. For every $X$, the coequalizer is preserved by $D$
2. every $\tilde{D}X$ extends to a search-algebra, so that each $ρ_X$ is a D-algebra morphism
3. for every $X$, $(\tilde{D}X, ρ ∘ now : X → \tilde{D}X)$ is a stable free elgot algebra on X, $ρ_X$ is a D-algebra morphism and $ρ_X = ((ρ_X ∘ now + id) ∘ out)^\#$
4. $\tilde{D}$ extends to a strong monad, so that $ρ$ is a strong monad morphism
```agda
module _ (D : DelayM) where
open DelayM D renaming (functor to D-Fun; monad to D-Monad; kleisli to D-Kleisli)
open Functor D-Fun using () renaming (F₁ to D₁)
open RMonad D-Kleisli
module _ (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where
Ď₀ : Obj → Obj
Ď₀ X = Coequalizer.obj (coeqs X)
cond-1 : Set (o ⊔ ⊔ e)
cond-1 = ∀ {X} → preserves D-Fun (coeqs X)
cond-2 : Set (o ⊔ ⊔ e)
cond-2 = {! !}
cond-3 : Set (o ⊔ ⊔ e)
cond-3 = {! !}
cond-4 : Set (o ⊔ ⊔ e)
cond-4 = {! !}
```