# Towards formalizing and extending differential programming using tangent categories

@inproceedings{Cruttwell2019TowardsFA, title={Towards formalizing and extending differential programming using tangent categories}, author={Geoff S. H. Cruttwell and Jonathan Gallagher and Benjamin MacAdam}, year={2019} }

This paper gives an interpretation of a simple differential programming language (over finite dimensional R vector spaces), into a setting derived from synthetic differential geometry (SDG). The main theorem of this paper is Theorem 5.6, where we establish that there is always an interpretation of our simple differential programming language into a category of partial maps of a well-adapted smooth topos that preserves the derivative and all the control structures of the differential programming… Expand

#### Tables from this paper

#### 5 Citations

Dioptics: a Common Generalization of Open Games and Gradient-Based Learners

- 2019

Compositional semantics have been shown for machine-learning algorithms [FST18] and open games [Hed18]; at SYCO 1, remarks were made noting the high degree of overlap in character and analogy between… Expand

Smart Choices and the Selection Monad

- Computer Science
- 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
- 2021

A small language is defined that supports decision-making abstraction, rewards, and probabilities, and three denotational semantics with auxiliary monads for reward and probability are given, and the two kinds of semantics coincide by proving adequacy theorems. Expand

Semantics for Automatic Differentiation Towards Probabilistic Programming Literature Review and Dissertation Proposal

- 2020

3 Literature review: Beyond Automatic Differentiation 7 3.1 Idea . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.2 Some common changes to the Gradient… Expand

Higher Order Automatic Differentiation of Higher Order Functions

- Computer Science
- ArXiv
- 2021

This work characterises a forward-mode AD method on a higher order language with algebraic data types as the unique structure preserving macro given a choice of derivatives for basic operations, and describes a rich semantics for differentiable programming, based on diffeological spaces. Expand

Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing

- Computer Science
- FoSSaCS
- 2020

It is shown that the characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces, and how the analysis extends to other AD methods by considering a continuation-based method. Expand

#### References

SHOWING 1-10 OF 40 REFERENCES

Differential Structure, Tangent Structure, and SDG

- Mathematics, Computer Science
- Appl. Categorical Struct.
- 2014

It is shown that tangent structures appropriately span a very wide range of definitions, from the syntactic and structural differentials arising in computer science and combinatorics, through the concrete manifolds of algebraic and differential geometry, and finally to the abstract definitions of synthetic differential geometry. Expand

Differential categories

- Mathematics, Computer Science
- Mathematical Structures in Computer Science
- 2006

The notion of a categorical model of the differential calculus is introduced, and it is shown that it captures the not-necessarily-closed fragment of Ehrhard–Regnier differential $\lambda$-calculus. Expand

A convenient differential category

- Mathematics, Computer Science
- ArXiv
- 2010

It is shown that the category of Mackey-complete, separated, topological convex bornological vector spaces and bornological linear maps is a differential category and will ultimately yield a wide variety of models of differential logics. Expand

Finiteness spaces

- Computer Science, Mathematics
- Mathematical Structures in Computer Science
- 2005

A new denotational model of linear logic based on the purely relational model, where webs are equipped with a notion of ‘finitary’ subsets satisfying a closure condition and proofs are interpreted as finitary sets is investigated. Expand

Tangent spaces and tangent bundles for diffeological spaces

- Mathematics
- 2014

We study how the notion of tangent space can be extended from smooth manifolds to diffeological spaces, which are generalizations of smooth manifolds that include singular spaces and… Expand

Differential Calculus over General Base Fields and Rings

- Mathematics
- 2004

Abstract We present an axiomatic approach to finite- and infinite-dimensional differential calculus over arbitrary infinite fields (and, more generally, suitable rings). The corresponding basic… Expand

Synthetic Differential Geometry

- Mathematics
- 1981

Preface to the second edition (2005) Preface to the first edition (1981) Part I. The Synthetic Ttheory: 1. Basic structure on the geometric line 2. Differential calculus 3. Taylor formulae - one… Expand

Restriction categories as enriched categories

- Computer Science, Mathematics
- Theor. Comput. Sci.
- 2014

It is shown that restriction categories can be seen as a kind of enriched category; this allows their theory to be studied by way of the enrichment and varying the base of this enrichment also allows the important notions of join and range restriction category to be understood in the same manner. Expand

On Köthe sequence spaces and linear logic

- Computer Science, Mathematics
- Mathematical Structures in Computer Science
- 2002

This work provides a simple setting in which typed λ-calculus and differential calculus can be combined and gives a few examples of computations. Expand

CARTESIAN DIFFERENTIAL CATEGORIES

- Mathematics
- 2009

This paper revisits the authors' notion of a dierential category from a dierent perspective. A dierential category is an additive symmetric monoidal category with a comonad (a \coalgebra modality")… Expand