approx-diff/notes.tex at main · fluid-org/approx-diff · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
\documentclass[acmsmall,screen]{acmart}

\usepackage{tabularx}
\usepackage{bbm}
\usepackage{bbold}
\usepackage{stmaryrd}
\usepackage{mathpartir}
\usepackage{subcaption}
\usepackage{tikz-cd}
\usepackage{xspace}

%\geometry{paperwidth=8.3in, paperheight=11.7in} % force to A4 for now
\settopmatter{printacmref=false}
\citestyle{acmauthoryear}
\raggedbottom

\usepackage[commandnameprefix=ifneeded,commentmarkup=footnote]{changes}
\input{macros}

\begin{document}

\title{Approximation as Differentiation: Notes}

\maketitle

\section{Overview}

Covered here:
\begin{itemize}
\item automatic differentiation (\secref{auto-diff})
\item stable functions (\secref{stable-functions})
\item $\CMon$, the category of commutative monoids (\secref{cmon})
\item $\CMon$-enrichment, including enriched functors and enriched Yoneda embedding (\secref{cmon-enriched})
\item biproducts and semi-additive categories (\secref{biproduct})
\item useful semi-additive categories (\secref{useful-semi-additive-categories}):
   \begin{itemize}
   \item category $\LatGal$ of bounded lattices and Galois connections (\secref{categories-with-biproducts:latgal})
   \item category $\LatConj$ of bounded distributive lattices and conjugate pairs
   (\secref{categories-with-biproducts:latconj})
   \item category $\FinVect_F$ of finite-dimensional vector spaces over a field $F$
   (\secref{categories-with-biproducts:fdvect})
   \end{itemize}
\item category $\Fam(I,\cat{C})$ of $I$-indexed families of objects of $\cat{C}$ (\secref{fam})
\item set-indexed products (\secref{set-indexed-product})
\item Grothendieck construction $\Grothendieck{\cat{C}}F$ and category of families $\Fam(\cat{C})$
(\secref{grothendieck})
\item useful categories of families for automatic approximation
(\secref{galois-slicing-auto-diff-via-fam}):
   \begin{itemize}
      \item Galois slicing via $\Fam(\LatGal)$ (\secref{galois-slicing-auto-diff-via-fam:galois-slicing})
      \item automatic differentiation via $\Fam(\FinVect)$ (\secref{galois-slicing-auto-diff-via-fam:auto-diff})
   \end{itemize}
\item matrices over a commutative semiring; $\Mat(\Two)$ as worked example (\secref{matrix})
\item stable coproducts (\secref{stable-coproducts})
% \item slicing interpretation of the source language via a strong monad on the semantic category
\end{itemize}

\noindent Inductive types from polynomial endofunctors, and the correctness development that
depends on them (predicate systems, glueing, agreement of the underlying interpretation),
previously covered here, now have their own document (\texttt{mu-types.pdf}).

\noindent $\Set$ will usually be $\Setoid$ in the Agda implementation but we will gloss that detail for now.

\input{notes/preliminaries}
\input{notes/auto-diff}
\input{notes/stability}
\input{notes/cmon}
\input{notes/cmon-enriched}
\input{notes/biproduct}
\input{notes/useful-semi-additive-categories}
\input{notes/fam}
\input{notes/set-indexed-product}
\input{notes/grothendieck}
\input{notes/auto-diff-galois-slicing-via-fam}
\input{notes/matrix}
\input{notes/stable-coproducts}
% \input{notes/slicing-interpretation}  % moved to unused: monadic slicing not load-bearing (see git history)

\bibliographystyle{ACM-Reference-Format}
\bibliography{bib}

\end{document}