A Mixed Linear and Graded Logic:
Proofs, Terms, and Models

Intuitionistic logic has a central role in the foundations of programming language theory, providing a logical basis for type theories and type systems, and other program reasoning principles. A significant amount of the expressivity of proof systems for intuitionistic logic (both natural deduction and sequent calculus forms) lies within the structure of the hypotheses – the context. Probing the foundations of this part of the logic has, perhaps surprisingly, yielded the very fertile field of substructural logics [39] including influential logics such as linear logic [14] and its variants, and the Lambek calculus [25].

By restricting the manipulation of hypotheses in the context we typically arrive at logics which align more closely with physical reality, where propositions are instead “resources” that cannot necessarily be copied, discarded, or reordered. Such restricted logics have been used to construct type systems for safely manipulating values that should be treated in a resourceful way, such as file handlers, pointers to mutable memory, or channels [43, 42].

However, such pervasive restrictions often hamper expressivity and thus some substructural logics then seek to carefully control the reintroduction of structural rules. For example, linear logic provides the $!$ modality (“of course”) for reintroducing weakening and contraction of propositions, which linear logic otherwise prohibits. However, this modality is coarse-grained: for those propositions under the modality, it re-enables all the structural rules that have been removed in linear logic. Subexponentials instead aim to be more fine-grained, offering families of modalities capturing specific structural rules [8, 22]. The related notion of grading [12, 31] gives an alternate view, providing an indexed family of modalities whose indices are subject to an algebra which accounts for any structural rules applied: structural rules are “counted” by the algebra (whose operations mirror the shape of structural rules). Bounded Linear Logic [15] is a special case where the family of modalities ${!}_{n}A$ uses indices $n$ which are natural numbers (or polynomial terms over naturals) counting the upper bound on usage of the proposition $A$. Various systems generalise this approach to arbitrary semirings to capture data-flow properties [1, 2, 5, 12, 13, 24, 28, 31, 33, 34, 36]. Such graded systems annotate hypotheses/variables in the context with elements of the semiring (“grades”) denoting their usage, e.g., $x{:}_{0}A⊢t:B$ types a term $t$ which does not use $x$ and $y{:}_{1+1}A⊢t^{\prime }:B$ types a term $t^{\prime }$ in which $y$ is used in two different subterms once each, accounted for by the semiring addition. A graded modality internalises the semiring grade, causing a multiplication to the grades of any captured dependencies when the graded modality is introduced, e.g., $y{:}_{0\ast (1+1)}A⊢\mathrm{\square }{t}^{\prime }:{\mathrm{\square }}_{0}B$.

We seek here to further understand the underlying structure of graded modal logics by following an “adjoint resolution” approach à la Benton’s seminal “A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models” at CSL 1994 [3]. Benton showed that the exponential modality of linear logic (modelled by a comonad) can be decomposed into an adjunction, defining a pair of “adjoint” logics (a linear logic and a non-linear intuitionistic, or “Cartesian”, logic) which embed into each other [3]. This provides a beautiful reduction of the core features of linear logic and its non-linearity modality. Adjoint logic applies the same idea but to subexponentials [37, 38]. We follow the same scheme, via the adjoint decomposition of graded modalities which generalise linear logic’s $!$ and which are traditionally modelled by graded exponential comonads [5, 6, 12, 13, 24, 34]. Whilst Benton’s work has a pair of adjoint modalities mediating between the two sublogics, we have a pair of a modality $\mathrm{𝖫𝗂𝗇}$ and a graded modality ${\mathrm{𝖦𝗋𝖽}}_r$. We give a categorical model, showing that these are captured by an LNL-like adjunction paired with a “strict action” for incorporating the grading, following the Fujii-Katsumata-Melliès adjoint decomposition of graded (co)monads [10, 24]. The result is a pair of logics which serve to explain and clarify the relationship between linearity and grading. We call our system Mixed Graded/Linear ($\mathrm{𝗆𝖦𝖫}$) Logic.

This pair of logics also shines light on a relationship between two styles of graded system in the literature: those which take linear types as their basis augmented with a graded modality [6, 12, 31] versus those with no base notion of linearity where grading is pervasive, tracking all substructurality [1, 2, 4, 7, 28, 30, 34]. Our linear fragment is analogous to the former whilst our graded fragment is analogous to the latter. The mutual embedding shows that these two styles of graded logics have a similar relationship to the adjoint relationship of intuitionistic logic and linear logic.

Aside from the internal motivation of better understanding the relationship between grading and linearity, an external motivation for this work is that it can provide a basis for flexible, safe programming with resources. By separating out the linear fragment from an intuitionistic graded fragment, one could avoid the strictures of linearity for working with standard data types which need not be linear, working only in the linear fragment for handling resources like file handles. The mutual embedding would allow the programmer to move smoothly between these two subcalculi, as seen also in other adjunction-based calculi, e.g., for concurrent programming [35]. The focus here however is on the core theory rather than developing these applications yet.

Since our focus is on the relationship between grading and linearity, we consider the semiring-graded modalities that generalise linear logic’s $!$. Other flavours of graded modality (e.g., graded monads for capturing side effecting behaviour [23, 32]) are not considered here.

We present first a sequent calculus for Mixed Graded/Linear logic, which comes in the form of a term assignment. Figure 1 collects the term syntax for reference; it will also be used in Section 4 for the natural deduction formulation. The syntax is explained with reference to its associated proof rules in the next section.

Benton’s approach has two proof systems [3]: one system of linear propositions (the L of LNL) with two contexts for linear and non-linear propositions respectively, and one system of non-linear propositions (the NL in LNL). We generalise this approach to the graded setting by replacing the non-linear parts with graded notions. Thus, our system ($\mathrm{𝗆𝖦𝖫}$) has two analogous proof systems: one of linear propositions with two contexts for linear and graded propositions, with judgments subscripted as ${⊢}_{\mathrm{𝖬𝖲}}$ (for “Mixed (linear/graded) Sequent”), and one system of graded propositions, with judgments subscripted as ${⊢}_{\mathrm{𝖦𝖲}}$ (“Graded Sequent”).

The syntax of Benton’s propositions is split into two, “conventional” (i.e., Cartesian / non-linear) and linear [3]. The syntax of our propositions is analogously split into two, graded and linear:

where $𝖩$ and $𝖨$ are unit types, and $⊠$ and $\otimes$ are tensor (product) operators in their respective domains. In the case of the linear domain, the product is the standard multiplicative conjunction. The $\mathrm{𝖫𝗂𝗇}$ modality encapsulates a linear proposition as a graded proposition, and the ${\mathrm{𝖦𝗋𝖽}}_r$ modality encapsulates a graded proposition (at grade $r$, whose structure is defined below) as a linear proposition. Thus, the two logics are interconnected by ${\mathrm{𝖦𝗋𝖽}}_{r}X$ and $\mathrm{𝖫𝗂𝗇}A$. Using these two modalities we will later define graded modalities ${\mathrm{\square }}_{r}A$ as ${\mathrm{𝖦𝗋𝖽}}_r(\mathrm{𝖫𝗂𝗇}A)$, similarly to how the of-course modality $\mathrm{!}A$ can be defined in LNL logic as the composition of two adjoint modalities.

The semiring governs the structural rules: the additive part of the semiring is involved in weakening and contraction, and the multiplicative part in usage and composition. Various concrete examples of interesting semirings are given at the end of Subsection 2.1.

Section 4 develops an equivalent natural deduction formulation of $\mathrm{𝗆𝖦𝖫}$. We then show that the natural deduction and the sequent calculus are interderivable without modifying the term witnessing a derivation. Thus, any semantic model of one is a model of the other. We opt to focus on the sequent calculus form for now without loss of generality.

We detail a denotational model for $\mathrm{𝗆𝖦𝖫}$ which is based on an adjoint decomposition of graded comonads. We introduce key definitions as needed.

A graded comonad can be summarised as a colax monoidal functor $\mathrm{\square }:ℐ\to [𝒞,𝒞]$ where $ℐ$ is a preordered monoid $(ℐ,1,\ast ,\le )$ treated as a monoidal category and $[𝒞,𝒞]$ is the category of endofunctors on $𝒞$ [33, 34]. Colax monoidality of $\mathrm{\square }$ means that the laws of a monoidal functor become 2-cells, providing the graded comonad operations:

which are thus natural transformations ${\epsilon }_A:{\mathrm{\square }}_{1}A\to A$. and ${\delta }_{r,s,A}:{\mathrm{\square }}_{(r\ast s)}A\to {\mathrm{\square }}_r({\mathrm{\square }}_{s}A)$.

Fujii et al. [10] gave a formal theory for graded monads, which can be easily dualised to graded comonads, showing that in an analogous way to an ordinary comonad, every graded comonad can be decomposed into an adjunction $\mathrm{𝖬𝗇𝗒}⊣\mathrm{𝖫𝗂𝗇}:ℳ\to 𝒞$ and (key to graded comonads) a monoidal action $\odot :ℛ\times 𝒞\to 𝒞$, and thus vice versa:

Along with some additional structure relating to substructurality (see below), this result provides a model of $\mathrm{𝗆𝖦𝖫}$ with $𝒞$ providing a model for $\mathrm{𝖦𝖲}$ derivations, $ℳ$ providing a model for $\mathrm{𝖬𝖲}$ derivations, the type constructor ${\mathrm{𝖦𝗋𝖽}}_r$ transporting from $\mathrm{𝖦𝖲}$ to $\mathrm{𝖬𝖲}$ modelled by $𝖫(r\odot -):𝒞\to ℳ$, and type constructor $\mathrm{𝖫𝗂𝗇}$ transporting $\mathrm{𝖬𝖲}$ to $\mathrm{𝖦𝖲}$ modelled by $𝖱:ℳ\to 𝒞$.

However we need additional structure for the (sub)structural behaviour of our logic. In the literature on graded modal type theories, graded comonads are extended to graded exponential comonads (sometimes called graded linear exponential comonads [24]) defined as a colax monoidal functor $\mathrm{\square }:ℛ\to [ℳ,ℳ]$ where $ℛ$ is a preordered semiring $(ℛ,1,\ast ,\mathrm{𝟢},+,\le )$ (viewed as a category), $[ℳ,ℳ]$ is the category of symmetric lax monoidal endofunctors on a symmetric monoidal category $ℳ$, and $\mathrm{\square }$ has additional symmetric lax monoidal structure for the additional monoidality of $ℛ$ and $[ℳ,ℳ]$ [12]. This additional structure provides natural transformations $w_A:{\mathrm{\square }}_{\mathrm{𝟢}}A\to 1$ and $c_{r,s,A}:{\mathrm{\square }}_{(r+s)}A\to ({\mathrm{\square }}_{r}A)\otimes ({\mathrm{\square }}_{s}A)$ capturing (graded) weakening and contraction, subject to comonoidal coherence conditions. This additional structure can be induced by the adjoint decomposition given an exponential action:

If we have all of the above properties then we refer to $\odot$ as an exponential action. This terminology recalls the exponential action of Brunel et al. [6] which is the same as the above but where strictness is instead laxness in their definition. Our definition is also similar to linear exponential graded comonads (see e.g., [24, 12]), but here the graded comonad is uncurried (in the form of an action) and has equalities for its natural transformations (strictness).

We define a strict exponential action to be an exponential action as above but where the monoidal structure $m_{𝖩}$ and $m_{⊠}$ is also strict, where for clarity (in the appendix) we sometimes orient the equality as a morphism, where in the opposite direction we denote these morphisms by $n_{𝖩,r}$ and $n_{⊠,r,X,Y}$ respectively. Strictness of the monoidal structure is needed for soundness of our model.

We now give the definition of the model of $\mathrm{𝗆𝖦𝖫}$, where we now use the opposite category ${ℛ}^{\mathrm{𝗈𝗉}}$ to capture the correct polarity of the approximation rules.

Thus an $\mathrm{𝗆𝖦𝖫}$ model is essentially an LNL model with a strict action. However, whilst Benton’s LNL models are initially stated to require that $ℳ$ is Cartesian closed, he goes on to show that Cartesian properties are induced for the Eilenberg-Moore category of $!$-coalgebras for a symmetric monoidal category [3]. In our setting, the Cartesian structure is not needed since the $\mathrm{𝖬𝖲}$ logic is a mix of graded and linear logic, rather than Cartesian and linear logic. That is, graded propositions do not have arbitrary weakening and contraction, but instead these structural rules are controlled by grades (and corresponding underlying categorical structure [12, 24]). Therefore, a symmetric monoidal closed $ℳ$ suffices.

From Definition 17, we define our denotational model of $\mathrm{𝗆𝖦𝖫}$:

Finally, we have our soundness and completeness theorems:

We now develop a natural deduction formulation of $\mathrm{𝗆𝖦𝖫}$. Whilst sequent calculus judgments were denoted ${⊢}_{\mathrm{𝖬𝖲}}$ and ${⊢}_{\mathrm{𝖦𝖲}}$, natural deduction judgments are correspondingly ${⊢}_{\mathrm{𝖬𝖳}}$ and ${⊢}_{\mathrm{𝖦𝖳}}$.

The syntax for terms is identical to the sequent calculus, collected in Figure 1. Appendix B [40] gives the introduction and elimination rules and structural rules for $\mathrm{𝗆𝖦𝖫}$’s natural deduction formulation. The unit constructors are $𝗃$ and $𝗂$. Tensor products in both systems are denoted by pairs of terms with corresponding let-expressions for eliminators. The graded modal introduction form $\mathrm{𝖫𝗂𝗇}l$ operates on mixed terms, dual to $\mathrm{𝖦𝗋𝖽}rt$ which operates on graded terms. The mixed syntax includes abstraction $\lambda x.l$ and function application $l_1{l}_2$.
The most interesting aspect is the rules for the modal operators:

In the sequent calculus presented in Section 2, the right rule for $\mathrm{𝖫𝗂𝗇}$ is in the graded subsystem, but the left rule is in the mixed subsystem. A similar idea arises here, the introduction rule for $\mathrm{𝖫𝗂𝗇}$ (rule ${\mathrm{𝖫𝗂𝗇}}_I$) is in the graded subsystem and the elimination rule (rule ${\mathrm{𝖫𝗂𝗇}}_E$) is in the mixed subsystem. Introducing ${\mathrm{𝖦𝗋𝖽}}_r$ formulas (rule ${\mathrm{𝖦𝗋𝖽}}_I$) has the effect of scaling the input grades by $r$. The elimination rule for ${\mathrm{𝖦𝗋𝖽}}_r$ (rule ${\mathrm{𝖦𝗋𝖽}}_E$) is a pattern match on the form of $l_1$. Since $\mathrm{𝖫𝗂𝗇}$ and $\mathrm{𝖦𝗋𝖽}$ are the decomposition of graded modalities (Section 3), the form of the elimination rule for ${\mathrm{𝖦𝗋𝖽}}_r$ is defined in a way which resembles that of elimination rules for graded modalities in other natural deduction-based type systems [31].

This formulation also has explicit graded structural rules:

In the transition from sequent calculus to natural deduction, left rules transform into elimination rules, and as a result the additional graded left rules in the mixed sequent calculus are no longer explicitly part of the system, but can be derived. We go on to prove that the sequent calculus of Section 2.1 is equivalent to the natural deduction system.

We give two main results related to the natural deduction system; the first is substitution for typing. Note that this reuses the row-vector multiplication operation of Section 2.2.