Oral
in
Workshop: Differentiable Programming Workshop
A Complete Axiomatization of Forward Differentiation
Gordon Plotkin
Abstract:
We give a complete decidable second-order equational axiomatisation of the forward differentiation of smooth multivariate functions. Differentiation is expressed using the binding structures available in second-order equational logic. The main mathematical theorem used is Severi’s multivariate Hermite interpolation theorem.