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.

翻译：递归余代数为建模递归算法及其终止性与正确性分析提供了优雅的范畴论工具。通过考虑适当索引族范畴上的余代数，相应算法的正确性仅从计算映射的类型即可内在得出。然而，证明底层余代数的递归性并非易事，且证明通常具有特定性。这种复杂性阻碍了证明助手中基于余代数定义的递归算法的形式化。我们提出一个构建余代数的框架，这些余代数在本质上是递归的，即余代数的类型从一开始就保证了递归性。我们的方法基于一个新颖概念：在由良基关系索引的族范畴上的良基函子。我们作为主要结果证明，每个良基函子的余代数都是递归的，并展示诸如排名函数等已知的递归性与终止性证明技术如何被这一抽象框架所包含。我们呈现若干案例研究，包括快速排序、欧几里得算法和CYK解析。主要理论结果及选定的案例研究已在Cubical Agda中完成形式化。