Линейная логика

Линейная логика (англ. linear logic) — подструктурная логика, предложенная Жан-Ивом Жираром^[англ.] как уточнение классической и интуиционистской логики, объединяющая двойственность первой со многими конструктивными свойствами последней^[1], введена и используется для логических рассуждений, учитывающих расход некоторого ресурса^[2]. Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для верификации сетевых протоколов, языки программирования, теория игр (игровая семантика)^[2] и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации)^[3], лингвистика^[4].

Описание

Синтаксис

Язык классической линейной логики (англ. 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) из-за характерной формы.

Линейную импликацию можно использовать в выводе при наличии ресурсов в ее левой части, а в результате получаются ресурсы из правой линейной импликации. Данное преобразование задает линейную функцию, что и дало начало термину «Линейная логика»^[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]

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

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

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

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

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

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

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

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

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

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

Отрицание:

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

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

Примечания

1. Girard, Jean-Yves (1987). "Linear logic" (PDF). Theoretical Computer Science. 50 (1): 1—102. doi:10.1016/0304-3975(87)90045-4. hdl:10338.dmlcz/120513. Архивировано (PDF) 6 мая 2021. Дата обращения: 24 марта 2021.
2. Алгоритмические вопросы алгебры и логики /КАРТОЧКА ПРОЕКТА, ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ. Дата обращения:18.07.2021  (неопр.). Дата обращения: 18 июля 2021. Архивировано 18 июля 2021 года.
3. Baez, John; Stay, Mike (2008). Bob Coecke (ed.). "Physics, Topology, Logic and Computation: A Rosetta Stone" (PDF). New Structures of Physics. Архивировано 22 марта 2021. Дата обращения: 24 марта 2021.
4. de Paiva, V. Dagstuhl Seminar 99341 on Linear Logic and Applications / V. de Paiva, J. van Genabith, E. Ritter. — 1999. Архивная копия от 22 ноября 2020 на Wayback Machine Источник  (неопр.). Дата обращения: 24 марта 2021. Архивировано 22 ноября 2020 года.
5. Ломазова, 2004.
6. Lincoln, 1992.
7. Beffara, 2013.
8. 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. Introduction to linear logic  (неопр.) (2013).

Ссылки

• Linear Logic, Stanford Encyclopedia of Philosophy