What would you do with a new model of linear logic?

Question

I have been working for some time with collaborators developing some models of linear logic which we are confident are new. However, none of us is deep enough in the field to answer the sceptic's question of "So what?"

Certainly there are people who are working in the domain who appear to have legitimate computer science or philosophical justifications for studying them. For example, one might want the model to include further features (interpreting an extension of linear logic), such as fixed point operations or differentiation in the form of codereliction. Since our models haven't been built with such extensions in mind, we don't know ahead of time if it's possible to extend the interpretation of linear logic, but more importantly we don't know what features people would be interested to find. Another example would be avoiding degeneracy: ensuring that the components of LL have distinct semantics, which is not the case in simple models such as the relational model. Of course we'll check these details, but we don't know what would be considered surprising or desirable here either.

So if I presented you with a fresh class of models of LL, what would you want to know about them? What would make them interesting to you? What problems would you hope that they could provide solutions to?

(I am deliberately omitting any details of the models because I am interested in general guidance and open questions.)

Answer 1

Linear logic is very valuable in the theory of programming languages, so one way of looking at your question is to see what value these new models have in terms of programming languages.

Most of the usefulness of models of programming languages lies in the "tension" between syntax and semantics. Here are a few items reflecting this tension (without pretension of being exhaustive) :

• negative results about expressiveness: by showing that a programming language has a model in which a certain feature does not exist, you show that that feature is not expressible in the syntax of the language. This has been done occasionally ("parallel or" in the $\lambda$-calculus, for example).
• full abstraction: it's a crucial problem of programming languages theory: find a model of a given programming language equating exactly those programs which are observationally equivalent in some given sense. This is one way of saying that syntax and semantics perfectly match.
• full completeness: this is when the interpretation functor is full: given two types $A,B$, each map $[A]\to[B]$ in the model corresponds to a program $A\to B$ in the programming language (or to a proof of the logical system).
• new programming constructs: if the model is not fully abstract or fully complete, then it has "more stuff" than the syntax. What is this extra stuff? Is it computationally interesting?
• finer interpretation of the syntax: maybe your model does not really add expressiveness but it provides an interpretation of the syntax which is interesting in its own way, for example because it suggests that certain features of the language may be expressed as composition of simpler features.
• quantitative features: in many cases, models of linear logic have the ability to say something quantitative about the dynamics of programs, e.g., how many steps does it take to reach a normal form? Maybe your models can be interesting in this sense.
• pure $\lambda$-calculus: this is more of a "niche" topic, but there are people who are interested in so called $\lambda$-theories (congruences on untyped $\lambda$-terms including $\beta$-equivalence) and with finding models yielding exactly a given $\lambda$-theory (I think there are open problems in this respect). If the Kleisli category of the comonad interpreting $!(-)$ in your model has a reflexive object (this is not always the case), then you have a model of the untyped $\lambda$-calculus and this model induces a $\lambda$-theory. It might be an interesting one!

In most cases, as you say, one builds a model with one of the above points in mind. For example, one has a language with certain features (non-determinism, probabilistic execution, quantum programming...) and tries to build a model of linear logic capable of interpreting those features. Or, in the other direction, one wants to build a model based on certain mathematical structures, and then import those structures in the syntax (this was the case of differential linear logic). Examples of the fifth bullet point are rare: linear logic itself was born in that way, another example is the study of polarity in linear logic via models in which connectives decompose through a polarity change.

Finally, a good idea is to go talk directly with experts in models of linear logic who are near you and are not present on MathOverflow. In your case, the first name that comes to my mind is Thomas Ehrhard. For what concerns models of the $\lambda$-calculus, an expert is Giulio Manzonetto. They are both in Paris and will be happy to take a look at your new models!

Answer 2

The first thing I'd do with a new model is to see how it relates to things I already know. For example, how does it relate to game semantics? What happens if I add weakening and contraction to the logic --- do I get some known models for more traditional logics?

The second thing I'd do is to try to develop an intuitive understanding of the new model. I'd hope that a good understanding could lead to some theorems, but I wouldn't try to guess theorems, or even general topics to be addressed by theorems, before getting an intuitive understanding.

Answer 3

The previous answers talk a lot about syntax and the computer science view. You can also start from the model and say: "Linear logic is a syntax for this model. You can talk about this model using the language of linear logic". This would be a more mathematical perspective. You can argue in this way if your model contains known mathematical structures, that people already find interesting.

But if were you, I would not care a lot about whether people will find this model useful or not, only about its intrinsic value. I don't think the goal of research is to please the community. I see much more value into the originality of some development. However, I would still care about the community in this way: if I don't publish anything, the added value for the community will be zero. So if this model seems to me at least a bit interesting, I will try to save it into the litterature.

A last word: degeneracies are not necessarily bad. The product and the coproduct are the same in Rel or in Vec. It creates a new feature: biproducts from which arise matrices and linear algebra. Note that in this way every model of differential linear logic with additive connectors is degenerate as a model of linear logic. When two connectors are equal, it gives new possibilities for building proofs by creating new situations where you can use the cut rule. You then have to think about how to eliminate these new cuts. From the point of view of proofs and morphisms, as opposed to formulas and provability, degeneracies provide a richer logic. In a sense, you have less formulas but more proofs.