The initial algebra for an endofunctor F provides a recursion and induction scheme for data structures whose constructors are described by F. The initial-algebra construction by Ad\'amek (1974) starts with the initial object (e.g. the empty set) and successively applies the functor until a fixed point is reached, an idea inspired by Kleene's fixed point theorem. Depending on the functor of interest, this may require transfinitely many steps indexed by ordinal numbers until termination. We provide a new initial algebra construction which is not based on an ordinal-indexed chain. Instead, our construction is loosely inspired by Pataraia's fixed point theorem and forms the colimit of all finite recursive coalgebras. This is reminiscent of the construction of the rational fixed point of an endofunctor that forms the colimit of all finite coalgebras. For our main correctness theorem, we assume the given endofunctor is accessible on a (weak form of) locally presentable category. Our proofs are constructive and fully formalized in Agda.

翻译：对于自函子F的初始代数为由F描述构造子的数据结构提供了递归与归纳方案。Adámek（1974）提出的初始代数构造始于初始对象（如空集），并连续应用该函子直至达到不动点，这一思路受Kleene不动点定理启发。根据所关注的函子特性，此过程可能需要经由序数索引的超限步骤直至终止。本文提出一种新的初始代数构造方法，该方法不基于序数索引链。相反，我们的构造松散地借鉴了Pataraia不动点定理的思想，通过形成所有有限递归余代数的余极限来实现。这让人联想到自函子的有理不动点构造——即通过形成所有有限余代数的余极限。在主要正确性定理的证明中，我们假设给定的自函子在（弱形式的）局部可表现范畴上可达。我们的证明是构造性的，并已在Agda中完全形式化。