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