Connecting models of differential linear logic with reloids
Zeinab Galal
IRIF, Université de Paris
http://www.theses.fr/s230573
Date(s) : 22/11/2018 iCal
11h00 - 12h30
Species of structures were introduced by Joyal as a unified framework for the theory of generating series in enumerative combinatorics.
Species are connected to Girard’s normal functor semantics of λ-calculus where terms are interpreted as power series with sets as coefficients.
Fiore et al. presented a generalised definition that both encompasses Joyal’s species and constitutes a model of differential linear logic.
For generalised species of structures, types are interpreted as groupoids which provides the connection with combinatorics whereas they are interpeted as sets in Girard’s normal functors and in the relational model. To investigate how these models interact, we introduce a variant of the relational model where objects are setoids (sets equipped with an equivalence relation) and morphisms are relations. We obtain a new model of differential linear logic (named Reloids) that allows for a less degenerate collapse from species than the one to normal functors or relations. We then show how to construct functors preserving the linear logic structure between these four models.
Catégories
