key: cord-0060370-as6tmymh
authors: Fukihara, Yōji; Katsumata, Shin-ya
title: Generalized Bounded Linear Logic and its Categorical Semantics
date: 2021-03-23
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-71995-1_12
sha: 1a5ce5c0d8729bf97457145927113b5c792c8785
doc_id: 60370
cord_uid: as6tmymh

We introduce a generalization of Girard et al.’s BLL called GBLL (and its affine variant GBAL). It is designed to capture the core mechanism of dependency in BLL, while it is also able to separate complexity aspects of BLL. The main feature of GBLL is to adopt a multi-object pseudo-semiring as a grading system of the !-modality. We analyze the complexity of cut-elimination in GBLL, and give a translation from BLL with constraints to GBAL with positivity axiom. We then introduce indexed linear exponential comonads (ILEC for short) as a categorical structure for interpreting the [Formula: see text]-modality of GBLL. We give an elementary example of ILEC using folding product, and a technique to modify ILECs with symmetric monoidal comonads. We then consider a semantics of BLL using the folding product on the category of assemblies of a BCI-algebra, and relate the semantics with the realizability category studied by Hofmann, Scott and Dal Lago.

Girard's linear logic is a refinement of propositional logic by restricting weakening and contraction in proofs [15] . Linear logic also has an of-course modality !, which restores these structural rules to formulas of the form !A.

Later, Girard et al. extended the !-modality with quantitative information so that usage of !-modal formulas in proofs can be quantitatively controlled [16] . This extension, called bounded linear logic (BLL for short), is successfully applied to a logical characterization of P-time computations.

Their extension takes two steps. First, the !-modality is extended to the form ! r A, where the index r is an element of a semiring [16, Section 2.4] . The index r is called grade in modern terminology [11, 13] . This extension and its variants have been employed in various logics and programming languages [7, 30, 14, 26, 28] . The categorical structure corresponding to ! r A is identified as graded linear exponential comonad [7, 13, 22] .

Second, the ! r -modality is further extended to the form ! x<p A, where p is a polynomial (called resource polynomial) giving the upper bound of x [16, Section 3] . The formula ! x<p A also binds free occurrences of the resource variable x in resource polynomials in A. Therefore, in BLL, both formulas and resource polynomials depend on the values stored in free resource variables. This dependency mechanism significantly increases the expressiveness of BLL, leading to a characterization of P-time complexity.

This characterization result was later revisited through a realizability semantics of BLL [16, 19, 10] . Inside this semantics, however, mechanisms for controlling complexity of program execution are hard-coded, and it is not very clear which semantics structure realizes the dependency mechanism of BLL. This leads us to seek a logical and categorical understanding of BLL's dependency mechanism hidden underneath the complexity-related features, such as resource polynomials and computability constraints.

As a result of the quest, we propose a generalization of BLL called GBLL, and study its categorical semantics. The central idea of the generalization is to replace the grading semiring of the ! r -modality with a particular multi-object pseudo-semiring realized as a 2-category. Let us see how this replacement works. In GBLL, each formula is formed by deriving a judgment of the form ∆ A, where ∆ is a set (called index set) and A is a raw formula. We may think that such a well-formed formula ∆ A denotes a ∆-indexed family { A i } i∈∆ of denotations. The formation rule for !-modal formula in GBLL is the following:

where the function f abstractly represents dependency. This modality is enough to express the ! x<p -modality of BLL: we express the bindig x < p under a resource variable context y as the function f p ( y) = ( y, 0) · · · ( y, p( y) − 1) that returns the list of environments extended with values less than p( y). Then the denotation of the ! f A-modality is given by a variable-arity operator D. For each index i ∈ ∆, the denotation is given by applying D to the denotations obtained by mapping A to list f (i):

! f A i = D( A j1 , · · · , A jn ) where j 1 · · · j n = f (i).

A simple example of a variable-arity modal operator is the folding product D(X 1 , · · · , X n ) = X 1 ⊗ · · · ⊗ X n . The pseudo-semiring structure on the class of functions of the form ∆ → (∆ ) * is given as follows. For the multiplication g • f , we adopt the Kleisli composition of the free monoid monad ( ) * , while for the addition f +g, the pointwise concatenation (f + g)(x) = f (x)g(x). However, these operations fail to satisfy one of the semiring axioms:

To fix this, we introduce (pointwise) list permutations as 2-cells between functions of type ∆ → (∆ ) * . These data form a 2-category Idx, which may be seen as a multi-object pseudosemiring. Weakening, contraction, digging and dereliction in GBLL interact with these operations, much like the ! r -modality in [7] .

We first study syntactic properties of GBLL. We introduce cut-elimination to GBLL and study its complexity property. It turns out that the proof technique used in BLL naturally extends to GBLL -as done in [16] , we classify cuts into reducible and irreducible ones, introduce proof weight, and show that the reduction steps of reducible cuts will terminate in cubic time of proof weights. We also examine the expressive power of GBLL by giving a translation from an extension of BLL with constraints that are seen in Dal Lago et al.'s QBAL [10] .

We next give a categorical semantics of GBLL. We introduce the concept of indexed linear exponential comonad (ILEC ); it is an Idx-graded linear exponential comonad satisfying a commutativity condition with respect to an underlying indexed SMCCs. Then, we present a construction of ILEC from a symmetric monoidal closed category C with a symmetric monoidal comonad on it. We apply this construction to the case where C is the category of assemblies over a BCI algebra [2, 20] , and relate the semantics of GBLL with the constructed ILEC and the realizability category studied in [19, 10] . Acknowledgment The first author was supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603). The authors are grateful to anonymous reviewers for comments, and Masahito Hasegawa, Naohiko Hoshino, Clovis Eberhart and Jérémy Dubut for fruitful discussions.

Preliminaries For a set ∆, by ∆ * we mean the set of finite sequences of ∆. The empty sequence is denoted by (). Juxtaposition of ∆ * -elements denotes the concatenation of sequences. For x ∈ ∆ * , by |x| we mean the length of x. We identify a natural number n and the set {0, · · · , n − 1}; note that 0 = ∅. We also identify a sequence x ∈ ∆ * and the function "λi ∈ |x| . the i-th element of x".

We first introduce a 2-category Idx (and its variant Idx a ), which may be seen as a multi-object pseudo-semiring. It consists of the following data 3 : 0-cells are sets (called index sets), and the hom-category Idx(∆, ∆ ), which is actually a groupoid, is defined by:

The identity 1-cell and the composition of 1-cells in Idx are denoted by i ∆ and (•), respectively. The composition is defined by (g•f )(x) def = g(y 1 ) · · · g(y n ) where y 1 · · · y n = f (x). The hom-category Idx(∆, ∆ ) has a symmetric strict monoidal structure:

the monoidal unit is the constant empty-sequence function 0(x) = (), the tensor product of f, g, denoted by f + g, is defined by the index-wise

We write J : Set → Idx for the inclusion, namely J∆ = ∆ and (Jf )(x) = f (x) (the singleton sequence).

Proposition 2.1. The composition • is symmetric strong monoidal in each argument. Especially, we have

We also define Idx a by replacing "bijection" in the definition of 2-cell of Idx with "injection". The hom-category Idx a (∆, ∆ ) has the 1-cell 0 as the terminal object, hence is a symmetric affine monoidal category.

Definition of GBLL Formulas We first fix a set-indexed sets {A(∆)} ∆∈Set of atomic propositions. Formulas are defined by the following BNF:

where a ∈ A(∆) for some set ∆, r is a function (called reindexing function) and f is a 1-cell in Idx. Formula formation rules are introduced to derive the pair ∆ A of an index set ∆ and a formula A. They are defined as follows:

The formula a r represents the atomic formula a precomposed with a reindexing function r. We write Fml(∆) = {A | ∆ A}. We next introduce the reindexing operation on formulas.

Definition 2.1. For a reindexing function r ∈ Set(∆, ∆ ), we define the reindexing operator ( )| r : Fml(∆ ) → Fml(∆) along r by

We routinely extend reindexing operators to sequences of formulas well-formed under a common index set.

We quotient the set of well-formed formulas by the least congruent equivalence relation generated from the following binary relation:

We see some formations of formulas in GBLL.

Example 2.1. Let us illustrate how a formula ! y<x 2 ! z<x+y A in BLL is represented in GBLL; here we assume that x, y, z are the only resource variables used in this formula. We first introduce a notation. Let E be a mathematical expression using variables x 1 · · · x n . Then by [E] n : N n → (N n+1 ) * we mean the function

. Then from a well-formed formula

Generalizing this, a BLL formula ! x<E A containing resource variables x 1 , · · · , x n corresponds to the GBLL formula ! [E]n A.

Example 2.2. We look at how we express the substitution of a resource polynomial A[x := p(x 1 , ..., x n )]. We define a function p n : N n → N n+1 by p n (x 1 , ..., x n ) def = (x 1 , ..., x n , p(x 1 , ..., x n )).

Then the reindexed formula N n A| p n corresponds to A[x := p(x 1 , · · · , x n )]. Example 2.3. We illustrate the equality between well-formed formulas. Consider a formula N A and a function r ∈ Set(N 3 , N). Then we equate formulas

where ∆ is an index set, Γ is a sequence of formulas well-formed under ∆, and A is a well-formed formula under ∆, respectively. The inference rules of GBLL are presented in Fig. 1 . Similarly, we define GBAL to be the system obtained by replacing Idx in Fig. 1 with Idx a . Example 2.4. We mimic a special case of the contraction rule in BLL

By contraction rule of GBLL, we obtain the following derivation for well-formed formulas N n+1 A and N n B, mimicking the contraction of BLL:

Here, we use the formula equality ! Jsn,i•[xj ]n A = ! [xj ]n (A|s n,j ).

Example 2.5. The reindexing operator can be extended to proofs. Let r be a reindexing function in Set(∆, ∆ ). Reindexing of the axiom rule ∆ | A A, by r is the axiom rule ∆ | A| r A| r . Reindexing of other rules except (P!) can be easily defined-the judgment ∆ | Γ A in each rule is replaced with ∆ | Γ | r A| r by reindexing. For (P!) rule, reindexing by r is given as follows:

In this paper, indexing 2-category is either Idx or Idx a . Allowing more general indexing 2-categories in GBLL is a future work. In his PhD thesis, Breuvart designed a linear logic similar to GBLL upon an abstract indexing mechanism called dependent semirings [5, Definition 3.2.4.5]. It consists of categories (S, U ) such that 1) each hom-set in S carries a (not necessarily commutative) ordered monoid structure (0, +) and the composition of S distributes over 0, +, and 2) U acts on S from both sides. Roughly speaking, S and U corresponds to our Idx op and Set op , respectively. We expect that a unification of dependent semirings and 2-categories Idx, Idx a would yield a suitable generalization of indexing categories for GBLL. This generalization will subsume the non-graded linear logic, and allow us to compare GBLLs over different idexing categories.

By a similar discussion to BLL [16] , instances of Cut inference are divided in two classes: reducible cuts and irreducible cuts. We define the weight of proof |π| for each proof π ∆ | Γ A and reduction steps of proofs, such that every reduction steps will terminate, for each index δ ∈ ∆, in polynomial steps of |π|(δ).

In GBLL (resp. GBAL) proofs, an instance of the Cut inference is irreducible if there are at least one Composition rule below it or if its left premise is obtained by a Composition rule with nonempty context and the other premise is obtained by a Weakening, !-Functor, Dereliction, Contraction or Composition inference. A reducible cut is Cut inferences that is not irreducible.

The definition of (ir)reducibility and weight is diverted from Girard's paper. Therefore, our system inherits from BLL the conditions under which cuts can be reduced. See also Section 2.4 in [16] .

Following [16] , we introduce the concept of weight of a proof. It is a function |π| : ∆ → N assigning a weight number |π|(δ) to a proof π at an index δ ∈ ∆. The weight number never increases at any reduction step of Cut in π. In the original BLL, weights are expressed by resource polynomials, while here, they are generalized to arbitrary functions. We remark that weights of the proofs involving Composition rules, which introduce ! f modality, use the length of the lists constructed by f . Definition 2.4. For a given proof π ∆ | Γ A of GBLL or GBAL, the weight of π is a function |π| : ∆ → N inductively defined as follows. A) When ∆ = ∅, |π| is the evident function. B) When ∆ = ∅, |π| is defined by the following rules:

1. For an Axiom rule π ∆ | A A, |π|(δ) def = 1.

2. If π is obtained from π by a unary rule except Contraction and Composition,

3. If π is obtained from π 1 and π 2 by a binary rule except Cut, |π|(δ)

4. If π is obtained from π 1 and π 2 by a Cut rule, |π|(δ)

5. If π is obtained from π by a Contraction rule, |π|(δ) def = |π |(δ) + 2 6. If π is obtained from π by a Composition rule, such as

Note that the summation γ∈f (δ) scans all elements in the list f (δ), hence the weight depends on the length of f (δ).

Theorem 2.1. For every proof π ∆ | Γ A and every δ ∈ ∆, reduction steps of reducible cuts will terminate in at most (|π|(δ)) 3 steps.

Proof (sketch). The proof is almost the same as Section 2.2 and Appendix A of [16] , except for the definition of the weight. Suppose that π one-step reduces into π . From the definition of the weight, either 1) for all index δ ∈ ∆, the weight decreases (that is, |π|(δ) > |π |(δ)), or 2) for all index δ ∈ ∆, the weight keeps (that is, |π|(δ) = |π |(δ)). The reduction of the former type is called symmetric or axiom reduction [ In the case where the weight keeps, we introduce another measure called the cut size π : ∆ → N of a proof π. Its definition is the same as the definition of weight except for Cut rule. For a proof π obtained by Cut rule from π 1 and π 2 , the cut size π (δ) is defined to be π 1 (δ) + π 2 (δ) + |π 1 |(δ) + |π 2 |(δ).

In each commutative reduction from π to π the cut size decrease at all index (that is, for all δ ∈ ∆, ||π||(δ) > ||π ||(δ)), and the cut size is at most the square of the weight (that is, for all δ ∈ ∆, ||π||(δ) ≤ (|π|(δ)) 2 ). Therefore, the total number of steps is at most the cube of the weight.

The number of reduction steps of a proof π and its weight depend on the length of lists computed by the Idx-morphisms occurring in π. However, to discuss the actual time complexity of cut-elimination, we further need to take into account the time complexity of the computation of Idx-morphisms. This would be achieved by looking at a subcategory of Idx computable within a certain time complexity. We leave this argument of analyzing the actual time complexity of cut-elimination as a future work.

We show that GBLL can express BLL via a translation. This translation is actually given to variants of these calculi, namely from BLL with constraints (called CBLL) to GBAL with positivity axioms (called GBAL + ).

CBLL is an extension of BLL with constraints, which are one of the features of Dal Lago and Hofmann's QBAL [10] . Constraints explicitly specify conditions imposed on resource variables, and it is natural to explicitly maintain these conditions throughout proofs. We also remark that in CBLL, weakening of !formulas ! x<p+q A ! x<p A is allowed, and atomic formulas are assumed to satisfy the positivity property (3.1).

GBAL + is designed for a sound translation from CBLL. Recall that GBAL is an extension of GBLL with weakening ! f +g A ! f A on !-formulas. Then GBAL + is a further extension of GBAL with the following positivity axioms of atomic formulas: for every n-ary atomic formula a ∈ A in CBLL, we introduce an atomic formula [a] ∈ A(N n ) to GBAL together with the axiom:

Here the definition of each notation is given in Section 3.1 and 3.3. Positivity axiom induces proofs V C (F ) | A A for every two formulas A, A such that A C A (the relation C for formulas is defined in Section 3.2).

We introduce basic concepts around CBLL, referring to its super-logic QBAL [10] . We put a reference in the beginning of each paragraph when the contents come from QBAL in [10] .

[10, Definition 2.1] Given a countably infinite set RV of resource variables, a resource monomial over RV is a finite product of binomial coefficients m i=1 xi ni , where the resource variables x 1 , · · · , x m are distinct and n 1 , · · · , n m ∈ N are natural numbers. A resource polynomial over RV is a finite sum of resource monomials. We write 1 as x 0 and x as x 1 for short. Each positive natural number n denotes a resource polynomial 1 + 1 + · · · + 1. Resource polynomials are closed under sum, product, bounded sum and composition [10, Lemma 2.2].

[10, Definition 2.3] A constraint is an inequality p ≤ q, where p and q are resource polynomials. We abbreviate p + 1 ≤ q as p < q. A constraint p ≤ q holds (written p ≤ q) if it is true in the standard model. A constraint set (denoted with C , D) is a finite set of constraints. A constraint p ≤ q is a consequence of a constraint set C (written C p ≤ q) if p ≤ q is a logical consequence of C . For every constraint sets C and D, we write C D iff C p ≤ q for every constraint p ≤ q in D. For each constraint set C , we define an order C on resource polynomials by p C q iff C p ≤ q.

[10, Definition 2.3] We define the polarity of occurrences of free resource variables. For a constraint p ≤ q, we say that an occurrence of a resource variable x in p is called negative, while the one in q is called positive.

Let A be a set of atomic formulas and assume that each atomic formula a ∈ A is associated with an arity ar(a). Formulas of CBLL are defined by:

where p in the formula ! x<p A satisifes x / ∈ FV(p). [10, Definition 2.6] Each occurrence of a free resource variable in a formula is classified into positive or negative. Below we inductively define a positive occurrence of a resource variable. An occurrence of x in:

a(p 1 , · · · , p ar(a) ) is always positive.

-A ⊗ B is positive iff it is in A and positive, or so in B. -! x <p A is positive iff it is in A and positive. We remark that an occurrence of a free resource variable in p is counted as negative in ! x <p A.

[10, Definition 2.8] We extend the order C on resource polynomials to the one on CBLL formulas. a(p 1 , · · · , p ar(a) ) C a(q 1 , · · · , q ar(a) ) iff ∀i.

[10, Section 2.3] A CBLL judgment is an expression Γ C A, where C is a constraint set, Γ is a multiset of formulas and A is a formula. A judgment Γ C A means that A is a consequence of Γ under the constraints C .

Inference rules (Fig. 2 ) are almost the same as those of QBAL; we omit the rules for ⊗, and Cut. Note that weakening is restricted to !-formulas. Every BLL proof of Γ A can be translated to a CBLL proof of Γ Ø A.

As mentioned at the beginning of Section 3, we will give a translation from CBLL to GBAL + . When translating a CBLL proof Γ C A, we also need to supply a set For Constraints We define an environment over a finite set F of resource variables to be a function from F to N; by V (F ) we mean the set of environments over F . Given an environment ρ ∈ V (F ) and a resource variable x ∈ F and n ∈ N, by ρ{x → n} we mean the environment over F ∪ {x} that extends ρ with a mapping x → n. Given a resource polynomial p such that F V (p) ⊆ F , by p : V (F ) → N we mean the function that evaluates the resource polynomial p under a given environment. For resource polynomials p 1 , · · · , p n such that FV(p i ) ⊆ F , we give a function p 1 , · · · , p n : (V (F )) → N n by p 1 , · · · , p n ρ = ( p 1 ρ, · · · , p n ρ).

Let ρ p ≤ q denote p ρ ≤ q ρ for a constraint p ≤ q with a set F of free resource variables (such that FV(p) ∪ FV(q) ⊆ F ) and for an environment ρ ∈ V (F ). For a subset S ⊂ V (F ) and for a constraint set C , S C is also defined similarly: for every ρ ∈ S and for every p ≤ q ∈ C , ρ p ≤ q. Given a constraint set C and a set F of resource variables such that FV(C ) ⊆ F , let a set V C (F ) and a function ι F,C : V C (F ) → V (F ) be given by:

For a resource polynomial p, a free resource variable x such that x / ∈ FV(p), a constraint set C and a set F of resource variables such that FV(p)∪FV For Proofs To give a translation of proofs, we define another notation. For a resource polynomial p, q, a set F of resource variables and a constraint set C such that FV(p) ∪ FV(C ) ⊆ F , a set [p, q) (F,C ) of environments is defined by

here t is a "fresh" resource variable such that t / ∈ F . Given a proof π Γ C A, a translation :

Then the conclusion of (!C) is obtained:

-For (!P) rule, let F = F ∪ {x} and C = C ∪ {x < p}. We can prove the translated conclusion from the translated premise by the following proof:

n times (!D)'s . . .

-For (!N) rule, we define index sets ∆ 0 , ∆ 1 , ∆ 2 and constraints C 0 , C 1 , C 2 by

There is an isomorphism r ∈ Set(∆ 1 , ∆ 2 ), and it holds an equation

. Therefore, (!N) rule can be translated to the following provable judgment: 

We give a categorical semantics of GBLL. First, notice that each index set ∆ determines a multiplicative linear logic under ∆. We model this situation by a setindexed symmetric monoidal closed categories, given by a functor C : Set op → SMCC strict . That is, for each ∆ ∈ Set, a symmetric monoidal closed category C∆ is given, and any function f : ∆ → ∆ induces a strict symmetric monoidal closed functor Cf : C∆ → C∆, performing renaming of indexes.

Upon this indexed symmetric monoidal closed categories, we introduce a categorical structure that models the ! f modality. We call it indexed linear exponential comonad. This is a generalization of the semiring-graded linear exponential comonad studied in [13, 22] . Our generalization replaces the semiring with Idx, which may be regarded as a many-object pseudo-semiring (Proposition 2.1).

We write [C, D] l for the category of symmetric lax monoidal functors from C to D and monoidal natural transformations between them. We equip it with the pointwise symmetric monoidal structure (İ,⊗) given byİX = I and (F⊗G)X = F X ⊗ GX for X ∈ C. The last axiom has two purposes: the equality Cr (Df A) = D(f • Jr )A is to allow reindexing functions to act from outside, and the other equality Df (CrA) = D(Cr • f )A is to make D invariant under internal reindexing of formulas. These equalities are tied up with the formula equivalence in (2.1) and the definition of reindexing at ! f A in Definition 2.1, respectively. We postpone a concrete example of ILEC to Section 4.2.

We interpret a well-formed formula ∆ A as an object ∆ A ∈ C∆. This is done by induction on the structure of the formula. We assume that each atomic formula a ∈ A(∆) comes with its interpretation as an object [a] ∈ C∆.

Proposition 4.1. For any r ∈ Set(∆, ∆ ) and well-formed formula ∆ A, we have ∆ A| r = Cr ∆ A .

Each proof π ∆ | Γ A of GBLL is interpreted as a morphism ∆ | Γ A : ∆ Γ → ∆ A in C∆. Here, for a sequence Γ = C 1 , · · · , C m of formulas, ∆ Γ denotes ∆ C 1 ⊗ · · · ⊗ ∆ C m . We write out the interpretation only for the cases of modalities, because the other rules, Axiom, Exchange, Cut, ⊗(L, R) and (L, R) are interpreted similarly to the semantics of multiplicative intuitionistic linear logic. Fig. 4 shows the interpretation of rules related to ! f . Theorem 4.1. For a proof π ∆ | Γ A, if π has a reducible cut and reduces into π by a reduction step, then π = π in C∆.

We present a construction of an indexed SMCCs C : Set op → SMCC strict and an ILEC D : Idx(∆, ∆ ) → [C∆ , C∆] l over C from a SMCC C, ⊗, I, , and a symmetric lax monoidal comonad V, m V , m V X,Y , , δ on C.

Construction of Indexed SMCCs First, for each index set ∆, we define the category ∆ C to be the product of ∆-many copies of C. We represent objects and morphisms of this category by maps X : ∆ → Obj(C) and maps

Here, 1) A denotes ∆ A for each well-formed formula ∆ A. 2) π denotes the proof of the premise of each rule. f : ∆ → Mor(C), respectively. Since SMCCs are closed under products, ∆ C is a SMCC by the component-wise tensor product and internal hom:

We then define the indexed SMCCs C by C∆ def = ∆ C.

Folding Product We next introduce the folding product functor T; we later compose it with the symmetric lax monoidal comonad V so that we can derive various ILECs over C. Note that T itself is also an ILEC; set V = Id. The type of T is ∆ * × (∆ C) −→ C, and is defined by

On morphisms, T maps a list permutation in the first argument to the symmetry morphism in C. T is symmetric strong monoidal in each argument. Moreover, each strong monoidal structure interacts well with each other, concluding that it becomes a multi-symmetric strong monoidal functor in the sense of [21] .

3. For f ∈ Idx(∆, ∆ ) and l = i 1 · · · i k ∈ ∆ * , let f (l) denote f (i 1 ) · · · f (i k ). Then it holds T(f (l), A) T(l, T(f ( ), A)) and this isomorphism is natural for A.

Remark 4.1. Usually the !-modal formula !A in linear logic is interpreted by the object consisting of many copies of the same data (referred as uniformity of !A [8] ). We leave the development of uniform folding product as a future work.

Construction of ILEC We now compose the folding product functor with the symmetric lax monoidal comonad V , to derive another ILEC. Let ∆, ∆ be index sets. We define a symmetric strong (hence colax) monoidal functor D :

Here, A ∈ ∆ C, and p and α are morphisms in ∆ C and Idx(∆, ∆ ), respectively. We also define a helper morphism γ l A : T(l, V • A) → V T(l, A) for (l 1 · · · l k ) ∈ ∆ * and A ∈ ∆ C. It is the multiple composite of m A,B :

It is routine to verify that this morphism is monoidal natural on l and A.

Two monoidal natural transformations : Di ∆ → Id ∆ C and δ g,f : 

Hofmann et al., and also Dal Lago et al. employ a realizability semantics to show that the complexity of BLL proof reductions belongs to P-time [19, 10] . In this section we compare their semantics and the simple semantics of GBLL constructed in the previous section. We instantiate C in the previous section with the realizability category over a BCI algebra (A, ·), which is a combinatory algebra based on B, C, I-combinators; see e.g. [2, 20] . We then form the realizability category Ass(A) by the following data: an object is a function f into P + A, where P + is the nonempty powerset construction, and a morphism from f to g is a function h : dom f → dom g with the following property: there exists an element e ∈ A such that for any x ∈ dom f and a ∈ f (x), we have e · a ∈ g(h(x)). The category Ass(A) is symmetric monoidal closed; see e.g. [20, Proposition 4] . The tensor product of f and g is given by (f ⊗ g)(x, y) = {u v | u ∈ f (x), v ∈ g(y)}, where u v is the BCI-algebra element corresponding to λx.xuv [20, Section 2].

Next, let ∆ be a set and consider the power category ∆ Ass(A). Under the axiom of choice, ∆ Ass(A) is equivalently described as follows: an object is a family of functions {f i } i∈∆ into P + A, and a morphism from {f i } i∈∆ to {g i } i∈∆ is a family of functions {h i : dom f i → dom g i } i∈∆ with the following property: there exists a function e : ∆ → A such that for any i ∈ ∆, x ∈ dom f i and a ∈ f i (x), we have e(i) · a ∈ g i (h i (x)).

This power category is quite close to the realizability category introduced in [19, Section 4] and [10, Section 4] . A membership statement a ∈ f i (x) for an object {f i } i∈∆ ∈ ∆ Ass(A) corresponds to a realizability statement i, a x in the realizability category (see [19] ). The major difference between these categories is twofold: 1) In the realizability category, a computability constraint is imposed on e : ∆ → A to achieve the characterization of P-time complexity. 2) Objects in the realizability category are limited to ∆ Ass(A)-objects such that all f i share the common domain. This is to synchronize with the set-theoretic semantics ignoring resource polynomials [19, Section 3] [10, Section 3].

We compute the bounded !-modality using the folding product ILEC T with respect to the indexed SMCC ( ) Ass(A). Let F be a finite set of variables, x ∈ F be a resource variable, p be a resource polynomial and C be a constraint set under F . For any object X in V C ∪{v≤p} (F ∪{v}) Ass(A), the folding product

This is different from the modality over the realizability category introduced in [ 

it only takes a single argument. This is again because their realizability semantics is designed to synchronize with the set-theoretic semantics ignoring resource polynomials -especially it interprets ! x≤p A = A . On the other hand, the bounded quantification computed in (4.4) does not ignore resource polynomials and indexing, as the domain of (4.4) is the index-dependent product j dom(X(i{v → j})). From this, we conjecture that the semantics of BLL using the ILEC T over ( ) Ass(A) realizes an index-dependent set-theoretic semantics of BLL -we leave this semantics as a future work.

We introduced GBLL, a generalization of Girard et al.'s BLL. We analyzed the complexity of cut-elimination in GBLL, and gave a translation from CBLL, an extension of BLL with constraints to GBAL + . We then introduced ILEC as a categorical structure for interpreting the !-modality of GBLL. The ILEC is a Idx-graded linear exponential comonad interacting well with a specified indexed SMCCs. We gave an elementary construction of ILEC using the folding product, and a technique to derive its variants by inserting symmetric monoidal comonads. We gave the semantics of BLL using the folding product on the category of assemblies of a BCI-algebra, and related with the realizability category studied in [19, 10] . Girard's BLL has a great influence on the subsequent development of indexed modalities and implicit complexity theory [16] . Hofmann and Scott introduced the realizability technique to BLL and semantically proved that BLL characterizes P-time complexity [19] . Their work was further enriched and studied by Dal Lago and Hofmann [10] . Gaboardi combined the !-modality involving variable binding with PCF and showed that the combined system is relatively complete [24] .

Bucciarelli and Ehrhard's indexed linear logic with exponential [9] is one of the closest systems to GBLL. However, the type of the !-modality is different: their system derives ∆ ! f A from ∆ A and an almost injective function f : ∆ → ∆; it is a function where each f −1 (i) is finite. To relate their system and GBLL, let us use the finite powerset construction P fin and convert f into its inverse f −1 : ∆ → P fin (∆ ). This exhibits the similarity with GBLL: GBLL relaxes P fin to ( ) * , and takes the inverse as the parameter for the !-modality. The novelty of this work to [9] is that a categorical axiomatization for the ! f modality is identified as an extension of the graded linear exponential comonads [7, 22] . Another novelty is to show that GBLL is enough to encode BLL.

As described in Section 1, the simple form of !-modality ! r A is also widely used in various type systems and programming languages. Examples include: INTML [30] , coeffect calculus [28,7] and its combination with effect systems [13] , Granule language [26] , bounded linear type system [14, 26] , type systems for the analysis of higher-order model-checking [18, 17] , a generic BLL-like logic B S LL over semirings [6] , Fuzz type system for function sensitivity and differential privacy [29, 12, 3] , and many more. A combination of ! r A with dependent type theory called QTT is also introduced in [25] and [4] . Among these systems, each of [12,26,1] supports 1) full universal and existential, 2) full universal and 3) partial universal quantification over grades, respectively.

The categorical structure corresponding to the simple form of !-modality appears in [7, 13, 22] and is identified as semiring-graded linear exponential comonad. Breuvart constructed various examples of semiring-graded linear exponential comonads on relational models of linear logic [6] using his slicing technique. In this work we replaced semirings to Idx, which may be seen as a multi-object pseudo-semiring. In the study of graded monad, Orchard et al. generalize the grading structure from ordered monoids to 2-categories [27] . The main difference from this work is that their generalized graded monad is defined over a single category, while an ILEC is defined over an indexed SMCCs.

A unified view of modalities in type systems

Linear realizability and full completeness for typed lambda-calculi

A semantic account of metric preservation

Syntax and semantics of quantitative type theory

Dissecting Denotational Semantics: From the Well-established H * to the More Recent Quantitative Coeffects

Modelling coeffects in the relational semantics of linear logic

A core quantitative coeffect calculus

On phase semantics and denotational semantics in multiplicative-additive linear logic

On phase semantics and denotational semantics: the exponentials

Typed Lambda Calculi and Applications

Towards a formal theory of graded monads

Linear dependent types for differential privacy

Combining effects and coeffects via grading

Bounded linear types in a resource semiring

Linear logic

Bounded linear logic: A modular approach to polynomial-time computability

An infinitary model of linear logic

Relational semantics of linear logic and higher-order model checking

Realizability models for bll-like languages

Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL

Pseudo-commutative monads and pseudo-closed 2-categories

S0022404902001330, special Volume celebrating the 70th birthday

A double category theoretic analysis of graded linear exponential comonads

24th EACSL Annual Conference on Computer Science Logic, CSL 2015

Linear dependent types and relative completeness

A List of Successes That Can Change the World -Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday

Quantitative program reasoning with graded modal types

Coeffects: Unified static analysis of contextdependence

Distance makes the types grow stronger: a calculus for differential privacy

Computation-by-interaction with effects

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use