paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Combining fixpoint and differentiation theory

结合不动点理论与微分理论
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 3/10 · 该论文属于范畴论与形式语义,研究微分范畴中不动点算子与导数的交互,并用于 Newton-Raphson 优化;与用户核心关注的静态分析、Agentic 程序、LLM 辅助形式化验证、浮点程序分析及贝叶斯程序分析均无直接关联,仅与不动点求解/数值近似有较间接的理论联系。引用 1 inbox
Zeinab Galal, Jean-Simon Pacaud Lemay
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:提出带不动点算子的笛卡尔微分范畴,并用新公理刻画微分与不动点的交互,应用于 Newton-Raphson 优化。

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

问题
如何在统一的范畴框架中同时处理导数与不动点,并准确刻画二者之间的交互?
方法
定义带不动点算子的笛卡尔微分范畴,添加联系不动点导数与导数不动点的公理,并研究 Conway 算子、闭范畴及典范模型。
评估
以标准可计算不动点的笛卡尔微分范畴为实例验证模型,并展示如何在该框架中形式化 Newton-Raphson 不动点逼近及推广到高阶语言。
原文摘要(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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{abs-2407-12691,
  title = {Combining fixpoint and differentiation theory},
  author = {Zeinab Galal and Jean-Simon Pacaud Lemay},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662108}
}