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

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

Описание

Синтаксис

Язык классической линейной логики (Шаблон:Lang-en) может быть описан в форме Бэкуса — Наура:

Шаблон:Math ::= Шаблон:Math | Шаблон:Math | Шаблон:Math | Шаблон:Math | Шаблон:Math

Где

• Шаблон:Math и Шаблон:Math — атомарные формулы,

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

Символ	Значение
⊗	мультипликативная конъюнкция («тензор», Шаблон:Lang-en)
⊕	аддитивная дизъюнкция
&	аддитивная конъюнкция
⅋	мультипликативная дизъюнкция («пар», Шаблон:Lang-en)
!	модальность «конечно» (Шаблон:Lang-en)
?	модальность «почему нет» (Шаблон:Lang-en)
1	единица для ⊗
0	нуль для ⊕
⊤	нуль для &
⊥	единица для ⅋

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

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

Шаблон:Math			Шаблон:Math
Шаблон:Math			Шаблон:Math
Шаблон:Math			Шаблон:Math
Шаблон:Math			Шаблон:Math
Шаблон:Math			Шаблон:Math
Шаблон:Math			Шаблон:Math

Содержательное толкование

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

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

Следует отметить, что Шаблон:Math является инволюцией, то есть, Шаблон:Math для всех утверждений. Шаблон:Math также называется линейным отрицанием Шаблон:Math.

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

Шаблон:Math.

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

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

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

Пример. Пусть D обозначает доллар, а C — плитку шоколада. Тогда покупку плитки шоколада можно обозначить как Шаблон:Math. Покупку можно выразить следующим выводом: Шаблон:Math, то есть, что доллар и возможность купить на него шоколадку приводят к шоколадке, а возможность купить шоколадку сохраняетсяШаблон:Sfn.

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

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

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

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

Фрагменты

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

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

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

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

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

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

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

$\frac{\mathrm{\Gamma },A,B,{\mathrm{\Gamma }}^{\prime }⊢\mathrm{\Delta }}{\mathrm{\Gamma },B,A,{\mathrm{\Gamma }}^{\prime }⊢\mathrm{\Delta }}\text{exL}\frac{\mathrm{\Gamma }⊢\mathrm{\Delta },A,B,{\mathrm{\Delta }}^{\prime }}{\mathrm{\Gamma }⊢\mathrm{\Delta },B,A,{\mathrm{\Delta }}^{\prime }}\text{exR}$

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

$\frac{\cdot }{A⊢A}\text{I}\frac{\mathrm{\Gamma }⊢\mathrm{\Sigma },A,\mathrm{\Delta }{\mathrm{\Gamma }}^{\prime },A,{\mathrm{\Sigma }}^{\prime }⊢{\mathrm{\Delta }}^{\prime }}{\mathrm{\Gamma },{\mathrm{\Gamma }}^{\prime },{\mathrm{\Sigma }}^{\prime }⊢\mathrm{\Sigma },\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }}\text{Cut}$

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

$\frac{\mathrm{\Gamma },A,B⊢\mathrm{\Delta }}{\mathrm{\Gamma },A\otimes B⊢\mathrm{\Delta }}\otimes \text{L}\frac{\mathrm{\Gamma }⊢A,\mathrm{\Delta }{\mathrm{\Gamma }}^{\prime }⊢B,{\mathrm{\Delta }}^{\prime }}{\mathrm{\Gamma },{\mathrm{\Gamma }}^{\prime }⊢A\otimes B,\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }}\otimes \text{R}$

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

$\frac{\mathrm{\Gamma },A⊢\mathrm{\Delta }{\mathrm{\Gamma }}^{\prime },B⊢{\mathrm{\Delta }}^{\prime }}{\mathrm{\Gamma },{\mathrm{\Gamma }}^{\prime },A\text{⅋}B⊢\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }}\text{⅋L}\frac{\mathrm{\Gamma }⊢A,B,\mathrm{\Delta }}{\mathrm{\Gamma }⊢A\text{⅋}B,\mathrm{\Delta }}\text{⅋R}$

Отрицание:

$\frac{\mathrm{\Gamma }⊢A,\mathrm{\Delta }}{\mathrm{\Gamma },A^{\mathrm{\perp }}⊢\mathrm{\Delta }}\mathrm{\perp }\text{L}\frac{\mathrm{\Gamma },A⊢\mathrm{\Delta }}{\mathrm{\Gamma }⊢A^{\mathrm{\perp }},\mathrm{\Delta }}\mathrm{\perp }\text{R}$

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

Литература

• Шаблон:Книга
• Шаблон:Публикация
• Шаблон:Cite web

Ссылки

• Linear Logic, Stanford Encyclopedia of Philosophy