Term Assignment and Categorical Models for Intuitionistic Linear Logic with Subexponentials
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908572624879616 |
|---|---|
| author | Rogozin, Daniel |
| author_facet | Rogozin, Daniel |
| contents | In this paper, we present a typed lambda calculus ${\bf SILL}(λ)_Σ$, a type-theoretic version of intuitionistic linear logic with subexponentials, that is, we have many resource comonadic modalities with some interconnections between them given by a subexponential signature. We also give proof normalisation rules and prove the strong normalisation and Church-Rosser properties for $β$-reduction by adapting the Tait-Girard method to subexponential modalities. Further, we analyse subexponentials from the point of view of categorical logic. We introduce the concepts of a Cocteau category and a $Σ$-assemblage to characterise models of linear type theories with a single exponential and affine and relevant subexponentials and a more general case respectively. We also generalise several known results from linear logic and show that every Cocteau category and a $Σ$-assemblage can be viewed as a symmetric monoidal closed category equipped with a family of monoidal adjunctions of a particular kind. In the final section, we give a stronger 2-categorical characterisation of Cocteau categories. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_12360 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Term Assignment and Categorical Models for Intuitionistic Linear Logic with Subexponentials Rogozin, Daniel Logic Category Theory In this paper, we present a typed lambda calculus ${\bf SILL}(λ)_Σ$, a type-theoretic version of intuitionistic linear logic with subexponentials, that is, we have many resource comonadic modalities with some interconnections between them given by a subexponential signature. We also give proof normalisation rules and prove the strong normalisation and Church-Rosser properties for $β$-reduction by adapting the Tait-Girard method to subexponential modalities. Further, we analyse subexponentials from the point of view of categorical logic. We introduce the concepts of a Cocteau category and a $Σ$-assemblage to characterise models of linear type theories with a single exponential and affine and relevant subexponentials and a more general case respectively. We also generalise several known results from linear logic and show that every Cocteau category and a $Σ$-assemblage can be viewed as a symmetric monoidal closed category equipped with a family of monoidal adjunctions of a particular kind. In the final section, we give a stronger 2-categorical characterisation of Cocteau categories. |
| title | Term Assignment and Categorical Models for Intuitionistic Linear Logic with Subexponentials |
| topic | Logic Category Theory |
| url | https://arxiv.org/abs/2507.12360 |