leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Added documentation and adjusted makefile

Browse source
This commit is contained in:
Leon Vatthauer 2023-09-11 20:54:21 +02:00
parent 58bab7cbf4
commit 34ba57b6ef
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 73 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
Makefile
View file

@ -20,7 +20,10 @@ open:
push: all push: all
mv public/Everything.html public/index.html mv public/Everything.html public/index.html
scp -r public hy84coky@cip2a7.cip.cs.fau.de:.www/bsc-thesis chmod +w public/Agda.css
mv public bsc-thesis
scp -r bsc-thesis hy84coky@cip2a7.cip.cs.fau.de:.www/
mv bsc-thesis public
Everything.agda: Everything.agda:

106
src/Monad/Instance/Delay.lagda.md
View file

@ -1,6 +1,5 @@
<!-- <!--
```agda ```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level open import Level
open import Categories.Category open import Categories.Category
open import Categories.Monad open import Categories.Monad
@ -31,13 +30,13 @@ import Categories.Morphism.Reasoning as MR
## Summary ## Summary
This file introduces the delay monad ***D*** This file introduces the delay monad ***D***
- [ ] *Proposition 1* Characterization of the delay monad ***D***
- [ ] *Proposition 2* ***D*** is commutative
## Code ## Code
```agda ```agda
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
```
<!--
```agda
open ExtensiveDistributiveCategory ED renaming (U to C; id to idC) open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
open Cocartesian (Extensive.cocartesian extensive) open Cocartesian (Extensive.cocartesian extensive)
open Cartesian (ExtensiveDistributiveCategory.cartesian ED) open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
@ -57,7 +56,9 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
open F-Coalgebra-Morphism renaming (f to u) open F-Coalgebra-Morphism renaming (f to u)
open F-Coalgebra open F-Coalgebra
``` ```
### *Proposition 1*: Characterization of the delay monad ***D*** -->
The delay monad is described via existence of final (Y + \_)-coalgebras, so first we need to define the (Y + \_)-functor:
```agda ```agda
delayF : Obj → Endofunctor C delayF : Obj → Endofunctor C
@ -68,21 +69,32 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
; homomorphism = ⟺ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ; homomorphism = ⟺ (+₁∘+₁ ○ +₁-cong₂ identity² refl)
; F-resp-≈ = +₁-cong₂ refl ; F-resp-≈ = +₁-cong₂ refl
} }
```
Using this functor we can define the delay monad ***D***:
```agda
record DelayM : Set (o ⊔ ℓ ⊔ e) where record DelayM : Set (o ⊔ ℓ ⊔ e) where
field field
algebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A)) coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A))
```
module D A = Functor (delayF A) These are all the fields this record needs!
Of course this doesn't tell us very much, so our goal will be to extract a monad from this definition.
Conventionally the delay monad is described via functions `now` and `later` where the former lifts a value into a computation and the latter postpones a computation by one time unit.
We can now define these functions by bisecting the isomorphism `out : DX ≅ X + DX` which we get by Lambek's lemma. (Here `DX` is the element of the final coalgebra for `X`)
```agda
module _ (X : Obj) where module _ (X : Obj) where
open Terminal (algebras X) using (⊤; !; !-unique) open Terminal (coalgebras X) using (⊤; !; !-unique)
open F-Coalgebra ⊤ renaming (A to DX) open F-Coalgebra ⊤ renaming (A to DX)
D₀ = DX D₀ = DX
out-≅ : DX ≅ X + DX out-≅ : DX ≅ X + DX
out-≅ = colambek {F = delayF X} (algebras X) out-≅ = colambek {F = delayF X} (coalgebras X)
-- note: out-≅.from ≡ ⊤.α -- note: out-≅.from ≡ ⊤.α
open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public
@ -95,14 +107,24 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
unitlaw : out ∘ now ≈ i₁ unitlaw : out ∘ now ≈ i₁
unitlaw = cancelˡ (_≅_.isoʳ out-≅) unitlaw = cancelˡ (_≅_.isoʳ out-≅)
```
Since `DX` is part of a final coalgebra, we can define a *coiteration operator* that sends every `Y ⇒ X + Y` to `Y ⇒ DX` for an arbitrary `Y`
TODO rephrase, add diagram
```agda
module _ {Y : Obj} where module _ {Y : Obj} where
coit : Y ⇒ X + Y → Y ⇒ DX coit : Y ⇒ X + Y → Y ⇒ DX
coit f = u (! {A = record { A = Y ; α = f }}) coit f = u (! {A = record { A = Y ; α = f }})
coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f
coit-commutes f = commutes (! {A = record { A = Y ; α = f }}) coit-commutes f = commutes (! {A = record { A = Y ; α = f }})
```
If we combine the interal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`.
At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `delayF` defined above, this gives us another morphism `ι : X × N ⇒ DX` by using the final coalgebras.
TODO add diagram
```agda
module _ (ℕ : ParametrizedNNO) where module _ (ℕ : ParametrizedNNO) where
open ParametrizedNNO ℕ open ParametrizedNNO ℕ
@ -111,7 +133,15 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
ι : X × N ⇒ DX ι : X × N ⇒ DX
ι = u (! {A = record { A = X × N ; α = _≅_.from iso }}) ι = u (! {A = record { A = X × N ; α = _≅_.from iso }})
```
With these definitions at hand, we can now indeed construct a monad (in extension form) as the triple `(F₀, unit, extend)`.
`F₀` corresponds to `D₀` of course and `unit` is `now`, the tricky part is kleisli lifting aka. `extend`.
TODO
```agda
monad : Monad C monad : Monad C
monad = Kleisli⇒Monad C (record monad = Kleisli⇒Monad C (record
@ -131,33 +161,33 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] } alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] }
extend : D₀ X ⇒ D₀ Y extend : D₀ X ⇒ D₀ Y
extend = u (! (algebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} extend = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
!∘i₂ : u (! (algebras Y) {A = alg}) ∘ i₂ ≈ idC !∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC
!∘i₂ = ⊤-id (algebras Y) (F-Coalgebras (delayF Y) [ ! (algebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] ) !∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (delayF Y) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] )
extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X
extendlaw = begin extendlaw = begin
out Y ∘ extend ≈⟨ pullˡ (commutes (! (algebras Y) {A = alg})) ⟩ out Y ∘ extend ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩
((idC +₁ (u (! (algebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ ((idC +₁ (u (! (coalgebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
(idC +₁ (u (! (algebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] (idC +₁ (u (! (coalgebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ]
∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
[ (idC +₁ (u (! (algebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) [ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f)
, (idC +₁ (u (! (algebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
[ [ (idC +₁ (u (! (algebras Y)))) ∘ i₁ [ [ (idC +₁ (u (! (coalgebras Y)))) ∘ i₁
, (idC +₁ (u (! (algebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f)
, (i₂ ∘ (u (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂
(([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl)
refl) ⟩∘⟨refl ⟩ refl) ⟩∘⟨refl ⟩
[ [ i₁ ∘ idC , (i₂ ∘ (u (! (algebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f) [ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f)
, (i₂ ∘ (u (! (algebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂
(elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η))
assoc) ⟩∘⟨refl ⟩ assoc) ⟩∘⟨refl ⟩
[ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎
extend-unique : (g : D₀ X ⇒ D₀ Y) → (out Y ∘ g ≈ [ out Y ∘ f , i₂ ∘ g ] ∘ out X) → extend ≈ g extend-unique : (g : D₀ X ⇒ D₀ Y) → (out Y ∘ g ≈ [ out Y ∘ f , i₂ ∘ g ] ∘ out X) → extend ≈ g
extend-unique g g-commutes = begin extend-unique g g-commutes = begin
extend ≈⟨ (!-unique (algebras Y) (record { f = [ g , idC ] ; commutes = begin extend ≈⟨ (!-unique (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin
out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩ out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩
[ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩ [ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩
[ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ [ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂
@ -232,15 +262,15 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
f ∎ f ∎
identityˡ' : ∀ {X} → extend (now X) ≈ idC identityˡ' : ∀ {X} → extend (now X) ≈ idC
identityˡ' {X} = Terminal.⊤-id (algebras X) (record { f = extend (now X) ; commutes = begin identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend (now X) ; commutes = begin
out X ∘ extend (now X) ≈⟨ pullˡ ((commutes (! (algebras X) {A = alg (now X)}))) ⟩ out X ∘ extend (now X) ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg (now X)}))) ⟩
((idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ ((idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
(idC +₁ (u (! (algebras X) {A = alg (now X)}))) (idC +₁ (u (! (coalgebras X) {A = alg (now X)})))
∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw X) ○ inject₁) refl ⟩∘⟨refl ⟩ ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw X) ○ inject₁) refl ⟩∘⟨refl ⟩
(idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
[ (idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ i₁ [ (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁
, (idC +₁ (u (! (algebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩ , (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩
[ i₁ ∘ idC , (i₂ ∘ (u (! (algebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩
[ i₁ ∘ idC , i₂ ∘ (extend (now X)) ] ∘ out X ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ [ i₁ ∘ idC , i₂ ∘ (extend (now X)) ] ∘ out X ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩ ([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
(idC +₁ extend (now X)) ∘ out X ∎ }) (idC +₁ extend (now X)) ∘ out X ∎ })
@ -257,13 +287,13 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g
extend-≈' {X} {Y} {f} {g} eq = begin extend-≈' {X} {Y} {f} {g} eq = begin
u (! (algebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (algebras Y) (record { f = (u (! (algebras Y) {A = alg g }) ∘ idC) ; commutes = begin u (! (coalgebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (coalgebras Y) (record { f = (u (! (coalgebras Y) {A = alg g }) ∘ idC) ; commutes = begin
α (⊤ (algebras Y)) ∘ u (! (algebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
α (⊤ (algebras Y)) ∘ u (! (algebras Y)) ≈⟨ commutes (! (algebras Y)) ⟩ α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y)) ≈⟨ commutes (! (coalgebras Y)) ⟩
(idC +₁ u (! (algebras Y))) ∘ α (alg g) ≈˘⟨ Functor.F-resp-≈ (delayF Y) identityʳ ⟩∘⟨ αf≈αg eq ⟩ (idC +₁ u (! (coalgebras Y))) ∘ α (alg g) ≈˘⟨ Functor.F-resp-≈ (delayF Y) identityʳ ⟩∘⟨ αf≈αg eq ⟩
(idC +₁ u (! (algebras Y)) ∘ idC) ∘ α (alg f) ∎ })) (idC +₁ u (! (coalgebras Y)) ∘ idC) ∘ α (alg f) ∎ }))
⟩∘⟨refl ⟩ ⟩∘⟨refl ⟩
(u (! (algebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩ (u (! (coalgebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩
extend g ∎ extend g ∎
``` ```
@ -271,6 +301,6 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
TODO TODO
### Proposition 31 : the category of uniform-iteration algebras coincides with the category of search-algebras ### Proposition 31 : the category of uniform-iteration coalgebras coincides with the category of search-coalgebras
TODO TODO