Abadi and Plotkin’s language in terms of differential structure
Abadi and Plotkin defined the Simple Differential Programming Language (SDPL) to be a functional programming language with a first order type system where every program can be reverse differentiated. Importantly this language has conditionals and recursive functions. In this talk we will develop the denotational semantics and source code transformation semantics from a categorical point of view using the technology of reverse differential join restriction categories. In particular, using an interpretation into such a category we will show that source code transformations are modelled correctly, that the trace-differentiation technique is modelled, and we will express a denotational semantics for SDPL into any such category with enough points. Finally, we will use the theory of these categories to derive a modification to the operational semantics that yields an exponential speedup on the differentiation of loops. Also, as a bonus, we will do recursion in a restriction category!
