-
Fixpoint constructions in focused orthogonality models of linear logic
Authors:
Marcelo Fiore,
Zeinab Galal,
Farzad Jafarrahmani
Abstract:
Orthogonality is a notion based on the duality between programs and their environments used to determine when they can be safely combined. For instance, it is a powerful tool to establish termination properties in classical formal systems. It was given a general treatment with the concept of orthogonality category, of which numerous models of linear logic are instances, by Hyland and Schalk. This…
▽ More
Orthogonality is a notion based on the duality between programs and their environments used to determine when they can be safely combined. For instance, it is a powerful tool to establish termination properties in classical formal systems. It was given a general treatment with the concept of orthogonality category, of which numerous models of linear logic are instances, by Hyland and Schalk. This paper considers the subclass of focused orthogonalities. We develop a theory of fixpoint constructions in focused orthogonality categories. Central results are lifting theorems for initial algebras and final coalgebras. These crucially hinge on the insight that focused orthogonality categories are relational fibrations. The theory provides an axiomatic categorical framework for models of linear logic with least and greatest fixpoints of types. We further investigate domain-theoretic settings, showing how to lift bifree algebras, used to solve mixed-variance recursive type equations, to focused orthogonality categories.
△ Less
Submitted 17 November, 2023; v1 submitted 18 September, 2023;
originally announced September 2023.
-
Stabilized profunctors and stable species of structures
Authors:
Marcelo Fiore,
Zeinab Galal,
Hugo Paquet
Abstract:
We introduce a bicategorical model of linear logic which is a novel variation of the bicategory of groupoids, profunctors, and natural transformations. Our model is obtained by endowing groupoids with additional structure, called a kit, to stabilize the profunctors by controlling the freeness of the groupoid action on profunctor elements.
The theory of generalized species of structures, based on p…
▽ More
We introduce a bicategorical model of linear logic which is a novel variation of the bicategory of groupoids, profunctors, and natural transformations. Our model is obtained by endowing groupoids with additional structure, called a kit, to stabilize the profunctors by controlling the freeness of the groupoid action on profunctor elements.
The theory of generalized species of structures, based on profunctors, is refined to a new theory of \emph{stable species} of structures between groupoids with Boolean kits. Generalized species are in correspondence with analytic functors between presheaf categories; in our refined model, stable species are shown to be in correspondence with restrictions of analytic functors, which we characterize as being stable, to full subcategories of stabilized presheaves. Our motivating example is the class of finitary polynomial functors between categories of indexed sets, also known as normal functors, that arises from kits enforcing free actions.
We show that the bicategory of groupoids with Boolean kits, stable species, and natural transformations is cartesian closed. This makes essential use of the logical structure of Boolean kits and explains the well-known failure of cartesian closure for the bicategory of finitary polynomial functors between categories of set-indexed families and cartesian natural transformations. The paper additionally develops the model of classical linear logic underlying the cartesian closed structure and clarifies the connection to stable domain theory.
△ Less
Submitted 28 February, 2024; v1 submitted 8 March, 2023;
originally announced March 2023.
-
Fixpoint operators for 2-categorical structures
Authors:
Zeinab Galal
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 recove…
▽ More
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.
△ Less
Submitted 6 June, 2023; v1 submitted 6 March, 2023;
originally announced March 2023.
-
Ilyashenko algebras based on transserial asymptotic expansions
Authors:
Zeinab Galal,
Tobias Kaiser,
Patrick Speissegger
Abstract:
We construct a Hardy field that contains Ilyashenko's class of germs at infinity of almost regular functions as well as all log-exp-analytic germs. In addition, each germ in this Hardy field is uniquely characterized by an asymptotic expansion that is an LE-series as defined by van den Dries et al. As these series generally have support of order type larger than that of the set of natural numbers,…
▽ More
We construct a Hardy field that contains Ilyashenko's class of germs at infinity of almost regular functions as well as all log-exp-analytic germs. In addition, each germ in this Hardy field is uniquely characterized by an asymptotic expansion that is an LE-series as defined by van den Dries et al. As these series generally have support of order type larger than that of the set of natural numbers, the notion of asymptotic expansion itself needs to be generalized.
△ Less
Submitted 8 January, 2019; v1 submitted 5 June, 2018;
originally announced June 2018.
