Русская Википедия:Линейная логика
Линейная логика (Шаблон:Lang-en — это подструктурная логика, предложенная Шаблон:Нп2 как уточнение классической и интуиционистской логики, объединяющая двойственность первой со многими конструктивными свойствами последней[1], введена и используется для логических рассуждений, учитывающих расход некоторого ресурса[2]. Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для верификации сетевых протоколов, языки программирования, теория игр (игровая семантика)[2] и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации)[3], лингвистика[4].
Описание
Синтаксис
Язык классической линейной логики (Шаблон:Lang-en) может быть описан в форме Бэкуса — Наура:
- Шаблон:Math ::= Шаблон:Math | Шаблон:Math | Шаблон:Math | Шаблон:Math | Шаблон:Math
Где
- логические связки и константы:
| Символ | Значение |
|---|---|
| ⊗ | мультипликативная конъюнкция («тензор», Шаблон:Lang-en) |
| ⊕ | аддитивная дизъюнкция |
| & | аддитивная конъюнкция |
| ⅋ | мультипликативная дизъюнкция («пар», Шаблон:Lang-en) |
| ! | модальность «конечно» (Шаблон:Lang-en) |
| ? | модальность «почему нет» (Шаблон:Lang-en) |
| 1 | единица для ⊗ |
| 0 | нуль для ⊕ |
| ⊤ | нуль для & |
| ⊥ | единица для ⅋ |
Бинарные связки ⊗, ⊕, & и ⅋ ассоциативны и коммутативны.
Каждое утверждение Шаблон:Math в классической линейной логике имеет двойственное Шаблон:Math, определяемое следующим образом:
| Шаблон:Math | Шаблон:Math | ||||
| Шаблон:Math | Шаблон:Math | ||||
| Шаблон:Math | Шаблон:Math | ||||
| Шаблон:Math | Шаблон:Math | ||||
| Шаблон:Math | Шаблон:Math | ||||
| Шаблон:Math | Шаблон:Math |
Содержательное толкование
В линейной логике (в отличие от классической) посылки часто рассматриваются как расходуемые ресурсы, поэтому выведенная или начальная формула может быть ограничена по числу использований.
Мультипликативная конъюнкция ⊗ аналогична операции сложения мультимножеств и может выражать объединение ресурсов.
Следует отметить, что Шаблон:Math является инволюцией, то есть, Шаблон:Math для всех утверждений. Шаблон:Math также называется линейным отрицанием Шаблон:Math.
Линейная импликация играет большую роль в линейной логике, хотя она и не включена в грамматику связок. Может быть выражена через линейное отрицание и мультипликативную дизъюнкцию
Связку ⊸ иногда называют «леденец на палочке» (Шаблон:Lang-en) из-за характерной формы.
Линейную импликацию можно использовать в выводе при наличии ресурсов в ее левой части, а в результате получаются ресурсы из правой линейной импликации. Данное преобразование задает линейную функцию, что и дало начало термину «Линейная логика»Шаблон:Sfn.
Модальность «конечно» (!) позволяет обозначить ресурс как неисчерпаемый.
Пример. Пусть D обозначает доллар, а C — плитку шоколада. Тогда покупку плитки шоколада можно обозначить как Шаблон:Math. Покупку можно выразить следующим выводом: Шаблон:Math, то есть, что доллар и возможность купить на него шоколадку приводят к шоколадке, а возможность купить шоколадку сохраняетсяШаблон:Sfn.
В отличие от классической и интуиционистской логик, линейная логика имеет два вида конъюнкций, что позволяет выражать ограниченность ресурсов. Добавим к предыдущему примеру возможность покупки леденца L. Выразить возможность покупки шоколадки или леденца можно выразить с помощью аддитивной конъюнкцииШаблон:Sfn:
Разумеется, выбрать можно только что-то одно. Мультипликативная конъюнкция обозначает присутствие обоих ресурсов. Так, на два доллара можно купить и шоколадку, и леденец:
Мультипликативная дизъюнкция A ⅋ B может пониматься как «если не А, так B», а выражаемая через неё линейная импликация A ⊸ B в таком случае имеет смысл «может ли B быть выведена из A ровно один раз?»Шаблон:Sfn
Аддитивная дизъюнкция A ⊕ B обозначает возможность как A, так и B, но выбор не за вамиШаблон:Sfn. Например, беспроигрышную лотерую, где можно выиграть леденец или шоколадку, можно выразить с помощью аддитивной дизъюнкции:
Фрагменты
Помимо полной линейной логики находят применение её фрагментыШаблон:Sfn:
- LL: разрешены все связки
- MLL: только мультипликативы (⊗, ⅋)
- MALL: только мультипликативы и аддитивы (⊗, ⅋, ⊕, &)
- MELL: только мультипликативы и экспоненциалы (⊗, ⅋, !, ?)
Разумеется, этим списком не исчерпываются все возможные фрагменты. Например, возможны различные Хорн-фрагменты, которые используют линейную импликацию (по аналогии с хорновскими дизъюнктами) в сочетаниях с различными связками.[5]
Фрагменты логики интересуют исследователей с точки зрения сложности их вычислительной интерпретации. В частности, М. И. Канович доказал, что полный MLL-фрагмент является NP-полным, а ⊕-хорновский фрагмент линейной логики с Шаблон:Нп3 (Шаблон:Lang-en) PSPACE-полон. Это можно проинтерпретировать как то, что управление использованием ресурсов — трудная задача даже в простейших случаях.[5]
Представление в виде исчисления секвенций
Один из способов определения линейной логики — это исчисление секвенций. Буквы Γ и ∆ обозначают списки предложений <math>A_1, ..., A_n</math>, и называются контекстами. В секвенции контекст помещается слева и справа от ⊢ («следует»), например: <math>\Gamma \vdash \Delta</math>. Ниже приведено исчисление секвенций для MLL в двустороннем форматеШаблон:Sfn.
Структурное правило — перестановка. Задано соответственно левое и правое правила вывода:
<math>\cfrac{\Gamma, A, B, \Gamma' \vdash \Delta}{\Gamma, B, A, \Gamma' \vdash \Delta}\; \text{exL}\qquad \cfrac{\Gamma \vdash \Delta, A, B, \Delta'}{\Gamma \vdash \Delta, B, A, \Delta'}\; \text{exR}</math>
Тождество и сечение:
<math>\cfrac{\cdot}{A \vdash A}\; \text{I}\qquad \cfrac{\Gamma \vdash \Sigma, A, \Delta \qquad \Gamma', A, \Sigma' \vdash \Delta'}{\Gamma, \Gamma', \Sigma' \vdash \Sigma, \Delta, \Delta'}\; \text{Cut}</math>
Мультипликативная конъюнкция:
<math>\cfrac{\Gamma, A, B \vdash \Delta}{\Gamma, A \otimes B \vdash \Delta}\; \otimes\text{L} \qquad \cfrac{\Gamma \vdash A, \Delta \qquad \Gamma' \vdash B, \Delta'}{\Gamma,\Gamma' \vdash A \otimes B, \Delta,\Delta'}\; \otimes\text{R} </math>
Мультипликативная дизъюнкция:
<math>\cfrac{\Gamma, A \vdash \Delta \qquad \Gamma', B \vdash \Delta'}{\Gamma, \Gamma', A \text{⅋} B \vdash \Delta, \Delta'}\; \text{⅋L} \qquad \cfrac{\Gamma \vdash A, B, \Delta}{\Gamma \vdash A \text{⅋} B, \Delta}\; \text{⅋R}</math>
Отрицание:
<math>\cfrac{\Gamma \vdash A, \Delta}{\Gamma, A^{\bot} \vdash \Delta}\; \bot\text{L} \qquad \cfrac{\Gamma, A \vdash \Delta}{\Gamma \vdash A^{\bot}, \Delta}\; \bot\text{R}</math>
Аналогичные правила можно определить для полной линейной логики, её аддитивов и экспоненциалов. Обратите внимание, что в линейную логику не добавлены структурные правила ослабления и сокращения, так как в общем случае утверждения (и их копии) не могут произвольно появляться и исчезать в секвенциях, как это принято в классической логике.
Примечания
Литература
Ссылки
- Linear Logic, Stanford Encyclopedia of Philosophy
- ↑ Шаблон:Cite journal
- ↑ 2,0 2,1 Шаблон:Cite web
- ↑ Шаблон:Cite journal
- ↑ Шаблон:Cite book Шаблон:Wayback
- ↑ 5,0 5,1 Max I. Kanovich. The complexity of Horn fragments of Linear Logic. Annals of Pure and Applied Logic 69 (1994) 195—241
