一句话：为不动点演算给出等式规范，并用可行性关系上的弦图提供图形化等式证明，重证滚动、对角、平方、融合与互递归等关键定理。
不动点演算为等式化地推理不动点提供了定理工具箱，但其基础概念（尤其最小不动点）本身并非等式定义，导致核心定理虽以等式形式陈述，证明却不能以等式风格书写。本文针对偏序集，给出不动点演算主要概念的等式规范，使更多证明可在等式风格下进行。为降低等式推理的复杂度，作者采用基于可行性关系范畴的弦图图形语言，提升推理的人机工效。最终给出滚动规则、对角规则、平方规则、不动点融合以及互递归定理等关键结果的图形化等式证明。
The fixed-point calculus is a toolbox of theorems for reasoning equationally about fixed points. However, the underlying concepts of the calculus are not defined equationally, including the central definition, that of least fixed point. Thus, although the key theorems of the fixed-point calculus are equational, their proofs are not. In this work, we give equational specifications for the main concepts of the fixed-point calculus for partially ordered sets, to allow more proofs to be written in an equational style. Since reasoning equationally can be cumbersome without appropriate abstractions, we employ the graphical language of string diagrams, based on a category of feasibility relations, to make reasoning more ergonomical. Our contributions culminate in graphical equational proofs of key results of the fixed-point calculus, including the rolling, diagonal, and square rules; fixed-point fusion; and the mutual recursion theorem.
@article{FreireGNP26,
title = {An Equational and Graphical Fixed-Point Calculus (Functional Pearl)},
author = {Gustavo de Mendonça Freire and Hugo Musso Gualandi and Hugo Nobrega and Joao Paixao},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828673}
}