Data Provenance as Automatic Differentiation
This provides a foundational theoretical framework that unifies several previously separate concepts (provenance, AD, slicing) for programming language semantics, but the results are theoretical and not yet demonstrated at scale.
The paper shows that data provenance can be modeled using the same semantic framework as automatic differentiation, where the derivative of a program over a commutative semiring of dependency information becomes a linear map between approximations. This unifies dependency analysis, automatic differentiation, and quantitative provenance under a single construction, with all results formalized in Agda.
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 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 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 conjugate pair of maps; when the lattice is a Boolean algebra, the two directions are moreover related by adjunction, recovering an approach called Galois slicing. 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.