get files from bsc
This commit is contained in:
commit
34003081dd
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
28 changed files with 5116 additions and 0 deletions
2
.chktexrc
Normal file
2
.chktexrc
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
# Exclude these environments from syntax checking
|
||||
VerbEnvir { tikzcd }
|
||||
61
.gitignore
vendored
Normal file
61
.gitignore
vendored
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
# agda
|
||||
*.agdai
|
||||
*.log
|
||||
Everything.agda
|
||||
agda/public/
|
||||
.direnv
|
||||
.DS_Store
|
||||
|
||||
# latex
|
||||
# put this to .git/info/exclude in git repos managing latex
|
||||
#
|
||||
# git ls-files --others --exclude-from=.git/info/exclude
|
||||
# Lines that start with '#' are comments.
|
||||
# For a project mostly in C, the following would be a good set of
|
||||
# exclude patterns (uncomment them if you want to use them):
|
||||
# *.[oa]
|
||||
.*.swp
|
||||
.#*
|
||||
*~
|
||||
_minted-main/
|
||||
# AUTOGENERATED
|
||||
# All wildcards below this marker are used to remove generated files in
|
||||
# 'make clean'
|
||||
*.aux
|
||||
*.fdb_latexmk
|
||||
*.log
|
||||
*.out
|
||||
thesis/*.pdf
|
||||
slides/*.pdf
|
||||
*.synctex.gz
|
||||
*.toc
|
||||
*.bbl
|
||||
*.blg
|
||||
*.idx
|
||||
*.ilg
|
||||
*.fls
|
||||
*.ind
|
||||
*.zip
|
||||
*.dvi
|
||||
*.eps
|
||||
*.bcf
|
||||
*.run.xml
|
||||
*.nav
|
||||
*.snm
|
||||
*.vrb
|
||||
*.vtc
|
||||
*.spl
|
||||
*.nlo
|
||||
*.nls
|
||||
*.auxlock
|
||||
.auctex-auto/
|
||||
_region_.tex
|
||||
*.xdv
|
||||
thesis/_minted-main/
|
||||
slides/_minted-main/
|
||||
thesis/main.bbl-SAVE-ERROR
|
||||
thesis/main.bcf-SAVE-ERROR
|
||||
thesis/main.tdo
|
||||
main.synctex(busy)
|
||||
thesis/main.pyg
|
||||
thesis/main.loe
|
||||
4
.vscode/ltex.dictionary.en-GB.txt
vendored
Normal file
4
.vscode/ltex.dictionary.en-GB.txt
vendored
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
Agda
|
||||
Vatthauer
|
||||
Moggi
|
||||
Capretta
|
||||
84
.vscode/ltex.dictionary.en-US.txt
vendored
Normal file
84
.vscode/ltex.dictionary.en-US.txt
vendored
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
cocartesian
|
||||
cartesian
|
||||
iso
|
||||
coproducts
|
||||
Coalgebras
|
||||
adjunctions
|
||||
coalgebras
|
||||
Adjunctions
|
||||
Lambek
|
||||
endofunctor
|
||||
pointful
|
||||
Kleisli
|
||||
functoriality
|
||||
formalizations
|
||||
Agda
|
||||
Coq
|
||||
agda-categories
|
||||
setoids
|
||||
sym-assoc
|
||||
setoid-enriched
|
||||
extensionality
|
||||
Setoid
|
||||
Moggi
|
||||
Cockett
|
||||
Bucalo
|
||||
equational
|
||||
coinductive
|
||||
corecursion
|
||||
coinduction
|
||||
coalgebra
|
||||
Capretta
|
||||
monic
|
||||
monicity
|
||||
intensional
|
||||
Fixpoint
|
||||
Elgot
|
||||
exponentials
|
||||
Pre-Elgot
|
||||
pre-Elgot
|
||||
quotiented
|
||||
quotients-as-setoid
|
||||
setoid
|
||||
Setoids
|
||||
Coproducts
|
||||
iff
|
||||
Quotienting
|
||||
bisimilarity
|
||||
corecursively
|
||||
coproduct
|
||||
adjunction
|
||||
counit
|
||||
epi
|
||||
F-coalgebra
|
||||
F-coalgebras
|
||||
F-Coalgebras
|
||||
terminality
|
||||
coinductively
|
||||
monos
|
||||
epis
|
||||
isos
|
||||
Corecursion
|
||||
subobject
|
||||
isomorphisms
|
||||
epicness
|
||||
fixpoint
|
||||
Martin-Löf
|
||||
Set₀
|
||||
Set₁
|
||||
bisimilar
|
||||
copatterns
|
||||
epimorphisms
|
||||
monomorphisms
|
||||
expressivity
|
||||
Friedrich-Alexander-Universität
|
||||
Erlangen-Nürnberg
|
||||
Goncharov
|
||||
denotational
|
||||
Plotkin
|
||||
monadic
|
||||
Vatthauer
|
||||
minimality
|
||||
coequalizer
|
||||
refl
|
||||
coList
|
||||
7
.vscode/ltex.hiddenFalsePositives.en-GB.txt
vendored
Normal file
7
.vscode/ltex.hiddenFalsePositives.en-GB.txt
vendored
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[agda] linenos=true, breaklines=true, encoding=utf8, fontsize=, frame=lines, autogobble\\E$"}
|
||||
{"rule":"WHITESPACE_RULE","sentence":"^\\Q[4][]##4\\E$"}
|
||||
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[ignoreall,show=definition]\\E$"}
|
||||
{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Q[ignoreall,show=definition]\\E$"}
|
||||
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[1]Coalgs(#1)\\E$"}
|
||||
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[cases] mycase Case .\\E$"}
|
||||
{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Q[cases] mycase Case .\\E$"}
|
||||
61
.vscode/ltex.hiddenFalsePositives.en-US.txt
vendored
Normal file
61
.vscode/ltex.hiddenFalsePositives.en-US.txt
vendored
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
{"rule":"POSSESSIVE_APOSTROPHE","sentence":"^\\QFurthermore, in mathematical textbooks equality between morphisms is usually taken for granted, i.e. there is some global notion of equality that is clear to everyone.\\E$"}
|
||||
{"rule":"SENTENCE_WHITESPACE","sentence":"^\\QKleisli').\\E$"}
|
||||
{"rule":"SENTENCE_WHITESPACE","sentence":"^\\QConstruction.\\E$"}
|
||||
{"rule":"NO_SPACE_CLOSING_QUOTE","sentence":"^\\Q[inline]Change quotation marks ”\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q”: Given a Kleisli triple \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we get a monad \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is the object mapping of the Kleisli triple together with the functor action \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is the morphism family of the Kleisli triple where naturality is easy to show and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a natural transformation defined as \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QLet \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid morphism, we define \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q point wise: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is defined corecursively by: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QThe following conditions hold: There exists a unit morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any DX, satisfying \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q For any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q there exists a unique morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfying: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q There exists a unique morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfying: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We will make use of the fact that every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a final coalgebra: [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] This follows by definition of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QWe call a morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q guarded if there exists an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that the following diagram commutes: &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QIt suffices to show \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, because then follows: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We prove this by coinduction using: [inline]Change name of morphism &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Q[inline]Make this more explicit The first step in both equations can be proven by monicity of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and then using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the dual diagram for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which is a direct consequence of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the last step holds generally for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QFirst we need to show naturality of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, i.e. we need to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q The needed coalgebra is shown in this diagram: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Next we check the strength laws: [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] To show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q we do coinduction using the following coalgebra: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] We don't need coinduction to show \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, but we need a small helper lemma: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which is a direct consequence of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QFirst we need to show naturality of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, i.e. we need to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q The coalgebra for coinduction is: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We write \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to abbreviate the rather long coalgebra, i.e. in this diagram \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Q&&&&&&& &&&&&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q then follows from this diagram.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QSince \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a final coalgebra we get the following proof principle: Given two morphisms \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q it suffices to show that there exists a coalgebra structure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that the following diagrams commute: &&&&&& &&&&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Uniqueness of the coalgebra morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q then gives us that indeed \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QFirst we need to show naturality of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, i.e. we need to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q The coalgebra for coinduction is: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We write \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to abbreviate the used coalgebra, i.e. in this diagram \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QNext we check the strength laws: [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] To show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q we do coinduction using the following coalgebra: &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] We don't need coinduction to show \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, but we need a small helper lemma: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which is a direct consequence of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QIt suffices to show \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, because then follows: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We prove this by coinduction using: &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Q[inline]Move this remark to the beginning of proof The first step in both equations can be proven by monicity of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and then using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the dual diagram for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which is a direct consequence of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QTo show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q it suffices to show that there exists a coalgebra structure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that the following diagrams commute: &&&&&& &&&&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Uniqueness of the coalgebra morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q then results in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q test: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q test: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:diamond Diamond\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object A for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: Note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: Note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: Note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: First, note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can equivalently be reformulated as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we are left to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: First, note that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can equivalently be reformulated as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q since \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we are left to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QLet \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid morphism, we define \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q point wise: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object A for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying the following axioms: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QGiven a functor \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, a (H-)guarded Elgot algebra consists of: An object \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, a H-algebra structure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying the following axioms: law:guardedfixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:guardeduniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:guardedcompositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QAn Elgot monad consists of A monad \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfying: Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Naturality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Codiagonal: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QLet \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid function, we define \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q point wise: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QGiven a function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the lifted function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is defined as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QConsider, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a setoid function that maps every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QNow, consider the following function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which tries running two computations and returns the one that finished first: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QLastly, consider the function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, which adds a number of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q constructors in front of a value and is given by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QConsider another setoid function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QNext, let us consider functions for counting steps of computations, first regard \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, which returns the number of steps a terminating computation has to take and is defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QConsider \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QFurthermore, consider the setoid function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Now, by coinduction we can easily follow that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"WHITESPACE_RULE","sentence":"^\\QFriedrich-Alexander-Universität Erlangen-Nürnberg [] Chair for Computer Science 8 Theoretical Computer Science Bachelor Thesis in Computer Science [0.5] Advisor: Sergey Goncharov Erlangen,\\E$"}
|
||||
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\Q[agda] linenos=true, breaklines=true, encoding=utf8, fontsize=, frame=lines, autogobble\\E$"}
|
||||
{"rule":"WHITESPACE_RULE","sentence":"^\\Q[4][]##4\\E$"}
|
||||
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\Q[cases] mycase Case .\\E$"}
|
||||
{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Q[cases] mycase Case .\\E$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QLet \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid morphism, we define \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q point wise: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QFurthermore, consider the setoid morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Now, by coinduction we can easily follow that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QConsider, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a setoid morphism that maps every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||
{"rule":"IF_IS","sentence":"^\\QConsider another setoid morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"DOUBLE_PUNCTUATION","sentence":"^\\QAgda implements a Martin-Löf style dependent type theory with inductive and coinductive types as well as an infinite hierarchy of universes Set_0, Set_1, , where usually Set_0 is abbreviated as Set.\\E$"}
|
||||
{"rule":"DOUBLE_PUNCTUATION","sentence":"^\\QAgda implements a Martin-Löf style dependent type theory with inductive and coinductive types as well as an infinite hierarchy of universes Set₀, Set₁, , where usually Set₀ is abbreviated as Set.\\E$"}
|
||||
27
.vscode/settings.json
vendored
Normal file
27
.vscode/settings.json
vendored
Normal file
|
|
@ -0,0 +1,27 @@
|
|||
{
|
||||
"latex-workshop.latex.tools": [
|
||||
{
|
||||
"name": "latexmk-main",
|
||||
"command": "latexmk",
|
||||
"args": [
|
||||
"-synctex=1",
|
||||
"-interaction=nonstopmode",
|
||||
"-file-line-error",
|
||||
"-shell-escape",
|
||||
"-pdf",
|
||||
"-xelatex",
|
||||
"-outdir=%OUTDIR%",
|
||||
"main.tex"
|
||||
],
|
||||
"env": {}
|
||||
}
|
||||
],
|
||||
"latex-workshop.latex.recipes": [
|
||||
{
|
||||
"name": "latexmk-main",
|
||||
"tools": [
|
||||
"latexmk-main"
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
16
Makefile
Normal file
16
Makefile
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
src = $(wildcard *.tex)
|
||||
pdf = $(src:.tex=.pdf)
|
||||
imgpdf = $(wildcard img/*.pdf)
|
||||
|
||||
.PHONY: all clean
|
||||
|
||||
all: $(pdf) $(imgpdf)
|
||||
|
||||
%.pdf: %.tex $(wildcard src/*.tex) $(wildcard *.bib) $(imgpdf)
|
||||
latexmk -pdf -xelatex -shell-escape -file-line-error -synctex=1 -halt-on-error -shell-escape $<
|
||||
|
||||
clean:
|
||||
latexmk -C $(src)
|
||||
rm -f $(wildcard *.out *.nls *.nlo *.bbl *.blg *-blx.bib *.run.xml *.bcf *.synctex.gz *.fdb_latexmk *.fls *.toc *.loe *.tdo *.bbl-SAVE-ERROR)
|
||||
rm -f $(wildcard src/*.aux)
|
||||
rm -rf $(wildcard _minted-main src/.auctex-auto _region_.prv)
|
||||
8
README.md
Normal file
8
README.md
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
# The thesis
|
||||
This folder contains the source of my thesis.
|
||||
|
||||
## Requirements
|
||||
Building the thesis requires a working xelatex installation. Since I am using the [minted]([minted](https://ctan.org/pkg/minted)) package for representing Agda code you will also need the Python syntax highlighter [Pygments](https://pygments.org/).
|
||||
|
||||
## Usage
|
||||
To compile the thesis just run `make` with the needed programs installed.
|
||||
50
agda/Coind.agda
Normal file
50
agda/Coind.agda
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
{-# OPTIONS --guardedness #-}
|
||||
|
||||
-- Agda code that is included in the thesis.
|
||||
-- just for making sure that everything used in the thesis actually compiles ;)
|
||||
|
||||
open import Agda.Builtin.Equality
|
||||
module Coind where
|
||||
module Streams where
|
||||
record Stream (A : Set) : Set where
|
||||
coinductive
|
||||
field
|
||||
head : A
|
||||
tail : Stream A
|
||||
open Stream
|
||||
|
||||
repeat : {A : Set} (a : A) → Stream A
|
||||
head (repeat a) = a
|
||||
tail (repeat a) = repeat a
|
||||
|
||||
record _≈_ {A} (s : Stream A) (t : Stream A) : Set where
|
||||
coinductive
|
||||
field
|
||||
head : head s ≡ head t
|
||||
tail : tail s ≈ tail t
|
||||
open _≈_
|
||||
|
||||
repeat-eq : ∀ {A} (a : A) → repeat a ≈ tail (repeat a)
|
||||
head (repeat-eq {A} a) = refl
|
||||
tail (repeat-eq {A} a) = repeat-eq a
|
||||
|
||||
module coLists where
|
||||
mutual
|
||||
data coList (A : Set) : Set where
|
||||
nil : coList A
|
||||
_∷_ : A → coList′ A → coList A
|
||||
|
||||
record coList′ (A : Set) : Set where
|
||||
coinductive
|
||||
field force : coList A
|
||||
open coList′
|
||||
|
||||
module repeatMutual where
|
||||
mutual
|
||||
repeat : {A : Set} (a : A) → coList A
|
||||
repeat′ : {A : Set} (a : A) → coList′ A
|
||||
repeat a = a ∷ repeat′ a
|
||||
force (repeat′ a) = repeat a
|
||||
|
||||
repeat : {A : Set} (a : A) → coList A
|
||||
repeat a = a ∷ λ { .force → repeat a }
|
||||
50
agda/Setoids.agda
Normal file
50
agda/Setoids.agda
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
-- Agda code that is included in the thesis.
|
||||
-- just for making sure that everything used in the thesis actually compiles ;)
|
||||
|
||||
module Setoids where
|
||||
open import Level
|
||||
|
||||
record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
||||
constructor _,_
|
||||
field
|
||||
fst : A
|
||||
snd : B
|
||||
open _×_
|
||||
|
||||
<_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (A → B) → (A → C) → A → (B × C)
|
||||
< f , g > x = (f x , g x)
|
||||
|
||||
record ⊤ {l} : Set l where
|
||||
constructor tt
|
||||
|
||||
! : ∀ {l} {X : Set l} → X → ⊤ {l}
|
||||
! _ = tt
|
||||
|
||||
data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
||||
i₁ : A → A + B
|
||||
i₂ : B → A + B
|
||||
|
||||
[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (A → C) → (B → C) → (A + B) → C
|
||||
[ f , g ] (i₁ x) = f x
|
||||
[ f , g ] (i₂ x) = g x
|
||||
|
||||
data ⊥ {l} : Set l where
|
||||
|
||||
¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
|
||||
¡ ()
|
||||
|
||||
distributeˡ⁻¹ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A × B) + (A × C) → A × (B + C)
|
||||
distributeˡ⁻¹ (i₁ (x , y)) = (x , i₁ y)
|
||||
distributeˡ⁻¹ (i₂ (x , y)) = (x , i₂ y)
|
||||
|
||||
distributeˡ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → A × (B + C) → (A × B) + (A × C)
|
||||
distributeˡ (x , i₁ y) = i₁ (x , y)
|
||||
distributeˡ (x , i₂ y) = i₂ (x , y)
|
||||
|
||||
curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (C × A → B) → C → A → B
|
||||
curry f x y = f (x , y)
|
||||
|
||||
eval : ∀ {a b} {A : Set a} {B : Set b} → ((A → B) × A) → B
|
||||
eval (f , x) = f x
|
||||
3
agda/agda.agda-lib
Normal file
3
agda/agda.agda-lib
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
name: agda
|
||||
include: .
|
||||
depend: standard-library
|
||||
372
bib.bib
Normal file
372
bib.bib
Normal file
|
|
@ -0,0 +1,372 @@
|
|||
@software{agda,
|
||||
author = {{Agda Developers}},
|
||||
title = {{Agda}},
|
||||
url = {https://agda.readthedocs.io/},
|
||||
version = {2.6.5}
|
||||
}
|
||||
|
||||
@inproceedings{agda-categories,
|
||||
author = {Hu, Jason Z. S. and Carette, Jacques},
|
||||
title = {Formalizing Category Theory in Agda},
|
||||
year = {2021},
|
||||
isbn = {9781450382991},
|
||||
publisher = {Association for Computing Machinery},
|
||||
address = {New York, NY, USA},
|
||||
url = {https://doi.org/10.1145/3437992.3439922},
|
||||
doi = {10.1145/3437992.3439922},
|
||||
abstract = {The generality and pervasiveness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design choices, and we present, motivate and explain the ones we picked. In particular, we find that alternative definitions or alternative proofs from those found in standard textbooks can be advantageous, as well as "fit" Agda's type theory more smoothly. Some definitions regarded as equivalent in standard textbooks turn out to make different "universe level" assumptions, with some being more polymorphic than others. We also pay close attention to engineering issues so that the library integrates well with Agda's own standard library, as well as being compatible with as many of supported type theories in Agda as possible.},
|
||||
booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
|
||||
pages = {327–342},
|
||||
numpages = {16},
|
||||
keywords = {formal mathematics, Agda, category theory},
|
||||
location = {Virtual, Denmark},
|
||||
series = {CPP 2021}
|
||||
}
|
||||
|
||||
@manual{agda-man,
|
||||
title = {Agda User Manual},
|
||||
author = {The Agda Team},
|
||||
year = {2024},
|
||||
month = {03},
|
||||
day = {06},
|
||||
version = {2.6.4.3},
|
||||
url = {https://agda.readthedocs.io/en/v2.6.4.3/}
|
||||
}
|
||||
|
||||
@software{agda-stdlib,
|
||||
author = {{The Agda Community}},
|
||||
month = dec,
|
||||
title = {{Agda Standard Library}},
|
||||
url = {https://github.com/agda/agda-stdlib},
|
||||
version = {2.0},
|
||||
year = {2023}
|
||||
}
|
||||
|
||||
@incollection{Altenkirch_2017,
|
||||
doi = {10.1007/978-3-662-54458-7_31},
|
||||
url = {https://doi.org/10.1007%2F978-3-662-54458-7_31},
|
||||
year = {2017},
|
||||
publisher = {Springer Berlin Heidelberg},
|
||||
pages = {534--549},
|
||||
author = {Thorsten Altenkirch and Nils Anders Danielsson and Nicolai Kraus},
|
||||
title = {Partiality, Revisited},
|
||||
booktitle = {Lecture Notes in Computer Science}
|
||||
}
|
||||
|
||||
@manual{coq-man,
|
||||
title = {The Coq Reference Manual},
|
||||
author = {The Coq Development Team},
|
||||
year = {2024},
|
||||
month = {03},
|
||||
day = {01},
|
||||
version = {8.19.1},
|
||||
url = {https://coq.inria.fr/doc/V8.19.0/refman/}
|
||||
}
|
||||
|
||||
@article{delay,
|
||||
author = {Venanzio Capretta},
|
||||
title = {General Recursion via Coinductive Types},
|
||||
journal = {CoRR},
|
||||
volume = {abs/cs/0505037},
|
||||
year = {2005},
|
||||
url = {http://arxiv.org/abs/cs/0505037},
|
||||
eprinttype = {arXiv},
|
||||
eprint = {cs/0505037},
|
||||
timestamp = {Mon, 13 Aug 2018 16:46:14 +0200},
|
||||
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0505037.bib},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@article{elgotalgebras,
|
||||
author = {Jir{\'{\i}} Ad{\'{a}}mek and
|
||||
Stefan Milius and
|
||||
Jir{\'{\i}} Velebil},
|
||||
title = {Elgot Algebras},
|
||||
journal = {CoRR},
|
||||
volume = {abs/cs/0609040},
|
||||
year = {2006},
|
||||
url = {http://arxiv.org/abs/cs/0609040},
|
||||
eprinttype = {arXiv},
|
||||
eprint = {cs/0609040},
|
||||
timestamp = {Mon, 04 Sep 2023 12:29:24 +0200},
|
||||
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0609040.bib},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@article{elgotmonad,
|
||||
title = {Elgot theories: a new perspective on the equational properties of iteration},
|
||||
volume = {21},
|
||||
doi = {10.1017/S0960129510000496},
|
||||
number = {2},
|
||||
journal = {Mathematical Structures in Computer Science},
|
||||
publisher = {Cambridge University Press},
|
||||
author = {Jir{\'{\i}} Ad{\'{a}}mek and
|
||||
Stefan Milius and
|
||||
Jir{\'{\i}} Velebil},
|
||||
year = {2011},
|
||||
pages = {417–480}
|
||||
}
|
||||
|
||||
@article{eqlm,
|
||||
author = {Bucalo, Anna and F\"{u}hrmann, Carsten and Simpson, Alex},
|
||||
title = {An Equational Notion of Lifting Monad},
|
||||
year = {2003},
|
||||
issue_date = {15 February 2003},
|
||||
publisher = {Elsevier Science Publishers Ltd.},
|
||||
address = {GBR},
|
||||
volume = {294},
|
||||
number = {1–2},
|
||||
issn = {0304-3975},
|
||||
url = {https://doi.org/10.1016/S0304-3975(01)00243-2},
|
||||
doi = {10.1016/S0304-3975(01)00243-2},
|
||||
abstract = {We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any equational lifting monad has a representation by a partial map classifier such that the Kleisli category of the former fully embeds in the partial category of the latter. Thus, equational lifting monads precisely capture the equational properties of partial maps as induced by partial map classifiers. The representation theorem also provides a tool for transferring nonequational properties of partial map classifiers to equational lifting monads. It is proved using a direct axiomatization of Kleisli categories of equational lifting monads. This axiomatization is of interest in its own right.},
|
||||
journal = {Theor. Comput. Sci.},
|
||||
month = {2},
|
||||
pages = {31–60},
|
||||
numpages = {30},
|
||||
keywords = {premonoidal categories, categories, partiality and partial categories, abstract Kleish, commutative strong monads}
|
||||
}
|
||||
|
||||
@inproceedings{goncharov2017unifying,
|
||||
title = {Unifying guarded and unguarded iteration},
|
||||
author = {Goncharov, Sergey and Schr{\"o}der, Lutz and Rauch, Christoph and Pir{\'o}g, Maciej},
|
||||
booktitle = {Foundations of Software Science and Computation Structures: 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings 20},
|
||||
pages = {517--533},
|
||||
year = {2017},
|
||||
organization = {Springer}
|
||||
}
|
||||
|
||||
@article{goncharov2018unguarded,
|
||||
title = {Unguarded recursion on coinductive resumptions},
|
||||
author = {Goncharov, Sergey and Schr{\"o}der, Lutz and Rauch, Christoph and Jakob, Julian},
|
||||
journal = {Logical Methods in Computer Science},
|
||||
volume = {14},
|
||||
year = {2018},
|
||||
publisher = {Episciences. org}
|
||||
}
|
||||
|
||||
@book{inductive,
|
||||
title = {Categorical programming with inductive and coinductive types},
|
||||
author = {Vene, Varmo},
|
||||
year = {2000},
|
||||
publisher = {Citeseer}
|
||||
}
|
||||
|
||||
@article{kozencoinduction,
|
||||
title = {Practical coinduction},
|
||||
author = {Kozen, Dexter and Silva, Alexandra},
|
||||
journal = {Mathematical Structures in Computer Science},
|
||||
volume = {27},
|
||||
number = {7},
|
||||
pages = {1132--1152},
|
||||
year = {2017},
|
||||
publisher = {Cambridge University Press}
|
||||
}
|
||||
|
||||
@article{lambek,
|
||||
title = {A fixpoint theorem for complete categories},
|
||||
author = {Lambek, Joachim},
|
||||
journal = {Mathematische Zeitschrift},
|
||||
volume = {103},
|
||||
pages = {151--161},
|
||||
year = {1968},
|
||||
publisher = {Springer}
|
||||
}
|
||||
|
||||
@inproceedings{Lane1971,
|
||||
title = {Categories for the Working Mathematician},
|
||||
author = {Saunders Mac Lane},
|
||||
year = {1971},
|
||||
url = {https://api.semanticscholar.org/CorpusID:122892655}
|
||||
}
|
||||
|
||||
@article{manes,
|
||||
title = {Algebraic Theories in a Category},
|
||||
author = {Manes, Ernest G},
|
||||
journal = {Algebraic Theories},
|
||||
pages = {161--279},
|
||||
year = {1976},
|
||||
publisher = {Springer}
|
||||
}
|
||||
|
||||
@article{moggi,
|
||||
author = {Moggi, Eugenio},
|
||||
title = {Notions of Computation and Monads},
|
||||
year = {1991},
|
||||
issue_date = {July 1991},
|
||||
publisher = {Academic Press, Inc.},
|
||||
address = {USA},
|
||||
volume = {93},
|
||||
number = {1},
|
||||
issn = {0890-5401},
|
||||
url = {https://doi.org/10.1016/0890-5401(91)90052-4},
|
||||
doi = {10.1016/0890-5401(91)90052-4},
|
||||
journal = {Inf. Comput.},
|
||||
month = {7},
|
||||
pages = {55–92},
|
||||
numpages = {38}
|
||||
}
|
||||
|
||||
@online{nad-delay,
|
||||
author = {Nils Anders Danielsson},
|
||||
title = {The delay monad, defined coinductively},
|
||||
url = {https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html},
|
||||
urlday = {15},
|
||||
urlmonth = {02},
|
||||
urlyear = {2024}
|
||||
}
|
||||
|
||||
@article{param-corec,
|
||||
title = {Parametric corecursion},
|
||||
journal = {Theoretical Computer Science},
|
||||
volume = {260},
|
||||
number = {1},
|
||||
pages = {139-163},
|
||||
year = {2001},
|
||||
note = {Coalgebraic Methods in Computer Science 1998},
|
||||
issn = {0304-3975},
|
||||
doi = {https://doi.org/10.1016/S0304-3975(00)00126-2},
|
||||
url = {https://www.sciencedirect.com/science/article/pii/S0304397500001262},
|
||||
author = {Lawrence S. Moss},
|
||||
abstract = {This paper gives a treatment of substitution for “parametric” objects in final coalgebras, and also presents principles of definition by corecursion for such objects. The substitution results are coalgebraic versions of well-known consequences of initiality, and the work on corecursion is a general formulation which allows one to specify elements of final coalgebras using systems of equations. One source of our results is the theory of hypersets, and at the end of this paper we sketch a development of that theory which calls upon the general work of this paper to a very large extent and particular facts of elementary set theory to a much smaller extent.}
|
||||
}
|
||||
|
||||
@inproceedings{quotienting,
|
||||
author = {Chapman, James and Uustalu, Tarmo and Veltri, Niccol\`{o}},
|
||||
title = {Quotienting the Delay Monad by Weak Bisimilarity},
|
||||
year = {2015},
|
||||
isbn = {9783319251493},
|
||||
publisher = {Springer-Verlag},
|
||||
address = {Berlin, Heidelberg},
|
||||
url = {https://doi.org/10.1007/978-3-319-25150-9_8},
|
||||
doi = {10.1007/978-3-319-25150-9_8},
|
||||
abstract = {The delay datatype was introduced by Capretta [3] as a means to deal with partial functions as in computability theory in Martin-L\"{o}f type theory. It is a monad and it constitutes a constructive alternative to the maybe monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay monad quotiented by weak bisimilarity is still a monad. In this paper, we consider Hofmann's alternative approach [6] of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the semi-classical axiom of countable choice. We have fully formalized our results in the Agda dependently typed programming language.},
|
||||
booktitle = {Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015 - Volume 9399},
|
||||
pages = {110–125},
|
||||
numpages = {16}
|
||||
}
|
||||
|
||||
@article{restriction,
|
||||
author = {Cockett, J. R. B. and Lack, Stephen},
|
||||
title = {Restriction Categories I: Categories of Partial Maps},
|
||||
year = {2002},
|
||||
issue_date = {January},
|
||||
publisher = {Elsevier Science Publishers Ltd.},
|
||||
address = {GBR},
|
||||
volume = {270},
|
||||
number = {1–2},
|
||||
issn = {0304-3975},
|
||||
url = {https://doi.org/10.1016/S0304-3975(00)00382-0},
|
||||
doi = {10.1016/S0304-3975(00)00382-0},
|
||||
abstract = {Given a category with a stable system of monics, one can form the corresponding category of partial maps. To each map in this category there is, on the domain of the map, an associated idempotent, which measures the degree of partiality. This structure is captured abstractly by the notion of a restriction category, in which every arrow is required to have such an associated idempotent. Categories with a stable system of monics, functors preserving this structure, and natural transformations which are cartesian with respect to the chosen monics, form a 2-category which we call MCat. The construction of categories of partial maps provides a 2-functor Par:Mcat→Cat. We show that Par can be made into an equivalence of 2-categories between MCat and a 2-category of restriction categories. The underlying ordinary functor Par&r0:Mcat&0 → Ca t0 of the above 2-functor Par turns out to be monadic, and, from this, we deduce the completeness and cocompleteness of the 2-categories of M-categories and of restriction categories. We also consider the problem of how to turn a formal system of subobjects into an actual system of subobjects. A formal system of subobjects is given by a functor into the category sLat of semilattices. This structure gives rise to a restriction category which, via the above equivalence of 2-categories, gives an M-category. This M-category contains the universal realization of the given formal subobjects as actual subobjects.},
|
||||
journal = {Theor. Comput. Sci.},
|
||||
month = {1},
|
||||
pages = {223–259},
|
||||
numpages = {37}
|
||||
}
|
||||
|
||||
@article{setoids,
|
||||
title = {Category theoretic structure of setoids},
|
||||
journal = {Theoretical Computer Science},
|
||||
volume = {546},
|
||||
pages = {145-163},
|
||||
year = {2014},
|
||||
note = {Models of Interaction: Essays in Honour of Glynn Winskel},
|
||||
issn = {0304-3975},
|
||||
doi = {https://doi.org/10.1016/j.tcs.2014.03.006},
|
||||
url = {https://www.sciencedirect.com/science/article/pii/S0304397514001819},
|
||||
author = {Yoshiki Kinoshita and John Power},
|
||||
keywords = {Setoid, Proof assistant, Proof irrelevance, Cartesian closed category, Coproduct, -category, -inserter, -category, -coinserter},
|
||||
abstract = {A setoid is a set together with a constructive representation of an equivalence relation on it. Here, we give category theoretic support to the notion. We first define a category Setoid and prove it is Cartesian closed with coproducts. We then enrich it in the Cartesian closed category Equiv of sets and classical equivalence relations, extend the above results, and prove that Setoid as an Equiv-enriched category has a relaxed form of equalisers. We then recall the definition of E-category, generalising that of Equiv-enriched category, and show that Setoid as an E-category has a relaxed form of coequalisers. In doing all this, we carefully compare our category theoretic constructs with Agda code for type-theoretic constructs on setoids.}
|
||||
}
|
||||
|
||||
@article{setoids,
|
||||
author = {Barthe, Gilles and Capretta, Venanzio and Pons, Olivier},
|
||||
title = {Setoids in type theory},
|
||||
year = {2003},
|
||||
issue_date = {March 2003},
|
||||
publisher = {Cambridge University Press},
|
||||
address = {USA},
|
||||
volume = {13},
|
||||
number = {2},
|
||||
issn = {0956-7968},
|
||||
url = {https://doi.org/10.1017/S0956796802004501},
|
||||
doi = {10.1017/S0956796802004501},
|
||||
abstract = {Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids and assesses their suitability as a basis for developing mathematics. According to whether the equality relation is required to be reflexive or not we have total or partial setoid, respectively. There is only one definition of total setoid, but four different definitions of partial setoid, depending on four different notions of setoid function. We prove that one approach to partial setoids in unsuitable, and that the other approaches can be divided in two classes of equivalence. One class contains definitions of partial setoids that are equivalent to total setoids; the other class contains an inherently different definition, that has been useful in the modeling of type systems. We also provide some elements of discussion on the merits of each approach from the viewpoint of formalizing mathematics. In particular, we exhibit a difficulty with the common definition of subsetoids in the partial setoid approach.},
|
||||
journal = {J. Funct. Program.},
|
||||
month = {mar},
|
||||
pages = {261–293},
|
||||
numpages = {33}
|
||||
}
|
||||
|
||||
@article{sol-thm,
|
||||
author = {Aczel, Peter and Ad\'{a}mek, Jir\'{\i} and Milius, Stefan and Velebil, Jir\'{\i}},
|
||||
title = {Infinite trees and completely iterative theories: a coalgebraic view},
|
||||
year = {2003},
|
||||
issue_date = {07 May 2003},
|
||||
publisher = {Elsevier Science Publishers Ltd.},
|
||||
address = {GBR},
|
||||
volume = {300},
|
||||
number = {1–3},
|
||||
issn = {0304-3975},
|
||||
url = {https://doi.org/10.1016/S0304-3975(02)00728-4},
|
||||
doi = {10.1016/S0304-3975(02)00728-4},
|
||||
abstract = {Infinite trees form a free completely iterative theory over any given signature--this fact, proved by Elgot, Bloom and Tindell, turns out to be a special case of a much more general categorical result exhibited in the present paper. We prove that whenever an endofunctor H of a category has final coalgebras for all functors H(-) + X, then those coalgebras, TX, form a monad. This monad is completely iterative, i.e., every guarded system of recursive equations has a unique solution. And it is a free completely iterative monad on H. The special case of polynomial endofunctors of the category Set is the above mentioned theory, or monad, of infinite trees.This procedure can be generalized to monoidal categories satisfying a mild side condition: if, for an object H, the endofunctor H ⊗ _ + I has a final coalgebra, T, then T is a monoid. This specializes to the above case for the monoidal category of all endofunctors.},
|
||||
journal = {Theor. Comput. Sci.},
|
||||
month = {5},
|
||||
pages = {1–45},
|
||||
numpages = {45},
|
||||
keywords = {coalgebra, completely iterative theory, monad, monoidal category, solution theorem}
|
||||
}
|
||||
|
||||
@article{uniformelgot,
|
||||
author = {Sergey Goncharov},
|
||||
title = {Uniform Elgot Iteration in Foundations},
|
||||
journal = {CoRR},
|
||||
volume = {abs/2102.11828},
|
||||
year = {2021},
|
||||
url = {https://arxiv.org/abs/2102.11828},
|
||||
eprinttype = {arXiv},
|
||||
eprint = {2102.11828},
|
||||
timestamp = {Fri, 26 Feb 2021 14:31:25 +0100},
|
||||
biburl = {https://dblp.org/rec/journals/corr/abs-2102-11828.bib},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@article{while,
|
||||
author = {Sergey Goncharov and
|
||||
Lutz Schr{\"{o}}der and
|
||||
Christoph Rauch},
|
||||
title = {(Co-)Algebraic Foundations for Effect Handling and Iteration},
|
||||
journal = {CoRR},
|
||||
volume = {abs/1405.0854},
|
||||
year = {2014},
|
||||
url = {http://arxiv.org/abs/1405.0854},
|
||||
eprinttype = {arXiv},
|
||||
eprint = {1405.0854},
|
||||
timestamp = {Mon, 13 Aug 2018 16:47:19 +0200},
|
||||
biburl = {https://dblp.org/rec/journals/corr/GoncharovSR14.bib},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@article{plotkin1975call,
|
||||
title = {Call-by-name, call-by-value and the $\lambda$-calculus},
|
||||
author = {Plotkin, Gordon D.},
|
||||
journal = {Theoretical computer science},
|
||||
volume = {1},
|
||||
number = {2},
|
||||
pages = {125--159},
|
||||
year = {1975},
|
||||
publisher = {Elsevier}
|
||||
}
|
||||
|
||||
@article{scott1993type,
|
||||
title = {A type-theoretical alternative to ISWIM, CUCH, OWHY},
|
||||
author = {Scott, Dana S},
|
||||
journal = {Theoretical Computer Science},
|
||||
volume = {121},
|
||||
number = {1-2},
|
||||
pages = {411--440},
|
||||
year = {1993},
|
||||
publisher = {Elsevier}
|
||||
}
|
||||
1176
img/fau.pdf
Normal file
1176
img/fau.pdf
Normal file
File diff suppressed because one or more lines are too long
BIN
img/tcs.pdf
Normal file
BIN
img/tcs.pdf
Normal file
Binary file not shown.
BIN
main.pdf
Normal file
BIN
main.pdf
Normal file
Binary file not shown.
248
main.tex
Normal file
248
main.tex
Normal file
|
|
@ -0,0 +1,248 @@
|
|||
\documentclass[a4paper,11pt,numbers=noenddot]{scrbook}
|
||||
|
||||
\usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry}
|
||||
\usepackage[ngerman, english]{babel}
|
||||
\babeltags{german=ngerman}
|
||||
% \usepackage{mathabx}
|
||||
% \usepackage{amssymb}
|
||||
\usepackage[dvipsnames]{xcolor} % Coloured text etc.
|
||||
\usepackage{amsthm}
|
||||
\usepackage{thmtools}
|
||||
\usepackage{fancyvrb}
|
||||
\usepackage{anyfontsize}
|
||||
% \usepackage{mathtools}
|
||||
% \usepackage{amsmath}
|
||||
\usepackage{mathpartir}
|
||||
% packages for draft version
|
||||
\usepackage{lineno}
|
||||
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
|
||||
\usepackage{unicode-math}
|
||||
|
||||
% mathpartir uses \atop, amsmath overrides it to throw a warning tho, so we override it back to the original!
|
||||
\makeatletter
|
||||
\let\atop\@@atop % chktex 1
|
||||
\makeatother
|
||||
|
||||
\usepackage{tikz}
|
||||
\usetikzlibrary{cd, babel, quotes}
|
||||
\usepackage{quiver}
|
||||
% \usepackage{stmaryrd} % for \llbracket and \rrbracket
|
||||
\usepackage{ifthen}
|
||||
\usepackage{xspace}
|
||||
\usepackage{makeidx}
|
||||
\usepackage{graphicx}
|
||||
\usepackage{fvextra}
|
||||
\usepackage[style=ieee, sorting=ynt, language=british]{biblatex} % advanced citations, british to make dates DD-MM-YYYY
|
||||
\usepackage[english=british]{csquotes} % biblatex recommended to load this
|
||||
\usepackage{etoolbox,xpatch}
|
||||
|
||||
\makeatletter
|
||||
\AtBeginEnvironment{minted}{\dontdofcolorbox}\def\dontdofcolorbox{\renewcommand\fcolorbox[4][]{##4}}\xpatchcmd{\inputminted}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{}\xpatchcmd{\mintinline}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{} % see https://tex.stackexchange.com/a/401250/
|
||||
\makeatother
|
||||
\usepackage{scrhack}
|
||||
|
||||
\usepackage{multicol}
|
||||
\usepackage[final]{hyperref}
|
||||
|
||||
|
||||
\addbibresource{bib.bib}
|
||||
%\usepackage[right]{showlabels}
|
||||
%\usepackage[justific=raggedright,totoc]{idxlayout}
|
||||
\usepackage[type=CC, modifier=by-sa,version=4.0]{doclicense}
|
||||
|
||||
% Listings package supporting unicode and agda highlighting
|
||||
\usepackage{minted}
|
||||
\setminted[agda]{
|
||||
linenos=true,
|
||||
breaklines=true,
|
||||
encoding=utf8,
|
||||
fontsize=\small,
|
||||
frame=lines,
|
||||
autogobble
|
||||
}
|
||||
% autoref for minted listings
|
||||
\providecommand*{\listingautorefname}{Listing}
|
||||
|
||||
|
||||
\addto\extrasenglish{
|
||||
\renewcommand{\chapterautorefname}{Chapter}
|
||||
\renewcommand{\sectionautorefname}{Section}
|
||||
\renewcommand{\subsectionautorefname}{Subsection}
|
||||
}
|
||||
|
||||
\newcommand\chap[1]{%
|
||||
\chapter*{#1}%
|
||||
\chaptermark{#1}%
|
||||
\addcontentsline{toc}{chapter}{#1}}
|
||||
|
||||
\declaretheorem[name=Definition,style=definition,numberwithin=chapter]{definition}
|
||||
\declaretheorem[name=Example,style=definition,sibling=definition]{example}
|
||||
\declaretheorem[style=definition,numbered=no]{exercise}
|
||||
\declaretheorem[name=Remark,style=definition,sibling=definition]{remark}
|
||||
\declaretheorem[name=Assumption,style=definition,sibling=definition]{assumption}
|
||||
\declaretheorem[name=Observation,style=definition,sibling=definition]{observation}
|
||||
\declaretheorem[name=Theorem,sibling=definition]{theorem}
|
||||
\declaretheorem[sibling=definition]{corollary}
|
||||
\declaretheorem[name=Fact,sibling=definition]{fact}
|
||||
\declaretheorem[sibling=definition]{lemma}
|
||||
\declaretheorem[sibling=lemma]{proposition}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% %
|
||||
% Spacing settings %
|
||||
% %
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\setlength{\parindent}{0pt}
|
||||
\setlength{\parskip}{6pt}
|
||||
% \setlength\parskip{\baselineskip}
|
||||
\setlength{\marginparsep}{0cm}
|
||||
\AtBeginEnvironment{minted}{\setlength{\parskip}{0pt}}
|
||||
|
||||
\title{Implementing Categorical Notions of Partiality and Delay in Agda}
|
||||
|
||||
\author{Leon Vatthauer}
|
||||
|
||||
\makeatletter
|
||||
\hypersetup{
|
||||
pdfauthor={\@author},
|
||||
pdftitle={\@title},
|
||||
% kill those ugly red rectangles around links
|
||||
hidelinks,
|
||||
}
|
||||
\newcommand*{\theauthor}{\@author}
|
||||
\makeatother
|
||||
|
||||
|
||||
\usepackage[scale=.85]{noto-mono}
|
||||
|
||||
\usepackage{mathrsfs}
|
||||
\usepackage{xargs}
|
||||
\usepackage{xstring}
|
||||
|
||||
\newcommand*{\dbtilde}[1]{\tilde{\raisebox{0pt}[0.85\height]{\(\tilde{#1}\)}}}
|
||||
|
||||
% https://unicodeplus.com/U+3016
|
||||
\newcommand*{\lbparen}{〖}
|
||||
\newcommand*{\rbparen}{〗}
|
||||
|
||||
% category C
|
||||
\newcommand*{\C}{\ensuremath{\mathscr{C}}}
|
||||
\newcommand*{\D}{\ensuremath{\mathscr{D}}}
|
||||
% objects of category
|
||||
\newcommand*{\obj}[1]{\ensuremath{\vert #1 \vert}}
|
||||
% category of elgot algebras on #1
|
||||
\newcommand*{\elgotalgs}[1]{\ensuremath{\mathit{ElgotAlgs}(#1)}}
|
||||
% category of monads on #1
|
||||
\newcommand*{\coalgs}[1]{\ensuremath{\mathit{Coalgs}(#1)}}
|
||||
\newcommand*{\monads}[1]{\ensuremath{\mathit{Monads}(#1)}}
|
||||
\newcommand*{\strongmonads}[1]{\ensuremath{\mathit{StrongMonads}(#1)}}
|
||||
% category of pre-Elgot monads on #1
|
||||
\newcommand*{\preelgot}[1]{\ensuremath{\mathit{PreElgot}(#1)}}
|
||||
\newcommand*{\strongpreelgot}[1]{\ensuremath{\mathit{StrongPreElgot}(#1)}}
|
||||
\newcommand*{\setoids}{\ensuremath{\mathit{Setoids}}}
|
||||
% free objects
|
||||
\newcommand*{\freee}[1]{\ensuremath{#1^\star}}
|
||||
\newcommand*{\free}[1]{
|
||||
\ensuremath{
|
||||
\IfSubStr{#1}{\circ}
|
||||
{{\freee{(#1)}}}
|
||||
{\IfSubStr{#1}{\;}
|
||||
{\freee{(#1)}}
|
||||
{\freee{#1}}
|
||||
}
|
||||
}
|
||||
}
|
||||
% right stability
|
||||
\newcommand*{\rss}[1]{\ensuremath{#1^\blacktriangleright}}
|
||||
\newcommand*{\rs}[1]{
|
||||
\ensuremath{
|
||||
\IfSubStr{#1}{\circ}{{\rss{(#1)}}}{\rss{#1}}
|
||||
}
|
||||
}
|
||||
% left stability
|
||||
\newcommand*{\lss}[1]{\ensuremath{#1^\blacktriangleleft}}
|
||||
\newcommand*{\ls}[1]{
|
||||
\ensuremath{
|
||||
\IfSubStr{#1}{\circ}{{\lss{(#1)}}}{\lss{#1}}
|
||||
}
|
||||
}
|
||||
% terminal coalgebra
|
||||
\newcommand*{\coalg}[1]{\ensuremath{\lbparen#1\rbparen}}
|
||||
|
||||
% discretized setoids
|
||||
\newcommand*{\disc}[1]{\ensuremath{\vert #1 \vert}}
|
||||
|
||||
% Defines the `mycase` environment, copied from https://tex.stackexchange.com/questions/251053/how-to-use-case-1-case-2-in-a-proof-ieee-confs
|
||||
\newcounter{cases}
|
||||
\newcounter{subcases}[cases]
|
||||
\newenvironment{mycase}
|
||||
{
|
||||
\setcounter{cases}{0}
|
||||
\setcounter{subcases}{0}
|
||||
\newcommand{\case}
|
||||
{
|
||||
\par\indent\stepcounter{cases}\textbf{Case \thecases.}
|
||||
}
|
||||
\newcommand{\subcase}
|
||||
{
|
||||
\par\indent\stepcounter{subcases}\textit{Subcase (\thesubcases):}
|
||||
}
|
||||
}
|
||||
{
|
||||
\par
|
||||
}
|
||||
\renewcommand*\thecases{\arabic{cases}}
|
||||
\renewcommand*\thesubcases{\roman{subcases}}
|
||||
|
||||
\begin{document}
|
||||
\pagestyle{plain}
|
||||
\input{src/titlepage}%
|
||||
\chapter*{Disclaimer}
|
||||
{\begin{german}
|
||||
Ich versichere, dass ich die Arbeit ohne fremde Hilfe und ohne Benutzung anderer als der angegebenen Quellen angefertigt habe und dass die Arbeit in gleicher oder ähnlicher Form noch keiner anderen Prüfungsbehörde vorgelegen hat und von dieser als Teil einer Prüfungsleistung angenommen wurde.
|
||||
Alle Ausführungen, die wörtlich oder sinngemäß übernommen wurden, sind als solche gekennzeichnet.
|
||||
|
||||
\vspace{5em}
|
||||
Erlangen, \foreignlanguage[date]{ngerman}{\today{}} \rule{7cm}{1pt}\\
|
||||
\phantom{Erlangen, \today{}} \theauthor{}
|
||||
\end{german}}
|
||||
|
||||
% \chapter*{Licensing}
|
||||
% \doclicenseThis{}
|
||||
|
||||
\include{src/00_abstract}
|
||||
|
||||
\tableofcontents
|
||||
|
||||
% \listoftodos\
|
||||
|
||||
\newcommandx{\unsure}[2][1=]{\todo[inline,linecolor=red,backgroundcolor=red!25,bordercolor=red,#1]{#2}}
|
||||
\newcommandx{\change}[2][1=]{\todo[linecolor=blue,backgroundcolor=blue!25,bordercolor=blue,#1]{#2}}
|
||||
\newcommandx{\info}[2][1=]{\todo[inline,linecolor=OliveGreen,backgroundcolor=OliveGreen!25,bordercolor=OliveGreen,#1]{#2}}
|
||||
\newcommandx{\improvement}[2][1=]{\todo[inline,linecolor=Plum,backgroundcolor=Plum!25,bordercolor=Plum,#1]{#2}}
|
||||
|
||||
|
||||
% for creating custom labels like (Fixpoint)
|
||||
\makeatletter
|
||||
\newcommand{\customlabel}[2]{%
|
||||
\protected@write \@auxout {}{\string \newlabel {#1}{{#2}{\thepage}{#2}{#1}{}} }% chktex 1
|
||||
\hypertarget{#1}{#2}%
|
||||
}
|
||||
\makeatother
|
||||
|
||||
\include{src/01_introduction}
|
||||
\include{src/02_preliminaries}
|
||||
\include{src/03_agda-categories}
|
||||
\include{src/04_partiality-monads}
|
||||
\include{src/05_iteration}
|
||||
\include{src/06_setoids}
|
||||
\include{src/07_conclusion}
|
||||
|
||||
\appendix
|
||||
|
||||
\medskip
|
||||
|
||||
\emergencystretch=1em
|
||||
\printbibliography[heading=bibintoc]{}
|
||||
|
||||
\end{document}
|
||||
40
quiver.sty
Normal file
40
quiver.sty
Normal file
|
|
@ -0,0 +1,40 @@
|
|||
% *** quiver ***
|
||||
% A package for drawing commutative diagrams exported from https://q.uiver.app.
|
||||
%
|
||||
% This package is currently a wrapper around the `tikz-cd` package, importing necessary TikZ
|
||||
% libraries, and defining a new TikZ style for curves of a fixed height.
|
||||
%
|
||||
% Version: 1.4.2
|
||||
% Authors:
|
||||
% - varkor (https://github.com/varkor)
|
||||
% - AndréC (https://tex.stackexchange.com/users/138900/andr%C3%A9c)
|
||||
|
||||
\NeedsTeXFormat{LaTeX2e}
|
||||
\ProvidesPackage{quiver}[2021/01/11 quiver]
|
||||
|
||||
% `tikz-cd` is necessary to draw commutative diagrams.
|
||||
\RequirePackage{tikz-cd}
|
||||
% `amssymb` is necessary for `\lrcorner` and `\ulcorner`.
|
||||
% \RequirePackage{amssymb}
|
||||
% `calc` is necessary to draw curved arrows.
|
||||
\usetikzlibrary{calc}
|
||||
% `pathmorphing` is necessary to draw squiggly arrows.
|
||||
\usetikzlibrary{decorations.pathmorphing}
|
||||
|
||||
% A TikZ style for curved arrows of a fixed height, due to AndréC.
|
||||
\tikzset{curve/.style={settings={#1},to path={(\tikztostart)
|
||||
.. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
|
||||
and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
|
||||
.. (\tikztotarget)\tikztonodes}},
|
||||
settings/.code={\tikzset{quiver/.cd,#1}
|
||||
\def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}},
|
||||
quiver/.cd,pos/.initial=0.35,height/.initial=0}
|
||||
|
||||
% TikZ arrowhead/tail styles.
|
||||
\tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}}
|
||||
\tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}}
|
||||
\tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}}
|
||||
% TikZ arrow styles.
|
||||
\tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}}
|
||||
|
||||
\endinput
|
||||
10
src/00_abstract.tex
Normal file
10
src/00_abstract.tex
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
\chapter*{Abstract}
|
||||
Moggi famously showed how to use category theory (specifically monads) to model the semantics of effectful computations.
|
||||
|
||||
In this thesis we will examine how to model possibly non-terminating computations, which requires a monad supporting some form of partiality.
|
||||
For that we will consider categorical properties that a monad that models partiality should satisfy and then compare concrete monads in view of these properties.
|
||||
|
||||
Capretta's delay monad is a typical example for a partiality monad, but it comes with a too intensional notion of built-in equality.
|
||||
Since fixing this seems to be impossible without additional axioms, we will examine a novel approach of defining a partiality monad that works in a general setting by making use of previous research on iteration theories and drawing on the inherent connection between partiality and iteration.
|
||||
|
||||
Finally, we will show that in the category of setoids this partiality monad instantiates to a quotient of the delay monad, yielding a concrete description of the partiality monad in this category.
|
||||
35
src/01_introduction.tex
Normal file
35
src/01_introduction.tex
Normal file
|
|
@ -0,0 +1,35 @@
|
|||
\chapter{Introduction}
|
||||
|
||||
Haskell is considered a purely functional programming language, though the notion of purity referenced is an informal one, not to be confused with the standard notion of pure function, which describes functions that do not have any side effects.
|
||||
Indeed, as a programming language that offers general recursion, Haskell does at least have to include partiality as a side effect. To illustrate this, consider the following standard list reversal function
|
||||
\begin{minted}{haskell}
|
||||
reverse :: [a] -> [a]
|
||||
reverse l = revAcc l []
|
||||
where
|
||||
revAcc [] a = a
|
||||
revAcc (x:xs) a = revAcc xs (x:a)
|
||||
\end{minted}
|
||||
and regard the following definition of an infinite list
|
||||
\begin{minted}{haskell}
|
||||
ones :: [Int]
|
||||
ones = 1 : ones
|
||||
\end{minted}
|
||||
|
||||
Of course evaluation of the term \texttt{reverse ones} will never terminate, hence it is clear that \texttt{reverse} is a partial function.
|
||||
Thus, in order to reason about Haskell programs, or generally programs of any programming language offering general recursion, one needs to be able to model partiality as a side effect.
|
||||
|
||||
Generally for modelling programming languages there are three prevailing methods. First is the operational approach studied by Plotkin~\cite{plotkin1975call}, where partial functions are used that map programs to their resulting values,
|
||||
secondly there is the denotational approach by Scott~\cite{scott1993type}, where programming languages are interpreted mathematically, by functions that capture the ``meaning'' of programs.
|
||||
For this thesis we will consider the third, categorical approach that has been introduced by Moggi~\cite{moggi}.
|
||||
In the categorical approach programs are interpreted in categories, where objects represent types and monads are used to model side effects.
|
||||
The goal for this thesis is thus to study monads which are suitable for modeling partiality.
|
||||
|
||||
We use the dependently typed programming language Agda~\cite{agda} as a safe and type-checked environment for reasoning in category theory, therefore in \autoref{chp:agda-cat} we start out by quickly showcasing the Agda programming language as well as the category theory library that we will be working with.
|
||||
In \autoref{chp:partiality} we will then consider various properties that partiality monads should satisfy and inspect Capretta's delay monad~\cite{delay}, which has been introduced in type theory as a coinductive data type and then studied as a monad in the category of setoids.
|
||||
We will examine the delay monad in a general categorical setting, where we prove strength and commutativity of this monad. However, it is not a minimal partiality monad, i.e.\ one that captures no other side effect besides some form of non-termination, since the monad comes with a too intensional notion of equality. In order to achieve minimality one can consider the quotient of the delay monad where a less intensional notion of equality is used. However, it is believed to be impossible to show that the monadic structure is preserved under such a quotient. In~\cite{quotienting} the axiom of countable choice has been identified as a sufficient assumption under which the monad structure is preserved.
|
||||
|
||||
In order to define a partiality monad using no such assumptions, we will draw on the inherent connection between iteration and recursion in \autoref{chp:iteration} to define a suitable partiality monad, by relating to previous research on iteration theories.
|
||||
This monad has first been introduced and studied in~\cite{uniformelgot} under weaker assumptions than we use, concretely by weakening the notion of Elgot algebra to the notion of uniform iteration algebra, which uses fewer axioms.
|
||||
During mechanization of the results concerning this monad it turned out that under the weaker assumptions, desirable properties like commutativity seem not to be provable, resulting in our adaptation of this monad.
|
||||
Lastly, in \autoref{chp:setoids} we will study this partiality monad in the category of setoids, where notably the axiom of countable choice is provable.
|
||||
In this category, the partiality monad turns out to be equivalent to a certain quotient of the delay monad.
|
||||
528
src/02_preliminaries.tex
Normal file
528
src/02_preliminaries.tex
Normal file
|
|
@ -0,0 +1,528 @@
|
|||
\chapter{Preliminaries}
|
||||
|
||||
We assume familiarity with basic categorical notions, in particular: categories, functors, functor algebras and natural transformations, as well as special objects like (co)products, terminal and initial objects and special classes of morphisms like isomorphisms (isos), epimorphisms (epis) and monomorphisms (monos). % chktex 36
|
||||
In this chapter we will introduce notation that will be used throughout the thesis and also introduce some notions that are crucial to this thesis in more detail.
|
||||
We write \(\obj{\C}\) for the objects of a category \( \C \), \(id_X\) for the identity morphism on \(X\), \((-) \circ (-)\) for the composition of morphisms and \(\C(X,Y)\) for the set of morphisms between \(X\) and \(Y\).
|
||||
We will also sometimes omit indices of the identity and of natural transformations in favor of readability.
|
||||
|
||||
\section{Distributive and Cartesian Closed Categories}
|
||||
Let us first introduce notation for binary (co)products by giving their usual diagrams: % chktex 36
|
||||
|
||||
% https://q.uiver.app/#q=WzAsOCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFs4LDAsIkEgKyBCIl0sWzYsMCwiQSJdLFsxMCwwLCJCIl0sWzgsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDQsImlfMSJdLFs2LDQsImlfMiIsMl0sWzUsNywiZiIsMl0sWzYsNywiZyJdLFs0LDcsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d
|
||||
\[
|
||||
\begin{tikzcd}
|
||||
A && {A \times B} && B && A && {A + B} && B \\
|
||||
\\
|
||||
&& C &&&&&& C
|
||||
\arrow["{\pi_1}"', from=1-3, to=1-1]
|
||||
\arrow["{\pi_2}", from=1-3, to=1-5]
|
||||
\arrow["g"', from=3-3, to=1-5]
|
||||
\arrow["f", from=3-3, to=1-1]
|
||||
\arrow["{\exists! \langle f , g \rangle}"', dashed, from=3-3, to=1-3]
|
||||
\arrow["{i_1}", from=1-7, to=1-9]
|
||||
\arrow["{i_2}"', from=1-11, to=1-9]
|
||||
\arrow["f"', from=1-7, to=3-9]
|
||||
\arrow["g", from=1-11, to=3-9]
|
||||
\arrow["{\exists ! [f , g]}", dashed, from=1-9, to=3-9]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
|
||||
We will furthermore overload this notation and write \(f \times g := \langle f \circ \pi_1 , g \circ \pi_2 \rangle \) and \(f + g := \lbrack i_1 \circ f , i_2 \circ g \rbrack \) on morphisms. To avoid parentheses we will use the convention that products bind stronger than coproducts.
|
||||
|
||||
We write \(1\) for the terminal object together with the unique morphism \(! : A \rightarrow 1\) and \(0\) for the initial object with the unique morphism \(¡ : A \rightarrow 0\).
|
||||
|
||||
Categories with finite products (i.e.\ binary products and a terminal object) are also called Cartesian and categories with finite coproducts (i.e.\ binary coproducts and an initial object) are called coCartesian.
|
||||
|
||||
\begin{definition}[Distributive Category]~\label{def:distributive}
|
||||
A Cartesian and coCartesian category \(\C \) is called distributive if the canonical (left) distributivity morphism \(dstl^{-1}\) is an isomorphism:
|
||||
% https://q.uiver.app/#q=WzAsMixbMCwwLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzMsMCwiWCBcXHRpbWVzIChZICsgWikiXSxbMCwxLCJkc3RsXnstMX0gOj0ge1xcbGJyYWNrIGlkIFxcdGltZXMgaV8xICwgaWQgXFx0aW1lcyBpXzIgXFxyYnJhY2t9IiwwLHsiY3VydmUiOi0zfV0sWzEsMCwiZHN0bCIsMCx7ImN1cnZlIjotM31dXQ==
|
||||
\[
|
||||
\begin{tikzcd}
|
||||
{X \times Y + X \times Z} &&& {X \times (Y + Z)}
|
||||
\arrow["{dstl^{-1} := {\lbrack id \times i_1 , id \times i_2 \rbrack}}", curve={height=-18pt}, from=1-1, to=1-4]
|
||||
\arrow["dstl", curve={height=-18pt}, from=1-4, to=1-1]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
|
||||
\end{definition}
|
||||
|
||||
\begin{remark}
|
||||
Definition~\ref{def:distributive} can equivalently be expressed by requiring that the canonical right distributivity morphism is an iso, giving these inverse morphisms:
|
||||
% https://q.uiver.app/#q=WzAsMixbMCwwLCJZIFxcdGltZXMgWCArIFpcXHRpbWVzIFgiXSxbMywwLCIoWSArIFopIFxcdGltZXMgWCJdLFswLDEsImRzdHJeey0xfSA6PSBbIGlfMSBcXHRpbWVzIGlkICwgaV8yIFxcdGltZXMgaWQgXSIsMCx7ImN1cnZlIjotM31dLFsxLDAsImRzdHIiLDAseyJjdXJ2ZSI6LTN9XV0=
|
||||
\[
|
||||
\begin{tikzcd}
|
||||
{Y \times X + Z\times X} &&& {(Y + Z) \times X}
|
||||
\arrow["{dstr^{-1} := [ i_1 \times id , i_2 \times id ]}", curve={height=-18pt}, from=1-1, to=1-4]
|
||||
\arrow["dstr", curve={height=-18pt}, from=1-4, to=1-1]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
|
||||
These two can be derived from each other by taking either
|
||||
\[dstr := (swap + swap) \circ dstl \circ swap \]
|
||||
or
|
||||
\[dstl := (swap + swap) \circ dstr \circ swap \]
|
||||
where \(swap := \langle \pi_2 , \pi_1 \rangle : A \times B \rightarrow B \times A\).
|
||||
\end{remark}
|
||||
|
||||
\begin{proposition}
|
||||
The distribution morphisms can be viewed as natural transformations i.e.\ they satisfy the following diagrams:
|
||||
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIFxcdGltZXMgKFkgK1opIl0sWzIsMCwiQSBcXHRpbWVzIChCICsgQykiXSxbMCwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzIsMSwiQSBcXHRpbWVzIEIgKyBBIFxcdGltZXMgQyJdLFszLDAsIihZICsgWikgXFx0aW1lcyBYIl0sWzUsMCwiKEIgKyBDKSBcXHRpbWVzIEEiXSxbMywxLCJZIFxcdGltZXMgWCArIFogXFx0aW1lcyBYIl0sWzUsMSwiQiBcXHRpbWVzIEEgKyBDIFxcdGltZXMgQSJdLFswLDEsImYgXFx0aW1lcyAoZyArIGgpIl0sWzIsMywiZiBcXHRpbWVzIGcgKyBmIFxcdGltZXMgaCJdLFswLDIsImRzdGwiXSxbMSwzLCJkc3RsIl0sWzQsNSwiKGcgKyBoKSBcXHRpbWVzIGYiXSxbNCw2LCJkc3RyIiwyXSxbNSw3LCJkc3RyIl0sWzYsNywiZyBcXHRpbWVzIGYgKyBoIFxcdGltZXMgZiJdXQ==
|
||||
\[
|
||||
\begin{tikzcd}[column sep=4ex]
|
||||
{X \times (Y +Z)} && {A \times (B + C)} & {(Y + Z) \times X} && {(B + C) \times A} \\
|
||||
{X \times Y + X \times Z} && {A \times B + A \times C} & {Y \times X + Z \times X} && {B \times A + C \times A}
|
||||
\arrow["{f \times (g + h)}", from=1-1, to=1-3]
|
||||
\arrow["{f \times g + f \times h}", from=2-1, to=2-3]
|
||||
\arrow["dstl", from=1-1, to=2-1]
|
||||
\arrow["dstl", from=1-3, to=2-3]
|
||||
\arrow["{(g + h) \times f}", from=1-4, to=1-6]
|
||||
\arrow["dstr"', from=1-4, to=2-4]
|
||||
\arrow["dstr", from=1-6, to=2-6]
|
||||
\arrow["{g \times f + h \times f}", from=2-4, to=2-6]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
We will prove naturality of \(dstl\), naturality for \(dstr\) is symmetric. We use the fact that \(dstl^{-1}\) is an iso and therefore also an epi.
|
||||
|
||||
\begin{alignat*}{1}
|
||||
& dstl \circ (f \times (g + h)) \circ dstl^{-1} \\
|
||||
=\; & dstl \circ (f \times (g + h)) \circ \lbrack id \times i_1 , id \times i_2 \rbrack \\
|
||||
=\; & dstl \circ \lbrack f \times ((g + h) \circ i_1) , f \times ((g + h) \circ i_2) \rbrack \\
|
||||
=\; & dstl \circ \lbrack f \times (i_1 \circ g) , f \times (i_2 \circ h) \rbrack \\
|
||||
=\; & dstl \circ \lbrack id \times i_1 , id \times i_2 \rbrack \circ (f \times g + f \times h) \\
|
||||
=\; & dstl \circ dstl^{-1} \circ (f \times g + f \times h) \\
|
||||
=\; & (f \times g + f \times h) \\
|
||||
=\; & (f \times g + f \times h) \circ dstl \circ dstl^{-1}\tag*{\qedhere}
|
||||
\end{alignat*}
|
||||
\end{proof}
|
||||
|
||||
\begin{proposition}
|
||||
The distribution morphisms satisfy the following properties:
|
||||
|
||||
\begin{enumerate}
|
||||
\item \(dstl \circ (id \times i_1) = i_1\)
|
||||
\item \(dstl \circ (id \times i_2) = i_2\)
|
||||
\item \([ \pi_1 , \pi_1 ] \circ dstl = \pi_1\)
|
||||
\item \(( \pi_2 + \pi_2 ) \circ dstl = \pi_2\)
|
||||
\item \(dstl \circ swap = (swap + swap) \circ dstr\)
|
||||
\item \(dstr \circ (i_1 \times id) = i_1\)
|
||||
\item \(dstr \circ (i_2 \times id) = i_2\)
|
||||
\item \((\pi_1 + \pi_1) \circ dstr = \pi_1\)
|
||||
\item \([ \pi_2 , \pi_2 ] \circ dstr = \pi_2\)
|
||||
\item \(dstr \circ swap = (swap + swap) \circ dstl\)
|
||||
\end{enumerate}
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
Let us verify the five properties concerning \(dstl\), the ones concerning \(dstr\) follow symmetrically:
|
||||
|
||||
\begin{enumerate}
|
||||
\item
|
||||
\begin{alignat*}{1}
|
||||
& dstl \circ (id \times i_1)
|
||||
\\=\;&dstl \circ [ id \times i_1 , id \times i_2 ] \circ i_1
|
||||
\\=\;&dstl \circ dstl^{-1} \circ i_1
|
||||
\\=\;&i_1
|
||||
\end{alignat*}
|
||||
\item
|
||||
\begin{alignat*}{1}
|
||||
& dstl \circ (id \times i_2)
|
||||
\\=\;&dstl \circ [ id \times i_1 , id \times i_2 ] \circ i_2
|
||||
\\=\;&dstl \circ dstl^{-1} \circ i_2
|
||||
\\=\;&i_2
|
||||
\end{alignat*}
|
||||
\item
|
||||
\begin{alignat*}{1}
|
||||
& \pi_1
|
||||
\\=\;&\pi_1 \circ dstl^{-1} \circ dstl
|
||||
\\=\;&[ \pi_1 \circ (id \times i_1) , \pi_1 \circ (id \times i_2) ] \circ dstl
|
||||
\\=\;&[ \pi_1 , \pi_1 ] \circ dstl
|
||||
\end{alignat*}
|
||||
\item
|
||||
\begin{alignat*}{1}
|
||||
& \pi_2
|
||||
\\=\;&\pi_2 \circ dstl^{-1} \circ dstl
|
||||
\\=\;&[ \pi_2 \circ (id \times i_1) , \pi_2 \circ (id \times i_2) ] \circ dstl
|
||||
\\=\;&(\pi_2 + \pi_2) \circ dstl
|
||||
\end{alignat*}
|
||||
\item
|
||||
\begin{alignat*}{1}
|
||||
& dstl \circ swap
|
||||
\\=\;&dstl \circ swap \circ dstr^{-1} \circ dstr
|
||||
\\=\;&dstl \circ [ swap \circ (i_1 \times id) , swap \circ (i_2 \times id) ] \circ dstr
|
||||
\\=\;&dstl \circ [ (id \times i_1) \circ swap , (id \times i_2) \circ swap ] \circ dstr
|
||||
\\=\;&dstl \circ [ id \times i_1 , id \times i_2 ] \circ (swap + swap) \circ dstr
|
||||
\\=\;&dstl \circ dstl^{-1} \circ (swap + swap) \circ dstr
|
||||
\\=\;&(swap + swap) \circ dstr\tag*{\qedhere}
|
||||
\end{alignat*}
|
||||
\end{enumerate}
|
||||
\end{proof}
|
||||
|
||||
\begin{definition}[Exponential Object]
|
||||
Let \(\C \) be a Cartesian category and \(X , Y \in \vert \C \vert \).
|
||||
An object \(X^Y\) is called an exponential object (of \(X\) and \(Y\)) if there exists an evaluation morphism \(eval : X^Y \times Y \rightarrow X\) and for any \(f : X \times Y \rightarrow Z\) there exists a morphism \(curry\; f : X \rightarrow Z^Y\) that is unique with respect to the following diagram:
|
||||
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJaIFxcdGltZXMgWSJdLFsyLDAsIlheWSBcXHRpbWVzIFkiXSxbMiwyLCJYIl0sWzEsMiwiZXZhbCJdLFswLDEsImN1cnJ5XFw7ZiBcXHRpbWVzIGlkIl0sWzAsMiwiZiIsMl1d
|
||||
\[
|
||||
\begin{tikzcd}
|
||||
{Z \times Y} && {X^Y \times Y} \\
|
||||
\\
|
||||
&& X
|
||||
\arrow["eval", from=1-3, to=3-3]
|
||||
\arrow["{curry\;f \times id}", from=1-1, to=1-3]
|
||||
\arrow["f"', from=1-1, to=3-3]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\end{definition}
|
||||
|
||||
\begin{proposition}
|
||||
Every exponential object \(X^Y\) satisfies the following properties:
|
||||
|
||||
\begin{enumerate}
|
||||
\item The mapping \(curry : \C(X \times Y , Z) \rightarrow \C(X \rightarrow Z^Y)\) is injective,
|
||||
\item \(curry(eval \circ (f \times id)) = f\) for any \(f : X \times Y \rightarrow Z\),
|
||||
\item \(curry\;f \circ g = curry(f \circ (g \times id))\) for any \(f : X \times Y \rightarrow Z, g : A \rightarrow X\).
|
||||
\end{enumerate}
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
\begin{enumerate}
|
||||
\item Let \(f, g : X \times Y \rightarrow Z\) and \(curry\;f = curry\;g\), then indeed
|
||||
\[f = eval \circ (curry\; f \times id) = eval \circ (curry\;g \times id) = g. \]
|
||||
|
||||
\item \(curry(eval \circ (f \times id)) = f\) follows instantly by uniqueness of \(curry(eval \circ (f \times id))\).
|
||||
\item Note that \(eval \circ (curry\;f \circ g \times id) = eval \circ (curry\;f \times id) \circ (g \times id) = f \circ (g \times id)\), thus we are done by uniqueness of \(curry(f \circ (g \times id))\).
|
||||
\qedhere
|
||||
\end{enumerate}
|
||||
\end{proof}
|
||||
|
||||
A Cartesian closed category is a Cartesian category \(\C \) that also has an exponential object \(X^Y\) for any \(X, Y \in \obj{\C} \).
|
||||
The internal logic of Cartesian closed categories is the simply typed \(\lambda \)-calculus, which makes them a suitable environment for interpreting programming languages.
|
||||
For the rest of this thesis we will work in an ambient distributive category \(\C\), that however need not be Cartesian closed as to be more general.
|
||||
|
||||
\section{F-Coalgebras}
|
||||
Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tuples \((X, \alpha : FX \rightarrow X)\) consisting of an object of \(\C \) and a morphism out of the functor. Initial F-algebras have been studied extensively as a means of modeling inductive data types together with induction and recursion principles~\cite{inductive}. For this thesis we will be more interested in the dual concept namely terminal coalgebras; let us formally introduce them now.
|
||||
|
||||
\begin{definition}[F-Coalgebra]
|
||||
A tuple \((X \in \obj{\C}, \alpha : X \rightarrow FX)\) is called an \emph{F-coalgebra} (hereafter referred to as just \emph{coalgebra}).
|
||||
\end{definition}
|
||||
|
||||
\begin{definition}[Coalgebra Morphisms]\label{def:coalgmorph}
|
||||
Let \((X, \alpha : X \rightarrow FX)\) and \((Y, \beta : Y \rightarrow FY)\) be two coalgebras. A morphism between these coalgebras is a morphism \(f : X \rightarrow Y\) such that the following diagram commutes:
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzAsMiwiWSJdLFsyLDAsIkZYIl0sWzIsMiwiRlkiXSxbMSwzLCJcXGJldGEiXSxbMCwyLCJcXGFscGhhIl0sWzAsMSwiZiIsMl0sWzIsMywiRmYiXV0=
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \&\& FX \\
|
||||
\\
|
||||
Y \&\& FY
|
||||
\arrow["\beta", from=3-1, to=3-3]
|
||||
\arrow["\alpha", from=1-1, to=1-3]
|
||||
\arrow["f"', from=1-1, to=3-1]
|
||||
\arrow["Ff", from=1-3, to=3-3]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
|
||||
\end{definition}
|
||||
|
||||
Coalgebras on a given functor together with their morphisms form a category that we call \(\coalgs{F}\).
|
||||
|
||||
\begin{proposition}
|
||||
\(\coalgs{F}\) is a category.
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
Let \((X , \alpha : X \rightarrow FX)\) be a coalgebra. The identity morphism on \((X , \alpha)\) is the identity morphism of \(\C\) that trivially satisfies \(\alpha \circ id = Fid \circ \alpha \).
|
||||
|
||||
Let \((X , \alpha : X \rightarrow FX), (Y, \beta : Y \rightarrow FY)\) and \((Z , \gamma : Z \rightarrow FZ)\) be coalgebras.
|
||||
Composition of \(f : (X, \alpha) \rightarrow (Y, \beta)\) and \(g : (Y, \beta) \rightarrow (Z, \gamma)\) is composition of the underlying morphisms in \(\C \) where:
|
||||
\begin{alignat*}{1}
|
||||
& \gamma \circ g \circ f \\
|
||||
=\; & Fg \circ \beta \circ f \\
|
||||
=\; & Fg \circ Ff \circ \alpha \\
|
||||
=\; & F(g \circ f) \circ \alpha\tag*{\qedhere}
|
||||
\end{alignat*}
|
||||
\end{proof}
|
||||
|
||||
The terminal object of \(\coalgs{F}\) is sometimes called \textit{final coalgebra}, we will however call it the \textit{terminal coalgebra} for consistency with initial F-algebras.
|
||||
Similarly to initial F-algebras, the final coalgebra can be used for modeling the semantics of coinductive data types where terminality of the coalgebra yields corecursion as a definitional principle and coinduction as a proof principle.
|
||||
Let us make the universal property of terminal coalgebras concrete.
|
||||
|
||||
\begin{definition}[Terminal Coalgebra]
|
||||
A coalgebra \((T, t : T \rightarrow FT)\) is called a terminal coalgebra if for any other coalgebra \((X, \alpha : X \rightarrow FX)\) there exists a unique morphism \(\coalg{\alpha} : X \rightarrow T\) satisfying:
|
||||
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzIsMCwiRlgiXSxbMCwyLCJUIl0sWzIsMiwiRlQiXSxbMCwxLCJcXGFscGhhIl0sWzIsMywidCJdLFswLDIsIlxcbGxicmFja2V0IFxcYWxwaGEgXFxycmJyYWNrZXQiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMSwzLCJGXFxsbGJyYWNrZXQgXFxhbHBoYSBcXHJyYnJhY2tldCJdXQ==
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \&\& FX \\
|
||||
\\
|
||||
T \&\& FT
|
||||
\arrow["\alpha", from=1-1, to=1-3]
|
||||
\arrow["t", from=3-1, to=3-3]
|
||||
\arrow["{\coalg{\alpha}}"', dashed, from=1-1, to=3-1]
|
||||
\arrow["{F\coalg{\alpha}}", from=1-3, to=3-3]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
We use the common notation \(\nu F\) to denote the terminal coalgebra for \(F\) (if it exists).
|
||||
\end{definition}
|
||||
|
||||
We will discuss the concrete form that induction and coinduction take in a type theory in \autoref{chp:agda-cat}. Let us now reiterate a famous Lemma concerning terminal F-coalgebras.
|
||||
|
||||
\begin{lemma}[Lambek's Lemma~\cite{lambek}]\label{lem:lambek}
|
||||
Let \((T, t : T \rightarrow FT)\) be a terminal coalgebra. Then \(t\) is an isomorphism.
|
||||
\end{lemma}
|
||||
% \begin{proof}
|
||||
% First note that \((FT, Ft : FT \rightarrow FFT)\) is also an F-coalgebra. This yields the unique morphism \(\coalg{Ft} : FT \rightarrow T\) satisfying:
|
||||
% % https://q.uiver.app/#q=WzAsNCxbMCwwLCJGVCJdLFsyLDAsIkZGVCJdLFswLDIsIlQiXSxbMiwyLCJGVCJdLFswLDEsIkZ0Il0sWzIsMywidCJdLFswLDIsIlxcbGxicmFja2V0IEZ0IFxccnJicmFja2V0IiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMywiRlxcbGxicmFja2V0IEZ0IFxccnJicmFja2V0Il1d
|
||||
% \[
|
||||
% \begin{tikzcd}[ampersand replacement=\&]
|
||||
% FT \&\& FFT \\
|
||||
% \\
|
||||
% T \&\& FT
|
||||
% \arrow["Ft", from=1-1, to=1-3]
|
||||
% \arrow["t", from=3-1, to=3-3]
|
||||
% \arrow["{\coalg{Ft}}"', dashed, from=1-1, to=3-1]
|
||||
% \arrow["{F\coalg{Ft}}", from=1-3, to=3-3]
|
||||
% \end{tikzcd}
|
||||
% \]
|
||||
|
||||
% \(\coalg{Ft}\) is inverse to \(t\):
|
||||
|
||||
% \begin{enumerate}
|
||||
% \item \(\coalg{Ft} \circ t : (T, t) \rightarrow (T, t)\) is a morphism between F-coalgebras since
|
||||
% \begin{alignat*}{1}
|
||||
% & F(\coalg{Ft} \circ t) \circ t \\
|
||||
% =\; & F \coalg{Ft} \circ t \circ t \\
|
||||
% =\; & F \coalg{Ft} \circ Ft \circ t \\
|
||||
% =\; & t \circ \coalg{Ft} \circ t
|
||||
% \end{alignat*}
|
||||
% By uniqueness of the identity on \((T, t)\) we follow that \(\coalg{Ft} \circ t = id\).
|
||||
|
||||
% \item \(t \circ \coalg{Ft} = id : (FT, Ft) \rightarrow (FT, Ft)\) follows by:
|
||||
% \begin{alignat*}{1}
|
||||
% & t \circ \coalg{Ft} \\
|
||||
% =\; & F\coalg{Ft} \circ Ft \\
|
||||
% =\; & F(\coalg{Ft} \circ t) \\
|
||||
% =\; & F(id) \\
|
||||
% =\; & id
|
||||
% \end{alignat*}
|
||||
% \end{enumerate}
|
||||
% \end{proof}
|
||||
|
||||
\section{Monads}
|
||||
Monads are widely known in functional programming as a means for modeling effects in ``pure'' languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
|
||||
|
||||
\begin{definition}[Monad]
|
||||
A monad \(\mathbf{T}\) on a category \(\C \) is a triple \((T, \eta, \mu)\), where \(T : \C \rightarrow \C \) is an endofunctor and \(\eta : Id \rightarrow T, \mu : TT \rightarrow T\) are natural transformations, satisfying the following laws:
|
||||
\begin{alignat*}{2}
|
||||
& \mu_X \circ \mu_{TX} & & = \mu_X \circ T\mu_X \tag*{(M1)}\label{M1} \\
|
||||
& \mu_X \circ \eta_{TX} & & = id_{TX} \tag*{(M2)}\label{M2} \\
|
||||
& \mu_X \circ T\eta_X & & = id_{TX} \tag*{(M3)}\label{M3}
|
||||
\end{alignat*}
|
||||
|
||||
These laws are expressed by the following diagrams:
|
||||
% with indices: % https://q.uiver.app/#q=WzAsOCxbMCwwLCJUVFRYIl0sWzIsMCwiVFRYIl0sWzAsMiwiVFRYIl0sWzIsMiwiVFgiXSxbNCwwLCJUWCJdLFs2LDAsIlRUWCJdLFs4LDAsIlRYIl0sWzYsMiwiVFgiXSxbMCwxLCJcXG11X3tUWH0iXSxbMCwyLCJUXFxtdV9YIiwyXSxbMSwzLCJcXG11X1giXSxbNSw3LCJcXG11X1giXSxbNCw1LCJcXGV0YV97VFh9Il0sWzYsNSwiVFxcZXRhX1giXSxbNCw3LCJpZF97VFh9IiwyXSxbNiw3LCJpZF97VFh9IiwyXSxbMiwzLCJcXG11X1giLDJdXQ==
|
||||
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJUVFRYIl0sWzIsMCwiVFRYIl0sWzAsMiwiVFRYIl0sWzIsMiwiVFgiXSxbNCwwLCJUWCJdLFs2LDAsIlRUWCJdLFs4LDAsIlRYIl0sWzYsMiwiVFgiXSxbMCwxLCJcXG11Il0sWzAsMiwiVFxcbXUiLDJdLFsxLDMsIlxcbXUiXSxbNSw3LCJcXG11Il0sWzQsNSwiXFxldGEiXSxbNiw1LCJUIl0sWzQsNywiaWQiLDJdLFs2LDcsImlkIiwyXSxbMiwzLCJcXG11IiwyXV0=
|
||||
\[
|
||||
\begin{tikzcd}
|
||||
TTTX && TTX && TX && TTX && TX \\
|
||||
\\
|
||||
TTX && TX &&&& TX
|
||||
\arrow["\mu", from=1-1, to=1-3]
|
||||
\arrow["T\mu"', from=1-1, to=3-1]
|
||||
\arrow["\mu", from=1-3, to=3-3]
|
||||
\arrow["\mu", from=1-7, to=3-7]
|
||||
\arrow["\eta", from=1-5, to=1-7]
|
||||
\arrow["T", from=1-9, to=1-7]
|
||||
\arrow["id"', from=1-5, to=3-7]
|
||||
\arrow["id"', from=1-9, to=3-7]
|
||||
\arrow["\mu"', from=3-1, to=3-3]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\end{definition}
|
||||
|
||||
\begin{definition}[Monad Morphism]\label{def:monadmorphism}
|
||||
A morphism between monads \((S : \C \rightarrow \C, \eta^S, \mu^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T)\) is a natural transformation \(\alpha : S \rightarrow T\) between the underlying functors such that the following diagrams commute.
|
||||
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzIsMCwiU1giXSxbMiwxLCJUWCJdLFszLDAsIlNTWCJdLFs1LDAsIlNUWCJdLFszLDEsIlNYIl0sWzcsMCwiVFRYIl0sWzcsMSwiVFgiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl1d
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \&\& SX \& SSX \&\& STX \&\& TTX \\
|
||||
\&\& TX \& SX \&\&\&\& TX
|
||||
\arrow["{\eta^S}", from=1-1, to=1-3]
|
||||
\arrow["\alpha", from=1-3, to=2-3]
|
||||
\arrow["{\eta^T}"', from=1-1, to=2-3]
|
||||
\arrow["S\alpha", from=1-4, to=1-6]
|
||||
\arrow["{\mu^S}"', from=1-4, to=2-4]
|
||||
\arrow["\alpha", from=1-6, to=1-8]
|
||||
\arrow["\alpha"', from=2-4, to=2-8]
|
||||
\arrow["{\mu^T}", from=1-8, to=2-8]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\end{definition}
|
||||
|
||||
This yields a category of monads on a given category \(\C\) that we call \(\monads{\C}\).
|
||||
|
||||
\begin{proposition}\label{prop:monadscat}
|
||||
\(\monads{\C}\) is a category.
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
The identity morphism of \(\monads{\C}\) is the identity natural transformation \(Id : F \rightarrow F\), which trivially respects the monad unit and multiplication. Composition of monad morphisms is composition of the underlying natural transformation, the diagrams then also follow easily.
|
||||
\end{proof}
|
||||
|
||||
Monads can also be specified in a second equivalent way that is better suited to describe computation.
|
||||
|
||||
\begin{definition}[Kleisli Triple]
|
||||
A Kleisli triple on a category \(\C \) is a triple \((F, \eta, {(-)}^*)\), where \(F : \obj{C} \rightarrow \obj{C}\) is a mapping on objects, \({(\eta_X : X \rightarrow FX)}_{X\in\obj{C}}\) is a family of morphisms and for every morphism \(f : X \rightarrow FY\) there exists a morphism \(f^* : FX \rightarrow FY\) called the Kleisli lifting, where the following laws hold:
|
||||
\begin{alignat*}{3}
|
||||
& \eta_X^* & & = id_{FX} \tag*{(K1)}\label{K1} \\
|
||||
& f^* \circ \eta_X & & = f & & \text{ for any } f : X \rightarrow FY \tag*{(K2)}\label{K2} \\
|
||||
& f^* \circ g* & & = {(f^* \circ g)}^* & & \text{ for any } f : Y \rightarrow FZ, g : X \rightarrow FY \tag*{(K3)}\label{K3}
|
||||
\end{alignat*}
|
||||
\end{definition}
|
||||
|
||||
Let \(f : X \rightarrow TY, g : Y \rightarrow TZ\) be two programs, where \(T\) is a Kleisli triple. These programs can be composed by taking: \(f^* \circ g : X \rightarrow TZ\), which is called Kleisli composition. Haskell's do-notation is a useful tool for writing Kleisli composition in a legible way. We will sometimes express \((f^* \circ g) x\) equivalently as
|
||||
\begin{minted}{haskell}
|
||||
do y <- g x
|
||||
f y
|
||||
\end{minted}
|
||||
|
||||
This yields the category of programs for a Kleisli triple that is called the Kleisli category.
|
||||
|
||||
\begin{definition}[Kleisli Category]
|
||||
Given a monad \(T\) on a category \(\C \), the Kleisli category \(\C^T\) is defined as:
|
||||
\begin{itemize}
|
||||
\item \(\vert \C^T \vert = \obj{C}\)
|
||||
\item \(\C^T(X, Y) = \C(X, TY)\)
|
||||
\item Composition of programs is Kleisli composition.
|
||||
\item The identity morphisms are the unit morphisms of \(T\), \(id_X = \eta_X : X \rightarrow TX\)
|
||||
\end{itemize}
|
||||
The laws of categories then follow from the Kleisli triple laws.
|
||||
\end{definition}
|
||||
|
||||
\begin{proposition}[\cite{manes}] The notions of Kleisli triple and monad are equivalent.
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
The crux of this proof is defining the triples, the proofs of the corresponding laws (functoriality, naturality, monad and Kleisli triple laws) are left out.
|
||||
|
||||
``\(\Rightarrow \)'':
|
||||
Given a Kleisli triple \((F, \eta, {(-)}^*)\),
|
||||
we obtain a monad \((F, \eta, \mu)\) where \(F\) is the object mapping of the Kleisli triple together with the functor action \(F(f : X \rightarrow Y) = {(\eta_Y \circ f)}^*\),
|
||||
\(\eta \) is the morphism family of the Kleisli triple where naturality is easy to show and \(\mu \) is a natural transformation defined as \(\mu_X = id_{FX}^*\)
|
||||
|
||||
|
||||
``\(\Leftarrow \)'': \\
|
||||
Given a monad \((F, \eta, \mu)\),
|
||||
we obtain a Kleisli triple \((F, \eta, {(-)}^*)\) by restricting the functor \(F\) on objects,
|
||||
taking the underlying mapping of \(\eta \) and defining \(f^* = \mu_Y \circ Ff\) for any \(f : X \rightarrow FY\).
|
||||
\end{proof}
|
||||
|
||||
For the rest of this thesis we will use both equivalent notions interchangeably to make definitions easier.
|
||||
|
||||
\section{Strong and Commutative Monads}
|
||||
Consider the following program in do-notation
|
||||
\begin{minted}{haskell}
|
||||
do y <- g x
|
||||
f (x , y)
|
||||
\end{minted}
|
||||
where \(g : X \rightarrow TY\) and \(f : X \times Y \rightarrow TZ\) are programs and \(\mathbf{T}\) is a monad. Kleisli composition does not suffice for interpreting this program, we will get stuck at
|
||||
\[X \overset{\langle id , g \rangle}{\longrightarrow} X \times TY \overset{?}{\longrightarrow} T(X \times Y) \overset{f^*}{\longrightarrow} TZ. \]
|
||||
|
||||
Instead, one needs the following stronger notion of monad.
|
||||
\begin{definition}[Strong Monad] A monad \((T, \eta, \mu)\) on a Cartesian category \(\C \) is called strong if there exists a natural transformation \(\tau_{X,Y} : X \times TY \rightarrow T(X \times Y)\) that satisfies the following conditions:
|
||||
\begin{alignat*}{2}
|
||||
& T\pi_2 \circ \tau_{1,X} & & = \pi_2 \tag*{(S1)}\label{S1} \\
|
||||
& \tau_{X,Y} \circ (id_X \times \eta_Y) & & = \eta_{X\times Y} \tag*{(S2)}\label{S2} \\
|
||||
& \tau_{X,Y} \circ (id_X \times \mu_Y) & & = \mu_{X\times Y} \circ T\tau_{X,Y} \circ \tau_{X,TY} \tag*{(S3)}\label{S3} \\
|
||||
& M \alpha_{X,Y,Z} \circ \tau_{X \times Y, Z} & & = \tau_{X, Y\times Z} \circ (id_X \times \tau_{Y, Z}) \circ \alpha_{X,Y,TZ} \tag*{(S4)}\label{S4}
|
||||
\end{alignat*}
|
||||
where \(\alpha_{X,Y,Z} = \langle \langle \pi_1 , \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2 \rangle : X \times (Y \times Z) \rightarrow (X \times Y) \times Z\) is the associativity morphism on products.
|
||||
\end{definition}
|
||||
|
||||
\begin{definition}[Strong Monad Morphism]\label{def:strongmonadmorphism}
|
||||
A morphism between two strong monads \((S : \C \rightarrow \C, \eta^S, \mu^S, \tau^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T, \tau^T)\) is a morphism between monads as in \autoref{def:monadmorphism} where additionally the following diagram commutes.
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgU1kiXSxbMCwyLCJTKFggXFx0aW1lcyBZKSJdLFsyLDIsIlQoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIFRZIl0sWzAsMSwiXFx0YXVeUyJdLFsxLDIsIlxcYWxwaGEiXSxbMCwzLCJpZCBcXHRpbWVzIFxcYWxwaGEiXSxbMywyLCJcXHRhdV5UIiwyXV0=
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
{X \times SY} \&\& {X \times TY} \\
|
||||
\\
|
||||
{S(X \times Y)} \&\& {T(X \times Y)}
|
||||
\arrow["{\tau^S}", from=1-1, to=3-1]
|
||||
\arrow["\alpha", from=3-1, to=3-3]
|
||||
\arrow["{id \times \alpha}", from=1-1, to=1-3]
|
||||
\arrow["{\tau^T}"', from=1-3, to=3-3]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\end{definition}
|
||||
|
||||
As with monads this yields a category of strong monads on \(\C\) that we call \(\strongmonads{\C}\).
|
||||
|
||||
Let us now consider the following two programs
|
||||
\begin{multicols}{2}
|
||||
\begin{minted}{haskell}
|
||||
do x <- p
|
||||
y <- q
|
||||
return (x, y)
|
||||
\end{minted}
|
||||
|
||||
\begin{minted}{haskell}
|
||||
do y <- q
|
||||
x <- p
|
||||
return (x, y)
|
||||
\end{minted}
|
||||
\end{multicols}
|
||||
Where \(p : TX\) and \(q : TY\) are computations of some monad \(T\). A monad where these programs are equal, is called commutative.
|
||||
|
||||
\begin{definition}[Commutative Monad]
|
||||
A strong monad \(\mathbf{T}\) is called commutative if the (right) strength \(\tau \) commutes with the induced left strength
|
||||
\[\sigma_{X,Y} = Tswap \circ \tau_{Y,X} \circ swap : TX \times Y \rightarrow T(X \times Y)\]
|
||||
that satisfies symmetrical conditions to the ones \(\tau \) satisfies.
|
||||
Concretely, \(\mathbf{T}\) is called commutative if the following diagram commutes:
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwyLCJUKFggXFx0aW1lcyBUWSkiXSxbMiwwLCJUKFRYIFxcdGltZXMgWSkiXSxbMiwyLCJUKFggXFx0aW1lcyBZKSJdLFswLDAsIlRYIFxcdGltZXMgVFkiXSxbMywxLCJcXHRhdSJdLFszLDAsIlxcc2lnbWEiLDJdLFswLDIsIlxcdGF1XioiLDJdLFsxLDIsIlxcc2lnbWFeKiJdXQ==
|
||||
\[
|
||||
\begin{tikzcd}
|
||||
{TX \times TY} && {T(TX \times Y)} \\
|
||||
\\
|
||||
{T(X \times TY)} && {T(X \times Y)}
|
||||
\arrow["\tau", from=1-1, to=1-3]
|
||||
\arrow["\sigma"', from=1-1, to=3-1]
|
||||
\arrow["{\tau^*}"', from=3-1, to=3-3]
|
||||
\arrow["{\sigma^*}", from=1-3, to=3-3]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\end{definition}
|
||||
|
||||
\section{Free Objects}
|
||||
Free objects, roughly speaking, are constructions for instantiating structure declarations in a minimal way.
|
||||
We will rely on free structures in \autoref{chp:iteration} to define a monad in a general setting. We recall the definition
|
||||
to establish some notation and then describe how to obtain a monad via existence of free objects.
|
||||
|
||||
\begin{definition}[Free Object]\label{def:free}
|
||||
Let \(\C, \D \) be categories and \(U : \C \rightarrow \D \) be a forgetful functor (whose construction usually is obvious). A free object on some object \(X \in \obj{\D}\) is an object \(FX \in \obj{\C}\) together with a morphism \(\eta : X \rightarrow UFX\) such that for any \(Y \in \obj{\C}\) and \(f : X \rightarrow UY\) there exists a unique morphism \(\free{f} : FX \rightarrow Y\) satisfying:
|
||||
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJVRlgiXSxbMCwxLCJmIl0sWzAsMiwiXFxldGEiLDJdLFsyLDEsIlVcXGZyZWV7Zn0iLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \& UY \\
|
||||
UFX
|
||||
\arrow["f", from=1-1, to=1-2]
|
||||
\arrow["\eta"', from=1-1, to=2-1]
|
||||
\arrow["{U\free{f}}"', dashed, from=2-1, to=1-2]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\end{definition}
|
||||
|
||||
\begin{proposition}\label{thm:freemonad}
|
||||
Let \(U : \C \rightarrow \D \) be a forgetful functor.
|
||||
If for every \(X \in \obj{\D}\) a free object \(FX \in \obj{C}\) exists then \((X \mapsto UFX, \eta : X \rightarrow UFX, \free{(f : X \rightarrow UFY)} : UFX \rightarrow UFY)\) is a Kleisli triple on \(\D \).
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
We are left to check the laws of Kleisli triples.
|
||||
|
||||
\begin{itemize}
|
||||
\item[\ref{K1}] \(\free{\eta} = id\)
|
||||
|
||||
By uniqueness of \(\free{\eta}\) it suffices to show that \(id \circ \eta = \eta \) which holds trivially.
|
||||
\item[\ref{K2}] \(\free{f} \circ \eta = f\) for any \(f : X \rightarrow UFY\)
|
||||
|
||||
This is the universal property concerning \(\free{f}\).
|
||||
\item[\ref{K3}] \(\free{f} \circ \free{g} = \free{\freee{f} \circ g}\) for any \(f : Y \rightarrow UFZ, g : X \rightarrow UFY\)
|
||||
|
||||
By uniqueness of \(\free{\freee{f} \circ g}\) we are left to show \(\free{f} \circ \free{g} \circ \eta = \free{f} \circ g\) which again follows directly by the universal property of \(\free{g}\).
|
||||
\qedhere
|
||||
\end{itemize}
|
||||
\end{proof}
|
||||
143
src/03_agda-categories.tex
Normal file
143
src/03_agda-categories.tex
Normal file
|
|
@ -0,0 +1,143 @@
|
|||
\chapter{Implementing Category Theory in Agda}\label{chp:agda-cat}
|
||||
|
||||
There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits of such a formalization are clear: having a usable formalization allows one to reason about categorical notions in a type checked environment that makes errors less likely.
|
||||
Ideally such a development will bring researchers together and enable them to work in a unified setting that enables efficient communication of ideas and concepts.
|
||||
In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library that serves as an extensive foundation of categorical definitions.
|
||||
This chapter shall serve as a quick introduction to the relevant parts of Agda's type theory, the agda-categories library, and the formalization of this thesis.
|
||||
|
||||
\section{The Underlying Type Theory}\label{sec:typetheory}
|
||||
Agda implements a Martin-Löf style dependent type theory with \emph{inductive} and \emph{coinductive types} as well as an infinite hierarchy of universes \texttt{Set₀, Set₁, \ldots}, where usually \texttt{Set₀} is abbreviated as \texttt{Set}.
|
||||
Recall that inductive types usually come with a principle for defining functions from inductive types, called \emph{recursion} and a principle for proving facts about the inhabitants of inductive types, called \emph{induction}.
|
||||
These are standard notions and need no further introduction.
|
||||
Coinductive types come with dual principles that are however lesser known.
|
||||
Dually to inductive types that are defined by their \emph{constructors}, coinductive types are defined by their \emph{destructors} or their observational behavior.
|
||||
Take the type of streams over a type \texttt{A}, for example. In Agda one would define this type as a coinductive record like so:
|
||||
\begin{minted}{agda}
|
||||
record Stream (A : Set) : Set where
|
||||
coinductive
|
||||
field
|
||||
head : A
|
||||
tail : Stream A
|
||||
\end{minted}
|
||||
i.e.\ the type of streams over \texttt{A} is defined by the two destructors \texttt{head : Stream A → A} and \texttt{tail : Stream A → Stream A} that return the head and the tail of the stream respectively. % chktex 26
|
||||
Now, \emph{corecursion} is a principle for defining functions into coinductive types by specifying how results of the function may be observed. Take for example the following function which defines an infinite stream repeating the same argument and is defined by use of Agda's \emph{copatterns}.
|
||||
\begin{minted}{agda}
|
||||
repeat : {A : Set} (a : A) → Stream A
|
||||
head (repeat a) = a
|
||||
tail (repeat a) = repeat a
|
||||
\end{minted}
|
||||
Let us introduce the usual notion of stream bisimilarity. Given two streams, they are bisimilar if their heads are equal and their tails are bisimilar.
|
||||
\begin{minted}{agda}
|
||||
record _≈_ {A} (s : Stream A) (t : Stream A) : Set where
|
||||
coinductive
|
||||
field
|
||||
head : head s ≡ head t
|
||||
tail : tail s ≈ tail t
|
||||
\end{minted}
|
||||
In this definition \texttt{\_≡\_} is the built-in propositional equality in Agda with the single constructor \texttt{refl}. We can now use coinduction as a proof principle to proof a fact about streams.
|
||||
\begin{minted}{agda}
|
||||
repeat-eq : ∀ {A} (a : A) → repeat a ≈ tail (repeat a)
|
||||
head (repeat-eq {A} a) = refl
|
||||
tail (repeat-eq {A} a) = repeat-eq a
|
||||
\end{minted}
|
||||
Where in the coinductive step we were able to assume that \texttt{repeat a ≈ tail(repeat a)} already holds and showed that thus \texttt{tail(repeat a) ≈ tail(tail(repeat a))} holds. % chktex 36
|
||||
|
||||
Streams are always infinite and thus this representation of coinductive types as coinductive records is well suited for them. However, consider the type of \emph{possibly} infinite lists, that we will call \texttt{coList}. In pseudo notation this type can be defined as
|
||||
\begin{minted}{agda}
|
||||
codata coList (A : Set) : Set where
|
||||
nil : coList A
|
||||
_∷_ : A → coList A → coList A
|
||||
\end{minted}
|
||||
That is, the coinductive type \texttt{coList} is defined by the constructors \texttt{nil} and \texttt{\_∷\_}.
|
||||
Agda does implement a second way of defining coinductive types that allows exactly such definitions, however the use of these sometimes called \emph{positive coinductive types} is discouraged, since it is known to break subject reduction~\cite{agda-man}\cite{coq-man}. Instead, sticking to coinductive records, we can define \texttt{coList} as two mutual types, one inductive and the other coinductive:
|
||||
\begin{minted}{agda}
|
||||
mutual
|
||||
data coList (A : Set) : Set where
|
||||
nil : coList A
|
||||
_∷_ : A → coList′ A → coList A
|
||||
record coList′ (A : Set) : Set where
|
||||
coinductive
|
||||
field force : coList A
|
||||
\end{minted}
|
||||
Unfortunately, this does add the overhead of having to define functions on \texttt{coList} as mutual recursive functions, e.g.\ the \texttt{repeat} function from before can be defined as
|
||||
\begin{minted}{agda}
|
||||
mutual
|
||||
repeat : {A : Set} (a : A) → coList A
|
||||
repeat′ : {A : Set} (a : A) → coList′ A
|
||||
repeat a = a ∷ repeat′ a
|
||||
force (repeat′ a) = repeat a
|
||||
\end{minted}
|
||||
or more succinctly using a \(\lambda\)-function
|
||||
\begin{minted}{agda}
|
||||
repeat : {A : Set} (a : A) → coList A
|
||||
repeat a = a ∷ λ { .force → repeat a }
|
||||
\end{minted}
|
||||
In \autoref{chp:setoids} we will work with such a coinductive type that is defined by constructors, hence to avoid the overhead of defining every data type twice and using mutual function definitions in the thesis, we will work in a type theory that does offer coinductive types with constructors and their respective corecursion and coinduction principles.
|
||||
However, in the formalization we stick to using coinductive records as to implement best practices.
|
||||
The translation between the two styles is straightforward, as illustrated by the previous example.
|
||||
|
||||
\section{Setoid Enriched Categories}
|
||||
Let us now consider how to implement category theory in Agda. The usual textbook definition of a category glosses over some design decisions that have to be made when implementing it in type theory. One would usually see something like this:
|
||||
\begin{definition}[Category]
|
||||
A category consists of
|
||||
\begin{itemize}
|
||||
\item A collection of objects
|
||||
\item A collection of morphisms between objects
|
||||
\item For every two morphisms \(f : X \rightarrow Y, g : Y \rightarrow Z\) another morphism \(g \circ f : X \rightarrow Z\) called the composition
|
||||
\item For every object \(X\) a morphism \(id_X : X \rightarrow X\) called the identity
|
||||
\end{itemize}
|
||||
where the composition is associative, and the identity morphisms are identities with respect to the composition.
|
||||
\end{definition}
|
||||
|
||||
Here \emph{collection} refers to something that behaves set-like, which is not a set and is needed to prevent size issues (there is no set of all sets, otherwise we would obtain Russel's paradox, but there is a collection of all sets), it is not immediately clear how to translate this to type theory.
|
||||
Furthermore, in mathematical textbooks equality between morphisms is usually taken for granted, i.e.\ there is some global notion of equality that is clear to everyone.
|
||||
In type theory we need to be more thorough as there is no global notion of equality, eligible for all purposes, e.g.\ the standard notion of propositional equality has issues when dealing with functions in that it requires extra axioms like functional extensionality.
|
||||
|
||||
The definition of category that we will work with can be seen in \autoref{lst:category} (unnecessary information has been stripped).
|
||||
The key differences to the definition above are firstly that instead of talking about collections, Agda's infinite \texttt{Set} hierarchy is utilized to prevent size issues.
|
||||
This notion of category is thus parametrized by 3 universe levels, one for objects, one for morphisms and one for equalities.
|
||||
A consequence is that the category does not contain a type of all morphisms, instead it contains a type of morphisms for any pair of objects.
|
||||
Furthermore, the types of morphisms are equipped with an equivalence relation \texttt{\_≈\_}, making them setoids.
|
||||
This addresses the aforementioned issue of how to implement equality between morphisms: the notion of equality is just added to the definition of a category. This version of the notion of category is also called a \emph{setoid-enriched category}.
|
||||
|
||||
As a consequence of using a custom equality relation, proofs like \texttt{∘-resp-≈} are needed throughout the library to make sure that operations on morphisms respect the equivalence relation. In the thesis we will omit such proofs, but they are contained in our formalization.
|
||||
Lastly, the designers of agda-categories also include symmetric proofs like \texttt{sym-assoc} to definitions, in this case to guarantee that the opposite category of the opposite category is equal to the original category, and a similar reason for requiring \texttt{identity²}, we won't address the need for these proofs and just accept the requirement as given for the rest of the thesis.
|
||||
|
||||
\begin{listing}[H]
|
||||
\begin{minted}{agda}
|
||||
record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
|
||||
field
|
||||
Obj : Set o
|
||||
_⇒_ : Obj → Obj → Set ℓ
|
||||
_≈_ : ∀ {A B : Obj } → (A ⇒ B) → (A ⇒ B) → Set e
|
||||
|
||||
id : ∀ {A : Obj} → (A ⇒ A)
|
||||
_∘_ : ∀ {A B C : Obj} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)
|
||||
|
||||
assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D}
|
||||
→ (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
|
||||
sym-assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D}
|
||||
→ h ∘ (g ∘ f) ≈ (h ∘ g) ∘ f
|
||||
identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
|
||||
identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
|
||||
identity² : ∀ {A} → id ∘ id {A} ≈ id {A}
|
||||
equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
|
||||
∘-resp-≈ : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B}
|
||||
→ f ≈ h
|
||||
→ g ≈ i
|
||||
→ f ∘ g ≈ h ∘ i
|
||||
\end{minted}
|
||||
\caption{Definition of Category~\cite{agda-categories}}
|
||||
\label{lst:category}
|
||||
\end{listing}
|
||||
|
||||
From this it should be clear how other basic notions like functors or natural transformations look in the library.
|
||||
|
||||
\section{The formalization}
|
||||
Every result and used fact (except for \autoref{prop:liftingkleisli}) in this thesis has been proven either in our own formalization\footnote{\href{https://git8.cs.fau.de/theses/bsc-leon-vatthauer}{https://git8.cs.fau.de/theses/bsc-leon-vatthauer}} or in the agda-categories library~\cite{agda-categories}.
|
||||
The formalization is meant to be used as a reference alongside this thesis, where concrete details of proofs can be looked up and verified.
|
||||
The preferred format for viewing the formalization is as automatically generated clickable HTML code\footnote{\href{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/}{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/}},
|
||||
where multiple annotations explaining the structure have been added in Markdown, however concrete explanations of the proofs and their main ideas are mostly just contained in this thesis.
|
||||
|
||||
In the future this formalization may be adapted into a separate library that uses the agda-categories library as a basis but is more focussed on the study of partiality monads and iteration theories.
|
||||
As such the formalization has been structured similar to the agda-categories library, where key concepts such as monads correspond to separate top-level folders, which contain the core definitions as well as folders for sub-concepts and their properties.
|
||||
572
src/04_partiality-monads.tex
Normal file
572
src/04_partiality-monads.tex
Normal file
|
|
@ -0,0 +1,572 @@
|
|||
\chapter{Partiality Monads}\label{chp:partiality}
|
||||
Moggi's categorical semantics~\cite{moggi} describe a way to interpret an effectful programming language in a category. For this one needs a (strong) monad \(T\) capturing the desired effects, then we can take the elements of \(TA\) as denotations for programs of type \(A\). The Kleisli category of \(T\) can be viewed as the category of programs, which gives us a way of composing programs (Kleisli composition).
|
||||
|
||||
For this thesis we will restrict ourselves to monads for modeling partiality, the goal of this chapter is to capture what it means to be a partiality monad and look at two common examples.
|
||||
|
||||
\section{Properties of Partiality Monads}
|
||||
We will now look at how to express the following non-controversial properties of a minimal partiality monad categorically:
|
||||
|
||||
|
||||
\begin{enumerate}
|
||||
\item Irrelevance of execution order
|
||||
\item Partiality of programs
|
||||
\item No other effect besides some form of non-termination
|
||||
\end{enumerate}
|
||||
|
||||
The first property of course holds for any commutative monad, the other two are more interesting.
|
||||
|
||||
To ensure that programs are partial, we recall the following notion by Cockett and Lack~\cite{restriction}, that axiomatizes the notion of partiality in a category:
|
||||
|
||||
\newcommand{\tdom}{\text{dom}\;}
|
||||
\begin{definition}[Restriction Structure]
|
||||
A restriction structure on a category \(\C\) is a mapping \(dom : \C(X, Y) \rightarrow \C(X , X)\) with the following properties:
|
||||
\begin{alignat*}{1}
|
||||
f \circ (\tdom f) & = f \\
|
||||
(\tdom f) \circ (\tdom g) & = (\tdom g) \circ (\tdom f) \\
|
||||
\tdom(g \circ (\tdom f)) & = (\tdom g) \circ (\tdom f) \\
|
||||
(\tdom h) \circ f & = f \circ \tdom (h \circ f)
|
||||
\end{alignat*}
|
||||
for any \(X, Y, Z \in \obj{\C}, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z\).
|
||||
\end{definition}
|
||||
|
||||
The morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness of \(f : X \rightarrow Y\). In the category of partial functions this takes the following form:
|
||||
|
||||
\[
|
||||
(\tdom f)(x) = \begin{cases}
|
||||
x & \text{if } f(x) \text{ is defined} \\
|
||||
\text{undefined} & \text{else}
|
||||
\end{cases}
|
||||
\]
|
||||
|
||||
That is, \(\tdom f\) is only defined on values where \(f\) is defined and for those values it behaves like the identity function.
|
||||
|
||||
\begin{definition}[Restriction Category]
|
||||
Every category has a trivial restriction structure by taking \(dom (f : X \rightarrow Y) = id_X\).
|
||||
We call categories with a non-trivial restriction structure \textit{restriction categories}.
|
||||
\end{definition}
|
||||
|
||||
For a suitable defined partiality monad \(T\) the Kleisli category \(\C^T\) should be a restriction category.
|
||||
|
||||
Lastly, we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides some sort of non-termination:
|
||||
|
||||
\begin{definition}[Equational Lifting Monad]\label{def:eqlm}
|
||||
A commutative monad \(T\) is called an \textit{equational lifting monad} if the following diagram commutes:
|
||||
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJUWCJdLFsyLDAsIlRYIFxcdGltZXMgVFgiXSxbMiwyLCJUKFRYIFxcdGltZXMgWCkiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiXFx0YXUiXSxbMCwyLCJUIFxcbGFuZ2xlIFxcZXRhICwgaWQgXFxyYW5nbGUiLDJdXQ==
|
||||
\[
|
||||
\begin{tikzcd}
|
||||
TX && {TX \times TX} \\
|
||||
\\
|
||||
&& {T(TX \times X)}
|
||||
\arrow["\Delta", from=1-1, to=1-3]
|
||||
\arrow["\tau", from=1-3, to=3-3]
|
||||
\arrow["{T \langle \eta , id \rangle}"', from=1-1, to=3-3]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
where \(\Delta_X : X \rightarrow X \times X\) is the diagonal morphism.
|
||||
\end{definition}
|
||||
|
||||
To make the equational lifting property more comprehensible we can alternatively state it using do-notation. The equational lifting property states that the following programs must be equal:
|
||||
|
||||
\begin{multicols}{2}
|
||||
\begin{minted}{haskell}
|
||||
do x <- p
|
||||
return (x , p)
|
||||
\end{minted}
|
||||
|
||||
\begin{minted}{haskell}
|
||||
do x <- p
|
||||
return (x , return x)
|
||||
\end{minted}
|
||||
\end{multicols}
|
||||
|
||||
That is, if some computation \(p : TX\) terminates with the result \(x : X\), then \(p = return\;x\) must hold afterwards. This of course implies that running \(p\) multiple times yields the same result as running \(p\) once.
|
||||
|
||||
\begin{proposition}[\cite{eqlm}]\label{prop:liftingkleisli}
|
||||
If \(T\) is an equational lifting monad the Kleisli category \(\C^T\) is a restriction category.
|
||||
\end{proposition}
|
||||
|
||||
Definition~\ref{def:eqlm} combines all three properties stated at the beginning of the section, so when studying partiality monads in this thesis, we ideally expect them to be equational lifting monads.
|
||||
For the rest of this chapter we will use these definitions to compare two monads that are commonly used to model partiality.
|
||||
|
||||
\section{The Maybe Monad}
|
||||
The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \rightarrow X + 1\) and \(\mu_X = [ id , i_2 ] : (X + 1) + 1 \rightarrow X + 1\).
|
||||
The monad laws follow easily.
|
||||
This is generally known as the maybe monad and can be viewed as the canonical example of an equational lifting monad.
|
||||
|
||||
\begin{theorem} M is an equational lifting monad.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
We define strength as
|
||||
\[ \tau_{X,Y} := X \times (Y + 1) \overset{dstl}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+!}{\longrightarrow} (X \times Y) + 1. \]
|
||||
|
||||
Naturality of \(\tau \) follows by naturality of \(dstl\)
|
||||
|
||||
\begin{alignat*}{1}
|
||||
& (id + !) \circ dstl \circ (id \times (f + id)) \\
|
||||
= \; & (id + !) \circ ((id \times f) + (id \times id)) \circ dstl \\
|
||||
= \; & ((id \times f) + !) \circ dstl \\
|
||||
= \; & ((id \times f) + id) \circ (id + !) \circ dstl.
|
||||
\end{alignat*}
|
||||
|
||||
The other strength laws and commutativity can be proven by using simple properties of distributive categories, we added these proofs to the formalization for completeness.
|
||||
|
||||
We are thus left to check the equational lifting law:
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0bCJdLFsyLDMsImlkK1xcOyEiXSxbMCwzLCJcXGxhbmdsZSBpXzEsaWRcXHJhbmdsZSArIFxcOyEiLDJdXQ==
|
||||
\[
|
||||
\begin{tikzcd}
|
||||
{X+1} &&& {(X+1)\times(X+1)} \\
|
||||
\\
|
||||
&&& {((X+1)\times X) +((X+1)\times 1)} \\
|
||||
\\
|
||||
&&& {((X+1)\times X)+1}
|
||||
\arrow["\Delta", from=1-1, to=1-4]
|
||||
\arrow["dstl", from=1-4, to=3-4]
|
||||
\arrow["{id+\;!}", from=3-4, to=5-4]
|
||||
\arrow["{\langle i_1,id\rangle + \;!}"', from=1-1, to=5-4]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
|
||||
This is easily proven by pre-composing with \(i_1\) and \(i_2\), indeed
|
||||
\begin{alignat*}{1}
|
||||
& (id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle
|
||||
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_1) \circ \langle i_1 , id \rangle
|
||||
\\=\;&(id\;+\;!) \circ i_1 \circ \langle i_1 , id \rangle
|
||||
\\=\;&i_1 \circ \langle i_1 , id \rangle,
|
||||
\end{alignat*}
|
||||
and
|
||||
\begin{alignat*}{1}
|
||||
& (id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle
|
||||
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_2) \circ \langle i_2 , id \rangle
|
||||
\\=\;&(id\;+\;!) \circ i_2 \circ \langle i_2 , id \rangle
|
||||
\\=\;&i_2 \;\circ \; ! \circ \langle i_2 , id \rangle
|
||||
\\=\;&i_2 \;\circ \; !.\tag*{\qedhere}
|
||||
\end{alignat*}
|
||||
\end{proof}
|
||||
|
||||
In the setting of classical mathematics this monad is therefore sufficient for modeling partiality, but in general it will not be useful for modeling non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modeling possibly non-terminating computations another monad has been introduced by Capretta~\cite{delay}.
|
||||
|
||||
\section{The Delay Monad}
|
||||
Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
|
||||
This datatype is usually defined by the two coinductive constructors \(now : X \rightarrow DX\) and \(later : DX \rightarrow DX\), where \(now\) lifts a value inside a computation and \(later\) intuitively delays a computation by one time unit.
|
||||
See \autoref{chp:setoids} for a type theoretical study of this monad.
|
||||
Categorically we obtain the delay monad by the terminal coalgebras \(DX = \nu A. X + A\), which we assume to exist.
|
||||
In this section we will show that these terminal coalgebras indeed yield a monad that is strong and commutative.
|
||||
|
||||
Since \(DX\) is defined as a terminal coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By \autoref{lem:lambek} the coalgebra structure \(out : DX \rightarrow X + DX\) is an isomorphism, whose inverse can be decomposed into the two constructors mentioned before: \(out^{-1} = [ now , later ] : X + DX \rightarrow DX\).
|
||||
|
||||
\begin{lemma}~\label{lem:delay}
|
||||
The following conditions hold:
|
||||
\begin{itemize}
|
||||
\item \(now : X \rightarrow DX\) and \(later : DX \rightarrow DX\) satisfy:
|
||||
\begin{equation*}
|
||||
out \circ now = i_1 \qquad\qquad\qquad out \circ later = i_2 \tag*{(D1)}\label{D1}
|
||||
\end{equation*}
|
||||
\item For any \(f : X \rightarrow DY\) there exists a unique morphism \(f^* : DX \rightarrow DY\) such that the following commutes.
|
||||
\begin{equation*}
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIlggKyBEWCJdLFswLDEsIkRZIl0sWzMsMSwiWSArIERZIl0sWzAsMSwib3V0Il0sWzAsMiwiZl4qIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywib3V0Il0sWzEsMywiWyBvdXQgXFxjaXJjIGYgLCBpXzIgXFxjaXJjIGZeKiBdIl1d
|
||||
\begin{tikzcd}
|
||||
DX &&& {X + DX} \\
|
||||
DY &&& {Y + DY}
|
||||
\arrow["out", from=1-1, to=1-4]
|
||||
\arrow["{f^*}", dashed, from=1-1, to=2-1]
|
||||
\arrow["out", from=2-1, to=2-4]
|
||||
\arrow["{[ out \circ f , i_2 \circ f^* ]}", from=1-4, to=2-4]
|
||||
\end{tikzcd}
|
||||
\tag*{(D2)}\label{D2}
|
||||
\end{equation*}
|
||||
\item There exists a unique morphism \(\tau : X \times DY \rightarrow D(X \times Y)\) such that:
|
||||
\begin{equation*}
|
||||
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFsyLDAsIlggXFx0aW1lcyAoWSArIERZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgKyBEKFggXFx0aW1lcyBZKSJdLFswLDEsIlxcdGF1IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzMsNCwiaWQgK1xcdGF1IiwyXSxbMSw0LCJvdXQiXV0=
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
{X \times DY} \&\& {X \times (Y + DY)} \&\& {X \times Y + X \times DY} \\
|
||||
{D(X \times Y)} \&\&\&\& {X \times Y + D(X \times Y)}
|
||||
\arrow["\tau", dashed, from=1-1, to=2-1]
|
||||
\arrow["{id \times out}", from=1-1, to=1-3]
|
||||
\arrow["dstl", from=1-3, to=1-5]
|
||||
\arrow["{id +\tau}"', from=1-5, to=2-5]
|
||||
\arrow["out", from=2-1, to=2-5]
|
||||
\end{tikzcd}
|
||||
\tag*{(D3)}\label{D3}
|
||||
\end{equation*}
|
||||
\end{itemize}
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
We will make use of the fact that every \(DX\) is a terminal coalgebra:
|
||||
\begin{itemize}
|
||||
\item[\ref{D1}] These follow by definition of \(now\) and \(later\):
|
||||
\begin{alignat*}{3}
|
||||
& out \circ now & & = out \circ out^{-1} \circ i_1 & = i_1
|
||||
\\&out \circ later &&= out \circ out^{-1} \circ i_2 &= i_2
|
||||
\end{alignat*}
|
||||
\item[\ref{D2}] We define \(f^* = \;\coalg{\alpha} \circ i_1\), where \(\coalg{\alpha}\) is the unique coalgebra morphism in this diagram:
|
||||
|
||||
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzcsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNywyLCJZICsgRFkiXSxbMCwxLCJcXGFscGhhIDo9IFsgWyBbIGlfMSAsIGlfMiBcXGNpcmMgaV8yIF0gXFxjaXJjIChvdXQgXFxjaXJjIGYpICwgaV8yIFxcY2lyYyBpXzEgXSBcXGNpcmMgb3V0ICwgKGlkICsgaV8yKSBcXGNpcmMgb3V0IF0iXSxbMiwwLCJpXzEiXSxbMCwzLCJcXGNvYWxne1xcYWxwaGF9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzMsNCwib3V0Il0sWzEsNCwiaWQgKyBcXGNvYWxne1xcYWxwaGF9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
DX \\
|
||||
{DX + DY} \&\&\&\&\&\&\& {Y + (DX + DY)} \\
|
||||
DY \&\&\&\&\&\&\& {Y + DY}
|
||||
\arrow["{\alpha := [ [ [ i_1 , i_2 \circ i_2 ] \circ (out \circ f) , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ]}", from=2-1, to=2-8]
|
||||
\arrow["{i_1}", from=1-1, to=2-1]
|
||||
\arrow["{\coalg{\alpha}}", dashed, from=2-1, to=3-1]
|
||||
\arrow["out", from=3-1, to=3-8]
|
||||
\arrow["{id + \coalg{\alpha}}", dashed, from=2-8, to=3-8]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
|
||||
Note that \(\coalg{\alpha} \circ i_2 = id : (DY, out) \rightarrow (DY, out)\), by uniqueness of the identity morphism and the fact that \(\coalg{\alpha} \circ i_2\) is a coalgebra morphism, since
|
||||
\begin{alignat*}{1}
|
||||
& out \circ \coalg{\alpha} \circ i_2
|
||||
\\=\;&(id+\coalg{\alpha}) \circ \alpha \circ i_2
|
||||
\\=\;&(id + \coalg{\alpha}) \circ (id + i_2) \circ out
|
||||
\\=\;&(id + \coalg{\alpha} \circ i_2) \circ out
|
||||
\end{alignat*}
|
||||
Let us verify that \(f^*\) indeed satisfies the requisite property:
|
||||
\begin{alignat*}{1}
|
||||
& out \circ \coalg{\alpha} \circ i_1
|
||||
\\=\;&(id + \coalg{\alpha}) \circ \alpha \circ i_1
|
||||
\\=\;&(id + \coalg{\alpha}) \circ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out
|
||||
\\=\;&[ [ (id + \coalg{\alpha}) \circ i_1 , (id + \coalg{\alpha}) \circ i_2 \circ i_2 ] \circ out \circ f , (id + \coalg{\alpha}) \circ i_2 \circ i_1 ] \circ out
|
||||
\\=\;&[ [ i_1 , i_2 \circ \coalg{\alpha} \circ i_2 ] \circ out \circ f , i_2 \circ \coalg{\alpha} \circ i_1 ] \circ out
|
||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out.
|
||||
\end{alignat*}
|
||||
|
||||
We are left to check uniqueness of \(f^*\). Let \(g : DX \rightarrow DY\) and \(out \circ g = [ out \circ f , i_2 \circ g ] \circ out\).
|
||||
Note that \([ g , id ] : DX + DY \rightarrow DY\) is a coalgebra morphism, since
|
||||
\begin{alignat*}{1}
|
||||
& out \circ [ g , id ]
|
||||
\\=\;&[ out \circ g , out ]
|
||||
\\=\;&[ [ out \circ f , i_2 \circ g ] \circ out , out]
|
||||
\\=\;&[ [ [ i_1 , i_2 ] \circ out \circ f , i_2 \circ g ] \circ out , (id + id) \circ out ]
|
||||
\\=\;&[ [ [ i_1 , i_2 \circ [g , id] \circ i_2 ] \circ out \circ f , i_2 \circ [g , id] \circ i_1 ] \circ out , (id + [g , id] \circ i_2) \circ out ]
|
||||
\\=\;&[ [ [ (id + [g , id]) \circ i_1 , (id + [g , id]) \circ i_2 \circ i_2 ] \circ out \circ f , (id + [g , id]) \circ i_2 \circ i_1 ] \circ out
|
||||
\\ \;&, (id + [g , id]) \circ (id + i_2) \circ out ]
|
||||
\\=\;&(id + [g , id]) \circ [ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ].
|
||||
\end{alignat*}
|
||||
|
||||
Thus, \([ g , id ] = \coalg{\alpha}\) by uniqueness of \(\coalg{\alpha}\).
|
||||
It follows that indeed \[g = [ g , id ] \circ i_1 =\;\coalg{\alpha} \circ i_1 = f^*.\]
|
||||
\item[\ref{D3}] Take \(\tau := \coalg{dstl \circ (id \times out)} : X \times DY \rightarrow D(X \times Y)\), the requisite property then follows by definition.
|
||||
\qedhere
|
||||
\end{itemize}
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}
|
||||
The following properties of \(\mathbf{D}\) hold:
|
||||
\begin{enumerate}
|
||||
\item \(out \circ Df = (f + Df) \circ out\)
|
||||
\item \(f^* = [ f , {(later \circ f)}^* ] \circ out\)
|
||||
\item \(later \circ f^* = {(later \circ f)}^* = f^* \circ later\)
|
||||
\end{enumerate}
|
||||
\end{lemma}
|
||||
\begin{proof} These identities follow by use of \autoref{lem:delay}:
|
||||
\begin{itemize}
|
||||
\item[1.] Note that definitionally: \(Df = {(now \circ f)}^*\) for any \(f : X \rightarrow TY\). The statement is then simply a consequence of~\ref{D1} and~\ref{D2}:
|
||||
\begin{alignat*}{1}
|
||||
& out \circ Df
|
||||
\\=\;&out \circ {(now \circ f)}^*
|
||||
\\=\;&[ out \circ now \circ f , i_2 \circ {(now \circ f)}^* ] \circ out\tag*{\ref{D2}}
|
||||
\\=\;&(f + Df) \circ out.\tag*{\ref{D1}}
|
||||
\end{alignat*}
|
||||
\item[2.] By uniqueness of \(f^*\) it suffices to show:
|
||||
\begin{alignat*}{1}
|
||||
& out \circ [ f , {(later \circ f)}^* ] \circ out
|
||||
\\=\;&[ out \circ f , out \circ {(later \circ f)}^* ] \circ out
|
||||
\\=\;&[out \circ f , [ out \circ later \circ f , i_2 \circ {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D2}}
|
||||
\\=\;&[out \circ f , i_2 \circ [ f , {(later \circ f)}^* ] \circ out ] \circ out.\tag*{\ref{D1}}
|
||||
\end{alignat*}
|
||||
\item[3.]
|
||||
This equational chain follows by monicity of \(out\):
|
||||
\begin{alignat*}{1}
|
||||
& out \circ {(later \circ f)}^*
|
||||
\\=\;&[ out \circ later \circ f , i_2 \circ {(later \circ f)}^*] \circ out\tag*{\ref{D2}}
|
||||
\\=\;&i_2 \circ [ f , {(later \circ f)}^*] \circ out\tag*{\ref{D1}}
|
||||
\\=\;&i_2 \circ f^*
|
||||
\\=\;&out \circ later \circ f^*\tag*{\ref{D1}}
|
||||
\\=\;&i_2 \circ f^*\tag*{\ref{D1}}
|
||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_2
|
||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ later\tag*{\ref{D1}}
|
||||
\\=\;&out \circ f^* \circ later. \tag*{\ref{D2}}
|
||||
\end{alignat*}
|
||||
\end{itemize}
|
||||
Thus, the postulated properties have been proven.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}
|
||||
\(\mathbf{D} := (D, now, {(-)}^*)\) is a Kleisli triple.
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
We will now use the properties proven in \autoref{lem:delay} to prove the Kleisli triple laws:
|
||||
\begin{itemize}
|
||||
\item[\ref{K1}]
|
||||
By uniqueness of \(now^*\) it suffices to show that \(out \circ id = [ out \circ now , i_2 \circ id ] \circ out\) which instantly follows by~\ref{D1}.
|
||||
\item[\ref{K2}] Let \(f : X \rightarrow DY\). We proceed by monicity of \(out\):
|
||||
\begin{alignat*}{1}
|
||||
& out \circ f^* \circ now
|
||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ now\tag*{\ref{D2}}
|
||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_1\tag*{\ref{D1}}
|
||||
\\=\;&out \circ f.
|
||||
\end{alignat*}
|
||||
\item[\ref{K3}] Let \(f : Y \rightarrow Z, g : X \rightarrow Z\) to show \(f^* \circ g^* = {(f^* \circ g)}^*\) by uniqueness of \({(f^* \circ g)}^*\) it suffices to show:
|
||||
\begin{alignat*}{1}
|
||||
& out \circ f^* \circ g^*
|
||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ g^*\tag*{\ref{D2}}
|
||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ [ out \circ g , i_2 \circ g^* ] \circ out\tag*{\ref{D2}}
|
||||
\\=\;&[ [ out \circ f , i_2 \circ f^* ] \circ out \circ g , i_2 \circ f^* \circ g^* ] \circ out
|
||||
\\=\;&[ out \circ f^* \circ g , i_2 \circ f^* \circ g^* ] \circ out.\tag*{\ref{D2}}
|
||||
\end{alignat*}
|
||||
\end{itemize}
|
||||
This concludes the proof.
|
||||
\end{proof}
|
||||
|
||||
Terminality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C}}\) yields the following proof principle.
|
||||
\begin{remark}[Proof by coinduction]~\label{rem:coinduction}
|
||||
Given two morphisms \(f, g : X \rightarrow DY\). To show that \(f = g\) it suffices to show that there exists a coalgebra structure \(\alpha : X \rightarrow Y + X\) such that the following diagrams commute:
|
||||
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCJdXQ==
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \&\& {Y + X} \&\& X \&\& {Y + X} \\
|
||||
DY \&\& {Y + DY} \&\& DY \&\& {Y + DY}
|
||||
\arrow["out", from=2-1, to=2-3]
|
||||
\arrow["\alpha", from=1-1, to=1-3]
|
||||
\arrow["f", from=1-1, to=2-1]
|
||||
\arrow["{id + f}", from=1-3, to=2-3]
|
||||
\arrow["\alpha", from=1-5, to=1-7]
|
||||
\arrow["g", from=1-5, to=2-5]
|
||||
\arrow["{id + g}", from=1-7, to=2-7]
|
||||
\arrow["out", from=2-5, to=2-7]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
Uniqueness of the coalgebra morphism \(\coalg{\alpha} : (X, \alpha) \rightarrow (DY, out)\) then results in \(f = g\).
|
||||
\end{remark}
|
||||
|
||||
\begin{lemma}
|
||||
\(\mathbf{D}\) is a strong monad.
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
Most of the following proofs are done via coinduction (Remark~\ref{rem:coinduction}). We will only give the requisite coalgebra structure. The proofs that the diagrams commute can be looked up in the Agda formalization.
|
||||
|
||||
First we need to show naturality of \(\tau \), i.e.\ we need to show that
|
||||
\[\tau \circ (f \times {(now \circ g)}^*) = {(now \circ (f \times g))}^* \circ \tau \]
|
||||
The coalgebra for coinduction is:
|
||||
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwyLCJEKEFcXHRpbWVzIEIpIl0sWzQsMiwiQVxcdGltZXMgQiArIEQoQSBcXHRpbWVzIEIpIl0sWzEsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzIsMCwiWCBcXHRpbWVzIFkgKyBYIFxcdGltZXMgRFkiXSxbNCwwLCJBIFxcdGltZXMgQiArIFggXFx0aW1lcyBEWSJdLFsxLDIsIm91dCJdLFswLDMsImlkIFxcdGltZXMgb3V0Il0sWzMsNCwiZHN0bCJdLFswLDEsIlxcY29hbGd7LX0iLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNCw1LCJmIFxcdGltZXMgZyArIGlkIl0sWzUsMiwiaWQgKyBcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
{X \times DY} \& {X \times (Y + DY)} \& {X \times Y + X \times DY} \&\& {A \times B + X \times DY} \\
|
||||
\\
|
||||
{D(A\times B)} \&\&\&\& {A\times B + D(A \times B)}
|
||||
\arrow["out", from=3-1, to=3-5]
|
||||
\arrow["{id \times out}", from=1-1, to=1-2]
|
||||
\arrow["dstl", from=1-2, to=1-3]
|
||||
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1]
|
||||
\arrow["{f \times g + id}", from=1-3, to=1-5]
|
||||
\arrow["{id + \coalg{\text{-}}}", dashed, from=1-5, to=3-5]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
We write \(\coalg{\text{-}}\) to abbreviate the used coalgebra, i.e.\ in the previous diagram
|
||||
\[\coalg{\text{-}} = \coalg{(f\times g + id) \circ dstl \circ (id \times out)}.\]
|
||||
|
||||
Next we check the strength laws:
|
||||
\begin{itemize}
|
||||
\item[\ref{S1}] To show that \({(now \circ \pi_2)}^* \circ \tau = \pi_2\) we do coinduction using the following coalgebra:
|
||||
% https://q.uiver.app/#q=WzAsNixbMCwwLCIxIFxcdGltZXMgRFgiXSxbMCwxLCJEWCJdLFszLDAsIlggKyAxIFxcdGltZXMgRFgiXSxbMywxLCJYICsgRFgiXSxbMSwwLCIxIFxcdGltZXMgWCArIERYIl0sWzIsMCwiMSBcXHRpbWVzIFggKyAxIFxcdGltZXMgRFgiXSxbMSwzLCJvdXQiXSxbMCwxLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywiaWQgKyBcXGNvYWxney19Il0sWzAsNCwiaWQgXFx0aW1lcyBvdXQiXSxbNCw1LCJkc3RsIl0sWzUsMiwiXFxwaV8yICsgaWQiXV0=
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
{1 \times DX} \& {1 \times X + DX} \& {1 \times X + 1 \times DX} \& {X + 1 \times DX} \\
|
||||
DX \&\&\& {X + DX}
|
||||
\arrow["out", from=2-1, to=2-4]
|
||||
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=2-1]
|
||||
\arrow["{id + \coalg{\text{-}}}", from=1-4, to=2-4]
|
||||
\arrow["{id \times out}", from=1-1, to=1-2]
|
||||
\arrow["dstl", from=1-2, to=1-3]
|
||||
\arrow["{\pi_2 + id}", from=1-3, to=1-4]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\item[\ref{S2}] We don't need coinduction to show \(\tau \circ (id \times now) = now\), but we will first need to establish
|
||||
\begin{equation*}
|
||||
\tau \circ (id \times out^{-1}) = out^{-1} \circ (id + \tau) \circ dstl, \tag*{(\(\ast \))}\label{helper}
|
||||
\end{equation*}
|
||||
which is a direct consequence of~\ref{D3}.
|
||||
With this we are done by
|
||||
\begin{alignat*}{1}
|
||||
& \tau \circ (id \times now) \\
|
||||
=\; & \tau \circ (id \times out^{-1}) \circ (id \times i_1) \\
|
||||
=\; & out^{-1} \circ (id + \tau) \circ dstl \circ (id \times i_1)\tag*{\ref*{helper}} \\
|
||||
=\; & now.
|
||||
\end{alignat*}
|
||||
\item[\ref{S3}] We need to check \(\tau^* \circ \tau = \tau \circ (id \times id^*)\), the coalgebra for coinduction is:
|
||||
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRERZIl0sWzAsMiwiRChYXFx0aW1lcyBZKSJdLFsxLDAsIlggXFx0aW1lcyAoRFkgKyBERFkpIl0sWzIsMCwiWCBcXHRpbWVzIERZICsgWCBcXHRpbWVzIEREWSJdLFsyLDIsIlggXFx0aW1lcyBZICsgRChYIFxcdGltZXMgWSkiXSxbMiwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBERFkiXSxbMCwxLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzEsNCwib3V0Il0sWzUsNCwiaWQgKyBcXGNvYWxney19IiwyXSxbMyw1LCJbIChpZCArIChpZCBcXHRpbWVzIG5vdykpIFxcY2lyYyBkc3RsIFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpICwgaV8yIF0iLDJdXQ==
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
{X \times DDY} \& {X \times (DY + DDY)} \& {X \times DY + X \times DDY} \\
|
||||
\&\& {X \times Y + X \times DDY} \\
|
||||
{D(X\times Y)} \&\& {X \times Y + D(X \times Y)}
|
||||
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1]
|
||||
\arrow["{id \times out}", from=1-1, to=1-2]
|
||||
\arrow["dstl", from=1-2, to=1-3]
|
||||
\arrow["out", from=3-1, to=3-3]
|
||||
\arrow["{id + \coalg{\text{-}}}"', from=2-3, to=3-3]
|
||||
\arrow["{[ (id + (id \times now)) \circ dstl \circ (id \times out) , i_2 ]}"', from=1-3, to=2-3]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\item[\ref{S4}] To show \(D\alpha \circ \tau = \tau \circ (id \times \tau) \circ \alpha \) by coinduction we take the coalgebra:
|
||||
% https://q.uiver.app/#q=WzAsNixbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgRFoiXSxbMCwyLCJEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIFogKyBEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwxLCJYIFxcdGltZXMgWSAgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzEsMCwiKFggXFx0aW1lcyBZKSBcXHRpbWVzIChaKyBEWikiXSxbMiwwLCIoWFxcdGltZXMgWSkgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzAsMSwiXFxjb2FsZ3stfSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsIm91dCJdLFszLDIsImlkICtcXGNvYWxney19IiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDUsImRzdGwiXSxbNSwzLCJcXGxhbmdsZSBcXHBpXzEgXFxjaXJjIFxccGlfMSAsIFxcbGFuZ2xlIFxccGlfMiBcXGNpcmMgXFxwaV8xICwgXFxwaV8yIFxccmFuZ2xlIFxccmFuZ2xlICsgaWQiLDJdXQ==
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
{(X \times Y) \times DZ} \& {(X \times Y) \times (Z+ DZ)} \& {(X\times Y) \times Z + (X \times Y) \times DZ} \\
|
||||
\&\& {X \times Y \times Z + (X \times Y) \times DZ} \\
|
||||
{D(X \times Y \times Z)} \&\& {X \times Y \times Z + D(X \times Y \times Z)}
|
||||
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1]
|
||||
\arrow["out", from=3-1, to=3-3]
|
||||
\arrow["{id +\coalg{\text{-}}}"', from=2-3, to=3-3]
|
||||
\arrow["{id \times out}", from=1-1, to=1-2]
|
||||
\arrow["dstl", from=1-2, to=1-3]
|
||||
\arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-3, to=2-3]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\end{itemize}
|
||||
Thus, it has been shown that \(\mathbf{D}\) is a strong monad.
|
||||
\end{proof}
|
||||
|
||||
To prove that \(\mathbf{D}\) is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} or \textit{Parametric Corecursion}~\cite{param-corec}. In our setting this takes the following form.
|
||||
|
||||
\begin{definition}
|
||||
We call a morphism \(g : X \rightarrow D (Y + X)\) \textit{guarded} if there exists a morphism \(h : X \rightarrow Y + D(Y+X)\) such that the following diagram commutes:
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzMsMCwiRCAoWSArWCkiXSxbMywxLCIoWSArIFgpICsgRChZICsgWCkiXSxbMCwxLCJZICsgRChZK1gpIl0sWzAsMSwiZyJdLFsxLDIsIm91dCJdLFszLDIsImlfMSArIGlkIiwyXSxbMCwzLCJoIiwyXV0=
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \&\&\& {D (Y +X)} \\
|
||||
{Y + D(Y+X)} \&\&\& {(Y + X) + D(Y + X)}
|
||||
\arrow["g", from=1-1, to=1-4]
|
||||
\arrow["out", from=1-4, to=2-4]
|
||||
\arrow["{i_1 + id}"', from=2-1, to=2-4]
|
||||
\arrow["h"', from=1-1, to=2-1]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
\end{definition}
|
||||
|
||||
\begin{corollary}[Solution Theorem]\label{cor:solution}
|
||||
Let \(g : X \rightarrow D(Y + X)\) be guarded.\ \textit{Solutions} of g are unique, i.e.\ given two morphisms \(f, i : X \rightarrow DY\) then
|
||||
\(f = {[ now , f ]}^* \circ g\) and \(i = {[ now , i ]}^* \circ g\) already implies \(f = i\).
|
||||
\end{corollary}
|
||||
\begin{proof}
|
||||
Let \(g : X \rightarrow D(Y + X)\) be guarded by \(h : X \rightarrow Y + D(Y+X)\) and \(f, i : X \rightarrow DY\) be solutions of g.
|
||||
It suffices to show \({[ now , f ]}^* = {[ now , i ]}^*\), because then follows that
|
||||
\[f = {[ now , f ]}^* \circ g = {[ now , i ]}^* \circ g = i.\]
|
||||
This is proven by coinduction using
|
||||
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcY29hbGd7LX0iXSxbMiwwLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
|
||||
\[
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
{D(Y + X)} \& {(Y + X) + D(Y+X)} \&\& {Y + D(Y+X)} \\
|
||||
DY \&\&\& {Y + DY}
|
||||
\arrow["out", from=2-1, to=2-4]
|
||||
\arrow["out", from=1-1, to=1-2]
|
||||
\arrow["{[ [ i_1 , h ] , i_2 ]}", from=1-2, to=1-4]
|
||||
\arrow["{id + \coalg{\text{-}}}", from=1-4, to=2-4]
|
||||
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=2-1]
|
||||
\end{tikzcd}
|
||||
\]
|
||||
which concludes the proof.
|
||||
\end{proof}
|
||||
|
||||
Let us record some facts that we will use to prove commutativity of \(\mathbf{D}\):
|
||||
|
||||
\begin{corollary}
|
||||
These properties of \(\tau \) and \(\sigma \) hold:
|
||||
\begin{alignat*}{2}
|
||||
& out \circ \tau & & = (id + \tau) \circ dstl \circ (id \times out)\tag*{(\(\tau_1\))}\label{tau1}
|
||||
\\&out \circ \sigma &&= (id + \sigma) \circ dstr \circ (out \times id)\tag*{(\(\sigma_1\))}\label{sigma1}
|
||||
\\&\tau \circ (id \times out^{-1}) &&= out^{-1} \circ (id + \tau) \circ dstl\tag*{(\(\tau_2\))}\label{tau2}
|
||||
\\& \sigma \circ (out^{-1} \times id) &&= out^{-1} \circ (id + \sigma) \circ dstr\tag*{(\(\sigma_2\))}\label{sigma2}
|
||||
\end{alignat*}
|
||||
\end{corollary}
|
||||
|
||||
\begin{proof}
|
||||
\begin{itemize}
|
||||
\item[\ref{tau1}] This is just~\ref{D3} restated.
|
||||
\item[\ref{sigma1}] Indeed, by use of~\ref{tau1}
|
||||
\begin{alignat*}{1}
|
||||
& out \circ \sigma
|
||||
\\=\;&out \circ Dswap \circ \tau \circ swap
|
||||
\\=\;&(swap + Dswap) \circ out \circ \tau \circ swap
|
||||
\\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ (id \times out) \circ swap \tag*{\ref{tau1}}
|
||||
\\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ swap \circ (out \times id)
|
||||
\\=\;&(swap + Dswap) \circ (id + \tau) \circ (swap + swap) \circ dstr \circ (out \times id)
|
||||
\\=\;&(id + \sigma) \circ dstr \circ (out \times id).
|
||||
\end{alignat*}
|
||||
\item[\ref{tau2}] By monicity of \(out\):
|
||||
\begin{alignat*}{1}
|
||||
& out \circ \tau \circ (id \times out^{-1})
|
||||
\\=\;&(id + \tau) \circ dstl \circ (id \times out) \circ (id \times out^{-1})\tag*{\ref{tau1}}
|
||||
\\=\;&(id + \tau) \circ dstl.
|
||||
\end{alignat*}
|
||||
\item[\ref{sigma2}] Again, by monicity of \(out\):
|
||||
\begin{alignat*}{1}
|
||||
& out \circ \sigma \circ (out^{-1} \times id)
|
||||
\\=\;&(id + \sigma) \circ dstr \circ (out \times id) \circ (out^{-1} \times id)\tag*{\ref{sigma1}}
|
||||
\\=\;&(id + \sigma) \circ dstr.\tag*{\qedhere}
|
||||
\end{alignat*}
|
||||
\end{itemize}
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}
|
||||
\(\mathbf{D}\) is commutative.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
Using \autoref{cor:solution} it suffices to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of some guarded morphism \(g\).
|
||||
|
||||
Let \(w := (dstr + dstr) \circ dstl \circ (out \times out)\) and take
|
||||
\[g := out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w.\]
|
||||
Note that \(g\) is trivially guarded by \([ id + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\).
|
||||
It thus suffices to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of \(g\). Consider
|
||||
|
||||
\[\tau^* \circ \sigma = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \tau^* \circ \sigma ] ] \circ w = {[ now , \tau^* \circ \sigma]}^* \circ g, \]
|
||||
and
|
||||
\[\sigma^* \circ \tau = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \sigma^* \circ \tau ] ] \circ w = {[ now , \sigma^* \circ \tau]}^* \circ g. \]
|
||||
|
||||
The last step in both equations can be proven generally for any \(f : DX \times DY \rightarrow D(X \times Y)\) using monicity of \(out\):
|
||||
\begin{alignat*}{1}
|
||||
& out \circ {[ now , f ]}^* \circ out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w
|
||||
\\=\; & [ out \circ [ now , f ] , i_2 \circ {[ now , f ]}^* ] \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D2}}
|
||||
\\=\; & [ id + \sigma , i_2 \circ {[ now , f]}^* \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D1}}
|
||||
\\=\; & [ id + \sigma , i_2 \circ [ \tau , {[ now , f]}^* \circ later \circ now \circ i_2 ] ] \circ w
|
||||
\\=\; & [ id + \sigma , i_2 \circ [ \tau , {[ later \circ now , later \circ f]}^* \circ now \circ i_2 ] ] \circ w
|
||||
\\=\; & [ id + \sigma , i_2 \circ [ \tau , later \circ f ] ] \circ w.
|
||||
\end{alignat*}
|
||||
|
||||
Let us now check the first step in the equation for \(\sigma^* \circ \tau \), the same step for \(\tau^* \circ \sigma \) is then symmetric. Again, we proceed by monicity of \(out\), which yields
|
||||
\begin{alignat*}{1}
|
||||
& out \circ \sigma^* \circ \tau
|
||||
\\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ out \circ \tau\tag*{\ref{D2}}
|
||||
\\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ (id + \tau) \circ dstl \circ (id \times out)\tag*{\ref{D3}}
|
||||
\\=\;&[ (id + \sigma) \circ dstr \circ (out \times id) , i_2 \circ \sigma^* \circ \tau ] \circ dstl \circ (id \times out)\tag*{\ref{sigma1}}
|
||||
\\=\;&[ (id + \sigma) \circ dstr \circ (out \times id) , i_2 \circ \sigma^* \circ \tau ] \circ ((out^{-1} \times id) + (out^{-1} \times id)) \circ dstl \circ (out \times out)
|
||||
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ \sigma^* \circ \tau \circ (out^{-1} \times id)] \circ dstl \circ (out \times out)
|
||||
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ \sigma^* \circ D(out^{-1} \times id) \circ \tau] \circ dstl \circ (out \times out)
|
||||
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ {(\sigma \times (out^{-1} \times id))}^* \circ \tau] \circ dstl \circ (out \times out)
|
||||
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ {(out^{-1} \circ (id + \sigma) \circ dstr)}^* \circ \tau] \circ dstl \circ (out \times out)\tag*{\ref{sigma2}}
|
||||
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ {(out^{-1} \circ (id + \sigma))}^* \circ Ddstr \circ \tau] \circ dstl \circ (out \times out)
|
||||
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ {(out^{-1} \circ (id + \sigma))}^* \circ [D i_1 \circ \tau , D i_2 \circ \tau] \circ dstr] \circ dstl \circ (out \times out)\tag*{\ref{Dcomm-helper}}
|
||||
\\=\;&[ (id + \sigma), i_2 \circ {(out^{-1} \circ (id + \sigma))}^* \circ [D i_1 \circ \tau , D i_2 \circ \tau]] \circ (dstr + dstr) \circ dstl \circ (out \times out)
|
||||
\\=\;&[ (id + \sigma), i_2 \circ [{(out^{-1} \circ i_1)}^* \circ \tau , {(out^{-1} \circ i_2 \circ \sigma)}^* \circ \tau]] \circ w
|
||||
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , {(later \circ \sigma)}^* \circ \tau]] \circ w \tag*{\ref{K1}}
|
||||
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , later \circ \sigma^* \circ \tau]] \circ w,
|
||||
\end{alignat*}
|
||||
where
|
||||
\[Ddstr \circ \tau = [ Di_1 \circ \tau , Di_2 \circ \tau ] \circ dstr \tag*{(*)}\label{Dcomm-helper}\]
|
||||
indeed follows by epicness of \(dstr^{-1}\):
|
||||
\begin{alignat*}{1}
|
||||
& Ddstr \circ \tau \circ dstr^{-1}
|
||||
\\=\;&[ Ddstr \circ \tau \circ (i_1 \times id) , Ddstr \circ \tau \circ (i_2 \times id) ]
|
||||
\\=\;&[ Ddstr \circ D(i_1 \times id) \circ \tau , Ddstr \circ D(i_2 \times id) \circ \tau ]
|
||||
\\=\;&[ Di_1 \circ \tau , Di_2 \circ \tau ].\tag*{\qedhere}
|
||||
\end{alignat*}
|
||||
\end{proof}
|
||||
|
||||
We have now seen that \(\mathbf{D}\) is strong and commutative, however it is not an equational lifting monad, since besides modeling non-termination, the delay monad also counts the execution time of a computation.
|
||||
This is a result of the too intensional notion of equality that this monad comes with.
|
||||
|
||||
In \autoref{chp:setoids} we will see a way to remedy this: taking the quotient of the delay monad where execution time is ignored.
|
||||
This will then yield an equational lifting monad on the category of setoids.
|
||||
However, in a general setting it is generally believed to be impossible to define a monad structure on this quotient.
|
||||
Chapman et al.~\cite{quotienting} have identified the axiom of countable choice (which crucially holds in the category of setoids) as a sufficient requirement for defining a monad structure on the quotient of \(\mathbf{D}\).
|
||||
1040
src/05_iteration.tex
Normal file
1040
src/05_iteration.tex
Normal file
File diff suppressed because it is too large
Load diff
521
src/06_setoids.tex
Normal file
521
src/06_setoids.tex
Normal file
|
|
@ -0,0 +1,521 @@
|
|||
\chapter{A Case Study on Setoids}\label{chp:setoids}
|
||||
|
||||
In \autoref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality, but it also considers computation time in its built-in notion of equality.
|
||||
One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified.
|
||||
In this chapter we will use the quotients-as-setoid approach, i.e.\ we will work in the category of setoids and show that the quotiented delay monad is an instance of the previously defined monad \(\mathbf{K}\) in this category.
|
||||
|
||||
\section{Setoids in Type Theory}
|
||||
We will now introduce the category that the rest of the chapter will take place in. Let us start with some basic definitions.
|
||||
|
||||
\begin{definition}[Setoid]
|
||||
A setoid is a tuple \((A, \overset{A}{=})\) where \(A\) (usually called the \textit{carrier}) is a type and \(\overset{A}{=}\) is an equivalence relation on the inhabitants of \(A\).
|
||||
\end{definition}
|
||||
|
||||
For brevity, we will not use the tuple notation most of the time, instead we will just say `Let \(A\) be a setoid' and implicitly call the equivalence relation \(\overset{A}{=}\).
|
||||
|
||||
\begin{definition}[Setoid Morphism]
|
||||
A morphism between setoids \(A\) and \(B\) constitutes a function \(f : A \rightarrow B\) between the carriers, such that \(f\) respects the equivalences, i.e.\ for any \(x,y : A\), \(x \overset{A}{=} y\) implies \(f\;x \overset{B}{=} f\;y\). We will denote setoid morphisms as \(A ⇝ B\).
|
||||
\end{definition}
|
||||
Let us now consider the function space setoid, which is of special interest, since it carries a notion of equality between functions.
|
||||
\begin{definition}[Function Space Setoid]
|
||||
Given two setoids \(A\) and \(B\), the function space setoid on these setoids is defined as \((A ⇝ B, \doteq)\) or just \(A ⇝ B\), where \(\doteq\) is the point wise equality on setoid morphisms.
|
||||
\end{definition}
|
||||
|
||||
Setoids together with setoid morphisms form a category that we will call \(\setoids\).
|
||||
Properties of \(\setoids\) have already been examined in~\cite{setoids}, however we will reiterate some of these properties now to introduce notation that will be used for the rest of the chapter.
|
||||
|
||||
\begin{proposition}
|
||||
\(\setoids\) is a distributive category.
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
To show that \(\setoids\) is (co)Cartesian we will give the respective data types and unique functions. % chktex 36
|
||||
For brevity, we will omit the proofs that the functions respect the corresponding equivalences, these are however included in the Agda standard library~\cite{agda-stdlib}.
|
||||
|
||||
\begin{itemize}
|
||||
\item \textbf{Products}:
|
||||
\begin{minted}{agda}
|
||||
record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
||||
constructor _,_
|
||||
field
|
||||
fst : A
|
||||
snd : B
|
||||
|
||||
<_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (A → B) → (A → C) → A → (B × C)
|
||||
< f , g > x = (f x , g x)
|
||||
\end{minted}
|
||||
The product setoid is denoted \((A \times B, \overset{\times}{=})\) or just \(A \times B\). Equality of products is defined in the canonical way.
|
||||
\item \textbf{Terminal Object}:
|
||||
\begin{minted}{agda}
|
||||
record ⊤ {l} : Set l where
|
||||
constructor tt
|
||||
|
||||
! : ∀ {l} {X : Set l} → X → ⊤ {l}
|
||||
! _ = tt
|
||||
\end{minted}
|
||||
The terminal setoid is thus \((\top, \overset{\top}{=})\), where \(\top \overset{\top}{=} \top\).
|
||||
\item \textbf{Coproducts}:
|
||||
\begin{minted}{agda}
|
||||
data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
||||
i₁ : A → A + B
|
||||
i₂ : B → A + B
|
||||
|
||||
[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (A → C) → (B → C) → (A + B) → C
|
||||
[ f , g ] (i₁ x) = f x
|
||||
[ f , g ] (i₂ x) = g x
|
||||
\end{minted}
|
||||
Similarly to products, the coproduct setoid is denoted \((A + B, \overset{+}{=})\) or just \(A + B\), where equality of coproducts is defined in the canonical way.
|
||||
\item \textbf{Initial Object}:
|
||||
\begin{minted}{agda}
|
||||
data ⊥ {l} : Set l where
|
||||
|
||||
¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
|
||||
¡ ()
|
||||
\end{minted}
|
||||
The initial setoid is then \((\bot, \emptyset)\), where the equivalence is the empty relation.
|
||||
\end{itemize}
|
||||
|
||||
Lastly we need to show that the canonical distributivity function is an iso. Recall that the canonical distributivity morphism is defined as \(dstl^{-1} = [ id \times i_1 , id \times i_2 ] : A \times B + A \times C \rightarrow A \times (B + C)\).
|
||||
This is equivalent to the following definition that uses pattern matching.
|
||||
\begin{minted}{agda}
|
||||
distributeˡ⁻¹ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (A × B) + (A × C) → A × (B + C)
|
||||
distributeˡ⁻¹ (i₁ (x , y)) = (x , i₁ y)
|
||||
distributeˡ⁻¹ (i₂ (x , y)) = (x , i₂ y)
|
||||
\end{minted}
|
||||
The inverse can then be defined similarly:
|
||||
\begin{minted}{agda}
|
||||
distributeˡ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ A × (B + C) → (A × B) + (A × C)
|
||||
distributeˡ (x , i₁ y) = i₁ (x , y)
|
||||
distributeˡ (x , i₂ y) = i₂ (x , y)
|
||||
\end{minted}
|
||||
Note that these functions are inverse by definition, and it follows quickly that they are setoid morphisms.
|
||||
\end{proof}
|
||||
|
||||
\begin{proposition}\label{prop:setoids-ccc}
|
||||
\(\setoids\) is Cartesian closed.
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
Let \(A\) and \(B\) be two setoids. The function space setoid \(A ⇝ B\) is an exponential object of \(A\) and \(B\), together with the functions \(curry\) and \(eval\) defined in the following listing.
|
||||
\begin{minted}{agda}
|
||||
curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (C × A → B) → C → A → B
|
||||
curry f x y = f (x , y)
|
||||
|
||||
eval : ∀ {a b} {A : Set a} {B : Set b} → ((A → B) × A) → B
|
||||
eval (f , x) = f x
|
||||
\end{minted}
|
||||
The universal property of exponential objects follows instantly.
|
||||
\end{proof}
|
||||
|
||||
\section{Quotienting the Delay Monad}
|
||||
In this section we will introduce data types only using inference rules. For that we adopt the convention that coinductive types are introduced by doubled lines while inductive types are introduced with a single line.
|
||||
|
||||
Now, recall from previous chapters that Capretta's delay monad~\cite{delay} is a coinductive type defined by the two constructors:
|
||||
\[
|
||||
\mprset{fraction={===}}\inferrule*{x : A}{now\; x : D\;A} \qquad
|
||||
\inferrule*{x : D\;A}{later \;x : D\;A} \qquad
|
||||
\]
|
||||
Furthermore, let us recall two different notions of bisimilarity between inhabitants of the delay type that have been studied previously in~\cite{quotienting}. Afterwards, we will reiterate some facts that have been proven in~\cite{quotienting} to then finally prove that the quotiented delay type extends to an instance of the monad \(\mathbf{K}\) that has been introduced in \autoref{chp:iteration}.
|
||||
|
||||
Let \(A\) be a setoid. Lifting the equivalence \(\overset{A}{=}\) to \(D\;A\) yields another equivalence called \emph{strong bisimilarity}. This equivalence is defined by the rules
|
||||
|
||||
\[
|
||||
\mprset{fraction={===}}\inferrule*{x \overset{A}{=} y}{x \sim y} \qquad
|
||||
\inferrule*{x \sim y}{later\; x \sim later\; y} \qquad
|
||||
\]
|
||||
|
||||
\begin{proposition}[\cite{quotienting}]
|
||||
\((D\;A, \sim)\) is a setoid and admits a monad structure.
|
||||
\end{proposition}
|
||||
|
||||
Computations in \((D\;A, \sim)\) are only identified if they evaluate to the same result in the same number of steps. In many contexts this behavior is too intensional. Instead, we will now consider the quotient of this setoid, where all computations that evaluate to the same result are identified. Let us first define a relation that states that two computations evaluate to the same result
|
||||
|
||||
\[
|
||||
\inferrule*{x \overset{A}{=} y}{now\;x \downarrow y} \qquad
|
||||
\inferrule*{x \downarrow c}{later\;x \downarrow c }.
|
||||
\]
|
||||
|
||||
Now, we call two computations \(p\) and \(q\) \emph{weakly bisimilar} or \(p \approx q\) if they evaluate to the same result, or don't evaluate at all, which is specified by the rules
|
||||
\[
|
||||
\mprset{fraction={===}}\inferrule*{a \overset{A}{=} b \\ x \downarrow a \\ y \downarrow b}{x \approx y} \qquad
|
||||
\inferrule*{x \approx y}{later \;x \approx later \;y} \qquad
|
||||
\]
|
||||
|
||||
\begin{proposition}[\cite{delay}]
|
||||
\((D\;A, \approx)\) is a setoid and admits a monad structure.
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
The monad unit is the constructor \(now : A \rightarrow D\;A\) and the multiplication \(\mu : D\;D\;A \rightarrow D\;A\) can be defined as follows:
|
||||
|
||||
\[\mu\;x = \begin{cases}
|
||||
z & \text{if } x = now\;z \\
|
||||
later(\mu\;z) & \text{if } x = later\;z
|
||||
\end{cases}\]
|
||||
|
||||
Given a function \(f : A \rightarrow B\), the lifted function \(Df : D\;A \rightarrow D\;B\) is defined as
|
||||
\[Df\;x = \begin{cases}
|
||||
now(f\;z) & \text{if } x = now\;z \\
|
||||
later(Df\;z) & \text{if } x = later\;z
|
||||
\end{cases}\]
|
||||
|
||||
It has been shown in~\cite{delay} that this indeed extends to a monad.
|
||||
\end{proof}
|
||||
|
||||
For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\) and \(\dbtilde{D}\;A = (D_A, \approx)\).
|
||||
|
||||
\begin{lemma}\label{lem:Delgot}
|
||||
Every \(\dbtilde{D}\;A\) can be equipped with an Elgot algebra structure.
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
We need to show that for every setoid \(A\) the resulting setoid \(\dbtilde{D}\;A\) extends to an Elgot algebra.
|
||||
|
||||
Let \(X\) be a setoid and \(f : X ⇝ \dbtilde{D}\;A + X\) be a setoid morphism, we define \(f^\sharp : X ⇝ \dbtilde{D}\;A\) point wise:
|
||||
\[
|
||||
f^\sharp\;x :=
|
||||
\begin{cases}
|
||||
a & \text{if } f\;x = i_1 (a) \\
|
||||
later\;(f^{\sharp}\;a) & \text{if } f\;x = i_2 (a)
|
||||
\end{cases}
|
||||
\]
|
||||
|
||||
Let us first verify that \(f^\sharp\) is indeed a setoid morphism, i.e.\ given \(x, y : X\) with \(x \overset{X}{=} y\), we need to show that \(f^\sharp\;x \approx f^\sharp\;y\). Since \(f\) is a setoid morphism we know that \(f\;x \overset{+}{=} f\;y\), which already implies that \(f^\sharp\;x \approx f^\sharp\;y\) by the definition of \(f^\sharp\). Note that by the same argument we can define an iteration operator that respects strong bisimilarity, let us call it \(f^{\tilde{\sharp}}\) as we will later need to distinguish between \(f^\sharp\) and \(f^{\tilde{\sharp}}\).
|
||||
|
||||
Next, we check the iteration laws:
|
||||
|
||||
\begin{itemize}
|
||||
\item \ref{law:fixpoint}: We need to show that \(f^\sharp \;x \approx [ id , f^\sharp ](f\;x)\) for any \(x : X\). Let us proceed by case distinction: % chktex 2
|
||||
\begin{mycase}
|
||||
\case{} \(f\;x = i_1\;a\)
|
||||
\[ f^\sharp\;x \approx a \approx [ id , f^\sharp ] (i_1\;a) \approx [ id , f^\sharp ] (f\;x) \]
|
||||
\case{} \(f\;x = i_2\;a\)
|
||||
\[ f^\sharp\;x \approx later (f^{\sharp}\;a) \approx f^\sharp\;a \approx [ id , f^\sharp ] (i_2 \;a) \approx [ id , f^\sharp ] (f\;x)\]
|
||||
\end{mycase}
|
||||
\item \ref{law:uniformity}: Let \(Y\) be a setoid and \(g : Y ⇝ \dbtilde{D}\;A + Y, h : X ⇝ Y\) be setoid morphisms, such that \((id + h) \circ f \doteq g \circ h\). We need to show that \(f^\sharp\;x \approx g^\sharp(h\;x)\), for any \(x : X\). Let us proceed by case distinction over \(f\;x\) and \(g (h\;x)\), note that by the requisite equation \((id + h) \circ f \doteq g \circ h\), we only need to consider two cases: % chktex 2
|
||||
\begin{mycase}
|
||||
\case{} \(f\;x = i_1\;a\) and \(g (h\;x) = i_1\;b\)\\
|
||||
Consider that \((id + h) \circ f \doteq g \circ h\) on \(x\) yields \(i_1 \; a \overset{+}{=} i_1 \; b\) and thus \(a \approx b\). Then indeed,
|
||||
\[f^\sharp\; x \approx a \approx b \approx g^\sharp (h\;x)\]
|
||||
\case{} \(f\;x = i_2\;a\) and \(g (h\;x) = i_2\;b\)\\
|
||||
Note that \((id + h) \circ f \doteq g \circ h\) on \(x\) yields \(i_2(h\;a) \overset{+}{=} i_2\;b\) and thus \(h\;a \overset{Y}{=} b\).
|
||||
We are done by coinduction, which yields
|
||||
\[f^\sharp\;x \approx later(f^\sharp\;a) \approx later(g^\sharp(h\;a)) \approx later(g^\sharp\;b) \approx g^\sharp (h\;x).\]
|
||||
\end{mycase}
|
||||
\item \ref{law:folding}: Let \(Y\) be a setoid and \(h : Y ⇝ X + Y\) a setoid morphism, we need to show that \({(f^\sharp + h)}^\sharp\;z \approx {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp\;z\) for any \(z : X + Y\). % chktex 2
|
||||
Let us first establish the following fact
|
||||
\[f^\sharp\;c \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c) \qquad \text{for any } c : X, \tag{*}\label{folding-helper}\]
|
||||
which follows by case distinction on \(f\;c\) and coinduction:
|
||||
\begin{mycase}
|
||||
\case{} \(f\;c = i_1\;a\)
|
||||
\[f^\sharp\;c \approx a \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c)\]
|
||||
\case{} \(f\;c = i_2\;a\)
|
||||
\[f^\sharp\;c \approx later(f^\sharp\;a) \approx later({[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;a)) \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c)\]
|
||||
\end{mycase}
|
||||
We will now proceed with the proof of \ref{law:folding}, by case distinction on \(z\): % chktex 2
|
||||
\begin{mycase}
|
||||
\case{} \(z = i_1\;x\)\\
|
||||
Another case distinction on \(f\;x\) yields:
|
||||
\subcase{} \(f\;x = i_1\;a\)\\
|
||||
We are done, since \({(f^\sharp + h)}^\sharp(i_1 \; x) \approx a \approx {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;x)\)
|
||||
\subcase{} \(f\;x = i_2\;a\)\\
|
||||
Now, using the fact we established prior
|
||||
\begin{alignat*}{1}
|
||||
& {(f^\sharp + h)}^\sharp(i_1 \; x)
|
||||
\\\approx\;&later(f^\sharp\;a)
|
||||
\\\approx\;&later({[(id + i_1) \circ f , i_2 \circ h]}^\sharp (i_1\;a))\tag{\ref{folding-helper}}
|
||||
\\\approx\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;x).
|
||||
\end{alignat*}
|
||||
\case{} \(z = i_2\;y\)\\
|
||||
Let us proceed by discriminating on \(h\;y\).
|
||||
\subcase{} \(h\;y = i_1\;a\)\\
|
||||
Indeed by coinduction,
|
||||
\begin{alignat*}{1}
|
||||
& {(f^\sharp + h)}^\sharp(i_2 \; y)
|
||||
\\\approx\;&later((f^\sharp + h)(i_1\;a))
|
||||
\\\approx\;&later({[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;a))
|
||||
\\\approx\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;y)
|
||||
\end{alignat*}
|
||||
\subcase{} \(h\;y = i_2\;a\)\\
|
||||
Similarly by coinduction,
|
||||
\begin{alignat*}{1}
|
||||
& {(f^\sharp + h)}^\sharp(i_2 \; y)
|
||||
\\\approx\;&later((f^\sharp + h)(i_2\;a))
|
||||
\\\approx\;&later({[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;a))
|
||||
\\\approx\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;y)
|
||||
\end{alignat*}
|
||||
\end{mycase}
|
||||
\end{itemize}
|
||||
This concludes the proof that every \(\dbtilde{D}\;A\) extends to an Elgot algebra.
|
||||
\end{proof}
|
||||
|
||||
In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a setoid \(Z\), we can discretize \(Z\) by replacing the equivalence relation with propositional equality, yielding \(\disc{Z} := (Z, \equiv)\). Now, the following corollary describes how to transform an iteration on \(\dbtilde{D}\;A\) into an iteration on \(\tilde{D}\;A\).
|
||||
|
||||
\begin{corollary}\label{cor:discretize}
|
||||
Given a setoid morphism \(g : X ⇝ \dbtilde{D}\;A + X\), there exists a setoid morphism \(\bar{g} : \disc{X} ⇝ \tilde{D}\;A + \disc{X}\) such that \(g^\sharp\;x \sim \bar{g}^{\tilde{\sharp}}\;x\) for any \(x : X\).
|
||||
\end{corollary}
|
||||
\begin{proof}
|
||||
It is clear that propositional equality implies strong bisimilarity and thus \(\bar{g}\) is a setoid morphism that behaves as \(g\) does but with a different type profile.
|
||||
The requisite property follows by case distinction on \(g\;x\).
|
||||
\begin{mycase}
|
||||
\case{} \(g\;x = i_1\;a\)\\
|
||||
We are done, since \(g^\sharp\;x \sim a \sim \bar{g}^{\tilde{\sharp}}\;x\)
|
||||
\case{} \(g\;x = i_2\;a\)\\
|
||||
By coinduction \(g^\sharp\;x \sim later(g^\sharp\;a) \sim later(\bar{g}^{\tilde{\sharp}}\;a) \sim \bar{g}^{\tilde{\sharp}}\;x\), which concludes the proof.
|
||||
\qedhere
|
||||
\end{mycase}
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}\label{thm:Dfreeelgot}
|
||||
Every \(\dbtilde{D}\;A\) can be equipped with a free Elgot algebra structure.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
We build on \autoref{lem:Delgot}, it thus suffices to show that for any setoid \(A\), the Elgot algebra \((\dbtilde{D}\;A, {(-)}^\sharp)\) together with the setoid morphism \(now : A ⇝ \dbtilde{D}\;A\) is a free such algebra.
|
||||
Given an Elgot algebra \((B, {(-)}^{\sharp_b})\) and a setoid morphism \(f : A ⇝ B\). We need to define an Elgot algebra morphism \(\free{f} : \dbtilde{D}\;A ⇝ B\). Consider \(g : \tilde{D}\;A ⇝ B + \tilde{D}\;A\) defined by
|
||||
\[g\;x =
|
||||
\begin{cases}
|
||||
i_1(f\;a) & \text{if } x = now\;a \\
|
||||
i_2\;a & \text{if } x = later\;a
|
||||
\end{cases}\]
|
||||
|
||||
\(g\) trivially respects strong bisimilarity, thus consider \(g^{\sharp_b} : \tilde{D}\;A ⇝ B\). We need to show that \(g^{\sharp_b}\) also respects weak bisimilarity, thus yielding the requisite function \(\free{f} = g^{\sharp_b} : \dbtilde{D}\;A ⇝ B\). However, the proof turns out to be rather complex, let us postpone it to~\autoref{cor:respects}.
|
||||
|
||||
Instead, we will continue with the proof. Let us now show that \(g^{\sharp_b}\) is iteration preserving. Given a setoid morphism \(h : X ⇝ \dbtilde{D}\;A + X\), we need to show that \(g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x\) for any \(x : X\). Using \autoref{cor:discretize} we will proceed to show
|
||||
\[g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\]
|
||||
|
||||
The second step instantly follows by \ref{law:uniformity}, considering that the identity function easily extends to a setoid morphism \(id : \disc{X} ⇝ X\), and thus the second step can be reduced to \({((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}(id\;x)\). % chktex 2
|
||||
For the first step consider
|
||||
\begin{alignat*}{1}
|
||||
& g^{\sharp_b} (h^\sharp\;x)
|
||||
\\\overset{B}{=}\;&g^{\sharp_b} (\bar{h}^{\tilde{\sharp}}\;x)\tag{\autoref{cor:discretize}}
|
||||
\\\overset{B}{=}\;&(g^{\sharp_b} \circ [ id , \bar{h}^{\tilde{\sharp}}])(i_2\;x)
|
||||
\\\overset{B}{=}\;&{([(id + i_1) \circ g , i_2 \circ i_2 ] \circ [i_1 , h])}^{\sharp_b} (i_2\;x)\tag{\ref{law:uniformity}}
|
||||
\\\overset{B}{=}\;&{((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\tag{\ref{law:compositionality}}
|
||||
\end{alignat*}
|
||||
|
||||
Thus, \(g^{\sharp_b}\) is an Elgot algebra morphism. We are left to check that \(g^{\sharp_b}\) satisfies the requisite properties of free objects. First, note that \(g^{\sharp_b} \circ now \doteq [ id , g^\sharp_b ] \circ g \circ now \doteq f\) by \ref{law:fixpoint} and the definition of \(g\). % chktex 2
|
||||
Next, we need to check uniqueness of \(g^{\sharp_b}\). It suffices to show that any two Elgot algebra morphisms \(e, h : \dbtilde{D}\;A ⇝ B\) satisfying \(e \circ now \doteq f\) and \(h \circ now \doteq f\) are equal.
|
||||
|
||||
First, note that the identity function extends to the following conversion setoid morphism \(conv : \tilde{D}\;A ⇝ \dbtilde{D}\;A\), since strong bisimilarity implies weak bisimilarity. Furthermore, consider the setoid morphism \(o : \tilde{D}\;A ⇝ \tilde{D}\;A + \tilde{D}\;A\) defined by
|
||||
\[o\;x := \begin{cases}
|
||||
i_1(now\;z) & \text{if } x = now\;z \\
|
||||
i_2\;z & \text{if } x = later\;z
|
||||
\end{cases}\]
|
||||
Now, by coinduction we can easily follow that
|
||||
\[x \approx {((conv + id) \circ o)}^\sharp\;x \qquad \text{for any } x : D\;A.\tag{\(∗\)}\label{uniq-helper}\]
|
||||
|
||||
Let us now return to the proof of uniqueness. We proceed by
|
||||
\begin{alignat*}{1}
|
||||
& e\;x
|
||||
\\\approx\;&e({((conv + id) \circ o)}^\sharp\;x)\tag{\ref{uniq-helper}}
|
||||
\\\approx\;&{((e \circ conv + id) \circ o)}^{\sharp_b}\;x\tag{Preservation}
|
||||
\\\approx\;&{((h \circ conv + id) \circ o)}^{\sharp_b}\;x
|
||||
\\\approx\;&h({((conv + id) \circ o)}^\sharp\;x)\tag{Preservation}
|
||||
\\\approx\;&h\;x.\tag{\ref{uniq-helper}}
|
||||
\end{alignat*}
|
||||
It thus suffices to show that \((e \circ conv + id)(o\;x) \approx (h \circ conv + id)(o\;x)\). Indeed, discriminating over \(x\) yields:
|
||||
|
||||
\begin{mycase}
|
||||
\case{} \(x = now\;z\)
|
||||
\begin{alignat*}{1}
|
||||
& (e \circ conv + id)(o(now\;z))
|
||||
\\\overset{+}{=}\;&(e \circ conv + id)(i_1(now\;z))
|
||||
\\\overset{+}{=}\;&e(now\;z)
|
||||
\\\overset{+}{=}\;&f\;z
|
||||
\\\overset{+}{=}\;&h(now\;z)
|
||||
\\\overset{+}{=}\;&(h \circ conv + id)(i_1(now\;z))
|
||||
\\\overset{+}{=}\;&(h \circ conv + id)(o(now\;z))
|
||||
\end{alignat*}
|
||||
\case{} \(x = later\;z\)
|
||||
\begin{alignat*}{1}
|
||||
& (e \circ conv + id)(o(later\;z))
|
||||
\\\overset{+}{=}\;&(e \circ conv + id)(i_2\;z)
|
||||
\\\overset{+}{=}\;&i_2\;z
|
||||
\\\overset{+}{=}\;&(h \circ conv + id)(i_2\;z)
|
||||
\\\overset{+}{=}\;&(h \circ conv + id)(o(later\;z))
|
||||
\end{alignat*}
|
||||
\end{mycase}
|
||||
|
||||
It has thus been proven that every \(\dbtilde{D}\;A\) admits a free Elgot algebra structure.
|
||||
\end{proof}
|
||||
|
||||
Let us now establish some functions for inspecting and manipulating the computation of elements of \(D\;A\). These functions and some key facts will then be used to finish the remaining proof needed for \autoref{thm:Dfreeelgot}.
|
||||
|
||||
First, consider the ordering with respect to execution time on elements of \(D\;A\), defined by
|
||||
\[
|
||||
\mprset{fraction={===}}\inferrule*{p: x \downarrow a}{now_\lesssim\;p : now\;a \lesssim x} \qquad
|
||||
\inferrule*{p : x \lesssim y}{later_\lesssim\;p : later\;x \lesssim later\;y}.
|
||||
\]
|
||||
Note that \(x \lesssim y\) implies \(x \approx y\) for any \(x, y : D\;A\), which follows easily by coinduction.
|
||||
|
||||
Now, consider the following function \(race : D\;A \rightarrow D\;A \rightarrow D\;A\) which tries running two computations and returns the one that finished first:
|
||||
\[race\;p\;q := \begin{cases}
|
||||
now\;a & \text{if } p = now\;a \\
|
||||
now\;b & \text{if } p = later\;a \text{ and } q = now\;b \\
|
||||
later\;(race\;a\;b) & \text{if } p = later\;a \text{ and } q = later\;b
|
||||
\end{cases}\]
|
||||
|
||||
The following Corollary, whose proof can be found in the formalization, will be needed.
|
||||
|
||||
\begin{corollary}\label{cor:race}
|
||||
\(race\) satisfies the following properties:
|
||||
\begin{alignat*}{3}
|
||||
& x \approx y & & \text{ implies } race\;x\;y \sim race\;y\;x & \text{for any } x, y : D\;A
|
||||
\\ &x \approx y && \text{ implies } race\;x\;y \lesssim y & \text{ for any } x, y : D\;A.
|
||||
\end{alignat*}
|
||||
\end{corollary}
|
||||
|
||||
Next, let us consider functions for counting steps of computations, first regard \(\Delta_0 : (x : D\;A) \rightarrow (a : A) \rightarrow (x \downarrow a) \rightarrow \mathbb{N}\), which returns the number of steps a terminating computation has to take and is defined by
|
||||
\[\Delta_0\;x\;a\;p := \begin{cases}
|
||||
0 & \text{if } x = now\;y \\
|
||||
(\Delta_0\; y\;a\;q) + 1 & \text{if } x = later\;y \text{ and } p = later_\downarrow q
|
||||
\end{cases}\]
|
||||
|
||||
Similarly, consider \(\Delta : (x, y : D\;A) \rightarrow x \lesssim y \rightarrow D(A \times \mathbb{N})\) defined by
|
||||
\[\Delta\;x\;y\;p := \begin{cases}
|
||||
now(a , \Delta_0\;x\;a\;q) & \text{if } x = now\;a \text{ and } p = now_\lesssim q \\
|
||||
later(\Delta\;a\;b\;q) & \text{if } x = later\;a, y = later\;b \text{ and } p = later_\lesssim q
|
||||
\end{cases}\]
|
||||
|
||||
Lastly, consider the function \(\iota : A \times \mathbb{N} \rightarrow D\;A\), which adds a number of \(later\) constructors in front of a value and is given by
|
||||
\[\iota\;(a, n) := \begin{cases}
|
||||
now\;x & \text{if } n = 0 \\
|
||||
later(\iota\;(a, m)) & \text{if } n = m + 1
|
||||
\end{cases}\]
|
||||
|
||||
Trivially, \(\iota\) extends to a setoid morphism \(\iota : A \times \mathbb{N} ⇝ \tilde{D}\;A\), where the equivalence on \(\mathbb{N}\) is propositional equality.
|
||||
Let us state two facts about \(\Delta\), the proofs can again be found in the formalization.
|
||||
\begin{corollary}\label{cor:delta}
|
||||
\(\Delta\) satisfies the following properties:
|
||||
\begin{alignat*}{4}
|
||||
& p : x \lesssim y & & \text{ implies } \tilde{D}(fst (\Delta\;x\;y\;p))\; & \sim x & & \text{ for any } x, y : D\;A\tag{\(\Delta_1\)}\label{delta1} \\
|
||||
& p : x \lesssim y & & \text{ implies } \iota^* (\Delta\;x\;y\;p) & \sim y & & \text{ for any } x, y : D\;A.\tag{\(\Delta_2\)}\label{delta2}
|
||||
\end{alignat*}
|
||||
\end{corollary}
|
||||
|
||||
Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
|
||||
|
||||
\begin{corollary}\label{cor:respects}
|
||||
The setoid morphism \(g^{\sharp_b} : \tilde{D}\;A ⇝ B\) defined in \autoref{thm:Dfreeelgot} respects weak bisimilarity, thus yielding \(\free{f} = g^{\sharp_b} : \dbtilde{D}\;A ⇝ B\).
|
||||
\end{corollary}
|
||||
\begin{proof}
|
||||
Let \(x, y : D\;A\) such that \(x \approx y\). Recall that by \autoref{cor:race} \(x \approx y\) implies \(p: race\;x\;y \lesssim y\) and symmetrically \(q: race\;y\;x \lesssim x\), now, using Corollaries~\ref{cor:race} and~\ref{cor:delta}:
|
||||
\begin{alignat*}{1}
|
||||
& g^{\sharp_b}\;x
|
||||
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*(\Delta\;(race\;y\;x)\;x\;q))\tag{\ref{delta2}}
|
||||
\\\overset{B}{=}\;&g^{\sharp_b}(\tilde{D}fst(\Delta\;(race\;y\;x)\;x\;q))\tag{\ref{respects-key-helper}}
|
||||
\\\overset{B}{=}\;&g^{\sharp_b}(race\;y\;x)\tag{\ref{delta1}}
|
||||
\\\overset{B}{=}\;&g^{\sharp_b}(race\;x\;y)\tag{\autoref{cor:race}}
|
||||
\\\overset{B}{=}\;&g^{\sharp_b}(\tilde{D}fst(\Delta\;(race\;x\;y)\;y\;p))\tag{\ref{delta1}}
|
||||
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*(\Delta\;(race\;x\;y)\;y\;p))\tag{\ref{respects-key-helper}}
|
||||
\\\overset{B}{=}\;&g^{\sharp_b}\;y.\tag{\ref{delta2}}
|
||||
\end{alignat*}
|
||||
|
||||
We have thus reduced the proof to showing that
|
||||
\[g^{\sharp_b} (\tilde{D}fst\;z) \overset{B}{=} g^{\sharp_b}(\iota^*\;z) \text{ for any } z : D(A \times \mathbb{N}). \tag{*}\label{respects-key-helper}\]
|
||||
|
||||
Let us proceed as follows
|
||||
\begin{alignat*}{1}
|
||||
& g^{\sharp_b} (\tilde{D}fst\;z)
|
||||
\\\overset{B}{=}\;&g_1^{\sharp_b}\;z\tag{\ref{law:uniformity}}
|
||||
\\\overset{B}{=}\;&g_2^{\sharp_b}\;z
|
||||
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*\;z). \tag{\ref{law:uniformity}}
|
||||
\end{alignat*}
|
||||
|
||||
Which leaves us to find suitable \(g_1, g_2 : \tilde{D}(A \times \mathbb{N}) ⇝ B + \tilde{D} (A \times \mathbb{N})\). Consider,
|
||||
\[g_1\;p := \begin{cases}
|
||||
i_1(f\;x) & \text{if } p = now\;(x, zero) \\
|
||||
i_2(\tilde{D}o (\iota\;(x,n))) & \text{if } p = now\;(x, n + 1) \\
|
||||
i_2\;q & \text{if } p = later\;q
|
||||
\end{cases}\]
|
||||
and
|
||||
\[g_2\;p := \begin{cases}
|
||||
i_1(f\;x) & \text{if } p = now\;(x , n) \\
|
||||
i_2\;q & \text{if } p = later\;q
|
||||
\end{cases}\]
|
||||
where \(o : A ⇝ A \times \mathbb{N}\) is a setoid morphism that maps every \(z : A\) to \((z , 0) : A \times \mathbb{N}\). The applications of \ref{law:uniformity} are then justified by the definitions of \(g_1\) and \(g_2\) as well as the fact that \(\iota \circ o \doteq now\). % chktex 2
|
||||
|
||||
We are thus done after showing that \(g_1^{\sharp_b}\;z \overset{B}{=} g_2^{\sharp_b}\;z\).
|
||||
Consider another setoid morphism
|
||||
\[g_3 : \tilde{D}(A \times \mathbb{N}) ⇝ B + \tilde{D}(A \times \mathbb{N}) + \tilde{D}(A \times \mathbb{N}),\]
|
||||
defined by
|
||||
\[g_3\;p := \begin{cases}
|
||||
i_1(f\;x) & \text{if } p = now\;(x, 0) \\
|
||||
i_2(i_1(\tilde{D}o(\iota\;(x,n)))) & \text{if } p = now\;(x, n + 1) \\
|
||||
i_2(i_2\;q) & \text{if } p = later\;q
|
||||
\end{cases}\]
|
||||
|
||||
Let us now proceed by
|
||||
\begin{alignat*}{1}
|
||||
& g_1^{\sharp_b}\;z
|
||||
\\\overset{B}{=}\;&{((id + [ id , id ]) \circ g_3)}^{\sharp_b}\;z
|
||||
\\\overset{B}{=}\;&{([ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] \circ g_3)}^{\sharp_b}\;z\tag{\ref{law:diamond}}
|
||||
\\\overset{B}{=}\;&g_2^{\sharp_b}\;z.
|
||||
\end{alignat*}
|
||||
|
||||
Where for the first step notice that \(g_1\;x \overset{+}{=} (id + [ id , id ])(g_3\;x)\) for any \(x : \tilde{D}(A \times \mathbb{N})\) follows simply by case distinction on \(x\). For the last step, it suffices to show that \([ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x) \overset{+}{=} g_2\;x\) for any \(x : \tilde{D}(A \times \mathbb{N})\). We proceed by case distinction on \(x\).
|
||||
|
||||
\begin{mycase}
|
||||
\case{} \(x = now\;(y, 0)\)\\
|
||||
The goal reduces to
|
||||
\begin{alignat*}{1}
|
||||
& [ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x)
|
||||
\\\overset{+}{=}\;&[ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (i_1(f\;y))
|
||||
\\\overset{+}{=}\;&i_1(f\;y)
|
||||
\\\overset{+}{=}\;&g_2\;x,
|
||||
\end{alignat*}
|
||||
which indeed holds by the definitions of \(g_2\) and \(g_3\).
|
||||
|
||||
\case{} \(x = now\;(y, n + 1)\)\\
|
||||
The goal reduces to
|
||||
\begin{alignat*}{1}
|
||||
& [ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x)
|
||||
\\\overset{+}{=}\;&[ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (i_2(i_1(\tilde{D}o(\iota\;(y,n)))))
|
||||
\\\overset{+}{=}\;&i_1({((id + [ id , id]) \circ g_3)}^{\sharp_b}((\tilde{D}o(\iota\;(y,n)))))
|
||||
\\\overset{+}{=}\;&i_1(f\;y)\tag{\ref{finalhelper}}
|
||||
\\\overset{+}{=}\;&g_2\;x
|
||||
\end{alignat*}
|
||||
|
||||
Where
|
||||
\[{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,n))) \overset{B}{=} f\;y \tag{\(∗\)}\label{finalhelper}\]
|
||||
follows by induction on \(n\):
|
||||
|
||||
\subcase{} \(n = 0\)\\
|
||||
We are done by
|
||||
\begin{alignat*}{1}
|
||||
& {((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,0)))
|
||||
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(now\;y))
|
||||
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(now(y,0))
|
||||
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id]) \circ g_3) (now(y,0))\tag{\ref{law:fixpoint}}
|
||||
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id])) i_1(f\;y)
|
||||
\\\overset{B}{=}\;&[ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] i_1(f\;y)
|
||||
\\\overset{B}{=}\;&f\;y
|
||||
\end{alignat*}
|
||||
|
||||
\subcase{} \(n = m + 1\)\\
|
||||
Assuming that \({((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,m))) \overset{B}{=} f\;y\), we are done by
|
||||
\begin{alignat*}{1}
|
||||
& {((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,m+1)))
|
||||
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(later(\iota\;(y,m))))
|
||||
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(later(\tilde{D}o(\iota\;(y,m))))
|
||||
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id]) \circ g_3) (later(\tilde{D}o(\iota\;(y,m))))\tag{\ref{law:fixpoint}}
|
||||
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id])) (i_2(i_2(\tilde{D}o(\iota\;(y,m)))))
|
||||
\\\overset{B}{=}\;&[ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ](\tilde{D}o(\iota\;(y,m)))
|
||||
\\\overset{B}{=}\;&f\;y
|
||||
\end{alignat*}
|
||||
|
||||
\case{} \(x = later\;p\)\\
|
||||
The goal reduces to
|
||||
\begin{alignat*}{1}
|
||||
& [ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x)
|
||||
\\\overset{+}{=}\;&[ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (i_2(i_2\;p))
|
||||
\\\overset{+}{=}\;&i_2\;p
|
||||
\\\overset{+}{=}\;&g_2\;x,
|
||||
\end{alignat*}
|
||||
which instantly follows by definition.
|
||||
\end{mycase}
|
||||
This finishes the proof of the Corollary and thus \autoref{thm:Dfreeelgot} holds.
|
||||
\end{proof}
|
||||
|
||||
We have shown in \autoref{thm:Dfreeelgot} that every \(\dbtilde{D}\;A\) extends to a free Elgot algebra. Together with \autoref{prop:setoids-ccc} and \autoref{thm:stability} this yields a description for the monad \(\mathbf{K}\) which has been defined in \autoref{chp:iteration}, in the category \(\setoids\).
|
||||
9
src/07_conclusion.tex
Normal file
9
src/07_conclusion.tex
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
\chapter{Conclusion}
|
||||
We have considered a novel approach to defining a monad suitable for modelling partiality from first principles, which has first been introduced in~\cite{uniformelgot}.
|
||||
Using the dependently typed programming language Agda, we were able to formally verify important properties of this monad:
|
||||
it is an equational lifting monad, i.e.\ a monad that offers no other side effect besides some form of non-termination and furthermore it turns out to be the initial pre-Elgot monad.
|
||||
Moreover, we have considered a concrete description of this monad in the category of setoids, where it turns out to be a quotient of the delay monad.
|
||||
|
||||
With this thesis we have thus created a small Agda library that contains categorical concepts concerning partiality and iteration theories.
|
||||
Future work might improve on this library by formalizing important results concerning partiality monads, such as the fact that every equational lifting monad has a restriction category as its Kleisli category.
|
||||
Furthermore, one can continue studying the delay monad in a categorical setting, by modeling the quotient by weak bisimilarity of the delay monad through a certain coequalizer, as has been done in~\cite{uniformelgot}, and then identifying assumptions under which this constitutes a suitable monad for modeling partiality.
|
||||
49
src/titlepage.tex
Normal file
49
src/titlepage.tex
Normal file
|
|
@ -0,0 +1,49 @@
|
|||
\begin{titlepage}
|
||||
\newcommand{\drop}{0.07\textheight}
|
||||
\begin{center}
|
||||
\begingroup%
|
||||
\vfill
|
||||
{\LARGE\textsc{%
|
||||
Friedrich-Alexander-Universität\\[2mm]
|
||||
Erlangen-Nürnberg%
|
||||
}}\\[\drop]
|
||||
{%
|
||||
% trim= left bottom right top
|
||||
\includegraphics[height=1.8cm,trim=0cm 0mm 0 0mm]{img/tcs}\\
|
||||
\textsc{\large Chair for Computer Science 8}\\
|
||||
\textsc{\large Theoretical Computer Science}}%\\[\drop]
|
||||
\vfill
|
||||
\rule{\textwidth}{1pt}\par
|
||||
\vspace{0.5\baselineskip}
|
||||
{% maybe \itshape?
|
||||
\Huge\bfseries
|
||||
\makeatletter
|
||||
\@title \\[1cm] % chktex 1
|
||||
\makeatother
|
||||
% \large\bfseries
|
||||
% \\ and \ldots
|
||||
% \\[1cm]
|
||||
\textbf{\large Bachelor Thesis in Computer Science}
|
||||
}\\[0.5\baselineskip]
|
||||
\rule{\textwidth}{1pt}\par
|
||||
\vfill
|
||||
{\Large{\makeatletter\@author\makeatother}
|
||||
%\\ {\large\normalsize{maybe-ur-mail@example.org}}
|
||||
}
|
||||
\vfill
|
||||
\large Advisor:
|
||||
\vfill
|
||||
\begin{tabular}{ccc}
|
||||
\large
|
||||
Sergey Goncharov
|
||||
\end{tabular}
|
||||
\vfill
|
||||
% trim= left bottom right top
|
||||
\includegraphics[height=1.8cm,trim=0cm -5mm 0 0mm]{img/fau}
|
||||
\vfill
|
||||
{\large Erlangen, \today}
|
||||
\endgroup
|
||||
\end{center}
|
||||
\end{titlepage}
|
||||
|
||||
% vim: tw=80 spell spelllang=en nocul
|
||||
BIN
thesis.pdf
Normal file
BIN
thesis.pdf
Normal file
Binary file not shown.
Loading…
Reference in a new issue