A Simple Differentiable Programming Language

TL;DR

This paper introduces a simple, expressive differentiable programming language with formal semantics, clarifying the relationship between implementation techniques and mathematical derivatives in automatic differentiation.

Contribution

It defines a small programming language with reverse-mode differentiation, providing both operational and denotational semantics and proving their equivalence.

Findings

Semantics of the language coincide, ensuring consistency.

Provides a formal foundation connecting implementation and mathematical derivatives.

Facilitates understanding of automatic differentiation in programming systems.

Abstract

Automatic differentiation plays a prominent role in scientific computing and in modern machine learning, often in the context of powerful programming systems. The relation of the various embodiments of automatic differentiation to the mathematical notion of derivative is not always entirely clear---discrepancies can arise, sometimes inadvertently. In order to study automatic differentiation in such programming contexts, we define a small but expressive programming language that includes a construct for reverse-mode differentiation. We give operational and denotational semantics for this language. The operational semantics employs popular implementation techniques, while the denotational semantics employs notions of differentiation familiar from real analysis. We establish that these semantics coincide.