Galois Slicing as Automatic Differentiation

TL;DR

This paper draws an analogy between Galois slicing and automatic differentiation, reformulating it categorically to extend its application to quantitative analysis and clarify its underlying choices.

Contribution

It introduces a categorical reformulation of Galois slicing inspired by automatic differentiation, enabling extensions to interval analysis and deeper understanding.

Findings

Reformulation of Galois slicing using categorical semantics.

Extension of Galois slicing to quantitative interval analysis.

Clarification of implicit choices in existing Galois slicing implementations.

Abstract

Galois slicing is a technique for program slicing for provenance, developed by Perera and collaborators. Galois slicing aims to explain program executions by demonstrating how to track approximations of the input and output forwards and backwards along a particular execution. In this paper, we explore an analogy between Galois slicing and differentiable programming, seeing the implementation of forwards and backwards slicing as a kind of automatic differentiation. Using the CHAD approach to automatic differentiation due to V\'ak\'ar and collaborators, we reformulate Galois slicing via a categorical semantics. In doing so, we are able to explore extensions of the Galois slicing idea to quantitative interval analysis, and to clarify the implicit choices made in existing instantiations of this approach.