Combining fixpoint and differentiation theory
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911958584786944 |
|---|---|
| author | Galal, Zeinab Lemay, Jean-Simon Pacaud |
| author_facet | Galal, Zeinab Lemay, Jean-Simon Pacaud |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_12691 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Combining fixpoint and differentiation theory Galal, Zeinab Lemay, Jean-Simon Pacaud Category Theory Logic in Computer Science 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. |
| title | Combining fixpoint and differentiation theory |
| topic | Category Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2407.12691 |