This is a known result that I’m using in some recent work I am writing up, and so I figured why not write a post about it.
In this post I am going to explain a simplification to Benton’s beautiful LNL models that reduces their complexity, but retains their expressive power. I learned of this simplification from Paul-André Melliès’ writings. First, let’s take a look at the original definition of LNL models, and how they relate to linear categories.
LNL Models
A Linear/Non-Linear (LNL) model is an symmetric monoidal adjunction
Intuitively, we can think of
LNL models are equivalent to Bierman’s linear categories. In fact, I wrote a blog post in 2018 on a simplification to linear categories, so check that post out if you are unfamiliar with linear categories. The of-course modality of linear logic, denoted by
An extremely useful result shown by Benton is that the functor
This is enough to ensure that the category
Given a linear category
To remedy these issues Benton found that the free coalgebras have an internal hom between them which is also free, and thus, by taking the full subcategory of
This is a lot of work to get an internal hom, but is it worth the work? Is it possible to ask for the category
The Simplified Model
Taking the following simplified model we show that it implies a linear category, we do not show the opposite, because it follows as a corollary from the original proof summarized above.
A Simplified Linear/Non-Linear (LNL) model is an adjunction
In the above I highlight the simplifications which are actually generalizations. We can see that this definition removes the requirements that
The requirement that
(p. 108, Proposition 12) Every lax monoidal structure,
on , induces an oplax monoidal structure on , and conversely. Furthermore, these mappings from to and back define an isomorphism giving a one-to-one relationship between the lax monoidal structure on one side of the adjunction and the other.(p. 112, Proposition 14) Suppose
is lax monoidal. Then the adjunction lifts to a monoidal adjunction iff the lax monoidal functor is strong. In the right-to-left case, the lax structure is associated with using part 1 and setting .
We can add symmetry to the above properties, and they still hold. Thus, the second result above gives us a means of recovering a lax monoidal structure on the functor
A Semi-simplified Linear/Non-Linear (SSLNL) model is an symmetric monoidal adjunction
Showing that this definition implies a linear category is easy, we can just use Benton’s proof (p. 16, Section 2.2.1). Thus, the simplified definition of a LNL model implies linear category.
At this point the only question left is, but what about non-linear implications / functions? In the original model the cartesian closed category is a model of non-linear logic / simply-type
We can indeed by first exploiting the adjunction and the fact that
Then there is a bijection:
This is a kind of currying, and is enough to interpret non-linear logic where we encode the formulas in the form of
Then sequents
Using this we can show that every equation in the theory is preserved by the interpretation. This proves that the interpretation soundly models the theory in an LNL model. Faithfulness ensures that every proof is caputed by our model.
This simplifies the model a lot, but how does it affect the syntactic side of things? Well, we get to remove the rules for non-linear implication, and derieve them which is appealing both theoretically and practically.