Initial Algebras Unchained – A Novel Initial Algebra Construction Formalized in Agda
ACM/IEEE Symposium on Logic in Computer Science(2024)
摘要
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ámek (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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要