Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Galois Slicing as Automatic Differentiation

Robert Atkey, Roly Perera

TL;DR

The paper reframes Galois slicing as a categorical analogue of automatic differentiation, showing that forward and backward approximations across input/output lattices form a structured tangent-like calculus. By leveraging CHAD-style semantics and the Category of Families, it separates values from their approximation information to enable executable, total-language models, and extends to higher-order constructs via embedding results and GLR-type definability theorems. It also introduces interval-based and tagging monads to support quantitative and presence/absence approximation data, and provides an Agda-implemented executable model. The work connects provenance-driven slicing with differentiable-programming foundations, offering a modular, extensible framework for quantitative slicing and future directions in recursion, inductive types, and source-to-source translations with potential applications in explainable AI and data transparency.

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ákár 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.

Galois Slicing as Automatic Differentiation

TL;DR

The paper reframes Galois slicing as a categorical analogue of automatic differentiation, showing that forward and backward approximations across input/output lattices form a structured tangent-like calculus. By leveraging CHAD-style semantics and the Category of Families, it separates values from their approximation information to enable executable, total-language models, and extends to higher-order constructs via embedding results and GLR-type definability theorems. It also introduces interval-based and tagging monads to support quantitative and presence/absence approximation data, and provides an Agda-implemented executable model. The work connects provenance-driven slicing with differentiable-programming foundations, offering a modular, extensible framework for quantitative slicing and future directions in recursion, inductive types, and source-to-source translations with potential applications in explainable AI and data transparency.

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ákár 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.

Paper Structure

This paper contains 42 sections, 18 theorems, 21 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Galois Program Slicing
  3. Galois Slicing and Automatic Differentiation
  4. Outline and Contributions
  5. Approximations as Tangents
  6. Manifolds, Smooth Functions, and Automatic Differentiation
  7. Stable Functions as Differentiable Functions
  8. Domains as a Qualitative Theory of Approximation
  9. Bounded Meets and Conditional Multiplicativity
  10. Stable functions and L-posets
  11. Summary
  12. Models of Galois Slicing for a Total Language
  13. The Category of Families Construction
  14. Categorical Properties of $\mathbf{Fam}(\mathcal{C})$
  15. Coproducts and Products
  16. ...and 27 more sections

Key Result

theorem 1

Bounded meet lattices and conditionally multiplicative functions form a category $\mathbf{CM}$. This category has products, coproducts, and exponentials.

Figures (3)

  • Figure 1: Syntax of types and terms
  • Figure 2: Well-typed terms over a signature $\Sigma$
  • Figure 3: Interpretation of types, contexts and terms

Theorems & Definitions (34)

  • Remark 1: Chain Rule
  • definition 1
  • definition 2
  • theorem 1
  • Remark 2: Chain Rule
  • definition 3: Stable function
  • definition 4: Galois connection
  • lemma 1
  • definition 5
  • lemma 2
  • ...and 24 more