diff --git a/tex/.vscode/ltex.dictionary.en-US.txt b/tex/.vscode/ltex.dictionary.en-US.txt index 4619b16..555561b 100644 --- a/tex/.vscode/ltex.dictionary.en-US.txt +++ b/tex/.vscode/ltex.dictionary.en-US.txt @@ -2,3 +2,8 @@ Vatthauer mycase Coalgebras Coalgebra +Milius +FAU +codomain +surjective +haskell diff --git a/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt b/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt new file mode 100644 index 0000000..d1b8528 --- /dev/null +++ b/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt @@ -0,0 +1,7 @@ +{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QThis is a summary of the course “Algebra of Programming” taught by Prof. Dr. Stefan Milius in the winter term 2023/2024 at the FAU Functions.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QFriedrich-Alexander-Universitity Erlangen-Nürnberg\\E$"} +{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\QThis is a summary of the course “Algebra of Programming” taught by Prof. Dr. Stefan Milius in the winter term 2023/2024 at the FAU .\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QThis is a summary of the course “Algebra des Programmierens” taught by Prof. Dr. Stefan Milius in the winter term 2023/2024 at the FAU .\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QFriedrich-Alexander-Universität Erlangen-Nürnberg\\E$"} +{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\QThis is a summary of the course “Algebra des Programmierens” taught by Prof. Dr. Stefan Milius in the winter term 2023/2024 at the FAU .\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfies the following two rules law:natident Identity law:natfusion Fusion Lists.\\E$"} diff --git a/tex/bib.bib b/tex/bib.bib new file mode 100644 index 0000000..51e931b --- /dev/null +++ b/tex/bib.bib @@ -0,0 +1,17 @@ +@article{poll1999algebra, + title = {Algebra of Programming by Richard Bird and Oege de Moor, Prentice Hall, 1996 (dated 1997).}, + author = {Poll, Erik and Thompson, Simon}, + journal = {Journal of Functional Programming}, + volume = {9}, + number = {3}, + pages = {347--354}, + year = {1999}, + publisher = {Cambridge University Press} +} + +@book{adamek1990abstract, + title = {Abstract and concrete categories}, + author = {Ad{\'a}mek, Ji{\v{r}}{\'\i} and Herrlich, Horst and Strecker, George}, + year = {1990}, + publisher = {Wiley-Interscience} +} diff --git a/tex/main.pdf b/tex/main.pdf new file mode 100644 index 0000000..b5b59d4 Binary files /dev/null and b/tex/main.pdf differ diff --git a/tex/main.tex b/tex/main.tex index bd7a373..f01707b 100644 --- a/tex/main.tex +++ b/tex/main.tex @@ -4,8 +4,11 @@ \usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry} \usepackage{scrlayer-fancyhdr} \usepackage{extramarks} +\usepackage[ngerman, english]{babel} +\babeltags{german=ngerman} \usepackage{anyfontsize} \usepackage{unicode-math} +\usepackage{amsmath} \usepackage[scale=.85]{noto-mono} % TODO find better unicode mono font \usepackage[final]{hyperref} \pagestyle{fancy} @@ -34,11 +37,26 @@ } %%%% +%%%% Code listings +\usepackage{minted} +\setminted[haskell]{ + linenos=true, + breaklines=true, + encoding=utf8, + fontsize=\small, + autogobble +} +\setmintedinline[haskell]{ + style=bw +} + +%%%% + %%%% Math packages \usepackage{amsthm} \usepackage{thmtools} \usepackage{tikz} -\usetikzlibrary{cd, quotes} +\usetikzlibrary{cd, babel, quotes} \declaretheorem[name=Definition,style=definition,numberwithin=section]{definition} \declaretheorem[name=Example,style=definition,sibling=definition]{example} \declaretheorem[style=definition,numbered=no]{exercise} @@ -52,6 +70,7 @@ \declaretheorem[sibling=lemma]{proposition} %%%% +%%%% href \makeatletter \hypersetup{ pdfauthor={\@author}, @@ -60,6 +79,13 @@ hidelinks, } \makeatother +%%%% + +%%%% Bibliography +\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 +\addbibresource{bib.bib} +%%%% %%%% Custom definitions: Commands and environments @@ -114,4 +140,8 @@ \include{sections/02_categories} \include{sections/03_constructions} %% + +\appendix +\emergencystretch=1em +\printbibliography[heading=bibintoc]{} \end{document} \ No newline at end of file diff --git a/tex/sections/01_introduction.tex b/tex/sections/01_introduction.tex index e14a262..77cd775 100644 --- a/tex/sections/01_introduction.tex +++ b/tex/sections/01_introduction.tex @@ -1,4 +1,182 @@ +% chktex-file 46 \section{Introduction} +This is a summary of the course ``Algebra des Programmierens'' taught by Prof.\ Dr.\ Stefan Milius in the winter term 2023/2024 at the FAU~\footnote{Friedrich-Alexander-Universität Erlangen-Nürnberg}. +The course is based on~\cite{poll1999algebra} with~\cite{adamek1990abstract} as a reference for category theory. + +Goal of the course is to develop a mathematical theory for semantics of data types and their accompanying proof principles. The chosen environment is the field of category theory. \subsection{Functions} -\subsection{Data Types} \ No newline at end of file +A function $f : X \rightarrow Y$ is a mapping from the set $X$ (the domain of $f$) to the set $Y$ (the codomain of $f$). +More concretely $f$ is a relation $f \subseteq X \times Y$ which is +\begin{itemize} + \item \emph{left-total}, i.e.\ for all $x \in X$ exists some $y \in Y$ such that $(x,y) \in f$; + \item \emph{right-unique}, i.e.\ any $(x,y),(x,y') \in f$ imply $y = y'$. +\end{itemize} + +Often, one is also interested in the symmetrical properties, a function is called +\begin{itemize} + \item \emph{injective} or \emph{left-unique} if for every $x,x' \in X$ the implication $f(x) = f(x') \rightarrow x = x'$ holds; + \item \emph{surjective} or \emph{right-total} if for every $y \in Y$ there exists an $x \in X$ such that $f(x) = y$; + \item \emph{bijective} if it is injective and surjective. +\end{itemize} + +\begin{example} + \begin{enumerate} + \item The identity function $id_A : A \rightarrow A$, $id_A(x) = x$ + \item The constant function $b! : A \rightarrow B$ for $b \in B$ defined by $b!(x) = b$ + \item The inclusion function $i_A : A \rightarrow B$ for $A \subseteq B$ defined by $i_A(x) = x$ + \item Constants $b : 1 \rightarrow B$, where $1 := {*}$. The function $b$ is in bijection with the set $B$. + \item Composition of function $f : A \rightarrow B, g : B \rightarrow C$ called $g \circ f : A \rightarrow C$ defined by $(g \circ f)(x) = g(f(x))$. + \item The empty function $¡ : \emptyset \rightarrow B$ + \item The singleton function $! : A \rightarrow 1$ + \end{enumerate} +\end{example} + +\subsection{Data Types} + +Programs work with data that should ideally be organized in a useful manner. +A useful representation for data in functional programming is by means of \emph{algebraic data types}. +Some basic data types (written in Haskell notation) are +\begin{minted}{haskell} + data Bool = True | False + data Nat = Zero | Succ Nat +\end{minted} + +These data types are declared by means of constructors, yielding concrete descriptions how inhabitants of these types are created. +\emph{Parametric data types} are additionally parametrized by another data type, e.g.\ +\begin{minted}{haskell} + data Maybe a = Nothing | Just a + data Either a b = Left a | Right b + data List a = Nil | Cons a (List a) +\end{minted} + + +Such data types (parametric or non-parametric) usually come with a principle for defining functions called recursion and in richer type systems (e.g.\ in a dependently typed setting) with a principle for proving facts about recursive functions called induction. +Equivalently, every function defined by recursion can be defined via a \emph{fold}-function which satisfies an identity and fusion law, which replace the induction principle. Let us now consider two examples of data types and illustrate this. + +\subsubsection{Natural Numbers} +The type of natural numbers comes with a fold function $foldn : C \rightarrow (Nat \rightarrow C) \rightarrow Nat \rightarrow C$ for every $C$, defined by +\begin{alignat*}{2} + & foldn\;c\;h\;zero & & = c \\ + & foldn\;c\;h\;(suc\;n) & & = h\;(foldn\;c\;h\;n) +\end{alignat*} + + +\begin{example} Let us now consider some functions defined in terms of $foldn$. + \begin{itemize} + \item $iszero : Nat \rightarrow Bool$ is defined by + \[iszero = foldn\;true\;false!\] + \item $plus : Nat \rightarrow Nat \rightarrow Nat$ is defined by + \[plus = foldn\;id (\lambda f\;n. succ (f\;n)) \] + \end{itemize} +\end{example} + +\begin{proposition} + $foldn$ satisfies the following two rules + \begin{enumerate} + \item \customlabel{law:natident}{\textbf{Identity}}: $foldn\;zero\;succ = id_{Nat}$ + \item \customlabel{law:natfusion}{\textbf{Fusion}}: for all $c : C$, $h, h' : Nat + \rightarrow C$ and $k : C \rightarrow C'$ with $kc = c'$ and $kh = h'k$ follows $k \circ foldn\;c\;h = foldn\;c'\;h'$, or diagrammatically: + % https://q.uiver.app/#q=WzAsNSxbMiwwLCJDIl0sWzQsMCwiQyJdLFsyLDIsIkMnIl0sWzQsMiwiQyciXSxbMCwwLCIxIl0sWzQsMCwiYyJdLFswLDIsImsiXSxbNCwyLCJjJyIsMl0sWzAsMSwiaCIsMl0sWzIsMywiaCciLDJdLFsxLDMsImsiLDFdXQ== + \[ + \begin{tikzcd}[ampersand replacement=\&] + 1 \&\& C \&\& C \\ + \\ + \&\& {C'} \&\& {C'} + \arrow["c", from=1-1, to=1-3] + \arrow["k", from=1-3, to=3-3] + \arrow["{c'}"', from=1-1, to=3-3] + \arrow["h"', from=1-3, to=1-5] + \arrow["{h'}"', from=3-3, to=3-5] + \arrow["k"{description}, from=1-5, to=3-5] + \end{tikzcd} + \] + implies + % https://q.uiver.app/#q=WzAsMyxbMCwwLCJOYXQiXSxbMiwwLCJDIl0sWzIsMiwiQyciXSxbMSwyLCJrIl0sWzAsMSwiZm9sZG5cXDtjXFw7aCJdLFswLDIsImZvbGRuXFw7YydcXDtoJyIsMl1d + \[ + \begin{tikzcd}[ampersand replacement=\&] + Nat \&\& C \\ + \\ + \&\& {C'} + \arrow["k", from=1-3, to=3-3] + \arrow["{foldn\;c\;h}", from=1-1, to=1-3] + \arrow["{foldn\;c'\;h'}"', from=1-1, to=3-3] + \end{tikzcd} + \] + \end{enumerate} +\end{proposition} +\begin{proof} + Both follow by induction over an argument $n : Nat$: + \begin{enumerate} + \item~\ref{law:natident}: + \begin{mycase} + \case{} $n = zero$ + \[foldn\;zero\;succ\;zero = zero = id\;zero\] + \case{} $n = succ\;m$ + \begin{alignat*}{1} + foldn\;zero\;succ\;(succ\;m) & = succ (foldn\;zero\;succ\;m) + \\&= succ\;m \tag{IH} + \\&= id (succ\;m) + \end{alignat*} + \end{mycase} + \item~\ref{law:natfusion}: + \begin{mycase} + \case{} $n = zero$ + \[k(foldn\;c\;h\;zero) = k\;c = c' = foldn\;c'\;h'\;zero\] + \case{} $n = succ\;m$ + \begin{alignat*}{1} + k(foldn\;c\;h\;(succ\;m)) & = k(h(foldn\;c\;h\;m)) + \\&= h'(k(foldn\;c\;h\;m)) + \\&= h'(foldn\;c'\;h'\;m) \tag{IH} + \\&= foldn\;c'\;h'\;(succ\;m) + \end{alignat*} + \end{mycase} + \end{enumerate} +\end{proof} + +\begin{example} + The identity and fusion laws can in turn be used to prove the following induction principle: + + For any predicate $p : Nat \rightarrow Bool$, + \begin{enumerate} + \item $p\;zero = true$ and + \item $p \circ succ = p$ + \end{enumerate} + implies $p = true!$. This follows by % chktex 40 + \begin{alignat*}{1} + & p + \\=\;&p \circ (foldn\;zero\;succ) \tag{\ref{law:natident}} + \\=\;&foldn\;true\;id \tag{\ref{law:natfusion}} + \\=\;&true! \circ (foldn\;zero\;succ) \tag{\ref{law:natfusion}} + \\=\;&true!. \tag{\ref{law:natident}} + \end{alignat*} + + Where the first application of~\ref{law:natfusion} is justified, since the diagram + % https://q.uiver.app/#q=WzAsNSxbMiwwLCJOYXQiXSxbNCwwLCJOYXQiXSxbMiwyLCJCb29sIl0sWzQsMiwiQm9vbCJdLFswLDAsIjEiXSxbNCwwLCJ6ZXJvIl0sWzAsMSwic3VjYyJdLFsxLDMsInAiXSxbMCwyLCJwIl0sWzIsMywiaWQiLDFdLFs0LDIsInRydWUiLDJdXQ== + \[\begin{tikzcd} + 1 && Nat && Nat \\ + \\ + && Bool && Bool + \arrow["zero", from=1-1, to=1-3] + \arrow["succ", from=1-3, to=1-5] + \arrow["p", from=1-5, to=3-5] + \arrow["p", from=1-3, to=3-3] + \arrow["id"{description}, from=3-3, to=3-5] + \arrow["true"', from=1-1, to=3-3] + \end{tikzcd}\] + commutes by the requisite properties of $p$, and the second application of~\ref{law:natfusion} is justified, since the diagram + % https://q.uiver.app/#q=WzAsNSxbMiwwLCJOYXQiXSxbNCwwLCJOYXQiXSxbMiwyLCJCb29sIl0sWzQsMiwiQm9vbCJdLFswLDAsIjEiXSxbNCwwLCJ6ZXJvIl0sWzAsMSwic3VjYyJdLFsxLDMsInRydWUhIl0sWzAsMiwidHJ1ZSEiXSxbMiwzLCJpZCIsMV0sWzQsMiwidHJ1ZSIsMl1d + \[\begin{tikzcd} + 1 && Nat && Nat \\ + \\ + && Bool && Bool + \arrow["zero", from=1-1, to=1-3] + \arrow["succ", from=1-3, to=1-5] + \arrow["{true!}", from=1-5, to=3-5] + \arrow["{true!}", from=1-3, to=3-3] + \arrow["id"{description}, from=3-3, to=3-5] + \arrow["true"', from=1-1, to=3-3] + \end{tikzcd}\] + trivially commutes. +\end{example} +\subsubsection{Lists} \ No newline at end of file diff --git a/tex/sections/02_datatypes.tex b/tex/sections/02_datatypes.tex deleted file mode 100644 index 2241169..0000000 --- a/tex/sections/02_datatypes.tex +++ /dev/null @@ -1 +0,0 @@ -\section{Functions and Data}