Ресурстарға сезімтал логика жүйесі

System of resource aware logic

Linear logic is a substructural logic proposed by Jean Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics (because linear logic can be seen as the logic of quantum information theory), as well as linguistics, particularly because of its emphasis on resource boundedness, duality, and interaction. Linear logic lends itself to many different presentations, explanations, and intuitions. Proof theoretically, it derives from an analysis of classical sequent calculus in which uses of (the structural rules) contraction and weakening are carefully controlled. Operationally, this means that logical deduction is no longer merely about an ever expanding collection of persistent "truths", but also a way of manipulating resources that cannot always be duplicated or thrown away at will. In terms of simple denotational models, linear logic may be seen as refining the interpretation of intuitionistic logic by replacing cartesian (closed) categories by symmetric monoidal (closed) categories, or the interpretation of classical logic by replacing Boolean algebras by C* algebras.

Both intuitionistic and classical implication can be recovered from linear implication by inserting exponentials: intuitionistic implication is encoded as !A ⊸ B, while classical implication can be encoded as ! ?A ⊸ ?B or !A ⊸ ? !B (or a variety of alternative possible translations). The idea is that exponentials allow us to use a formula as many times as we need, which is always possible in classical and intuitionistic logic. Formally, there exists a translation of formulas of intuitionistic logic to formulas of linear logic in a way that guarantees that the original formula is provable in intuitionistic logic if and only if the translated formula is provable in linear logic. Using the Gödel–Gentzen negative translation, we can thus embed classical first order logic into linear first order logic.

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 candy, and having a dollar by $1. To state the fact that a dollar will buy you one candy bar, we might write the implication $1 ⇒ candy. But in ordinary (classical or intuitionistic) logic, from A and A ⇒ B one can conclude A ∧ B. 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, 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 $1 ⇒ candy, we express the property of the vending machine as a linear implication $1 ⊸ candy. From $1 and this fact, we can conclude candy, but not $1 ⊗ candy. In general, we can use the linear logic proposition A ⊸ B to express the validity of transforming resource A into resource B. 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 (A ⊗ B) 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 gum ⊗ drink. The constant 1 denotes the absence of any resource, and so functions as the unit of ⊗. Additive conjunction (A & B) 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 $1 ⊸ (candy & chips & drink). We do not write $1 ⊸ (candy ⊗ chips ⊗ drink), which would imply that one dollar suffices for buying all three products together. However, from $1 ⊸ (candy & chips & drink), we can correctly deduce $3 ⊸ (candy ⊗ chips ⊗ drink), where The unit ⊤ of additive conjunction can be seen as a wastebasket for unneeded resources. For example, we can write $3 ⊸ (candy ⊗ ⊤) 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 (A ⊕ B) 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 $1 ⊸ (candy ⊕ chips ⊕ drink). The constant 0 represents a product that cannot be made, and thus serves as the unit of ⊕ (a machine that might produce A or 0 is as good as a machine that always produces A because it will never succeed in producing a 0). So unlike above, we cannot deduce $3 ⊸ (candy ⊗ chips ⊗ drink) from this.