change-structures.tex

% Toggle comments for preamble and topmatter to typeset in ACM style

%\input{preamble-standard}
\input{preamble-acm}

\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{stmaryrd}
\usepackage{todonotes}
\usepackage{etoolbox}
\usepackage{appendix}

% Packages where the order matters
\usepackage[safeinputenc,natbib=true]{biblatex}
\usepackage{cleveref}
\usepackage{hyperref}

\newcommand{\todoall}[1]{\todo[inline,color=black!30,author=All]{#1}}
\newcommand{\todokcg}[1]{\todo[inline,color=pink!60,author=Katriel]{#1}}
\newcommand{\todompj}[1]{\todo[inline,color=yellow!40,author=Michael]{#1}}
\newcommand{\todomario}[1]{\todo[inline,color=blue!40,author=Mario]{#1}}

\input{notation}

\newif\ifproofs
% Comment out to disable proofs
\proofstrue

\addbibresource{paper.bib}

\begin{document}

%\input{topmatter-standard}
\input{topmatter-acm}

\begin{abstract}
  Incremental computation has recently been studied using the concepts of \emph{change
  structures} and \emph{derivatives} of programs. The derivative of a program allows updating the output
  of a program based on a change to its input.

  We generalise change structures to a Cartesian closed category of \emph{change actions},
  and study their algebraic properties. We develop change actions for several common structures
  in computer science, including directed-complete partial orders and Boolean algebras.

  We then show how to compute derivatives of fixpoints, leading to a
  generic account of incremental \emph{evaluation} of Datalog,
  as well as incremental \emph{updating} of evaluated Datalog programs.
\end{abstract}

\title{Fixing incremental computation}
\subtitle{Derivatives for dcpos, fixpoints, and the semantics of Datalog}

\maketitle

\section{Introduction}
\label{sec:intro}

Consider the following classic Datalog program, which computes the transitive
closure of an edge relation $e$:
\begin{align*}
  tc(x, y) &\leftarrow e(x, y)\\
  tc(x, y) &\leftarrow e(x, z) \wedge tc(z, y)
\end{align*}

The semantics of Datalog tell us that the denotation of this program is the
least fixpoint of the rule $tc$. Kleene's Theorem tells us that we can reach
this by repeating applying the rule, starting from the empty relation. For example, supposing
that $e = \{ (1, 2), (3, 4), (5, 6) \}$:

\begin{center}
  \begin{tabular} {|c|c|c|}
    \hline
    Iteration & Newly deduced facts & Accumulated contents of $tc$ \\
    \hline
    1 & $\{ (1, 2)\}$ & $\{ (1, 2) \}$\\
    2 & $\{ (1,2), (3,4) \}$ & $\{ (1, 2), (3,4) \}$\\
    3 & $\{ (1,2), (3,4), (5,6) \}$ & $\{ (1, 2), (3,4), (5,6) \}$\\
    4 & $\{ (1,2), (3,4), (5,6) \}$ & $\{ (1, 2), (3,4), (5,6) \}$\\
    \hline 
  \end{tabular}
\end{center}

And then we have reached fixpoint, so we are done.

However, this process is quite wasteful. We deduced $(1,2)$ at every iteration,
even though we had already deduced it in the first iteration. In fact, for a
chain of $n$ such edges we will deduce $O(n^2)$ facts along the way.

The standard improvement to this is ``semi-naive'' evaluation, where we transform
the program into a \emph{delta} program that only deduces the new facts at each
iteration, which we gradually accumulate \autocite[See][section
13.1]{abiteboul1995foundations}.
\begin{align*}
  \Delta tc_{0}(x, y) &\leftarrow e(x, z)\\
  \Delta tc_{i+1}(x, y) &\leftarrow e(x, z) \wedge \Delta_i tc(z, y)\\
  tc_{0}(x, y) &\leftarrow e(x, z)\\
  tc_{i+1}(x, y) &\leftarrow tc_{i}(x,y) \vee \Delta_{i+1} tc(x,y)
\end{align*}

\begin{center}
  \begin{tabular} {|c|c|c|}
    \hline
    Iteration & Newly deduced facts & Accumulated contents of $tc$ \\
    \hline
    1 & $\{ (1, 2)\}$ & $\{ (1, 2) \}$\\
    2 & $\{ (3,4) \}$ & $\{ (1, 2), (3,4) \}$\\
    3 & $\{ (5,6) \}$ & $\{ (1, 2), (3,4), (5,6) \}$\\
    4 & $\{ \}$ & $\{ (1, 2), (3,4), (5,6) \}$\\
    \hline
  \end{tabular}
\end{center}

This is much better - we have turned a quadratic computation into a linear one.

But the delta rule translation works only for traditional Datalog. It is common to
liberalise the term syntax to support, say, disjunction, existential quantification, and parity-stratified
negation.\footnote{Parity-stratified negation means that recursive calls must
  appear under an even number of negations. This ensures that the rule remains
  monotone, so the least fixpoint semantics still exists.}

Then we can write programs like the following, where we compute whether all the
nodes in a subtree given by $child$ have some property $p$:
\begin{align*}
  treeProperty(x) &\leftarrow p(x) \wedge \neg \exists y . (child(x,y) \wedge \neg treeProperty(y))
\end{align*}

This is essentially a recursion through a \emph{universal} quantifier. We would
like to be able to use semi-naive evaluation for this rule too, but the simple delta
transformation does not produce a correct incremental program, and it is unclear how to extend it (and the
correctness proof) to handle such cases.

This is of more than theoretical interest - the research
in this paper was carried out at Semmle, which
makes heavy use of a commercial Datalog implementation
\autocites{semmleWebsite}{avgustinov2016ql}{sereni2008adding}{schafer2010type}.
Semmle's implementation includes parity-stratified negation, and other non-standard
features, so we are faced with a dilemma: either abandon the new language
features, or abandon incremental computation.

There is a piece of folkloric knowledge in the Datalog community that hints at a
solution: the semi-naive translation of a rule corresponds to the
\emph{derivative} of that rule \autocites{bancilhon1986naive}[section
3.2.2]{bancilhon1986amateur}. The idea of performing incremental computation using derivatives has been
studied recently by \textcite{cai2014changes}, who give an account using
\emph{change structures}. They use this to provide a framework for incrementally evaluating lambda calculus programs.

However, \citeauthor{cai2014changes}'s work isn't directly applicable to Datalog: the tricky part
of Datalog's semantics is the \emph{fixpoint}, and we need some addtional theory to tell us how to
handle incremental evaluation of fixpoint computations.\footnote{In fact, we can prove these
results for fixpoint computations over dcpos in general, which opens up the
possibility of using these result in domain theory, which uses fixpoints to
represent recursion in programming language semantics.}

This paper bridges that gap. We start by generalizing change structures to
\emph{change actions} (\cref{sec:changeActions}). Change actions are weaker than change structures, but
have nice categorical properties (\cref{sec:category}), and exist for more structures.

We then show how to compute fixpoints incrementally, and also how to perform
incremental updates of already computed fixpoint expressions, given a change to
the function of which the fixpoint is taken (\cref{sec:fixpoints}).

Finally, we put all this together into a generic account of incremental
computation and update of Datalog programs, showing how to handle 
language constructs such as negation, disjunction, and additional well-behaved
extensions (\cref{sec:datalog}). This provides the world's first incremental
evaluation and update mechanism for Datalog that can handle arbitrary additional
term constructs (\cref{sec:extensions}).

\section{Change actions}
\label{sec:changeActions}

The core concept we will work with is a \emph{change action}. A change action is
a set along with a set of \emph{changes} that can be ``applied'' to elements of
the base set using an operator $\cplus$ (pronounced ``smush''). We also require
some structure on the changes themselves: they must form a \emph{monoid action}
on the base set.\footnote{The requirement that the change set be a monoid is convenient but in
  fact inessential: given any set with an action on the base set, we can take the
  free monoid over the action set to obtain a monoid action.}

\begin{defn}[Change actions]
  A \emph{change action} is defined as:

  \begin{displaymath}
    \cstr{A} \defeq \cstruct{A}{\changes{A}}{\cplus}
  \end{displaymath}

  where $A$ is a set, $(\changes{A}, \splus, \mzero)$ is a monoid, and $\cplus$ gives a monoid action on $A$.

  We will call $A$ the base set, and $\changes{A}$ the change set of the change
  action. We may abbreviate $\cstruct{A}{\changes{A}}{\cplus}$ to $\cstr{A}_\cplus$.
\end{defn}

The fact that the change set is a monoid action gives us a reason to think that
change actions are an adequate representation of changes: any set of
transformations on the base set which is closed under composition can be
represented as a monoid action, so we are able to capture all of these as change actions.

The primary motivation for change actions is that they let us define
\emph{derivatives} for functions.

\begin{defn}[Derivatives]
  A \emph{derivative} of a function $f: \cstr{A}_\cplus \rightarrow \cstr{B}_\cpluss$ is a function $\derive{f}: A \times \changes{A} \rightarrow
  \changes{B}$ such that
  \begin{displaymath}
    f(a \cplus \change{a}) = f(a) \cpluss \derive{f}(a, \change{a})
  \end{displaymath}

  A function which has a derivative is called \emph{differentiable}.
\end{defn}

Derivatives need not be unique, in general, so we will speak of ``a''
derivative.\footnote{In several places we will need to pick an arbitrary
  derivative for some construction. In general this needs the Axiom of Choice,
  but in most practical cases we will want to have a computable derivative
  operator for our domain, which alleviates the problem. In addition, thin
  change actions (\cref{sec:thin}) have unique derivatives.}

Derivatives capture the essence of incremental computation: given the value of a
function at a point, and a change to that point, they tell you how to compute
the new value of the function.

The choice of the name ``derivative'' is also not a coincidence. While these
derivatives do not look quite like derivatives in real analysis, they \emph{do}
bear a strong resemblance to derivatives in other areas (such as synthetic differential geometry), and
they satisfy the standard chain rule.

\begin{thm}[The Chain Rule]
  Let $f: \cstr{A}_\cplus \rightarrow \cstr{B}_\cpluss$, $g: \cstr{B}_\cpluss \rightarrow \cstr{C}_\cplusss$ be differentiable functions. Then $g \circ f$ is also
  differentiable, with derivative given by
  \begin{displaymath}
    \derive{(g \circ f)}(x, \change{x}) = \derive{g}\left(f(x), \derive{f}(x, \change{x})\right)
  \end{displaymath}
  or, in curried form
  \begin{displaymath}
    \derive{(g \circ f)}(x)(\change{x}) = \derive{g}(f(x)) \circ \derive{f}(x)
  \end{displaymath}
\end{thm}

Here are some recurring examples of changes actions:
\begin{itemize}
  \item $\cstr{A}_\discrete \defeq \cstruct{A}{\emptyset}{\emptyset}$ is the discrete change action on any base set.
  \item $\cstr{A}_\Rightarrow \defeq \cstruct{A}{A^A}{\ev}$, where $A^A$ denotes the exponential object and $\ev$ is the evaluation map.
  \item $[A]$, the type of lists (or streams) of elements of type $A$, has a
    change structure over concatenation ($\doubleplus$): $\cstruct{[A]}{[A]}{\doubleplus}$.
  \item $\{A\}$, the type of sets, has change actions $\cstruct{\{A\}}{\{A\}}{\cup}$, $\cstruct{\{A\}}{\{A\}}{\cap}$.
\end{itemize}

Indeed, any monoid $(A, \splus)$ can be seen as a change action
$\cstruct{A}{A}{\splus}$, and the final two examples are instances of this. Many practical change actions
can be constructed in this way. In particular, for any change action $\cstruct{A}{\changes{A}}{\cplus}$,
$\cstruct{\changes{A}}{\changes{A}}{\splus}$ is also a change action. This means
that we don't have to do any extra work to talk about higher derivatives of
functions - we can always take $\changes{\changes{A}} = \changes{A}$.

Many other notions in computer science can be naturally understood in terms of change actions, e.g. databases
and database updates, files and diffs, Git repositories and commits, even video compression
algorithms that encode a frame as a series of changes to the previous frame.

\subsection{Complete change actions and minus operators}

Complete change actions are an important class of change actions, because they
have changes between \emph{any} two values in the base set.

\begin{defn}[Complete change actions]
  A change action is \emph{complete} if for any $a, b \in A$, there is
  a change $\change{a} \in \changes{A}$ such that $a \cplus \change{a} = b$.
\end{defn}

Complete change actions have convenient ``minus operators'' that allow us to
compute the difference between two values.

\begin{defn}[Minus operator]
  A \emph{minus operator} is a function $\cminus: A \times A \rightarrow \changes{A}$ such that $a \cplus (b \cminus a) = b$.
\end{defn}

\begin{prop}[Completeness equivalences]
  Let $\cstr{A}$ be a change action. Then the following are equivalent:
  \begin{itemize}
    \item $\cstr{A}$ is complete.
    \item The monoid action of $\cplus$ on $A$ is transitive.
    \item There is a minus operator on $\cstr{A}$.
    \item Any function from any change action into $\cstr{A}$ is differentiable.
  \end{itemize}
\end{prop}

This last property is of the utmost importance, since we are often concerned with the differentiability
of functions.

\begin{defn}[Minus derivative]
  Given a minus operator $\cminus$, we have a derivative for any function $f$,
  defined as
  \begin{displaymath}
    \derive{f}_\cminus(a, \change{a}) \defeq f(a \cplus \change{a}) \cminus f(a)
  \end{displaymath}
\end{defn}

\subsection{Thin change actions}
\label{sec:thin}

There can be multiple changes representing the difference
between two elements. This is true for many change actions, but the change
actions for which there \emph{is} only one such change are particularly
well-behaved, so it's worth naming them.

\begin{defn}[Thin change actions]
  A change action is \emph{thin} if whenever $a \cplus \change{a}
  = a \cplus \change{b}$ for some $a \in A$, it is the case that $\change{a} = \change{b}$.
\end{defn}

Many change actions are not thin, for example $\cstruct{\NN}{\ZZ}{+}$ (as $0 + (-1)
= 0 + (-2)$ in $\NN$).

\begin{prop}[Thin equivalences]
  Let $\cstr{A}$ be a change action. Then the following are equivalent.
  \begin{itemize}
    \item $\cstr{A}$ is thin.
    \item The monoid action of $\cplus$ on $A$ is free.
    \item If $\cstr{A}$ has a minus operator $\cminus$, then $(a \cplus \change{a})
      \cminus a = \change{a}$.
  \end{itemize}
\end{prop}

Thinness gives us uniqueness of derivatives:

\begin{prop}
  Let $\cstr{B}$ be a thin change action, and $f: \cstr{A} \rightarrow \cstr{B}$. Then $f$ has at
  most one derivative.

  Conversely, if $\textrm{id}: \cstr{B} \rightarrow \cstr{B}$ has exactly one derivative, then
  $B$ is thin.
\end{prop}

\section{The category of change actions}
\label{sec:category}

We are arguing that change actions provide a good model for incremental
computation in general. That means we want to be able to easily construct change
actions over the wide variety of datatypes that we actually use in programming.

We can do this by showing that the category of change actions has the usual
useful constructions: products, coproducts, and exponentials. These are the
building blocks from which we create our datatypes, and they will also be useful
for our proofs in \cref{sec:fixpoints}: in particular, the \emph{evaluation map}
$\ev$ that we get from exponentials will turn out to be differentiable, and its
derivative has a deep connection to the incremental evaluation of functions (\cref{prop:incrementalization}).

\begin{defn}[Category of change actions]
  We define the category $\cat{CAct}$ of change actions. The objects are
  change actions and the morphisms are differentiable functions. 
\end{defn}

\subsection{Equivalence with PreOrd}

There is a natural preorder on the base set of a change action, given by reachability
under the action:

\begin{defn}[Reachability order]
  $a \reachOrder b$ iff there is a $\change{a} \in \changes{A}$ such that $a \cplus
  \change{a} = b$.
\end{defn}

We can characterize many of the properties of change actions in terms of the reachability order,
which suggests a connection between $\cat{CAct}$ and the category of preorders, $\cat{PreOrd}$.

\begin{prop}
  A function is differentiable iff it is monotone with respect to the
  reachability order. 
\end{prop}

\begin{corollary}
  Two change actions are isomorphic iff their posets under the reachability
  order are isomorphic.
\end{corollary}

\begin{corollary}
  Any function from a discrete change action or into a complete change
  action is differentiable.
\end{corollary}

Indeed, the correspondence between a change action and its reachability preorder gives rise to
a (full and faithful) functor $\reach : \cat{CAct} \rightarrow \cat{PreOrd}$ that acts as the
identity on morphisms.

Conversely, any preorder $\leq$ on some set $A$ induces a change action
$\cstr{A}_\leq \defeq \cstruct{A}{\leq^\star}{\cplus_\star}$.
The action $\cplus_\star$ is defined as the extension of $\cplus_\leq$ to the free
monoid $\leq^\star$, where $\cplus_\leq$ is defined as:
\[
\begin{aligned}
   \cplus_\leq &: (A \times \leq) \rightarrow A&\\
   a \cplus_\leq (b, c) &\defeq
     \begin{cases}
     c&\text{ if $a = b$}\\
     b&\text{ otherwise}
     \end{cases}
\end{aligned}
\]

The mapping to $\cstr{A}_\leq$ gives rise to a (full and faithful) functor
$\direct : \cat{PreOrd} \rightarrow \cat{CAct}$, again acting as the identity on morphisms.

These two functors are in fact enough to give us an equivalence between the categories
$\cat{CAct}$ and $\cat{PreOrd}$.

\begin{thm}[Equivalence of $\cat{CAct}$, $\cat{PreOrd}$]
  The functor $\reach$ from $\cat{CAct}$ to $\cat{PreOrd}$ together with the
  functor $\direct$ in the opposite direction form an equivalence of categories.
\end{thm}
\ifproofs
\begin{proof}
  See \cref{prf:preordEquivalence}.
\end{proof}
\fi

Since $\cat{PreOrd}$ is topological over $\cat{Set}$ \autocite[][Chapter V]{adamek2004abstract}, 
(and hence complete and co-complete) and also an exponential ideal of $\cat{Cat}$
(and hence Cartesian closed), this gives us a proof of the existence of limits, colimits, and exponentials in $\cat{CAct}$.

\begin{corollary}
  The category $\cat{CAct}$ has all limits, colimits and exponential objects.
\end{corollary}

\subsection{Explicit constructions}

Having shown that $\cat{CAct}$ is equivalent to $\cat{PreOrd}$ it may seem
redundant to give explicit recipes for constructing products, coproducts, and exponentials.
However, we can give constructions that are much nicer than the ones
which we get via $\cat{PreOrd}$, which is important for using them in
practical computation.

\begin{prop}[Products]
  Let $\cstr{A} = \cstruct{A}{\changes{A}}{\cplus}$ and $\cstr{B} =
  \cstruct{B}{\changes{B}}{\cpluss}$ be change actions.

  Then $\cstr{A} \times \cstr{B} \defeq \cstruct{A \times B}{\changes{A} \times
  \changes{B}}{\cplus \times \cpluss}$ is their categorical product.
\end{prop}
\ifproofs
\begin{proof}
  See \cref{prf:products}.
\end{proof}
\fi

\begin{prop}[Coproducts]
  Let $\cstr{A} = \cstruct{A}{\changes{A}}{\cplus}$ and $\cstr{B} =
  \cstruct{B}{\changes{B}}{\cpluss}$ be change actions.

  Then $\cstr{A} + \cstr{B} \defeq \cstruct{A + B}{\changes{A} \times
  \changes{B}}{\cplusvee}$ is their categorical coproduct, with $\cplusvee$ defined as:
  \begin{align*}
    i_1 a \cplusvee (\change{a}, \change{b}) &\defeq \iota_1 (a \cplus \change{a})\\
    i_2 b \cplusvee (\change{a}, \change{b}) &\defeq \iota_2 (b \cplus \change{b})
  \end{align*}
\end{prop}
\ifproofs
\begin{proof}
  See \cref{prf:coproducts}.
\end{proof}
\fi

\begin{prop}[Exponentials]
\label{prop:exponentials}
  Let $\cstr{A}_\cplus$ and $\cstr{B}_\cpluss$ be change actions. We will say a map 
  $\change{f} : (\cstr{A} \rightarrow \cstr{B}) \rightarrow (\cstr{A} \rightarrow \cstr{B})$ 
  is \emph{pointwise $\reachOrder$-increasing} iff, for every $f : \cstr{A} \rightarrow \cstr{B}$
  and $a \in \cstr{A}$, it is the case that $f(a) \reachOrder \change{f}(f)(a)$.
  We will denote the set of pointwise $\reachOrder$-increasing functions by $\rightarrow_{\reachOrder}$.
  \todompj{Why can't we just say ``increasing with respect to the reachability
    order lifted to functions''?}
  \todomario{We can, but I thought it might be more clear to write it explicitly - feel free
    to change it}

  Then $\cstruct{\cstr{A} \rightarrow \cstr{B}}
    {(\cstr{A} \rightarrow \cstr{B}) \rightarrow_{\reachOrder} (\cstr{A} \rightarrow \cstr{B})}
    {\lambda f . \lambda \change{f} . \change{f}(f)}$
  is a change action with base
  set $\cstr{A} \rightarrow \cstr{B}$, with monoidal structure given by function composition.
  Furthermore, it is the exponential object $\cstr{B}^{\cstr{A}}$ in $\cat{CAct}$.
\end{prop}
\ifproofs
\begin{proof}
  First, we note that, if $f : \cstr{A} \rightarrow \cstr{B}$, $\change{f} \in \changes{(\cstr{A} \rightarrow \cstr{B})}$
  and $a \in \cstr{A}$, since $\change{f}$ is pointwise $\reachOrder$-increasing, $\change{f}(f)(a)$ is reachable
  from $f(a)$, and thus there is some $\change{b} \in \changes{B}$ satisfying $f(a) \cplus \change{b} = \change{f}(f)(a)$.
  We will often abuse the notation and use $\change{f}_\Delta(f)(a)$ to refer such a change (although, in general, the Axiom
  of Choice is necessary to find such a $\change{b}$).

  \todomario{this is terrible and I hate it}
  \todompj{Agreed}

  Furthermore, if $f, g : \cstr{A} \rightarrow \cstr{B}$ and for all $a$ we have $f(a) \reachOrder g(a)$, then there exists
  some function change $\change{gf}$ sending $f$ to $g$ (it suffices to pick the change that maps $f$ to $g$ and every other
  differentiable map to itself).

  We are now ready to proceed with the proof. The evaluation map is, as expected, identical to its definition in $\cat{Set}$:
  \begin{align*}
    &\ev : (\cstr{A} \rightarrow \cstr{B}) \times \cstr{A} \rightarrow \cstr{B}\\
    &\ev((f, a)) \defeq f(a)
  \end{align*}

  We need first to show that it is differentiable: this is straightforward to check. Indeed, suppose 
  $a \in \changes{A}, f : \cstr{A} \rightarrow \cstr{B}, \change{a} \in \changes{A}, \change{f} \in \changes{(\cstr{A} \rightarrow \cstr{B})}$.
  Then, for $f'$ an arbitrary derivative of $f$, let:
  \begin{align*}
    &\derive{\ev} : (((\cstr{A} \rightarrow \cstr{B}) \times \cstr{A}) \times (\changes{(\cstr{A} \rightarrow \cstr{B})} \times \changes{A})) \rightarrow \changes{B}\\
    &\derive{\ev}((f, a), (\change{f}, \change{a})) \defeq \derive{f}(a, \change{a}) \cdot \change{f}_\Delta(f)(a \cplus \change{a})
  \end{align*}

  Then $\derive{\ev}$ is a derivative of the evaluation map $\ev$:
  \begin{itemize}
    \item[ ]$\ev((f, a) \cplus (\change{f}, \change{a}))$
    \item[=]\{ definition of $\ev$\}\\
    $\ev(\change{f}(f), a \cplus \change{a})$
    \item[=]\{ definition of $\changes{\cstr{A} \rightarrow \cstr{B}}$\}\\
    $\change{f}(f)(a \cplus \change{a})$
    \item[=]\{ $\change{f}$ is pointwise $\reachOrder$-increasing\}\\
    $f(a \cplus \change{a}) \cplus \change{f}_\Delta(f)(a \cplus \change{a})$
    \item[=]\{ differentiability of $f$\}\\
    $f(a) \cplus [ f'(a, \change{a})\cdot \change{f}_\Delta(f)(a \cplus \change{a}) ]$
    \item[=]\{ definition of $\ev$\}\\
    $\ev(f, a) \cplus \ev'((f, a), (\change{f}, \change{a}))$
  \end{itemize}

  It remains to prove that a function $f : \cstr{A} \times \cstr{B} \rightarrow \cstr{C}$ is differentiable iff its curried
  version $\curry{f} : \cstr{A} \rightarrow \cstr{C}^{\cstr{B}}$ is.
  First, suppose $f$ is differentiable, and let $\change{a} \in \changes{A}$. Then 
  \begin{itemize}
  \item[ ]$\curry{f}(a \cplus \change{a})$
  \item[=]\{ definition of $\curry{f}$\}\\
  $\lambda b . f(a \cplus \change{a}, b)$
  \item[=]\{ differentiability of $f$\}\\
  $\lambda b . f(a, b) \cplus \derive{f}((a, b), (\change{a}, \mzero))$
  \end{itemize}
  We note that $\curry{f}(a \cplus \change{a})$ is differentiable, and $\curry{f}(a)(b) \reachOrder \curry{f}(a \cplus \change{a})(b)$,
  hence there is some function change $\change{f}_{a, \change{a}}$ mapping $\curry{f}(a)$ to $\curry{f}(a \cplus \change{a})$. The map
  $\lambda a . \lambda \change{a} . \change{f}_{a, \change{a}}$ is, then, a derivative of $\curry{f}$.

  Conversely, suppose $\curry{f} : \cstr{A} \rightarrow \cstr{C}^{\cstr{B}}$ is differentiable, let $(a, b) \in \cstr{A} \times \cstr{B}$
  and let $(\change{a}, \change{b}) \in \changes{A} \times \changes{B}$. Then:
  \begin{itemize}
    \item[ ]$f((a, b) \cplus (\change{a}, \change{b}))$
    \item[=]\{ definition of $\cplus$ on products\}\\
    $f((a \cplus \change{a}, b \cplus \change{b}))$
    \item[=]\{ definition of $\curry{f}$\}\\
    $\curry{f}(a \cplus \change{a})(b \cplus \change{b})$
    \item[=]\{ differentiability of $\curry{f}$\}\\
    $(\curry{f}(a) \cplus \derive{(\curry{f})}(a, \change{a}))(b \cplus \change{b})$
    \item[=]\{ $\derive{(\curry{f})}(a, \change{a})$ is pointwise $\reachOrder$-increasing \}\\
    $\curry{f}(a)(b \cplus \change{b}) \cplus \derive{(\curry{f})}(a, \change{a})_\Delta(\curry{f}(a), b \cplus \change{b})$
    \item[=]\{ differentiability of $\curry{f}(a)$\}\\
    $\curry{f}(a)(b) \cplus [ \derive{\curry{f}(a)}(b, \change{b}) \cdot \derive{(\curry{f})}(a, \change{a})_\Delta(\curry{f}(a), b \cplus \change{b}) ]$
    \item[=]\{ definition of $\curry{f}$\}\\
    $f(a, b) \cplus [ \derive{\curry{f}(a)}(b, \change{b}) \cdot \derive{(\curry{f})}(a, \change{a})_\Delta(\curry{f}(a), b \cplus \change{b}) ]$
  \end{itemize}
\end{proof}
\fi

The resulting change action is rather unwieldy and it's hard to perform actual computation on it. Fortunately, in many
cases, it is equivalent to a much simpler one.
\begin{lemma}[Pointwise function changes]
  Let $\cstr{B}$ be a change action. If $\cplus : B \times \changes{B} \rightarrow B$ is differentiable
  with respect to its first argument, then the change action
  $\cstruct{\cstr{A} \rightarrow \cstr{B}}{\cstr{A} \rightarrow \cstr{\changes{B}}}{\cplus_\rightarrow}$, with the action
  $\cplus_\rightarrow$ and the monoidal structure defined pointwise, is the exponential
  object $\cstr{B}^{\cstr{A}}$.
\end{lemma}
\ifproofs
\begin{proof}
  We prove first that $\cplus_\rightarrow$ is indeed a valid action, i.e. given functions $f : \cstr{A} \rightarrow \cstr{B}$
  and $\change{f} : A \rightarrow \changes{B}$, $f \cplus_\rightarrow \change{f}$ is differentiable.
  Letting $a \in A, \change{a} \in \changes{A}$, we have:
  \begin{itemize}
    \item[ ]$(f \cplus_\rightarrow \change{f})(a \cplus \change{a})$
    \item[=]$f (a \cplus \change{a}) \cplus \change{f}(a \cplus \change{a})$
    \item[=]$(f (a) \cplus \derive{f}(a, \change{a})) \cplus \change{f}(a \cplus \change{a})$
    \item[=]$(f (a) \cplus \change{f}(a \cplus \change{a})) \cplus \partial_1\cplus(f(a), \change{f}(a \cplus \change{a}))(\derive{f}(a, \change{a}))$
    \item[=]$(f (a) \cplus \change{f}(a)) \cplus (\derive{\change{f}}(a, \change{a}) \cdot \partial_1\cplus(f(a), \change{f}(a \cplus \change{a}))(\derive{f}(a, \change{a})))$
  \end{itemize}
  Thus $\lambda a . \lambda \change{a} .\derive{\change{f}}(a, \change{a}) \cdot \partial_1\cplus(f(a), \change{f}(a \cplus \change{a}))(\derive{f}(a, \change{a}))$
  is a derivative for $f \cplus \change{f}$.

  In order to show that it is isomorphic to the previous exponential structure, we prove that the induced
  reachability order is the same.
  \todomario{Nevermind, this is in fact false because the changes need to be differentiable but they may not! Quite a problem.}
  \todomario{The question boils down to whether there is always a differentiable derivative, which is tricky.}
\end{proof}
\fi

Derivatives of the evaluation map correspond to incremental evaluation of functions:

\begin{prop}[Incrementalization]
\label{prop:incrementalization}
  Let $f: \cstr{A} \rightarrow \cstr{B}$, $a \in A$, $\change{a} \in
  \changes{A}$, $\change{f} \in \changes{(A \rightarrow B)}$, and let
  $\derive{\ev}$ be a derivative of the evaluation map.

  Then
  \begin{displaymath}
    (f \cplus \change{f})(a \cplus \change{a}) = f(a) \cplus \derive{\ev}((f, a), (\change{f}, \change{a}))
  \end{displaymath}

\end{prop}

Conveniently, our proof of \cref{prop:exponentials} gives us actual derivatives for the evaluation map:

\todomario{Redo this!}
\begin{prop}[Derivatives of the evaluation map]
\label{prop:evDerivatives}
  Let $f: \cstr{A} \rightarrow \cstr{B}$, $a \in A$, $\change{a} \in
  \changes{A}$, $\change{f} \in \changes{(A \rightarrow B)}$.

  Then if $f$ is differentiable
  \begin{displaymath}
    \derive{\ev}_1 \defeq \derive{f}(a, \change{a}) \splus \change{f}(a \cplus \change{a})
  \end{displaymath}
  
  is a derivative for the evaluation map.

  Or, if $f \cplus \change{f}$ is differentiable
  \begin{displaymath}
    \derive{\ev}_2 \defeq \change{f}(a) \splus \derive{(f \cplus \change{f})}(a, \change{a})
  \end{displaymath}

  is a derivative for the evaluation map.
\end{prop}
\ifproofs
\begin{proof}
  The first is shown in the proof of \cref{prop:exponentials}, the second is
  similar but begins by taking the derivative of $f \cplus \change{f}$.
\end{proof}
\fi

\subsection{The category of thin change actions}

\begin{prop}
  The product $\cstr{A} \times \cstr{B}$ of change actions $\cstr{A}$ and $\cstr{B}$ is thin if and only if both $\cstr{A}$ and $\cstr{B}$ are.
  Furthermore, whenever $\cstr{A}$ and $\cstr{B}$ are complete, then so is $\cstr{A} \times \cstr{B}$.

  The exponential object $\cstr{A} \Rightarrow \cstr{B}$ of change actions $\cstr{A}$ and $\cstr{B}$ is thin if $\cstr{B}$ is.
  Furthermore, whenever $\cstr{B}$ is complete, then so is $\cstr{A} \Rightarrow \cstr{B}$.
\end{prop}

Thus, the category of thin change actions is Cartesian closed as well.

\section{Change actions over other structures}
\label{sec:moreStructures}

We are aiming to work over Boolean algebras with fixpoints, which is where we
will interpret Datalog. We will work up to that gradually, adding power as we
progress from posets, to directed-complete partial orders, and
finally to Boolean algebras.

\subsection{Posets}

If the base set of a change action is a poset, then this gives us a natural
order on the change set.

\begin{defn}[Change order]
  $\change{a} \changeOrder \change{b}$ iff for all $a \in A$ it is the case that $a \cplus \change{a} \leq a \cplus \change{b}$.
\end{defn}

If the change action is thin, then the order is antisymmetric, and a
full partial order.

Having a monotone order on the changes is very useful.

\begin{thm}[Sandwich lemma]
  \label{thm:sandwich}
  Let $\supderive{f}$ and $\subderive{f}$ be a derivatives for $f$, $\changeOrder$ be a preorder on $\changes{B}$ such that $\cplus$ is monotone with
  respect to it, and $g$ be such that

  \begin{displaymath}
    \supderive{f} \changeOrder g \changeOrder \subderive{f}
  \end{displaymath}

  Then $g$ is a derivative for $f$.
\end{thm}

If we have minimal and maximal derivatives then this gives us a full
characterisation of all the derivatives for a function.

\begin{thm}[Characterization of derivatives]
\label{thm:derivativeCharacterization}
  Let $\cstr{A}$ and $\cstr{B}$ be a change actions, let
  $f: \cstr{A} \rightarrow \cstr{B}$ be a function, and let $\subderiveM{f}$ and
  $\supderiveM{f}$ be minimal and maximal derivatives of $f$, respectively.
  Then the derivatives of $f$ are precisely
  the functions $\derive{f}$ such that
  \begin{displaymath}
    \subderiveM{f} \changeOrder \derive{f} \changeOrder \supderiveM{f}
  \end{displaymath}
\end{thm}
\ifproofs
\begin{proof}
  Follows easily from \cref{thm:sandwich} and minimality/maximality.
\end{proof}
\fi

This theorem gives us leeway when trying to pick a derivative: we can pick out the
bounds, and that tells us how much ``wiggle room'' we have. This is helpful
because some of the intermediary functions may be much easier to compute than
others, as we will see in \cref{sec:datalogDifferentiability}.

One way to get minimal and maximal derivatives is from minimal and maximal minus
operators (if we are in a complete change action).

\begin{defn}[Minus ordering]
  $\cminus_1 \minusOrder \cminus_2$ iff for all $a,b \in A$, $a \cminus_1 b
  \changeOrder a \cminus_2 b$.
\end{defn}

This implies an ordering on the corresponding derivatives: if $\cminus_1 \minusOrder \cminus_2$ then
$\derive{f}_{\cminus_1} \changeOrder \derive{f}_{\cminus_2}$.

Which gives us a correspondence between maximal minus operators and maximal derivatives.

\begin{prop}
  \label{prop:maximalMinusDerivatives}
  If $\cminus$ is a minimal (maximal) minus operator with respect to
  $\minusOrder$, then $\derive{f}_\cminus$ is a minimal (maximal) derivative.
\end{prop}

\subsection{Directed-complete partial orders}

Directed-complete partial orders give us the well known notion of
\emph{Scott-continuity}. We define \emph{continuous} change actions,
which are well-behaved with respect to continuity.

\begin{defn}[Continuous change actions]
  A change action $\cstr{A}$ is \emph{continuous} if
  \begin{itemize}
    \item $A$ and $\changes{A}$ are dcpos.
    \item $\cplus$ and $\splus$ are Scott-continuous in both arguments.
  \end{itemize}
\end{defn}

\begin{corollary}
  \label{cor:bottomPlusBottom}
  Let $\cstr{A}$ be a continuous change structure. Then $\bot_A \cplus
  \bot_{\changes{A}} = \bot_A$.
\end{corollary}
\ifproofs
\begin{proof}
  $\bot_{\changes{A}} \leq \mzero$, therefore
  \begin{displaymath}
    \bot_A \leq \bot_A \cplus \bot_{\changes{A}} \leq \bot_A \cplus \mzero = \bot_A
  \end{displaymath}
\end{proof}
\fi

We also have the following lemma (which is just a re-statement of a well-known
property of Scott-continuous functions, see e.g. \cite[Lemma~3.2.6]{abramsky1994domain}):

\begin{prop}[Distributivity of limits across arguments]
  \label{prop:distributivityLimit}
  A function $f : A \times B \rightarrow C$ is continuous iff it is continuous in each variable separately.
\end{prop}

A direct corollary of this property is the following result, reminiscent of a well-known theorem of calculus:

\begin{corollary}[Continuity of differentiation]
  \label{cor:diffContinuous}
  Let $\cstr{A}$, $\cstr{B}$ be change actions, with $\cstr{B}$ continuous and let $\{f_i\}$ and $\{\derive{f_i}\}$ be
  $I$-indexed directed families of functions in $A \rightarrow B$ and $A \times \changes{A} \rightarrow \changes{B}$.

  Then, if for every $i \in I$ is the case that $\derive{f_i}$ is a derivative of $f_i$, then $\sqcup_{i \in I} \{ \derive{f_i} \}$ is
  a derivative of $\sqcup_{i \in I} \{ f_i \}$.
\end{corollary}
\ifproofs
\begin{proof}
  It suffices to apply $\cplus$ and \cref{prop:distributivityLimit} to the directed families $\{ f_i(a) \}$ and
  $\{ \derive{f_i}(a, \change{a}) \}$.
\end{proof}
\fi

We also state the following additional fixpoint lemma. This is a specialization of
Becik's Theorem \autocite[][section 10.1]{winskel1993formal}, but it has a straightforward direct proof.

\begin{prop}[Factoring of fixpoints]
  \label{prop:factoringFixpoints}
  Let $A$ and $B$ be dcpos, $f : A \rightarrow A$ and $g: A \times B \rightarrow B$ be continuous, and let
  \begin{displaymath}
    h(a, b) \defeq (f(a), g(a, b))
  \end{displaymath}
  Then
  \begin{displaymath}
    \lfp(h) = (\lfp(f), \lfp(g(\lfp(f))))
  \end{displaymath}
\end{prop}
\ifproofs
\begin{proof}
  See \cref{prf:factoringFixpoints}.
\end{proof}
\fi

\subsection{Boolean algebras}

Boolean algebras have a complete, continuous change structure.

\begin{prop}
  Let $L$ be a Boolean algebra. Define
  \begin{displaymath}
    \cstr{L}_\superpose \defeq \cstruct{L}{L \times L}{\twist}
  \end{displaymath}
  where
  \begin{displaymath}
    a \twist (p, q) \defeq (a \vee p) \wedge \neg q
  \end{displaymath}
  and the monoid operator is
  \begin{displaymath}
    (p, q) \splus (r, s) \defeq ((p \wedge \neg q) \vee r, (q \wedge \neg r) \vee s)
  \end{displaymath}

  Then $\cstr{L}_\superpose$ is a complete, continuous change action on $L$.
\end{prop}
\ifproofs
\begin{proof}
  See \cref{prf:lsuperpose}.
\end{proof}
\fi

We can think of $\cstr{L}_\superpose$ as tracking changes as pairs of ``upwards'' and
``downwards'' changes, where the monoid action simply applies both.\footnote{We
  can, in fact, make it precise that $\cstr{L}_\superpose$ is an ``upwards''
  and ``downwards'' change action glued together, but here it is simpler to
  just go directly to the useful change action.}  

Boolean algebras also have concrete definitions for maximal and minimal minus
operators.

\begin{prop}
  Let $L$ be a Boolean algebra. Then
  \begin{align*}
    a \cminus_\bot b &= (a \wedge \neg b, b)\\
    a \cminus_\top b &= (a, b \wedge \neg a)
  \end{align*}

  define minimal and maximal minus operators.
\end{prop}

In particular, \cref{thm:derivativeCharacterization} along with
\cref{prop:maximalMinusDerivatives} give us bounds for
all the derivatives on Boolean algebras:

\begin{corollary}
\label{cor:booleanCharacterization}
  Let $L$ be a Boolean algebra with the $\cstr{L}_\superpose$ change action, $A$ be
  a change action, and $f: A \rightarrow
  L$ a function. Then the derivatives of $f$ are precisely those functions
  $\derive{f}$ such that
  \begin{displaymath}
    f(a \cplus \change{a}) \cminus_\bot f(a)
    \changeOrder
    \derive{f}(a, \change{a})
    \changeOrder
    f(a \cplus \change{a}) \cminus_\top f(a)
  \end{displaymath}
\end{corollary}

This makes \cref{thm:derivativeCharacterization} actually usable in practice, as
we have concrete definitions for our bounds (which, again, we will make use of in \cref{sec:datalogDifferentiability}).

\section{Fixpoints}
\label{sec:fixpoints}

In directed-complete partial orders we can define a least fixpoint operator $\lfp$ in terms of the
iteration function $\iter$:
\begin{align*}
  &\lfp : (A \rightarrow A) \rightarrow A\\
  &\lfp \defeq \sqcup_{n \in \NN} \{ \iter_n \}\\
  &\iter : (A \rightarrow A) \times \NN \rightarrow A\\
  &\iter(f, n) \defeq f^n(\bot)
\end{align*}

The iteration function is going to be the basis for everything in this section:
we can differentiate it with respect to $n$, and this will give us a way to get
to the next iteration incrementally; and we can differentiate it with respect to
$f$, and this will give us a way to get from iterating $f$ to iterating $f
\cplus \change{f}$.\footnote{The sharp-eyed reader may have noticed that we
  could also differentiate $\iter$ with respect to the base point (which we have
  given as just $\bot$).}

To avoid confusion, we shall write $\iter_f$ when we are holding $f$ constant,
and $\iter_n$ when we are holding $n$ constant.

\subsection{Incremental computation of fixpoints}

The following theorems provide a
generalization of semi-naive evaluation to any differentiable function over a
continuous change action. We will want to apply this to the semantics of
Datalog, for which we will need to differentiate its semantics. We will see the
details of how to do this in \cref{sec:datalogDifferentiability}.

Since we are trying to incrementalize the iterative step, we start by taking the
derivative of $\iter$ with respect to $n$.

\begin{prop}[Derivative of the iteration map with respect to $n$]
  Let $\cstr{A}$ be a complete change structure. Then $\iter_f$ is differentiable, and a derivative is given by:
  \begin{align*}
    &\derive{\iter_f}: \NN \times \changes{\NN} \rightarrow \changes{A}\\
    &\derive{\iter_f}(0, m) \defeq \iter_f(m) \cminus \bot\\
    &\derive{\iter_f}(n+1, m) \defeq \derive{f}(\iter_f(n), \derive{\iter_f}(n, m))
  \end{align*}
\end{prop}
\ifproofs
\begin{proof}
  See \cref{prf:iterDerivativesN}.
\end{proof}
\fi

We can then compute $\derive{\iter_f(n)}$ along with $\iter_f(n)$ via mutual recursion.
We want to do this by computing a fixpoint, so we can rewrite it as a recurrence
relation:
\begin{align*}
  &\nextiter_f : (A, \changes{A}) \rightarrow (A, \changes{A})\\
  &\nextiter_f (\bot, \bot) \defeq (\bot, f(\bot) \cminus \bot)\\
  &\nextiter_f (a, \change{a}) \defeq (a \cplus \change{a}, \derive{f}(a, \change{a}))
\end{align*}
Which has the property that
\begin{align*}
  &\nextiter_f^n (\bot, \bot) = (\iter_f(n), \derive{\iter_f}(n, 1))
\end{align*}

\begin{thm}[Incremental computation of least fixpoints]
\label{thm:diffFP}
  Let $\cstr{A}$ be a continuous change action, $f: \cstr{A} \rightarrow
  \cstr{A}$ be continuous and differentiable.

  Then $\lfp(f) = \pi_1(\sqcup_{n \in \NN}(\nextiter_f^n(\bot)))$.
\end{thm}
\ifproofs
\begin{proof}
  See \cref{prf:fixpointIter}.
\end{proof}
\fi

This gives us a way to compute our fixpoint incrementally, by adding successive
changes to our accumulator until we reach fixpoint.

Note that we have \emph{not} taken the fixpoint of $\nextiter_f$, since it is
not continuous. So while this allows us to compute fixpoints that converge in
finitely many steps, it does not let us handle the infinite case.

\subsection{Derivatives of fixpoints}
\label{sec:fixpointDerivatives}

The previous section has shown us how to use derivatives to compute fixpoints
more efficiently, but we might also want to take the derivative of the fixpoint
operator itself. The typical case for this will be where we have some fixpoint
\begin{displaymath}
  \fixpoint (\lambda X . F(E, X))
\end{displaymath}
and we now wish to apply a change to $E$ and compute
\begin{displaymath}
  \fixpoint (\lambda X . F(E \cplus \change{E}, X))
\end{displaymath}

This amounts to applying a change to the \emph{function} whose fixpoint we are taking.

In Datalog this would allow us to update a recursively defined relation given an
update one of its non-recursive dependencies, or the base extensional database.
For example, we might want to take the transitive closure relation
and update it by changing the edge relation $e$.

However, this requires us to have a derivative for the fixpoint operator
$\fixpoint$ with respect to the function which it takes the fixpoint of.
We can get quite close in the general case, but to get a precise
derivative we'll need to do a bit more work.

\begin{defn}
  Let $\cstr{A}$ be a change structure, $\fixpoint_A$ a fixpoint operator, and
  $\derive{\ev}$ be a derivative of the evaluation map.

  Then we define
  \begin{align*}
    &\adjust : (A \rightarrow A) \times \changes{(A \rightarrow A)} \rightarrow (\changes{A} \rightarrow \changes{A})\\
    &\adjust(f, \change{f}) \defeq \lambda\ \change{a} . \derive{\ev}((f,
    \fixpoint_A(f), (\change{f}, \change{a})))\\
    &\derive{\fixpoint_A} : (A \rightarrow A) \times \changes{(A \rightarrow A)} \rightarrow \changes{A}\\
    &\derive{\fixpoint_A}(f, \change{f}) \defeq \fixpoint_{\changes{A}}(\adjust(f, \change{f}))
  \end{align*}
\end{defn}

\begin{thm}[Pseudo-derivatives of fixpoints]
\label{thm:fixpointDiff}
  Let
  \begin{itemize}
    \item $\cstr{A}$ be a change action
    \item $\fixpoint : (\cstr{A} \rightarrow \cstr{A}) \rightarrow \cstr{A}$ be a fixpoint operator
    \item $f: \cstr{A} \rightarrow \cstr{A}$ be a differentiable function
    \item $\change{f} \in \changes{(A \rightarrow A)}$ be a function change 
    \item $\derive{\ev}$ be a derivative of the evaluation map
  \end{itemize}

  Then a change $\change{w} \in \Delta A$ satisfies
  the equation:
  \begin{equation}\label{eqn:fixcondition}
    \change{w} = \adjust(f, \change{f})(\change{w})
  \end{equation}
  if and only if $\fixpoint(f) \cplus \change{w}$ is a fixpoint of $f \cplus \change{f}$.

  In particular, $\fixpoint(f) \cplus \derive{\fixpoint}(f, \change{f})$ is a fixpoint
  of $f \cplus \change{f}$.
\end{thm}
\ifproofs
\begin{proof}
  See \cref{prf:fixpointPseudoDerivatives}.
\end{proof}
\fi

This is not enough to give us a true derivative, because we have only shown
that $\fixpoint(f) \cplus \derive{\fixpoint}(f, \change{f})$ computes \emph{a} fixpoint, not necessarily
the same one computed by $\fixpoint{(f \cplus \change{f})}$.

However, if we restrict ourselves to directed-complete partial orders, least
fixpoints, and continuous change actions, then $\derive{\lfp}$ \emph{is} a
derivative of $\lfp$. This is not too onerous a restriction, since this is
the setting in which we normally compute fixpoints anyway.

Since $\lfp$ is characterized as the limit of a chain of functions,
\cref{cor:diffContinuous} suggests a way to compute its derivative. If we can find a derivative
$\derive{\iter_n}$ of each iteration map 
such that the resulting set $\{ \derive{\iter_n} \}$ is directed, then $\sqcup_{n \in \NN}\derive{\iter_n}$ will be a derivative of $\lfp$.

These correspond to the other derivative of $\iter$ - this time with respect to
$f$. While we are differentiating with respect to $f$, we are still going to
need to define our derivatives inductively in terms of $n$.

\begin{prop}[Derivative of the iteration map with respect to $f$]
  $\iter_n$ is differentiable and a derivative is given by:
  \begin{align*}
    &\derive{\iter_n} : (A \rightarrow A) \times \changes{(A \rightarrow A)} \rightarrow \changes{A}\\
    &\derive{\iter_0} (f, \change{f}) \defeq \bot_{\changes{A}}\\
    &\derive{\iter_{n+1}} (f, \change{f}) \defeq \derive{\ev}((f, \iter_n(f)), (\change{f}, \derive{\iter_n}(f, \change{f})))
  \end{align*}
\end{prop}
\ifproofs
\begin{proof}
  See \cref{prf:iterDerivativesF}.
\end{proof}
\fi

As before, we can now compute $\derive{\iter_n}$ together with $\iter_n$ by
mutual recursion. 
\begin{align*}
  &\nextiter_{f, \change{f}} : (A, \changes{A}) \rightarrow (A, \changes{A})\\
  &\nextiter_{f, \change{f}} (a, \change{a}) \defeq (f(a), \derive{\ev}((f, a), (\change{f}, \change{a})))
\end{align*}
Which has the property that
\begin{align*}
  &\nextiter_{f, \change{f}}^n (\bot, \bot) = (\iter_n(f), \derive{\iter_n}(f, \change{f}))
\end{align*}

In fact, the recursion here is not \emph{mutual}: $\iter_n$ does
not depend on $\derive{\iter_n}$. However, writing it in this way makes it
amenable to computation by fixpoint, and we are about to see that we can avoid
the recomputation of $\iter_n$ by using \cref{prop:factoringFixpoints}.

\begin{thm}[Derivatives of least fixpoint operators]
  \label{thm:leastFixpointDiff}
  Let
  \begin{itemize}
    \item $\cstr{A}$ be a continuous change action
    \item $f : \cstr{A} \rightarrow \cstr{A}$ be a continuous, differentiable function
    \item $\change{f} \in A \rightarrow \changes{A}$ be a function change
    \item $\derive{\ev}$ be a derivative of the evaluation map, continuous with
      respect to $a$ and $\change{a}$.
  \end{itemize}
  Then $\derive{\lfp}$ is a derivative of $\lfp$.
\end{thm}
\ifproofs
\begin{proof}
  See \cref{prf:fixpointDerivatives}.
\end{proof}
\fi

Computing the derivative still requires computing a fixpoint (over the change
lattice), but this may still be significantly less expensive than the
alternative ``update strategy'': throw everything away and start
again (which will itself require a fixpoint computation).

\section{Datalog}
\label{sec:datalog}

Datalog is a well-known simple logic programming language \autocite[See][part D]{abiteboul1995foundations}.
It is also a textbook example of the need for incremental computation, since as we have seen
(\cref{sec:intro}) the naive computation of its semantics can be very expensive.

The aim of this section is to argue that by viewing the computation
of Datalog semantics as composed of differentiable functions we can
bring the machinery that we've developed so far to bear, and give a flexible
account of incremental evaluation. 

Firstly, however, we must show that we can see the semantics of Datalog in terms
of elements that we know how to handle: Boolean algebras and fixpoints.

\subsection{Denotational semantics}

Datalog is usually given a logical semantics wherein we look for models that
satisfy the program. We will instead give a simple denotational semantics that treats a Datalog
program as denoting a family of relations.

One obstacle to this approach is giving a denotation to negations. We adopt an
equivalent of the usual closed-world assumption to solve this.

\begin{defn}[Closed-world assumption and negation]
  There exists a universal relation $\universalRel$.

  Negation on relations is defined as
  \begin{displaymath}
    \neg R \defeq \universalRel \setminus R
  \end{displaymath}
\end{defn}

This makes $\Rel$ into a Boolean algebra.

\begin{defn}[Term semantics]
  A Datalog term $T$ denotes a function from its free relation variables to
  $\Rel$, $\denote{\_} : \Term \rightarrow \Rel^n \rightarrow \Rel$

  $\denote{t}$ takes an argument $\overline{X} : \Rel^n$. However, this is
  passed down unchanged through all recursive calls, so we will leave it
  implicit except where it is used.

  \begin{align*}
    \denote{R_j} &\defeq X_j \tag{where $X_i$ is the $i$th element of $\overline{X}$}\\
    \denote{T \wedge U} &\defeq \denote{T} \cap \denote{U}\\
    \denote{T \vee U} &\defeq \denote{T} \cup \denote{U}\\
    \denote{\exists x. T} &\defeq \pi_x(\denote{T})\\
    \denote{\neg T} &\defeq \neg \denote{T}\\
    \denote{x=y} &\defeq \Delta(x, y) \tag{ where $\Delta$ is the diagonal relation}
  \end{align*}
\end{defn}

Since $\Rel$ is a Boolean algebra, and so is $\Rel^n$, the denotation
functions of terms are functions between Boolean algebras.

\begin{defn}[Immediate consequence operator]
  Given a program $\mathcal{P} = \overline{P}$, the immediate consequence operator $\consq: \Rel^n \rightarrow \Rel^n$ is defined as follows:
  \begin{displaymath}
    \consq(\overline{R}) = \overline{\denote{P_j}(\overline{R})} \tag{where $P_j$ is the $j$th component of $\overline{P}$}
  \end{displaymath}
\end{defn}

That is, given a value for the program, we pass in all the relations
to the denotation of each predicate, to get a new product of relations.

\begin{defn}[Program semantics]
  The semantics of a program $\mathcal{P}$ is defined to be
  \begin{displaymath}
    \denote{\mathcal{P}} \defeq \lfp_{\Rel^n}(\consq)
  \end{displaymath}
  and may be calculated by iterative application of $\consq$ to $\bot$ until
  fixpoint is reached.
\end{defn}

Whether or not this program semantics exists will depend on whether the fixpoint
exists. Typically this is ensured by constraining the program such that $\consq$
is monotone (or, in the context of a dcpo, continuous). We can be agnostic
about this when applying \cref{thm:diffFP}, but we it will be a requirement to
apply \cref{thm:leastFixpointDiff}.

\subsection{Differentiability of Datalog semantics}
\label{sec:datalogDifferentiability}

In order to apply the machinery we have developed, we need the semantics $\denote{\_}$ to
be differentiable. However, it is a function on Boolean algebras, and we know
that the $\cstr{L}_\superpose$ change action is complete, so in fact we know that
$\denote{\_}$ must be differentiable.

However, this does not mean that we have a \emph{good} derivative for
$\denote{\_}$. The derivative that we know we have for complete change actions
is quite bad:
\begin{displaymath}
  \derive{f}(a, \change{a}) = f(a \cplus \change{a}) \cminus f(a)
\end{displaymath}
Naively computed, this requires \emph{more} work than evaluating $f(a \cplus \change{a})$ directly!

However, \cref{cor:booleanCharacterization} gives us a range of derivatives to
choose from, and we can optimize within that range to find one that satisfies
our constraints.

In the case of Datalog, the change ordering on the change action also
corresponds to the size of the derivative as a pair of relations. The minimal
derivative contains precisely the elements that are newly added or removed,
whereas the maximal derivative contains all the elements that have \emph{ever}
been added or removed. This means that \cref{cor:booleanCharacterization} allows
us to \emph{approximate} the most precise derivative while still being
guaranteed that the result is sound.\footnote{The idea of using an approximation
to the precise derivative, and a soundness condition, appears in \textcite{bancilhon1986amateur}.}

There is also the question of how to compute the derivative. Fortunately, the
maximal and minimal minus operators are actually representable as pairs of terms
in our Datalog, and so we can compute the derivative via a pair of terms that
satisfy those bounds, allowing us to reuse our machinery for evaluating Datalog
terms.\footnote{Indeed, if this process is occurring in an optimizing compiler,
  the derivative terms can themselves be optimized. This is likely to be
  beneficial, since the initial terms may be quite complex.}

This does give us additional constraints that the derivative terms must satisfy:
for example, we need to be able to evaluate them; and we may wish to pick terms that will be easy or cheap
for our evaluation engine to evaluate, even if the results are larger.

The upshot of these considerations is that the optimal choice of derivatives is likely
to be quite dependent on the precise variant of Datalog being evaluated, and the
specifics of the evaluation engine. Here is one possibility.\footnote{These are
  the rules actually in use at Semmle. We arrived at them by starting with the
  minimal derivative and then simplifying and weakening it while preserving the
  bound given by the maximal derivative.}

\newcommand{\bothdiff}{\diamond}
\newcommand{\bothchanges}{\rho}
\begin{thm}[Concrete Datalog term derivatives]
\label{thm:concreteDatalog}
  We give two mutually recursive definitions,
  $\updiff: \Term \rightarrow \changes{\Rel^n} \rightarrow \changes{\Rel}$ and
  $\downdiff: \Term \rightarrow \changes{\Rel^n} \rightarrow \changes{\Rel}$, such
  that $\updiff(t) \times \downdiff(t)$ is a derivative for the semantics of a Datalog term $t$.

  $\updiff$ and $\downdiff$ define functions which take an argument
  $\bothchanges: \changes{\Rel^n}$ . However, this argument is passed down
  unchanged through all recursive calls until it is used, so we shall leave it
  implicit until it is used.

  Additionally, let
  \begin{displaymath}
    \diamond X \defeq X \twist (\updiff X, \downdiff X)
  \end{displaymath}
  in the following.

  \begin{align*}
  \updiff(\bot) &\defeq \bot\\
  \updiff(\top) &\defeq \bot\\
  \updiff(R_j) &\defeq \updiff R_j \tag{where $\updiff R_j$ is the first component of the $j$th element of $\bothchanges$}\\
  \updiff(T\vee U) &\defeq \updiff T \vee \updiff U\\
  \updiff(T\wedge U) &\defeq (\updiff T\wedge \bothdiff U)
                           \vee
                           (\updiff U \wedge \bothdiff T)\\
  \updiff(\neg T) &\defeq \downdiff T\\
  \updiff(\exists x.T) &\defeq \exists x.\updiff T\\
    \\
  \downdiff\bot &\defeq \bot\\
  \downdiff\top &\defeq \bot\\
  \downdiff R &\defeq \downdiff R_j \tag{where $\downdiff R_j$ is the second component of the $j$th element of $\bothchanges$}\\
  \downdiff(T\vee U) &\defeq (\downdiff T \wedge \neg \bothdiff U)
                           \vee
                           (\downdiff U \wedge \neg \bothdiff T)\\
  \downdiff(T\wedge U) &\defeq (\downdiff T\wedge U) \vee (T \wedge \downdiff U)\\
  \downdiff(\neg T) &\defeq \updiff T\\
  \downdiff(\exists x.T) &\defeq \exists x.\downdiff T \wedge \neg \exists x.\bothdiff T
  \end{align*}
\end{thm}
\ifproofs
\begin{proof}
  Straightforward structural induction.
\end{proof}
\fi

There is a symmetry between the cases for $\wedge$ and $\vee$ between $\updiff$
and $\downdiff$, but the cases for $\exists$ look quite different.
This is because we have chosen a dialect of Datalog without a primitive universal quantifier.
If we did have one, its cases would be dual to those for $\exists$, namely:
\begin{align*}
\updiff(\forall x.T) &= \exists x. \updiff T \wedge \forall x. \bothdiff T\\
\downdiff(\forall x.T) &= \forall x. \downdiff T
\end{align*}

We can now give a derivative for our $treeProperty$ program!

Here is the upwards difference:
\begin{align*}
  \updiff treeProperty(x) \leftarrow & p(x)\\
    &\wedge
    \exists y. (
      child(x, y)
      \wedge
      \updiff treeProperty(y)
    )\\
    &\wedge 
    \neg \exists y. (
      child(x, y)
      \wedge
      \neg \bothdiff treeProperty(y)
    )
\end{align*}

This is not especially easy to compute. The third conjunct amounts to
recomputing the whole of the recursive part. The second conjunct gives us a
guard: we only need to do the work if there is \emph{some} change in the body of
our existential. This shows that our derivatives aren't a panacea: it is simply \emph{hard} to compute
downwards differences for $\exists$ (and, equivalently, upwards differences for
$\forall$). However, we can do significantly better than nothing, and the
difficulty is largely isolated to difficult subterms.

\subsection{Incremental evaluation of Datalog}

We can easily extend a derivative for the term semantics to a derivative for $\consq$.

\begin{corollary}
\label{corollary:consqDiff}
  $\consq$ is differentiable.
\end{corollary}

Putting this together with the results from \cref{sec:fixpoints}, we get two results.

\begin{thm}[Differential evaluation of Datalog semantics]
\label{thm:diffEval}
  Datalog program semantics can be evaluated incrementally.
\end{thm}
\ifproofs
\begin{proof}
  Corollary of \cref{thm:diffFP} and \cref{corollary:consqDiff}.
\end{proof}
\fi

This is a generalization of semi-naive evaluation to use any derivative for the
term semantics.

\begin{thm}[Differential update of Datalog semantics]
\label{thm:diffUpdate}
  Datalog program semantics can be incrementally updated with changes to non-recursive relations.
\end{thm}
\ifproofs
\begin{proof}
  Corollary of \cref{thm:leastFixpointDiff} and \cref{corollary:consqDiff}.
\end{proof}
\fi

This is a generalization of the view-update problem for Datalog, including recursive views.

\subsection{Extensions to Datalog}
\label{sec:extensions}

Our formulation of Datalog term semantics and differential evaluation is quite
generic and composable, so it is relatively easy to extend the language with new
term constructs.

A new term construct must have:
\begin{itemize}
  \item An interpretation as a function on its free relation variables.
  \item An implementation of $\updiff$ and $\downdiff$.
\end{itemize}

These are very easy conditions to satisfy. The former is needed for the construct to even
make sense, and because we are using the complete change structure
$\cstr{L}_\superpose$, the latter can \emph{always} be satisfied by using the maximal or
minimal derivative. This justifies our claim that we can support
\emph{arbitrary} additional term constructs: although the maximal and minimal
derivatives are likely to be very bad derivatives, having them
available as options means that we can still work them into the overall process.
Even if we have a term construct which we cannot find a good derivative for, we only lose incremental
evaluation for those subterms, and not for anything else.

This does not say anything about monotonicity. New term constructs may
be required to be monotone if they are to participate in recursion, but we are
interested in derivatives even for non-monotone terms because they allow us to
use \cref{thm:diffUpdate}.

This is important in practice for Semmle's variant of Datalog, which includes
aggregation and other primitives with interesting derivatives. 

\section{Related work}

\subsection{Change actions and incremental computation}

\subsubsection{Change structures}
\label{sec:relatedChangeStructures}

The seminal paper in this area is \textcite{cai2014changes}. We use the notions
defined in that excellent paper heavily, but we deviate in three regards: the
inclusion of minus operators, the nature of function changes, and the use of
dependent types.

We have omitted minus operators from our definition because
there are many interesting change actions that are not complete and so cannot
have a minus operator (for example, $\cstruct{\ZZ}{\ZZ}{+}$ does, but $\cstruct{\ZZ}{\NN}{+}$ does
not). Where we can find a change structure with a minus operator, often we are
forced to use unwieldy representations for change sets, and
\citeauthor{cai2014changes} cite this as their reason for using a dependently
typed type of changes. For example, the change actions described before on sets and lists are clearly
useful for incremental computation on streams, yet they do not admit minus operators - instead, one would
be forced to work with e.g. multisets admitting negative arities, as \citeauthor{cai2014changes} do.

Our notion of function changes is different to \citeauthor{cai2014changes}'s.
Our function changes (when well behaved) correspond to what \citeauthor{cai2014changes} call as
\emph{pointwise differences} (for the subsequent paragraphs we shall adopt
their terminology) \autocite[See][section 2.2]{cai2014changes}. As they point out, you can reconstruct their
function changes from pointwise changes and derivatives, so the two formulations
are equivalent. This gives us the following correspondences:
\begin{itemize}
  \item Our \emph{derivatives of the evaluation map} are \citeauthor{cai2014changes}'s \emph{function changes}
  \item Our \emph{function changes} are (usually) \citeauthor{cai2014changes}'s \emph{pointwise differences}
\end{itemize}

Our equivalent to \citeauthor{cai2014changes}'s ``Incrementalization'' lemma
(\cref{prop:incrementalization}) is an important lemma for us as well - it is used
crucially in \cref{sec:fixpointDerivatives}. However, the incremental computation part of
the lemma simply follows from the fact that we are using the derivative of the
evaluation map - any derivative will do. It is then a further fact that we can
find actual definitions for this derivative (\cref{prop:evDerivatives}).

\citeauthor{cai2014changes} say that the reason they use their function changes instead of pointwise
differences as the primitive notion is that a function change has access to more
information, and so is easier to optimize \autocite[][section
2.2]{cai2014changes}. In contrast, we have not found pointwise differences to be
significantly harder to work with in practice, or more difficult to compute (at least in our implementations
for Datalog). On the other hand, from a theoretical point of view our function changes correspond to the
exponentials that we get from the categorical equivalence with $\cat{PreOrd}$,
and (when we can use them) pointwise differences are easier to work with.

However, this is largely an issue of presentation: if it turned out that it was
significantly easier to work with function changes rather than pointwise
changes, then there is nothing preventing a ``plugin'' for \citeauthor{cai2014changes}'s system providing the
ability to create either or both.

The equivalence of our presentations means that our work should be compatible
with ILC. The rules we give in \cref{sec:datalogDifferentiability} are more or
less a ``change semantics'' for Datalog \autocite[See][section
3.5]{cai2014changes}. In particular, this is likely to be of interest for languages like
Datafun (see \cref{sec:embeddingDatalog} below) which embed Datlog or logic programming behaviour within a broader
programming context.

Since we do not require a minus operator to always be defined, we do not need
our changes to depend on the value being changed. However,
if we want to extend our formalism to synthetic differential geometry we \emph{will} need
dependently typed changes, since the type of the tangent space at a point is
dependent on the point.

In fact, a slightly different dependently-typed formulation arises if we consider changes
to be indexed \emph{both} by the source and the target. This means
thinking of our base set as a category, with changes $\Delta_a^b$ between $a$
and $b$ as morphisms between $a$ and $b$. In this interpretation, a function is
differentiable iff it is a functor (i.e. has an action (its derivative) taking a
change in $\Delta_a^b$ to one in $\Delta_{f(a)}^{f(b)}$). The correspondence
with $\cat{PreOrd}$ still holds, but it is with the 2-categorical version of
$\cat{PreOrd}$ where each poset is viewed as a category.

This approach seems promising, although it introduces some
interesting additional restrictions (functoriality implies $\derive{f}(\change{a} \splus \change{b}) =
\derive{f}(\change{a}) \splus \derive{f}(\change{b})$; naturality of function
changes implies that the two derivatives from \cref{prop:evDerivatives} are equal). These seem
reasonable, but we don't know exactly what the consequences would be.

\citeauthor{cai2014changes} also discuss \emph{self-maintainable} derivatives,
which are derivatives that do not use their first argument, and hence can be
evaluated using only the change argument. These appear in traditional semi-naive
evaluation of Datalog too: \emph{linear} Datalog rules which have only a single
recursive reference can be converted into delta rules which only mention the
delta of the recursive predicate \autocite[See][section
13.1]{abiteboul1995foundations}. For our more complex derivatives it is less
easy to tell whether a term will have a self-maintainable derivative or not, but
the consequences of non-linearity remain very noticeable in practice.
Self-maintainable derivatives are also interesting because they produce 
\emph{commutative} changes (since they do not depend on the base point), and so can be
evaluated in parallel for multiple incoming changes. This seems worthy of
further study, and could provide a model for CRDTs.

\subsubsection{S-acts}

S-acts and their categorical structure have received a fair amount of attention
over the years (\textcite{kilp2000monoids} is a good
overview). However, there is a key difference between our $\cat{CAct}$ and the category of
S-acts $\cat{SAct}$: the objects of $\cat{SAct}$ all maintain the same monoid
structure, whereas we are interested in changing both the base set \emph{and} the structure of the act.

There are similarities: if we compare the definition of an ``act-preserving''
homeomorphism in $\cat{SAct} $\autocite[See][]{kilp2000monoids} we can see that the structure is
quite similar to the definition of differentiability:
\begin{displaymath}
  f(a \splus s) = f(a) \splus s
\end{displaymath}
as opposed to
\begin{displaymath}
  f(a \cplus s) = f(a) \cplus \derive{f}(a, s)
\end{displaymath}
That is, we use $\derive{f}$ to transform the action element into the new
monoid, whereas in $\cat{SAct}$ it simply remains the same.

In fact, $\cat{SAct}$ is a subcategory of $\cat{CAct}$, where we only
consider change actions with change set $S$, and the only functions are those
whose derivative is $\lambda a. \lambda d. d$.

\subsubsection{Derivatives of fixpoints}

\textcite{arntz2017fixpoints} gives a derivative operator for fixpoints based on
the framework in \textcite{cai2014changes}. However, since we have different
notions of function changes, the result is inapplicable as
stated. In addition, we require a somewhat different set of conditions, in particular we
don't require our changes to always be increasing.

\subsection{Datalog}

\subsubsection{Incremental evaluation}

The earliest explication of semi-naive evaluation as a derivative process
appears in \textcite{bancilhon1986naive}. The idea of using an approximate derivative
and the requisite soundness condition appears as a throwaway comment in
\textcite[][section 3.2.2]{bancilhon1986amateur}, and as far as we know nobody has since
developed that approach.

As far as we know, traditional semi-naive is the state of
the art in incremental, bottom-up, Datalog evaluation, and there are no strategies that
accommodate additional language features such as parity-stratified negation and aggregates.

\subsubsection{Incremental updates}

There is existing literature on incremental updates to relational algebra
expressions. In particular \textcite{griffin1997improved} following
\textcite{qian1991incremental} shows the essential insight that it is necessary to
track both an ``upwards'' and a ``downwards'' difference, and produces a set of
rules that look quite similar to those we derive in \cref{thm:concreteDatalog}.

Where our presentation improves over \citeauthor{griffin1997improved} is mainly in
the genericity of the presentation. Our machinery works for a wider variety of
algebraic structures, and it is clear how the parts of the proof work together
to produce the result. In addition, it is easy to see how to extend the proofs
to cover additional language constructs.

\citeauthor{griffin1997improved} are interested in \emph{minimal} changes. These correspond to
minimal derivatives in the sense of \cref{cor:booleanCharacterization}. However,
while minimality (or proximity to minimality) is desirable (since it decreases
the size of the derivatives as relations), it is important to be able to trade
it off against other considerations. For example, at
Semmle we use the derivatives given in \cref{thm:concreteDatalog}, which are not minimal.

There are some inessential points of difference as well: we work on Datalog,
rather than relational algebra; and we use set semantics rather than bag
semantics. This is largely a matter of convenience: Datalog is an easier
language to work with, and set semantics allows a much wider range of valid
simplifications. However, all the same machinery applies to relational algebra
with bag semantics, it is simply necessary to produce a valid version of \cref{thm:concreteDatalog}.

We also solve the problem of updating \emph{recursive} expressions. As far as we
know, this is unsolved in general. Most of the attempts to solve it have
focussed on Datalog rather than relational algebra, since Datalog is designed to
make heavy use of recursion.

Several approaches
\autocites{gupta1993maintaining}{harrison1992maintenance}
make use of a common tactic: one can get to the new fixed
point by starting from \emph{any} point below it, and then iterating the
semantics again to fixpoint. The approach, then, is to find a way to delete as
few tuples as possible to get below the new fixpoint, and then iterate again
(possibly using an incremental version of the semantics).

This is a perfectly reasonable approach, and given a good, domain-specific,
means of getting below the fixpoint, they can be quite efficient (likely more
efficient than our method). The main defect of these approaches is that they
\emph{are} domain specific, and hence inflexible with respect to changes in the
language or structure, whereas our approach is quite generic.

Other approaches \autocites{dong2000incremental}{urpi1992method} consider only
restricted subsets of Datalog, or incur other substantial constraints, and our results
are thus significantly more general.

\subsubsection{Embedding Datalog}
\label{sec:embeddingDatalog}

Datafun (\textcite{arntz2016datafun}) is a functional programming language that embeds
Datalog, allowing significant improvements in genericity, such as the use of
higher-order functions. Since we have directly defined a change action and
derivative operator for Datalog, our work could be used as a ``plugin'' in the sense
of \citeauthor{cai2014changes}, allowing Datafun to compute its internal fixpoints
incrementally, but also allowing Datafun expressions to be fully incrementally updated.

\section{Conclusions and future work}

We have presented change actions and their properties, and provided novel
strategies for incrementally evaluating fixpoints and the semantics of Datalog.

Our work opens several avenues for future investigation.

Firstly, the abstract definition of change actions could be extended to a
dependently-typed version as gestured towards in
\cref{sec:relatedChangeStructures}. We believe this might smooth over many of
the technical difficulties, and also provide a structure that is compatible with
synthetic differential geometry, where the type of the tangent bundle at a point
depends on the point.

Secondly, the theory of change actions on domains could be developed. Since
domains are commonly used to define programming language semantics, this could
open up opportunities for incremental evaluation of many programming languages,
even those that do not fit into the model of \citeauthor{cai2014changes}'s ILC.

Finally, combining our concrete Datalog derivatives with a system similar to ILC
in a language such as Datafun would be an exciting demonstration of the compositional
power of this approach.

\printbibliography


\appendix
\appendixpage
\section{Proofs}

\subsection{The category of change actions}

\begin{proof}
  \label{prf:preordEquivalence}
  On one direction, if $U$ is a preorder, it's trivial to check that $\reach (\direct (U)) = U$.

  On the other direction, we need to find a natural isomorphism between $\direct \circ \reach$
  and the identity functor. First, we note that the base set for the change action
  $\direct(\reach(A))$ is the same as the base set for $\cstr{A}$.

  We claim that the desired natural isomorphism is given by the
  the identity on the base sets. It remains to prove that the identities
  $id_A : \cstr{A} \rightarrow \direct(\reach(A))$ and
  $id_{A_{\reachOrder}} : \direct(\reach(A)) \rightarrow \cstr{A}$
  are indeed differentiable in both directions.

  In one direction, a derivative is given by
  \begin{displaymath}
    \derive{id}_A(a, \change{a}) \defeq (a, a \cplus \change{a})
  \end{displaymath}
  Conversely, let $(a, b) \in \reachOrder$. By definition of $\reachOrder$, there is some
  $\change{}_{(a, b)} \in \changes{A}$ satisfying $a \cplus \change{}_{(a,b)} = b$.
  This gives a definition for the derivative of the identity on pairs:
  \begin{displaymath}
    \derive{id}_{A_{\reachOrder}}(a, (a, b)) \defeq \change{}_{(a, b)}
  \end{displaymath}
  which can be extended freely to the whole change set $\reachOrder^\star$. 
\end{proof}

\begin{proof}
  \label{prf:products}
  Let $\cstr{Y}$ be a change action, and $f_1: \cstr{Y} \rightarrow \cstr{A}$, $f_2: \cstr{Y}
  \rightarrow \cstr{B}$ be morphisms.

  Then the product morphism in $\cat{Set}$, $\pair{f_1}{f_2}$ is the product
  morphism in $\cat{CAct}$. It can easily be
  shown that $\pair{\derive{f_1}}{\derive{f_2}}$ is a derivative of $\pair{f_1}{f_2}$,
  hence $\pair{f_1}{f_2}$ is a morphism in $\cat{SAct}$.

  Commutativity and uniqueness follow from the corresponding properties of the
  product in the $\cat{Set}$.
\end{proof}

\begin{proof}
  \label{prf:coproducts}
  Let $\cstr{Y}$ be a change action, and $f_1 : \cstr{A} \rightarrow \cstr{Y}$, $f_2 : \cstr{B}
  \rightarrow \cstr{Y}$ be differentiable functions.

  As before, it suffices to prove that the universal function $[f_1, f_2]$ in $\cat{Set}$ is a differentiable
  function from $\cstruct{A + B}{\changes{A} \times \changes{B}}{\cplusvee}$ into $Y$. It's easy to see
  that the following morphism is a derivative:
  \begin{align*}
    \derive{[f_1, f_2]} (i_1 a, (\change{a}, \change{b})) &\defeq f_1'(a, \change{a})\\
    \derive{[f_1, f_2]} (i_2 b, (\change{a}, \change{b})) &\defeq f_2'(b, \change{b})
  \end{align*}
\end{proof}

\subsection{Change actions over other structures}

\begin{proof}
  \label{prf:factoringFixpoints}
  Let
  \begin{displaymath}
    p(b) = (\lfp f, g(\lfp(f), b))
  \end{displaymath}
  Then $h(h^i(\bot)) \leq p(p^i(\bot)))$ (by simple induction), and so by continuity
  \begin{displaymath}
    \lfp(h) = \sqcup_{i \in \NN} h^i(\bot) \leq \sqcup_{i \in \NN} p^i(\bot) = \lfp(p)
  \end{displaymath}

  But $h(\lfp(p)) = \lfp(p)$, so $\lfp(h) \leq \lfp(p)$, since $\lfp(h)$ is least.

  Hence $\lfp(h) = \lfp(p) = (\lfp(f), \lfp(g(\lfp(f))))$.
\end{proof}

\begin{proof}
  \label{prf:lsuperpose}
  We show that the monoid action property holds:
  \begin{align*}
    &a \twist \left[(p, q) \splus (r, s)\right]\\
    &= a \twist ((p \wedge \neg q) \vee r, (q \wedge \neg r) \vee s)\\
    &= \left(
      a \vee
      \left(
        \left(
          p \wedge \neg q
        \right)
        \vee r
      \right)
    \right)
    \wedge \neg
    \left(
      \left(
        q \wedge \neg r
      \right)
      \vee s
    \right)\\
    &= \left(
      \left(
        \left(
          a \vee p
        \right)
        \wedge
        \left(
          a \vee \neg q
        \right)
      \right)
      \vee r
    \right)
    \wedge
    \left(
      \neg q \vee r
    \right)
    \wedge
    \neg s
    \tag{distributing $\vee$ over $\wedge$, applying de Morgan rules}\\
    &= \left(
      \left(
        \left(
          a \vee p
        \right)
        \wedge
        \left(
          a \vee \neg q
        \right)
        \wedge
        \neg q
      \right)
      \vee r
    \right)
    \wedge
    \neg s
    \tag{un-distributing $\vee$ over $\wedge$ }\\
    &= \left(
      \left(
        \left(
          a \vee p
        \right)
        \wedge
        \neg q
      \right)
      \vee r
    \right)
    \wedge
    \neg s
    \tag{$(A \vee B) \wedge B = B$}\\
    &= a \twist (p, q) \twist (r, s)
  \end{align*}

  Completeness is easy to show.

  $L$ is a complete lattice, so certainly a dcpo. $\cstr{L}_\superpose$ is a
  dcpo with $\bigvee (p_i, q_i) \defeq (\bigvee p_i, \bigwedge q_i)$.

  Continuity of $\twist$ in its second argument:
  \begin{align*}
    &a \twist \bigvee (p_i, q_i)\\
    &= a \twist (\bigvee p_i, \bigwedge q_i)\\
    &= (a \vee \bigvee p_i) \wedge (\neg \bigwedge q_i)\\
    &= (a \vee \bigvee p_i) \wedge (\bigvee \neg q_i) \tag{applying de Morgan}\\
    &= \bigvee (a \vee p_i) \wedge \neg q_i \tag{$\vee$ and $\wedge$ are continuous}\\
    &= \bigvee a \twist (p_i, q_i)
  \end{align*}

  Continuity $\twist$ in its first argument and continuity of $\splus$ follow easily from their definitions and the continuity
  of $\vee$ and $\wedge$.
\end{proof}

\subsection{Fixpoints}

\begin{proof}
  \label{prf:iterDerivativesN}
  By induction on $n$. We show the inductive step.
  \begin{align*}
    &\iter_f((n+1) + m)\\
    &=f(\iter_f(n + m)) \tag{definition of $\iter_f$}\\
    &=f(\iter_f(n) \cplus \derive{\iter_f}(n, m)) \tag{by induction}\\
    &=\iter_f(n+1) \cplus \derive{f}(\iter_f(n), \derive{\iter_f}(n, m)) \tag{$f$ is differentiable, definition of $\iter_f$}
  \end{align*}
\end{proof}

\begin{proof}
  \label{prf:fixpointIter}
  \begin{align*}
    &\lfp(\iter_f)\\
    &=\sqcup_{n \in \NN} \iter_f(n)\\
    &=\sqcup_{n \in \NN} \pi_1 (\nextiter_f^n(\bot))\\
    &=\pi_1 (\sqcup_{n \in \NN} \nextiter_f^n(\bot)) \tag{$\pi_1$ is continuous}
  \end{align*}
\end{proof}

\begin{proof}
  \label{prf:fixpointPseudoDerivatives}
  Let $\change{w} \in \Delta A$ satisfy \cref{eqn:fixcondition}. Then
  \begin{align*}
    &(f \cplus \change{f})(\fixpoint_A(f) \cplus \change{w})\\
    &= f(\fixpoint(f))
    \cplus
    \adjust(f, \change{f})(\change{w})
    \tag{by \cref{prop:incrementalization}}\\
    &= \fixpoint(f)
    \cplus
    \change{w}
    \tag{rolling the fixpoint and \cref{eqn:fixcondition}}
  \end{align*}

  Hence $\fixpoint(f) \cplus \change{w}$ is a fixpoint of $f \cplus \change{f}$. The converse
  follows from reversing the direction of the proof.
\end{proof}

\begin{proof}
  \label{prf:iterDerivativesF}
  The base case follows from \cref{cor:bottomPlusBottom}.

  For the inductive step:
  \begin{align*}
    &\iter_{n+1}(f \cplus \change{f})\\
    &=(f \cplus \change{f})(\iter_{n}(f \cplus \change{f}))\\
    &= (f \cplus \change{f})(
        \iter_{n}(f)
        \cplus \derive{\iter_{n}}(f, \change{f})
      )
    \tag{ by induction}\\
    &= f(\iter_n(f)) \cplus \derive{\ev}((f, \iter_{n}(f)), (\change{f},
      \derive{\iter_{n}}(f, \change{f})))
    \tag{by \cref{prop:incrementalization}}\\
    & =\iter_{n+1}(f) \cplus \derive{\iter_{n+1}}(f, \change{f})))
  \end{align*}
\end{proof}

\begin{proof}
  \label{prf:fixpointDerivatives}
  $\derive{\iter_n}$ and $\nextiter_{f, \change{f}}$ are continuous since
  $\derive{\ev}$ and $f$ are.

  Hence the set $\{ \derive{\iter}_n \}$ is directed, and so $\sqcup_{i \in \NN}
  \derive{\iter_i}$ is indeed a derivative for $\lfp$.

  We now show that it is equivalent to $\derive{\lfp}$:
  \begin{align*}
    &\sqcup_{n \in \NN} \derive{\iter_n}(f, \change{f})\\
    &=\sqcup_{n \in \NN} \pi_2(\nextiter_{f, \change{f}}^n(\bot))\\
    &=\pi_2(\sqcup_{n \in \NN} \nextiter_{f, \change{f}}^n(\bot))) \tag{$\pi_2$ is continuous}\\
    &= \pi_2 (\lfp(\nextiter_{f, \change{f}})) \tag{$\nextiter_{f, \change{f}}$ is continuous, Kleene's Theorem}\\
    &= \pi_2 ((\lfp(f), \lfp (\lambda\ \change{a}. \derive{\ev}((f, \lfp f), (\change{f}, \change{a})))))
    \tag{by \cref{prop:factoringFixpoints}, and the definition of $\nextiter$}\\
    &= \pi_2 ((\lfp(f), \lfp(\adjust(f, \change{f})))\\
    &= \lfp(\adjust(f, \change{f}))\\
    &= \derive{\lfp}(f, \change{f})
  \end{align*}
\end{proof}

\end{document}