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中完成形式化。