Linear Logic Comments

[I don't remember how long ago I wrote this. I'm sure that when I did, the current linear logic article wasn't in the Wiki, and I think it very authoritatively replaces this "essay" at least in the latter's original intent. I could see deleting this page, except perhaps for the value of the comments and discussion that people have added after my original text. -- Jack Waugh 2003-08-11]

I have seen the term "linear logic" used in a way that has nothing to do with linear equations (described at Linear Programming?). In the literature I saw, Linear Logic means a discipline where an object reference can only be used once. In fact, you must use it exactly once. To destroy a reference requires an explicit mention. To "split" a reference also does. So for example, where in, say Smalltalk (an imperative OO language), you could write:

foo: anArgument ^ anArgument + anArgument

a linear-logic language would (assuming a similar syntax) require something like

foo: anArgument | tmp1 tmp2 | tmp1, tmp2 := anArgument asTwoCopies. ^ tmp1 + tmp2

(This assumes an extention to Smalltalk syntax where you could have a call return multiple results, which you could then store in variables.)

Since the restrictions I outlined above prevent an object from having more (or less) than one reference to it at a time, there is never shared reference to a mutable object. Consequently, linear-logic languages exhibit referential transparency, so they qualify as pure functional languages. But what linear logic buys you is that an implementation can reuse the storage of an object for a derivitave object. For example, suppose:

foo at: 1 put: 2

means an array just like foo (assume foo is an array) except that the first element has been replaced with the number 2. Then the implementation can just store 2 at the first location in the memory formerly used for foo and can use the same memory for the result. It can do that confidently because it knows that the calling code just used up the reference foo and can't be about to use it again.

Does linear logic simplify garbage collection? Not much, I guess, because if you allow the explicit reference splitting and destroying, you can still generate garbage, and collecting it remains the same problem.

[Where have you taken this idea of splitting references? (This is not a rhetorical question: do you have references?). As you correctly pointed out at the beginning of this essay, [..] Linear Logic means a discipline where an object reference can only be used once. [..] As I understand it, with splitting references you mean duplicate references, correct me if I am wrong. But a split (duplicated) reference is no more a linear reference by its own definition. So linear logic does not simplify garbage collection, but completely avoids it.

See Lively Linear Lisp -- 'Look Ma, No Garbage!' and other Henry Baker's papers on this subject.

Well, I just realized that this is an essay from our old Wiki so he probably will not respond. Anyway his understanding of linear logic seems to me fallacious or I have misunderstood him.. Can anyone enlighten me?

-- Mad70]

The reference on the the splitting of references is:

Ken Kahn, Vijay Saraswat. Actors as a special case of concurrent constraint (logic) programming. In OOPSLA/ECOOP 1990. (See Actor for a link to this paper).

On page 60, top of the right column, the authors mention the necessity of explicitly splitting references in Lucy, the language that the paper introduces as the "missing link" between concurrent constraint programming (represented by the language Janus, which the paper also describes) and the Actor model of Hewitt and Agha.

Rereading my text above, I can imagine a possible source of confusion between two notions of "reference". Those are reference to an immutable object, vs. reference to a mutable object.

Suppose the language only permitted "references" to "immutable objects" (arguably most simply described as simply "values") as arguments and returned values. Then with the constraint of linearity, that you can't ignore an argument nor can you use it in more than one place, there is no need for garbage collection. If you explictly free the value or "object", the implementation knows there are no other "references" to the "object" (as John Carter points out below, the reference count is exactly one), so it can release the memory right away. No need for collection.

In such a language, any notion of "splitting" the "reference" would just be semantically equivalent (except perhaps in regard to time or space performance) to copying the value. That is probably what I was thinking about when I wrote the original example above where I first mentioned splitting.

The reference splitting described by Saraswat and Kahn, however, involves refereces to mutable objects (Actors in their case). So it's not quite the same thing. If you can explicitly split and destroy references to mutable objects, you just as much need a collector as in a language like Smalltalk where the splitting and destroying is implicit.

-- Jack Waugh 2003-08-11

(Linear logic can help when it is rolled into stack-handling, as Monads are often implemented.)

A website

A paper

Think of it as "reference counting on the fingers of one thumb".

It is the way we learnt that the world works back in preschool. If I have an object and I give it to you, I no longer have it. If I take it back, you no longer have it.

My two-year-old toddler understands that.

Now I see Linear Logic as an important simplifier. We have suffered from "pass-by-name", "pass-by-reference", "pass-by-value" semantics long enough. What we really want is "I hand this object to you", "You borrow this object only to read from", "I hand this object to you to modify, you will give it right back again." "You will give an object to me".

C++ makes a baby step towards this with const. const is basically "You can borrow this object to read from".

In fact I claim that the contract between calling routine and function regarding the read only, hand in, modify and hand out semantics is more important than Strict Typing?. The language should require the client to specify which semantics he requires, verify that it matches the called routines declaration and enforce it.

I see this as an important step towards True Encapsulation?. -- John Carter