Линейная логика
Линейная логика (англ. Linear Logic — это подструктурная логика[англ.], предложенная Жан-Ивом Жираром (англ. Jean-Yves Girard) как уточнение классической и интуиционистской логики, объединяющая двойственность первой со многими конструктивными свойствами последней[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]
Представление в виде исчисления секвенций
Один из способов определения линейной логики — это исчисление секвенций. Буквы Γ и ∆ обозначают списки предложений [math]\displaystyle{ A_1, ..., A_n }[/math], и называются контекстами. В секвенции контекст помещается слева и справа от ⊢ («следует»), например: [math]\displaystyle{ \Gamma \vdash \Delta }[/math]. Ниже приведено исчисление секвенций для MLL в двустороннем формате[7].
Структурное правило — перестановка. Задано соответственно левое и правое правила вывода:
[math]\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} }[/math]
Тождество и сечение:
[math]\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} }[/math]
Мультипликативная конъюнкция:
[math]\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} }[/math]
Мультипликативная дизъюнкция:
[math]\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} }[/math]
Отрицание:
[math]\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} }[/math]
Аналогичные правила можно определить для полной линейной логики, её аддитивов и экспоненциалов. Обратите внимание, что в линейную логику не добавлены структурные правила ослабления и сокращения, так как в общем случае утверждения (и их копии) не могут произвольно появляться и исчезать в секвенциях, как это принято в классической логике.
Примечания
- ↑ (1987) «Linear logic». Theoretical Computer Science 50 (1): 1–102. doi:10.1016/0304-3975(87)90045-4.
- ↑ 2,0 2,1 Алгоритмические вопросы алгебры и логики /КАРТОЧКА ПРОЕКТА, ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ. Дата обращения:18.07.2021. Дата обращения: 18 июля 2021. Архивировано 18 июля 2021 года.
- ↑ (2008) «Physics, Topology, Logic and Computation: A Rosetta Stone». New Structures of Physics.
- ↑ de Paiva, V. Dagstuhl Seminar 99341 on Linear Logic and Applications / V. de Paiva, J. van Genabith, E. Ritter. — 1999. Архивная копия от 22 ноября 2020 на Wayback Machine
- ↑ 5,0 5,1 Ломазова, 2004.
- ↑ 6,0 6,1 6,2 Lincoln, 1992.
- ↑ 7,0 7,1 Beffara, 2013.
- ↑ 8,0 8,1 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
