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

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску

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

Описание[править | править код]

Синтаксис[править | править код]

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

A ::= pp | AAAA | A & AAA | 1 ∣ 0 ∣ ⊤ ∣ ⊥ |  !A ∣ ?A

Где

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

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

Каждое утверждение A в классической линейной логике имеет двойственное A, определяемое следующим образом:

(p) = p (p) = p
(AB) = AB (AB) = AB
(AB) = A & B (A & B) = AB
(1) = ⊥ (⊥) = 1
(0) = ⊤ (⊤) = 0
(!A) = ?(A) (?A) = !(A)

Содержательное толкование[править | править код]

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

Мультипликативная конъюнкция ⊗ аналогична операции сложения мультимножеств и может выражать объединение ресурсов.

Следует отметить, что (.) является инволюцией, то есть, A⊥⊥ = A для всех утверждений. A также называется линейным отрицанием A.

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

AB := AB.

Связку ⊸ иногда называют «леденец на палочке» (англ. lollipop) из-за характерной формы.

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

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

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

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

DL & C

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

DDLC

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

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

DLC

Фрагменты[править | править код]

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

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

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

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

Представление в виде исчисления секвенций[править | править код]

Один из способов определения линейной логики — это исчисление секвенций. Буквы Γ и ∆ обозначают списки предложений , и называются контекстами. В секвенции контекст помещается слева и справа от ⊢ («следует»), например: . Ниже приведено исчисление секвенций для MLL в двустороннем формате[7].

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

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

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

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

Отрицание:

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

Примечания[править | править код]

  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.
  2. 1 2 Алгоритмические вопросы алгебры и логики /КАРТОЧКА ПРОЕКТА, ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ. Дата обращения:18.07.2021
  3. Baez, John; Stay, Mike (2008). Bob Coecke, ed. “Physics, Topology, Logic and Computation: A Rosetta Stone” (PDF). New Structures of Physics.
  4. de Paiva, V. Dagstuhl Seminar 99341 on Linear Logic and Applications / V. de Paiva, J. van Genabith, E. Ritter. — 1999.
  5. 1 2 Ломазова, 2004.
  6. 1 2 3 Lincoln, 1992.
  7. 1 2 Beffara, 2013.
  8. 1 2 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).

Ссылки[править | править код]