一句话：提出 well-founded functor 框架，使余代数的类型自动保证递归性，从而内在获得算法正确性与终止性。
递归余代数用范畴工具建模递归算法并分析终止性与正确性：在合适索引族范畴上，算法正确性可由计算映射的类型内在推出。但证明底层余代数的递归性通常不平凡，且多为特设证明，阻碍其在证明助手中形式化。本文提出构造“内在递归”余代数的框架，核心是良基关系索引族范畴上的良基函子。主要结果证明良基函子的任意余代数都是递归的，并表明 ranking function 等经典终止性证明技术可被该抽象框架涵盖。作者以 Quicksort、Euclidean algorithm 和 CYK parsing 为例，并在 Cubical Agda 中形式化了主定理与部分案例。
Recursive coalgebras provide an elegant categorical tool for modelling recursive algorithms and analysing their termination and correctness. By considering coalgebras over categories of suitably indexed families, the correctness of the corresponding algorithms follows intrinsically just from the type of the computed maps. However, proving recursivity of the underlying coalgebras is non-trivial, and proofs are typically ad hoc. This layer of complexity impedes the formalization of coalgebraically defined recursive algorithms in proof assistants. We introduce a framework for constructing coalgebras which are intrinsically recursive in the sense that the type of the coalgebra guarantees recursivity from the outset. Our approach is based on the novel concept of a well-founded functor on a category of families indexed by a well-founded relation. We show as our main result that every coalgebra for a well-founded functor is recursive, and demonstrate that well-known techniques for proving recursivity and termination such as ranking functions are subsumed by this abstract setup. We present a number of case studies, including Quicksort, the Euclidian algorithm, and CYK parsing. Both the main theoretical result and selected case studies have been formalized in Cubical Agda.
@article{paperbot3756,
title = {Intrinsically Correct Algorithms and Recursive Coalgebras},
author = {Cass Alexandru and Henning Urbat and Thorsten Wißmann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808309}
}