Каждое утверждение A в классической линейной логике имеет двойственноеA⊥, определяемое следующим образом:
(p)⊥ = p⊥
(p⊥)⊥ = p
(A ⊗ B)⊥ = A⊥ ⅋ B⊥
(A ⅋ B)⊥ = A⊥ ⊗ B⊥
(A ⊕ B)⊥ = A⊥ & B⊥
(A & B)⊥ = A⊥ ⊕ B⊥
(1)⊥ = ⊥
(⊥)⊥ = 1
(0)⊥ = ⊤
(⊤)⊥ = 0
(!A)⊥ = ?(A⊥)
(?A)⊥ = !(A⊥)
Содержательное толкование
В линейной логике (в отличие от классической) посылки часто рассматриваются как расходуемые ресурсы, поэтому выведенная или начальная формула может быть ограничена по числу использований.
Мультипликативная конъюнкция ⊗ аналогична операции сложения мультимножеств и может выражать объединение ресурсов.
Следует отметить, что (.)⊥ является инволюцией, то есть, A⊥⊥ = A для всех утверждений. A⊥ также называется линейным отрицаниемA.
Линейная импликация играет большую роль в линейной логике, хотя она и не включена в грамматику связок. Может быть выражена через линейное отрицание и мультипликативную дизъюнкцию
A ⊸ B := A⊥ ⅋ B.
Связку ⊸ иногда называют «леденец на палочке» (англ.lollipop) из-за характерной формы.
Линейную импликацию можно использовать в выводе при наличии ресурсов в ее левой части, а в результате получаются ресурсы из правой линейной импликации. Данное преобразование задает линейную функцию, что и дало начало термину «Линейная логика»[5].
Модальность «конечно» (!) позволяет обозначить ресурс как неисчерпаемый.
Пример. Пусть D обозначает доллар, а C — плитку шоколада. Тогда покупку плитки шоколада можно обозначить как D ⊸ C. Покупку можно выразить следующим выводом: D⊗ !(D ⊸ C) ⊢ C⊗!(D ⊸ C), то есть, что доллар и возможность купить на него шоколадку приводят к шоколадке, а возможность купить шоколадку сохраняется[5].
В отличие от классической и интуиционистской логик, линейная логика имеет два вида конъюнкций, что позволяет выражать ограниченность ресурсов. Добавим к предыдущему примеру возможность покупки леденца L. Выразить возможность покупки шоколадки или леденца можно выразить с помощью аддитивной конъюнкции[6]:
D ⊸ L & C
Разумеется, выбрать можно только что-то одно. Мультипликативная конъюнкция обозначает присутствие обоих ресурсов. Так, на два доллара можно купить и шоколадку, и леденец:
D ⊗ D ⊸ L ⊗ C
Мультипликативная дизъюнкция A ⅋ B может пониматься как «если не А, так B», а выражаемая через неё линейная импликация A ⊸ B в таком случае имеет смысл «может ли B быть выведена из A ровно один раз?»[6]
Аддитивная дизъюнкцияA ⊕ B обозначает возможность как A, так и B, но выбор не за вами[6]. Например, беспроигрышную лотерую, где можно выиграть леденец или шоколадку, можно выразить с помощью аддитивной дизъюнкции:
D ⊸ L ⊕ C
Фрагменты
Помимо полной линейной логики находят применение её фрагменты[7]:
LL: разрешены все связки
MLL: только мультипликативы (⊗, ⅋)
MALL: только мультипликативы и аддитивы (⊗, ⅋, ⊕, &)
MELL: только мультипликативы и экспоненциалы (⊗, ⅋, !, ?)
Разумеется, этим списком не исчерпываются все возможные фрагменты. Например, возможны различные Хорн-фрагменты, которые используют линейную импликацию (по аналогии с хорновскими дизъюнктами) в сочетаниях с различными связками.[8]
Фрагменты логики интересуют исследователей с точки зрения сложности их вычислительной интерпретации. В частности, М. И. Канович доказал, что полный MLL-фрагмент является NP-полным, а ⊕-хорновский фрагмент линейной логики с правилом ослабления[англ.] (англ.weakening rule) PSPACE-полон. Это можно проинтерпретировать как то, что управление использованием ресурсов — трудная задача даже в простейших случаях.[8]
Представление в виде исчисления секвенций
Один из способов определения линейной логики — это исчисление секвенций. Буквы Γ и ∆ обозначают списки предложений , и называются контекстами. В секвенции контекст помещается слева и справа от ⊢ («следует»), например: . Ниже приведено исчисление секвенций для MLL в двустороннем формате[7].
Структурное правило — перестановка. Задано соответственно левое и правое правила вывода:
Аналогичные правила можно определить для полной линейной логики, её аддитивов и экспоненциалов. Обратите внимание, что в линейную логику не добавлены структурные правила ослабления и сокращения, так как в общем случае утверждения (и их копии) не могут произвольно появляться и исчезать в секвенциях, как это принято в классической логике.
↑ 12Max I. Kanovich. The complexity of Horn fragments of Linear Logic. Annals of Pure and Applied Logic 69 (1994) 195—241
Литература
Ломазова И. А.6.5. Вложенные сети Петри и Линейная логика // Вложенные сети Петри: моделирование анализ распределенных систем с объектной структурой. — М.: Научный мир, 2004. — С. 175—185. — 208 с. — ISBN 5-89176-247-1.
Patrick Lincoln. Linear logic // ACM SIGACT News. — 1992. — Т. 23, № 2 (май).