Editing Linear logic (section)

==The resource interpretation==

Lafont (1993) first showed how intuitionistic linear logic can be explained as a logic of resources, so providing the logical language with access to formalisms that can be used for reasoning about resources within the logic itself, rather than, as in classical logic, by means of non-logical predicates and relations.  [[Tony Hoare]] (1985)'s classic example of the vending machine can be used to illustrate this idea.

Suppose we represent having a candy bar by the atomic proposition {{math|<VAR>candy</VAR>}}, and having a dollar by {{math|<VAR>$1</VAR>}}. To state the fact that a dollar will buy you one candy bar, we might write the implication {{math|<VAR>$1</VAR> ⇒ <VAR>candy</VAR>}}.  But in ordinary (classical or intuitionistic) logic, from {{math|<VAR>A</VAR>}} and {{math|<VAR>A</VAR> ⇒ <VAR>B</VAR>}} one can conclude {{math|<VAR>A</VAR> &and; <VAR>B</VAR>}}.  So, ordinary logic leads us to believe that we can buy the candy bar and keep our dollar!  Of course,
we can avoid this problem by using more sophisticated encodings,{{clarify|reason=It is difficult to guess what this might mean without a link|date=May 2015}} although typically such encodings suffer from the [[frame problem]].  However, the rejection of weakening and contraction allows linear logic to avoid this kind of spurious reasoning even with the "naive" rule.  Rather than {{math|<VAR>$1</VAR> ⇒ <VAR>candy</VAR>}}, we express the property of the vending machine as a ''linear'' implication {{math|<VAR>$1</VAR>  ⊸ <VAR>candy</VAR>}}.  From {{math|<VAR>$1</VAR>}} and this fact, we can conclude {{math|<VAR>candy</VAR>}}, but ''not'' {{math|<VAR>$1</VAR> ⊗ <VAR>candy</VAR>}}.  In general, we can use the linear logic proposition {{math|<VAR>A</VAR> ⊸ <VAR>B</VAR>}} to express the validity of transforming resource {{math|<VAR>A</VAR>}} into resource {{math|<VAR>B</VAR>}}.

Running with the example of the vending machine, consider the "resource interpretations" of the other multiplicative and additive connectives.  (The exponentials provide the means to combine this resource interpretation with the usual notion of persistent [[logical truth]].)

Multiplicative conjunction {{math|(<VAR>A</VAR> ⊗ <VAR>B</VAR>)}} denotes simultaneous occurrence of resources, to be used as the consumer directs. For example, if you buy a stick of gum and a bottle of soft drink, then you are requesting {{math|<VAR>gum</VAR> ⊗ <VAR>drink</VAR>}}. The constant 1 denotes the absence of any resource, and so functions as the unit of ⊗.

Additive conjunction {{math|(<VAR>A</VAR> & <VAR>B</VAR>)}} represents alternative occurrence of resources, the choice of which the consumer controls. If in the vending machine there is a packet of chips, a candy bar, and a can of soft drink, each costing one dollar, then for that price you can buy exactly one of these products.  Thus we write {{math|<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> & <VAR>chips</VAR> & <VAR>drink</VAR>)}}.  We do ''not'' write {{math|<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> ⊗ <VAR>chips</VAR> ⊗ <VAR>drink</VAR>)}}, which would imply that one dollar suffices for buying all three products together.  However, from  {{math|(<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> & <VAR>chips</VAR> & <VAR>drink</VAR>)) ⊗ (<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> & <VAR>chips</VAR> & <VAR>drink</VAR>)) ⊗ (<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> & <VAR>chips</VAR> & <VAR>drink</VAR>))}}, we can correctly deduce {{math|<VAR>$3</VAR> ⊸ (<VAR>candy</VAR> ⊗ <VAR>chips</VAR> ⊗ <VAR>drink</VAR>)}}, where {{math|<VAR>$3</VAR> :{{=}} <VAR>$1</VAR> ⊗ <VAR>$1</VAR> ⊗ <VAR>$1</VAR>}}.  The unit ⊤ of additive conjunction can be seen as a wastebasket <!--or [[Garbage collection (computer science)|garbage collector]]--> for unneeded resources. For example, we can write {{math|<VAR>$3</VAR> ⊸ (<VAR>candy</VAR> ⊗ ⊤)}} to express that with three dollars you can get a candy bar and some other stuff, without being more specific (for example, chips and a drink, or $2, or $1 and chips, etc.).

Additive disjunction {{math|(<VAR>A</VAR> ⊕ <VAR>B</VAR>)}} represents alternative occurrence of resources, the choice of which the machine controls.  For example, suppose the vending machine permits gambling: insert a dollar and the machine may dispense a candy bar, a packet of chips, or a soft drink.  We can express this situation as {{math|<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> ⊕ <VAR>chips</VAR> ⊕ <VAR>drink</VAR>)}}.  The constant 0 represents a product that cannot be made, and thus serves as the unit of ⊕ (a machine that might produce {{math|<VAR>A</VAR>}} or {{math|0}} is as good as a machine that always produces {{math|<VAR>A</VAR>}} because it will never succeed in producing a 0). So unlike above, we cannot deduce {{math|<VAR>$3</VAR> ⊸ (<VAR>candy</VAR> ⊗ <VAR>chips</VAR> ⊗ <VAR>drink</VAR>)}} from this.