mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
final slides
This commit is contained in:
parent
9fa6f8e0ed
commit
be2d12cbf1
3 changed files with 32 additions and 16 deletions
|
@ -127,3 +127,19 @@ numpages = {16}
|
||||||
biburl = {https://dblp.org/rec/journals/corr/abs-2102-11828.bib},
|
biburl = {https://dblp.org/rec/journals/corr/abs-2102-11828.bib},
|
||||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
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}
|
||||||
|
}
|
|
@ -29,8 +29,8 @@ module reverse where
|
||||||
fin-colist : Colist ℕ
|
fin-colist : Colist ℕ
|
||||||
fin-colist = 1 ∷ ♯ (2 ∷ ♯ (3 ∷ ♯ []))
|
fin-colist = 1 ∷ ♯ (2 ∷ ♯ (3 ∷ ♯ []))
|
||||||
|
|
||||||
inf-colist : Colist ℕ
|
ones : Colist ℕ
|
||||||
inf-colist = 1 ∷ ♯ inf-colist
|
ones = 1 ∷ ♯ ones
|
||||||
|
|
||||||
-- run reverse fin-colist for 5 steps
|
-- run reverse fin-colist for 5 steps
|
||||||
-- run reverse inf-colist for 1000 steps
|
-- run reverse ones for 1000 steps
|
|
@ -170,7 +170,7 @@ The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complet
|
||||||
\end{block}
|
\end{block}
|
||||||
\end{frame}
|
\end{frame}
|
||||||
|
|
||||||
\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Monads~\cite{elgotmonad}}
|
\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Monads~\cite{elgotmonad}~\cite{while}}
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
A monad $\mathbf{T}$ is an Elgot monad if it has an iteration operator $(f : X \rightarrow T(Y + X))^\dagger : X \rightarrow TY$ satisfying:
|
A monad $\mathbf{T}$ is an Elgot monad if it has an iteration operator $(f : X \rightarrow T(Y + X))^\dagger : X \rightarrow TY$ satisfying:
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
|
|
Loading…
Reference in a new issue