Marcelo Fiore ; Zeinab Galal ; Hugo Paquet - Stabilized profunctors and stable species of structures

lmcs:11048 - Logical Methods in Computer Science, February 29, 2024, Volume 20, Issue 1 - https://doi.org/10.46298/lmcs-20(1:17)2024
Stabilized profunctors and stable species of structuresArticle

Authors: Marcelo Fiore ; Zeinab Galal ; Hugo Paquet

    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.


    Volume: Volume 20, Issue 1
    Published on: February 29, 2024
    Accepted on: January 22, 2024
    Submitted on: March 9, 2023
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Category Theory,Mathematics - Logic
    Funding:
      Source : OpenAIRE Graph
    • Probabilistic program semantics; Funder: French National Research Agency (ANR); Code: ANR-19-CE48-0014

    Consultation statistics

    This page has been seen 1001 times.
    This article's PDF has been downloaded 242 times.