Jonathan Gallagher

Title: Differentiation is progressive
Abstract:
The Takahashi triangle property for abstract rewriting systems contrasts ‘good’ and ‘bad’ developments of a simultaneous set of rewrites: for every bad development, there is a better development that converts the result into the result of the good development. Takahashi used the triangle property to study the confluence and standardization theorems of the lambda calculus at the same time.
In this talk, we will show that the equational theory of differentiation can be cast in terms of rewriting modulo equations, and that moreover developments in this rewriting system have a version of the triangle property that is applicable to rewriting modulo equations. In particular, this rewriting system has the Church-Rosser modulo property.