Federico Olimpieri
LIS, Aix-Marseille
https://www.federicolimpieri.it/
Date(s) : 11/04/2024 iCal
11 h 00 min - 12 h 30 min
We establish a formal correspondence between resource calculi
and appropriate linear multicategories. We consider the cases of
(symmetric) representable, symmetric closed and autonomous
multicategories. For all these structures, we prove that morphisms of
the corresponding free constructions can be presented by means of typed
resource terms, up to a reduction relation and a structural equivalence.
Thanks to the linearity of the calculi, we can prove strong
normalization of the reduction by combinatorial methods, defining
appropriate decreasing measures. From this, we achieve a general
coherence result: morphisms that live in the free multicategorical
structures are the same whenever the normal forms of the associated
terms are equal. As further application, we obtain syntactic proofs of
Mac Lane’s coherence theorems for (symmetric) monoidal categories.
Catégories