Skip to yearly menu bar Skip to main content

Workshop: Differentiable Programming Workshop

A Complete Axiomatization of Forward Differentiation

Gordon Plotkin


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.