Now the question is in Twitter, pestering me again, and I still do not have a proper answer. But I have a suggestion, given to me by Luiz Carlos Pereira, a good friend and collaborator. (It took me more than 3 hours ransacking my old notebooks to find it, so I feel that I should write it down, as well as I can, in this week of drowning-by-reviews...)
Now, everyone knows and some of us do enjoy shopping. The earlier Linear Logic examples were all about Camels and Malborough packets. Some people decided to change them to chocolate and coffee, but the vending machines stayed. Now in this era of Amazon and Walmart, let us describe a "FashionMall Semantics". (In Rio, "fashion mall" is not a common noun compound, but a proper noun. It's a sophisticated shopping center in one of the most unequal, on your face, terrible, parts of town, where the `favela' and the uber-consumption face each other, in threatening ways. still...)
Anyways the FashionMall in Sao Conrado has all kinds of stores you might want to buy nice things from. So if the mall issued tickets for shopping, you could think of these tickets as ways of satisfying consumers' orders:
- If the mall gave you a ticket marked A\otimes B, then the mall has to have both A and B in stock and when you use your ticket, you take both A and B home.
- If the mall gave you a ticket marked A&B, their stock has to have both, but you, the customer, can only take one of them home. You can choose which one A or B you take home.
- If the mall gave you a ticket marked A\oplus B, the stock only has to have one of A or B and the seller will choose which one it will give you.
So far so good and similar to other explanations of Linear Logic using commercial transactions. But what can we say about A\par B? Well, if the mall gives you a ticket marked A\par B they must have both in their stock, you, the customer can only take one home, but you can take it back to the mall and swap it for the other one, if you want to do it. (The par operator is commutative, in the way that linear implication is not...)You do have to keep one of the two (A or B), though.
So more interesting still, if the mall gave you a ticket marked A\lollipop B what can we say? Then we have a complicated transaction: if the buying of the antecedent A is satisfied, then the buying of the consequent B has to be satisfied, whatever these buyings may be. (some might use "higher-order rule" to describe this transaction, but this is somewhat familiar from BHK-style interpretations.) Following this line of reasoning, a transaction A\lollipop \bot could be a transaction that cannot be satisfied.
And the units of Linear Logic, what happens to them? Well some "buys" cannot be satisfied, because the mall does not have the required stock. Other buys cannot be satisfied independently of the stock, just relating to what the costumer and the seller want to do.
There is much more that we need to work out to make sure these intuitive notions agree with the mathematics of Full Intuitionistic Linear Logic, but I hope this is enough to start the conversation. (and it gives me the chance to post a picture of friends Per, Steve and Richard, as well as the late Vladimir Voevodsky whom I had never had the pleasure of meeting: he really seemed a nice guy.)