一个不需迭代的初始代数定理
An Initial Algebra Theorem Without Iteration
摘要:
Trnková等人的初始代数定理国家,在温和的假设下,一个endofunctor有一个初始代数提供了它有一个预固定点。证明关键取决于transmitting迭代函子,事实上表明,等价地,(超限)初始代数链停止。给出了初始代数定理的构造性证明,避免了函子的超限迭代。对于函子的给定预不动点$A$,利用Pataraia定理得到了单调函数在由$A$的所有子代数构成的偏序上的最小不动点.由于递归余代数的性质,这个最小不动点产生一个初始代数。我们获得了新的结果,不动点和初始代数的类别丰富的有向完全偏序,再次没有迭代。使用超限迭代,我们等价地获得收敛的初始代数链作为一个等价条件,整体上产生一个简化版本的原始证明。
英文摘要:
The Initial Algebra Theorem by Trnková et al.~states, under mild assumptions, that an endofunctor has an initial algebra provided it has a pre-fixed point. The proof crucially depends on transfinitely iterating the functor and in fact shows that, equivalently, the (transfinite) initial-algebra chain stops. We give a constructive proof of the Initial Algebra Theorem that avoids transfinite iteration of the functor. For a given pre-fixed point $A$ of the functor, it uses Pataraia's theorem to obtain the least fixed point of a monotone function on the partial order formed by all subobjects of $A$. Thanks to properties of recursive coalgebras, this least fixed point yields an initial algebra. We obtain new results on fixed points and initial algebras in categories enriched over directed-complete partial orders, again without iteration. Using transfinite iteration we equivalently obtain convergence of the initial-algebra chain as an equivalent condition, overall yielding a streamlined version of the original proof.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。