一句话:提出带不动点算子的笛卡尔微分范畴,并用新公理刻画微分与不动点的交互,应用于 Newton-Raphson 优化。
微分与不动点的交互在计算机科学和数学中有重要应用,但此前缺少统一的范畴框架。本文研究带不动点算子的笛卡尔微分范畴,并引入一条关键公理,将不动点的导数与导数的迭代不动点联系起来。作者证明常见的可计算不动点的笛卡尔微分范畴给出该结构的典范模型,并讨论不动点算子是 Conway 算子以及底范畴为闭范畴的情形。作为应用,该框架适合形式化用于快速逼近不动点的 Newton-Raphson 优化,并可扩展到高阶语言。
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.