25
$\begingroup$

Probably the most common application of linear types in PL is to use them to give languages which control aliasing (i.e., a linear value has a single pointer to it, more or less).

But there's a slight mismatch between this usage and typical denotational models of linear logic. IIRC, Benton showed that if a Cartesian closed category has a strong commutative monad, then its category of algebras will be symmetric monoidal closed (ie, a model of linear logic). But this theorem doesn't apply to the alias-control usage, since the state monad is not commutative. And indeed, in the past few years Simpson and his coworkers have given calculi for general strong monads, which are not term calculi for linear logic.

So my question is, what is the denotational semantics of linear languages with state? Is there a non-degenerate (ie, tensor is not a Cartesian product) symmetric monoidal closed category in which allocation, reading, and linear update can be modeled?

$\endgroup$
2
  • 7
    $\begingroup$ This is the kind of question I would be expecting you to be answering Neel, not asking. ;-) $\endgroup$ Nov 8, 2010 at 22:20
  • 6
    $\begingroup$ if you can attract researchers to cstheory.stackoverflow.com who are capable of answering this question, then the world will be a better place for it. $\endgroup$ Nov 11, 2010 at 10:11

2 Answers 2

9
$\begingroup$

It seems to me that the direction you should consider looking in revolves around game semantics for general references and the related semantics for linear logic, such as those based on Conway games. An algebraic account of references in game semantics by Paul-André Melliès and Nicolas Tabareau is probably the best place to start. In this paper linear logic is relaxed to so-called tensor logic to get things to work, so it is not quite the setting you want. But they do rely on Conway games, so there is certainly a connection with models of linear logic. They also do not really exploit linearity as in linear types, but the machinery is there to do so if you want to, I believe.

The work of Jim Laird (such as A Game Semantics of Names and Pointers) and Guy McCusker may also contribute to your quest. The recent interesting thesis Game semantics for an object-oriented language by Nicholas Wolverson pushes these ideas further in an OO setting. He considers in detail linear threading, only one operation active at a time, and describes how to add linear classes. Both rely on linear typing. Again, however, the underlying model is not strictly a model of linear logic, but it's close.

$\endgroup$
4
  • 1
    $\begingroup$ Just curious Neel. Was this of any use to you, or did you know about all of this stuff already? $\endgroup$ Nov 15, 2010 at 14:04
  • $\begingroup$ I know this stuff (but not well), but game semantics is a lot more sophisticated than what I'm looking for. Most people have an intuition for linear state which is not far from the old-fashioned Strachey view of an imperative computation as an element of a monadic type $T(A) = S \to A \times S$, and I was hoping there was a model of linear state which would resemble that. Basically, I was hoping there was something you could show a first-year grad student without terrifying them. :) $\endgroup$ Nov 17, 2010 at 11:36
  • 1
    $\begingroup$ Maybe Uday Reddy's Global state considered unnecessary: An introduction to object-based semantics, J. Lisp and Symbolic Computation, 9(1996):7-76. $\endgroup$ Nov 17, 2010 at 11:49
  • $\begingroup$ I'm reading that now, actually! $\endgroup$ Nov 17, 2010 at 13:52
8
$\begingroup$

(Gosh, Neel, that was a tough question.)

The "folk model" of linear logic is definitely the coherent spaces model, discussed in Girard's Linear Logic paper (and also in "Proofs and Types"). This is not degenerate in the sense you describe.

Whether this semantics throws any light on how a linear functional language can be implemented, I am not sure. When you are talking about allocation, reading and linear update, you are indeed talking about the implementation. So, perhaps, your question might be formulated as, "how do I prove correct the implementation of a linear functional language that uses state-update?" I don't know the answer to that, but I think it must exist in the papers that propose linear update implementations.

$\endgroup$
5
  • $\begingroup$ Actually, it's too easy to prove the correctness of implementations of linear state -- linearity is such a strong structural constraint that you hardly need any semantics to do these proofs. As a result, I don't know a simple denotational semantics of linear state. The two closest things to what I want are your work on object-based semantics, and the "length spaces" model of Hofmann in his work on implicit complexity. $\endgroup$ Feb 29, 2012 at 11:21
  • $\begingroup$ Actually, I wouldn't describe object-based semantics as modeling "linear state". It is rather "sequential state" and "linear objects", the latte being imposed by SCI. The games models of Idealized Algol, which are also "object-based" in the same sense, don't have linear anything. $\endgroup$
    – Uday Reddy
    Feb 29, 2012 at 13:37
  • $\begingroup$ Can you some references for where such correctness proofs might be found? (Sorry, turning the question back at you!) $\endgroup$
    – Uday Reddy
    Feb 29, 2012 at 13:38
  • 1
    $\begingroup$ The simplest soundness proof for a linear language with state I know is Ahmed, Fluet and Morisett's "L3: A Linear Language with Locations". (ttic.uchicago.edu/~amal/papers/linloc-fi07.pdf) In the paper, they give a simple logical relation, but mention that a syntactic progress-and-preservation proof also goes through. $\endgroup$ Feb 29, 2012 at 13:55
  • $\begingroup$ Here is another piece of work that just came to my attention. Try citeseer for Stephen Cooper, "On Linear Types and Imperative Update" link. I should have known about this, but didn't. $\endgroup$
    – Uday Reddy
    Mar 1, 2012 at 0:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.