A complete equational axiomatisation of partial differentiation

TL;DR

This paper formalizes the rules of partial differentiation within equational logic, proving the theory's completeness and related properties like decidability, using polynomial interpretations and Severi's interpolation theorem.

Contribution

It provides a complete equational axiomatisation of partial differentiation, incorporating function variables and binding, with proofs of completeness and decidability.

Findings

The theory is complete with respect to polynomial interpretations.

Decidability of the equational theory is established.

All multivariate Hermite problems are solvable via Severi's interpolation theorem.

Abstract

We formalise the well-known rules of partial differentiation in a version of equational logic with function variables and binding constructs. We prove the resulting theory is complete with respect to polynomial interpretations. The proof makes use of Severi's interpolation theorem that all multivariate Hermite problems are solvable. We also present a number of related results, such as decidability and equational completeness.