Wißmann T, Milius S (2024)
Publication Type: Conference contribution
Publication year: 2024
Publisher: Institute of Electrical and Electronics Engineers Inc.
Conference Proceedings Title: Proceedings - Symposium on Logic in Computer Science
Event location: Tallinn, EST
ISBN: 9798400706608
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.
APA:
Wißmann, T., & Milius, S. (2024). Initial Algebras Unchained - A Novel Initial Algebra Construction Formalized in Agda. In Proceedings - Symposium on Logic in Computer Science. Tallinn, EST: Institute of Electrical and Electronics Engineers Inc..
MLA:
Wißmann, Thorsten, and Stefan Milius. "Initial Algebras Unchained - A Novel Initial Algebra Construction Formalized in Agda." Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, EST Institute of Electrical and Electronics Engineers Inc., 2024.
BibTeX: Download