Generalized Bounded Linear Logic and its Categorical Semantics

Abstract

We introduce GBLL and GBAL, generalizations of Girard et al.'s BLL. The calculus extracts an underlying fundamental structure of BLL, while separates complexity-related issues in BLL. We analyze the complexity of cut-elimination in GBLL, and give a translation of QBLL, a fragment of QBAL (a variant of BLL by Dal Lago and Hofmann), into GBAL.We then introduce indexed linear exponential comonads (ILEC for short) as a categorical structure for interpreting the !-modality of GBLL. This is obtained by extending the grading semiring of graded linear exponential comonads to the 2-category Idx, which may be seen as a multiobject pseudo-semiring. We give an elementary example of ILEC using folding product, and its modification via symmetric monoidal comonads. We then instantiate this elementary example with the category of assemblies of a BCI-algebra, and discuss (dis)similarity with the realizability category studied by [18, 9].