approx-diff/main.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
83
84
85
86
87
88
89
90
91
92
93
\ifdefined\submissionmode
  \documentclass[acmsmall,screen,review,anonymous]{acmart}
\else
  \documentclass[acmsmall,screen,nonacm]{acmart}
\fi

\usepackage{tabularx}
\usepackage{bbm}
\usepackage{bbold}
\usepackage{booktabs}
\usepackage{enumitem}
\usepackage{mathpartir}
\usepackage{subcaption}
\usepackage{tikz-cd}
\usepackage{xspace}
% \finalmode (set by main-final.tex) renders the clean version.
\ifdefined\finalmode
  \usepackage[final,commandnameprefix=ifneeded,commentmarkup=footnote]{changes}
\else
  \usepackage[commandnameprefix=ifneeded,commentmarkup=footnote]{changes}
\fi
\usepackage{changebar}
\ifdefined\finalmode\nochangebars\fi

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

\input{macros}

\begin{document}

\title{Data Provenance as Automatic Differentiation}

\author{Robert Atkey}
\email{robert.atkey@strath.ac.uk}
\orcid{0000-0002-4414-5047}
\affiliation{%
  \institution{University of Strathclyde}
  \city{Glasgow}
  \country{UK}}

\author{Roly Perera}
\email{roly.perera@cl.cam.ac.uk}
\orcid{0000-0001-9249-9862}
\affiliation{%
  \institution{University of Cambridge}
  \city{Cambridge}
  \country{UK}
}
\additionalaffiliation{%
   \institution{University of Bristol}
   \city{Bristol}
   \country{UK}
}

\begin{abstract}
  Automatic differentiation (AD) computes the derivative of a program alongside the program itself,
  as a linear map between tangent spaces, propagated forwards or backwards along an execution. We present a
  semantic framework that models \emph{data provenance} via the same construction: taking scalars from a
  commutative semiring of dependency information rather than the real numbers, the derivative of a program
  becomes a linear map between spaces of approximations of its input and output. The choice of semiring
  determines the notion of provenance. Over the two-element Boolean algebra, the Jacobian of a program
  records which input positions each output position may depend on, and composing Jacobians forwards or
  backwards is \emph{dependency analysis} in the manner of forward- and reverse-mode AD. More generally, over
  distributive lattices the Jacobian and its transpose propagate dependency information forwards and
  backwards as a \emph{conjugate pair} of maps; when the lattice is a Boolean algebra, the two directions are
  moreover related by adjunction, recovering an approach called \emph{\GPS}. We interpret a higher-order total
  functional language in this framework, prove that every program of first-order type denotes such a Jacobian,
  and instantiate the semiring to obtain dependency tracking (Booleans), automatic differentiation (reals),
  and quantitative interval provenance (the tropical semiring) as examples. All results are formalised in
  Agda.
\end{abstract}
\maketitle

\input{main/introduction}
\input{main/approx-as-tangents}
\input{main/models}
\input{main/language}
\input{main/examples}
\input{main/definability}
\input{main/related-work}
\input{main/conclusion}

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

% \pagebreak
% \appendix
% \input{appendix/notes}

\end{document}