Fixpoint operators for 2-categorical structures
From MaRDI portal
Publication:6428580
arXiv2303.03440MaRDI QIDQ6428580FDOQ6428580
Authors: Zeinab Galal 
Publication date: 6 March 2023
Abstract: Fixpoint operators are tools to reason on recursive programs and data types obtained by induction (e.g. lists, trees) or coinduction (e.g. streams). They were given a categorical treatment with the notion of categories with fixpoints. A theorem by Plotkin and Simpson characterizes existence and uniqueness of fixpoint operators for categories satisfying some conditions on bifree algebras and recovers the standard examples of the category Cppo (-complete pointed partial orders and continuous functions) in domain theory and the relational model in linear logic. We present a categorification of this result and develop the theory of 2-categorical fixpoint operators where the 2-dimensional framework allows to model the execution steps for languages with (co)inductive principles. We recover the standard categorical constructions of initial algebras and final coalgebras for endofunctors as well as fixpoints of generalized species and polynomial functors.
This page was built for publication: Fixpoint operators for 2-categorical structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6428580)
