Combining fixpoint and differentiation theory
Zeinab Galal, Jean-Simon Pacaud Lemay
TL;DR
This work develops a denotational framework that unifies differentiation and recursion by introducing Cartesian differential fixpoint categories, which equip Cartesian differential categories with a parametrized fixpoint operator satisfying a differential-fixpoint rule. The framework shows that, in the presence of Conway/trace structure, the differential and tangent interactions yield equivalent rules, and it preserves linearity under fixpoints, enabling robust semantics for differential lambda-calculi with recursion. The authors provide multiple concrete models (including relations, weighted relations, formal power series, and profunctor-based enrichments) and demonstrate an effective Newton-Raphson style optimization scheme within this setting, culminating in a general convergence theory based on Taylor expansions. The results pave the way for broader applications to differential programming languages, coherent/ reverse differentiation, and local fixpoint theories, with potential extensions to tangent and restriction categories and fixpoint objects.
Abstract
Interactions between derivatives and fixpoints have many important applications in both computer science and mathematics. In this paper, we provide a categorical framework to combine fixpoints with derivatives by studying Cartesian differential categories with a fixpoint operator. We introduce an additional axiom relating the derivative of a fixpoint with the fixpoint of the derivative. We show how the standard examples of Cartesian differential categories where we can compute fixpoints provide canonical models of this notion. We also consider when the fixpoint operator is a Conway operator, or when the underlying category is closed. As an application, we show how this framework is a suitable setting to formalize the Newton-Raphson optimization for fast approximation of fixpoints and extend it to higher order languages.