Reference. Stabilized profunctors and stable species of structures

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 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.

Cite

Cite as @fiore-2024-stabilized (helia, typst) · \cite{fiore-2024-stabilized} (LaTeX)
BibTeX
bibtex · 1 line
@article{fiore-2024-stabilized, title={Stabilized profunctors and stable species of structures}, volume={20}, ISSN={1860-5974}, url={http://dx.doi.org/10.46298/lmcs-20(1:17)2024}, DOI={10.46298/lmcs-20(1:17)2024}, journal={Logical Methods in Computer Science}, publisher={Centre pour la Communication Scientifique Directe (CCSD)}, author={Fiore, Marcelo and Galal, Zeinab and Paquet, Hugo}, year={2024}, month=Feb, number = {1} }
hayagriva YAML (typst)
yaml · 18 lines
fiore-2024-stabilized:
  type: article
  title: Stabilized profunctors and stable species of structures
  author:
  - Fiore, Marcelo
  - Galal, Zeinab
  - Paquet, Hugo
  date: 2024-02
  url: http://dx.doi.org/10.46298/lmcs-20(1:17)2024
  serial-number:
    doi: 10.46298/lmcs-20(1:17)2024
    issn: 1860-5974
  parent:
    type: periodical
    title: Logical Methods in Computer Science
    publisher: Centre pour la Communication Scientifique Directe (CCSD)
    issue: 1
    volume: 20
Cited by (1)

Modular abstract syntax trees (MAST): substitution tensors with second-class sorts fiore-2025-modular

We adapt Fiore, Plotkin, and Turi’s treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value lambda-calculus (CBV) and Levy’s Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appearing in variable contexts changes the characterisation of the abstract syntax from monoids in monoidal categories to actions in actegories. We reproduce much of the development through bicategorical arguments. We apply the resulting theory by proving substitution lemmata for varieties of CBV.
DOI · arXiv
Cites 51 works (4 here)
With notes (4)

A Combinatorial Approach to Higher-Order Structure for Polynomial Functors fiore-2022-a

Polynomial functors are categorical structures used in a variety of applications across theoretical computer science; for instance, in database theory, denotational semantics, functional programming, and type theory. A well-known problem is that the bicategory of finitary polynomial functors between categories of indexed sets is not cartesian closed, despite its success and influence on denotational models and linear logic. This paper introduces a formal bridge between the model of finitary polynomial functors and the combinatorial theory of generalised species of structures. Our approach consists in viewing finitary polynomial functors as free analytic functors, which correspond to free generalised species. In order to systematically consider finitary polynomial functors from this combinatorial perspective, we study a model of groupoids with additional logical structure; this is used to constrain the generalised species between them. The result is a new cartesian closed bicategory that embeds finitary polynomial functors.
DOI

Indexed containers altenkirch_indexed_2015

We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide normal forms for strictly positive families in much the same way that containers provide normal forms for strictly positive types. Interestingly, this step from containers to indexed containers is achieved without having to extend the core type theory. Most of the construction presented here has been formalized using the Agda system.
PDF · DOI · pldb

Glueing and orthogonality for models of linear logic hyland_glueing_2003

We present the general theory of the method of glueing and associated technique of orthogonality for constructing categorical models of all the structure of linear logic: in particular we treat the exponentials in detail. We indicate simple applications of the methods and show that they cover familiar examples.
DOI

Linear logic girard_linear_1987

The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
DOI
External (47)
fiore-2024-stabilized reference entries/refs/fiore-2024-stabilized/fiore-2024-stabilized.hel