Введение
Линейная логика — это субструктурная логика, предложенная Жаном Ивом Жираром как развитие классической и интуиционистской логики, объединяющее двойственность первой с множеством конструктивных свойств второй. Хотя эта логика изучалась и сама по себе, в более широком смысле идеи линейной логики оказали влияние на такие области, как языки программирования, семантика игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации), а также лингвистика, особенно благодаря её акценту на ограниченности ресурсов, двойственности и взаимодействию. Линейная логика допускает различные представления, объяснения и интуитивные интерпретации. С точки зрения теории доказательств, она выводится из анализа классического исчисления секвенций, в котором использование (структурных правил) сокращения и ослабления подвергается тщательному контролю. Операционально это означает, что логический вывод — это не просто постоянно расширяющийся набор устойчивых "истин", но и способ манипулирования ресурсами, которые не всегда можно дублировать или произвольно уничтожать. В терминах простых денотационных моделей, линейная логика может рассматриваться как уточнение интерпретации интуиционистской логики путем замены декартовых (закрытых) категорий на симметричные моноидальные (закрытые) категории, или интерпретации классической логики путем замены булевых алгебр на C*-алгебры.
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.
Кодирование классической/интуиционистской логики в линейной логике
И интуиционистское, и классическое следование можно восстановить из линейного следования путем вставки экспоненциалов: интуиционистское следование кодируется как !A ⊸ B, в то время как классическое следование может быть кодировано как !?A ⊸ ?B или !A ⊸ ?!B (или различными альтернативными возможными переводами). Идея заключается в том, что экспоненциалы позволяют нам использовать формулу столько раз, сколько нам нужно, что всегда возможно в классической и интуиционистской логике. Формально существует перевод формул интуиционистской логики в формулы линейной логики таким образом, чтобы гарантировать, что исходная формула доказуема в интуиционистской логике тогда и только тогда, когда переведенная формула доказуема в линейной логике. Используя отрицательный перевод Гёделя — Гентцена, мы можем таким образом встроить классическую логику первого порядка в линейную логику первого порядка.
Интерпретация ресурса
Лафонт (1993) впервые показал, как интуиционистскую линейную логику можно объяснить как логику ресурсов, тем самым предоставляя логическому языку доступ к формализмам, которые могут быть использованы для рассуждений о ресурсах внутри самой логики, а не, как в классической логике, посредством нелогических предикатов и отношений. Классический пример Тони Хоара (1985) о торговом автомате может быть использован для иллюстрации этой идеи. Предположим, что наличие шоколадного батончика мы представляем атомным высказыванием "конфеты", а наличие доллара – $1. Чтобы выразить тот факт, что доллар позволяет купить один шоколадный батончик, мы можем записать импликацию $1 ⇒ конфеты. Но в обычной (классической или интуиционистской) логике из A и A ⇒ B следует A ∧ B. Таким образом, обычная логика приводит нас к убеждению, что мы можем купить шоколадку и сохранить свой доллар! Конечно, мы можем избежать этой проблемы, используя более сложные кодировки, хотя обычно такие кодировки страдают от проблемы фрейма. Однако отказ от ослабления и сжатия позволяет линейной логике избегать такого рода ошибочных рассуждений даже с использованием "наивного" правила. Вместо $1 ⇒ конфеты, мы выражаем свойство торгового автомата как линейную импликацию $1 ⊸ конфеты. Из $1 и этого факта мы можем заключить конфеты, но не $1 ⊗ конфеты. В общем случае, мы можем использовать линейно-логическое высказывание A ⊸ B для выражения допустимости преобразования ресурса A в ресурс B. Развивая пример торгового автомата, рассмотрим "интерпретации ресурсов" других мультипликативных и аддитивных связок. (Экспоненциалы предоставляют средства для объединения этой ресурсной интерпретации с обычным понятием постоянной логической истинности.) Мультипликативная конъюнкция (A ⊗ B) обозначает одновременное наличие ресурсов, которые будут использоваться по усмотрению потребителя. Например, если вы покупаете жвачку и бутылку газировки, вы запрашиваете жвачка ⊗ газировка. Константа 1 обозначает отсутствие какого-либо ресурса и, следовательно, функционирует как единица для ⊗. Аддитивная конъюнкция (A & B) представляет собой альтернативное наличие ресурсов, выбор которых контролируется потребителем. Если в торговом автомате есть пачка чипсов, шоколадный батончик и банка газировки, каждый из которых стоит один доллар, то за эту цену вы можете купить ровно один из этих продуктов. Таким образом, мы записываем $1 ⊸ (конфеты & чипсы & газировка). Мы не записываем $1 ⊸ (конфеты ⊗ чипсы ⊗ газировка), что подразумевало бы, что одного доллара достаточно для покупки всех трех продуктов вместе. Однако из $1 ⊸ (конфеты & чипсы & газировка) мы можем корректно вывести $3 ⊸ (конфеты ⊗ чипсы ⊗ газировка), где единица аддитивной конъюнкции может рассматриваться как мусорная корзина для ненужных ресурсов. Например, мы можем записать $3 ⊸ (конфеты ⊗ ⊤), чтобы выразить, что за три доллара вы можете получить шоколадный батончик и что-то еще, не уточняя (например, чипсы и газировку, или $2, или $1 и чипсы и т.д.). Аддитивная дизъюнкция (A ⊕ B) представляет собой альтернативное наличие ресурсов, выбор которых контролируется машиной. Например, предположим, что торговый автомат допускает азартные игры: вставьте доллар, и машина может выдать шоколадный батончик, пачку чипсов или газировку. Мы можем выразить эту ситуацию как $1 ⊸ (конфеты ⊕ чипсы ⊕ газировка). Константа 0 представляет собой продукт, который невозможно произвести, и, таким образом, служит единицей для ⊕ (машина, которая может произвести A или 0, так же хороша, как машина, которая всегда производит A, поскольку ей никогда не удастся произвести 0). Следовательно, в отличие от предыдущего случая, мы не можем вывести $3 ⊸ (конфеты ⊗ чипсы ⊗ газировка) из этого.
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.