I (_(Jack Waugh)) have seen the term "linear logic" used in a way that has nothing to do with linear equations (described at '''LinearProgramming''').  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:

<pre>foo: anArgument

  ^ anArgument + anArgument</pre>

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

<pre>foo: anArgument

  | tmp1 tmp2 |

  tmp1, tmp2 := anArgument asTwoCopies.
  ^ tmp1 + tmp2</pre>

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

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 or applicative 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

<code>foo at: 1 put: 2</code>

means an array just like <var>foo</var> (assume <var>foo</var> 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 <var>foo</var> 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.

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

_(A website|http://www.linearity.org/)

_(A paper|ftp://publications.ai.mit.edu/ai-publications/1500-1999/AITR-1627.ps)

<hr>

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 LinearLogic 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 <code>const</code>. <code>const</code> 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)
