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.
A Linear/Non-Linear (LNL) model is an symmetric monoidal adjunction , where:
Intuitively, we can think of as a model of intuitionistic logic (or the simply-typed -calculus), as a model of intuitionistic linear logic, and the functors and as modalities that allows one to translate formulas on one side to the other. The adjunction ensures that these translations are well behaved.
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 , is characterized in linear categories by a symmetric monoidal comonad on a symmetric monoidal closed category. Benton showed that we can define the of-course modality as , and hence, is the comonad induced by the adjunction. Furthermore, since the adjunction is monoidal and between two symmetric monoidal functors, the induced comonad is symmetric monoidal as well.
An extremely useful result shown by Benton is that the functor is strong monoidal; e.g., the following isomorphisms hold:
This is enough to ensure that the category with the induced comonad of the adjunction forms a linear category. Thus, LNL models imply linear categories, but the other direction is more interesting.
Given a linear category we need to find a cartesian closed category and a symmetric monoidal closed category that form an LNL model. It is well known that for any comonad on some category , there are two adjunctions and between the category and the coEilenberg-Moore category – the category of -coalgebras – and the Kleisli category – the category of free -coalgebra respectively, where and are the forgetful and free functors. Benton showed that is cartesian, but it is not the case in general that is, because the product of two free coalgebras may not be free. Furthermore, neither of these are closed in general.
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 of all the exponential objects – objects with an internal hom – then we get a cartesian closed category, and this full subcategory contains . Then he identifies a second cartesian closed category of all of the finite products of free coalgebras in the category of exponential objects. We can use either of these to form a LNL model.
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 in the definition of LNL model to be simply cartesian, and then finding such a category from a linear category is easy, it’s . The answer turns out to be positive.
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 , where:
In the above I highlight the simplifications which are actually generalizations. We can see that this definition removes the requirements that be closed, the adjunction be symmetric monoidal, and the functor be monoidal. This is nice, because generalizing the definition makes finding LNL models easier.
The requirement that be strong symmetric monoidal paired with an adjunction is a particularly strong property. First, suppose is an adjunction between monoidal categories; so and are plan functors. The there are two really nice results:
(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 . Therefore, simplified LNL models imply the following definition:
A Semi-simplified Linear/Non-Linear (SSLNL) model is an symmetric monoidal adjunction , where:
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 -calculus and on the other side we have a model of linear logic. Can we still obtain an encoding of non-linear logic using the simplified definition?
We can indeed by first exploiting the adjunction and the fact that is closed. Let and be objects in and respectively. Then define the object:
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 for linear formulas in . In more detail, the interpretation is in the form of a faithful functor defined on types as follows:
Then sequents are interpreted as morphisms from to .
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.