Interested Article - Линейная логика

Линейная логика ( англ. Linear Logic) — подструктурная логика , предложенная как уточнение классической и интуиционистской логики , объединяющая двойственность первой со многими конструктивными свойствами последней , введена и используется для логических рассуждений, учитывающих расход некоторого ресурса . Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для верификации сетевых протоколов , языки программирования , теория игр () и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации ) , лингвистика .

Описание

Синтаксис

Язык классической линейной логики ( англ. classic linear logic, CLL) может быть описан в форме Бэкуса — Наура :

A ::= p ∣ p ^⊥ | A ⊗ A ∣ A ⊕ A | A & A ∣ A ⅋ A | 1 ∣ 0 ∣ ⊤ ∣ ⊥ | ! A ∣ ? A

Где

p и p ^⊥ — атомарные формулы ,

логические связки и константы:

Символ	Значение
⊗	мультипликативная конъюнкция («тензор», англ. "tensor")
⊕	аддитивная дизъюнкция
&	аддитивная конъюнкция
⅋	мультипликативная дизъюнкция («пар», англ. "par")
!	модальность «конечно» ( англ. "of course")
?	модальность «почему нет» ( англ. "why not")
1	единица для ⊗
0	нуль для ⊕
⊤	нуль для &
⊥	единица для ⅋

Бинарные связки ⊗, ⊕, & и ⅋ ассоциативны и коммутативны .

Каждое утверждение 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) из-за характерной формы.

Линейную импликацию можно использовать в выводе при наличии ресурсов в ее левой части, а в результате получаются ресурсы из правой линейной импликации. Данное преобразование задает линейную функцию , что и дало начало термину «Линейная логика» .

Модальность «конечно» (!) позволяет обозначить ресурс как неисчерпаемый.

Пример. Пусть D обозначает доллар, а C — плитку шоколада. Тогда покупку плитки шоколада можно обозначить как D ⊸ C . Покупку можно выразить следующим выводом: D ⊗ !( D ⊸ C ) ⊢ C⊗!( D ⊸ C ) , то есть, что доллар и возможность купить на него шоколадку приводят к шоколадке, а возможность купить шоколадку сохраняется .

В отличие от классической и интуиционистской логик , линейная логика имеет два вида конъюнкций, что позволяет выражать ограниченность ресурсов. Добавим к предыдущему примеру возможность покупки леденца L. Выразить возможность покупки шоколадки или леденца можно выразить с помощью аддитивной конъюнкции :

D ⊸ L & C

Разумеется, выбрать можно только что-то одно. Мультипликативная конъюнкция обозначает присутствие обоих ресурсов. Так, на два доллара можно купить и шоколадку, и леденец:

D ⊗ D ⊸ L ⊗ C

Мультипликативная дизъюнкция A ⅋ B может пониматься как «если не А, так B», а выражаемая через неё линейная импликация A ⊸ B в таком случае имеет смысл «может ли B быть выведена из A ровно один раз?»

Аддитивная дизъюнкция A ⊕ B обозначает возможность как A, так и B, но выбор не за вами . Например, беспроигрышную лотерую, где можно выиграть леденец или шоколадку, можно выразить с помощью аддитивной дизъюнкции:

D ⊸ L ⊕ C

Фрагменты

Помимо полной линейной логики находят применение её фрагменты :

LL: разрешены все связки
MLL: только мультипликативы (⊗, ⅋)
MALL: только мультипликативы и аддитивы (⊗, ⅋, ⊕, &)
MELL: только мультипликативы и экспоненциалы (⊗, ⅋, !, ?)

Разумеется, этим списком не исчерпываются все возможные фрагменты. Например, возможны различные Хорн-фрагменты, которые используют линейную импликацию (по аналогии с хорновскими дизъюнктами ) в сочетаниях с различными связками.

Фрагменты логики интересуют исследователей с точки зрения сложности их вычислительной интерпретации. В частности, М. И. Канович доказал, что полный MLL-фрагмент является NP-полным , а ⊕-хорновский фрагмент линейной логики с (англ.) (( англ. weakening rule) PSPACE-полон . Это можно проинтерпретировать как то, что управление использованием ресурсов — трудная задача даже в простейших случаях.

Представление в виде исчисления секвенций

Один из способов определения линейной логики — это исчисление секвенций . Буквы Γ и ∆ обозначают списки предложений $A_{1},...,A_{n}$ $A_{1},...,A_{n}$ , и называются контекстами . В секвенции контекст помещается слева и справа от ⊢ («следует»), например: $\Gamma \vdash \Delta$ $\Gamma \vdash \Delta$ . Ниже приведено исчисление секвенций для MLL в двустороннем формате .

Структурное правило — перестановка. Задано соответственно левое и правое правила вывода:

${\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}}$ ${\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}}$

Тождество и сечение :

${\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}}$ ${\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}}$

Мультипликативная конъюнкция:

${\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}}$ ${\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}}$

Мультипликативная дизъюнкция:

${\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}}$ ${\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}}$

Отрицание:

${\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}}$ ${\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}}$

Аналогичные правила можно определить для полной линейной логики, её аддитивов и экспоненциалов. Обратите внимание, что в линейную логику не добавлены структурные правила ослабления и сокращения, так как в общем случае утверждения (и их копии) не могут произвольно появляться и исчезать в секвенциях, как это принято в классической логике.

Примечания

(1987). (PDF) . Theoretical Computer Science . 50 (1): 1—102. doi : . : . (PDF) из оригинала 6 мая 2021 . Дата обращения: 24 марта 2021 .
↑ (неопр.) . Дата обращения: 18 июля 2021. 18 июля 2021 года.
Baez, John ; Stay, Mike (2008). (ed.). (PDF) . New Structures of Physics . из оригинала 22 марта 2021 . Дата обращения: 24 марта 2021 .
/ V. de Paiva, J. van Genabith, E. Ritter. — 1999. (неопр.) . Дата обращения: 24 марта 2021. Архивировано 22 ноября 2020 года.
↑ .
↑ .
↑ .
↑ Max 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 (май).
Emmanuel Beffara. (неопр.) (2013).