Линейная логика: различия между версиями
[непроверенная версия] | [отпатрулированная версия] |
РоманСузи (обсуждение | вклад) syntax |
Спасено источников — 1, отмечено мёртвыми — 0. Сообщить об ошибке. См. FAQ.) #IABot (v2.0.9.5 |
||
(не показаны 42 промежуточные версии 8 участников) | |||
Строка 1: | Строка 1: | ||
'''Линейная логика''' ({{lang-en| |
'''Линейная логика''' ({{lang-en|linear logic}}) — [[подструктурная логика]], предложенная {{нп5|Жирар, Жан-Ив|Жан-Ивом Жираром|en|Jean-Yves Girard}} как уточнение [[Классическая логика|классической]] и [[Интуиционистское исчисление высказываний|интуиционистской логики]], объединяющая [[закон двойственности|двойственность]] первой со многими конструктивными свойствами последней<ref>{{cite journal|last1=Girard|first1=Jean-Yves|year=1987|title=Linear logic|url=http://girard.perso.math.cnrs.fr/linear.pdf|journal=Theoretical Computer Science|volume=50|issue=1|pages=1–102|doi=10.1016/0304-3975(87)90045-4|hdl=10338.dmlcz/120513|author1-link=Jean-Yves Girard|access-date=2021-03-24|archive-date=2021-05-06|archive-url=https://web.archive.org/web/20210506154411/http://girard.perso.math.cnrs.fr/linear.pdf|date=}}</ref>, введена и используется для логических рассуждений, учитывающих расход некоторого ресурса<ref name=rscf-project16-11-10252>{{Cite web |url=https://rscf.ru/project/16-11-10252/ |title=Алгоритмические вопросы алгебры и логики /КАРТОЧКА ПРОЕКТА, ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ. Дата обращения:18.07.2021 |access-date=2021-07-18 |archive-date=2021-07-18 |archive-url=https://web.archive.org/web/20210718072845/https://rscf.ru/project/16-11-10252/ |deadlink=no }}</ref>. Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для [[верификация|верификации]] [[сетевые протоколы|сетевых протоколов]], [[Язык программирования|языки программирования]], [[теория игр]] ([[игровая семантика]])<ref name=rscf-project16-11-10252/> и [[квантовая физика]] (поскольку линейную логику можно рассматривать как логику [[Квантовая теория информации|квантовой теории информации]])<ref>{{cite journal|first1=John|last1=Baez|author1-link=John Baez|first2=Mike|last2=Stay|year=2008|title=Physics, Topology, Logic and Computation: A Rosetta Stone|editor=Bob Coecke|editor-link=Bob Coecke|journal=New Structures of Physics|url=http://math.ucr.edu/home/baez/rosetta.pdf|access-date=2021-03-24|archive-date=2021-03-22|archive-url=https://web.archive.org/web/20210322044110/https://arxiv.org/abs/0903.0340|date=}}</ref>, [[лингвистика]]<ref>{{cite book|title=Dagstuhl Seminar 99341 on Linear Logic and Applications|first1=V.|last1=de Paiva|author1-link=Valeria de Paiva|first2=J.|last2=van Genabith|first3=E.|last3=Ritter|year=1999|url=http://www.dagstuhl.de/Reports/99/99341.pdf}} {{Wayback|url=http://www.dagstuhl.de/Reports/99/99341.pdf |date=20201122173450 }} {{Cite web |url=http://www.dagstuhl.de/Reports/99/99341.pdf |title=Источник |access-date=2021-03-24 |archive-date=2020-11-22 |archive-url=https://web.archive.org/web/20201122173450/http://www.dagstuhl.de/Reports/99/99341.pdf |deadlink=unfit }}</ref>. |
||
== Описание == |
|||
== Логические связки == |
|||
=== Синтаксис === |
=== Синтаксис === |
||
Язык '''''классической |
Язык '''''классической линейной логики''''' ({{lang-en|classic linear logic, CLL}}) может быть описан в [[Форма Бэкуса — Наура|форме Бэкуса — Наура]]: |
||
: {{math|<VAR>A</VAR>}} ::= {{math|<VAR>p</VAR> ∣ <VAR>p</VAR><sup>⊥</sup>}} | {{math| <VAR>A</VAR> ⊗ <VAR>A</VAR> ∣ <VAR>A</VAR> ⊕ <VAR>A</VAR>}} | {{math| <VAR>A</VAR> & <VAR>A</VAR> ∣ <VAR>A</VAR> ⅋ <VAR>A</VAR>}} | {{math| 1 ∣ 0 ∣ ⊤ ∣ ⊥}} | {{math| !<VAR>A</VAR> ∣ ?<VAR>A</VAR>}} |
|||
{| style="margin:auto" |
|||
Где |
|||
* {{math|<VAR>p</VAR>}} и {{math|<VAR>p</VAR><sup>⊥</sup>}} — [[атомарная формула|атомарные формулы]], |
|||
* логические связки и константы: |
|||
{| class="wikitable" |
|||
|- |
|||
! Символ || Значение |
|||
|- |
|||
| style="text-align:center;" | ⊗ || мультипликативная конъюнкция («тензор», {{lang-en|"tensor"}}) |
|||
|- |
|||
| style="text-align:center;" | ⊕ || аддитивная дизъюнкция |
|||
|- |
|||
| style="text-align:center;" | & || аддитивная конъюнкция |
|||
|- |
|||
| style="text-align:center;" | ⅋ || мультипликативная дизъюнкция («пар», {{lang-en|"par"}}) |
|||
|- |
|||
| style="text-align:center;" | ! || модальность «конечно» ({{lang-en|"of course"}}) |
|||
|- |
|||
| style="text-align:center;" | ? || модальность «почему нет» ({{lang-en|"why not"}}) |
|||
|- |
|- |
||
| style="text-align:center;" | 1 || [[Единица (алгебра)|единица]] для ⊗ |
|||
| {{math|<VAR>A</VAR>}} |
|||
| ::= |
|||
| {{math|<VAR>p</VAR> ∣ <VAR>p</VAR><sup>⊥</sup>}} |
|||
|- |
|- |
||
| style="text-align:center;" | 0 || нуль для ⊕ |
|||
| |
|||
| {{math|∣}} |
|||
| {{math| <VAR>A</VAR> ⊗ <VAR>A</VAR> ∣ <VAR>A</VAR> ⊕ <VAR>A</VAR>}} |
|||
|- |
|- |
||
| style="text-align:center;" | ⊤ || нуль для & |
|||
| |
|||
| {{math|∣}} |
|||
| {{math| <VAR>A</VAR> & <VAR>A</VAR> ∣ <VAR>A</VAR> ⅋ <VAR>A</VAR>}} |
|||
|- |
|- |
||
| style="text-align:center;" | ⊥ || единица для ⅋ |
|||
| |
|||
| {{math|∣}} |
|||
| {{math| 1 ∣ 0 ∣ ⊤ ∣ ⊥}} |
|||
|- |
|- |
||
| |
|||
| {{math|∣}} |
|||
| {{math| !<VAR>A</VAR> ∣ ?<VAR>A</VAR>}} |
|||
|} |
|} |
||
Бинарные связки ⊗, ⊕, & и ⅋ [[Ассоциативность (математика)|ассоциативны]] и [[Коммутативность|коммутативны]]. |
|||
Here {{math|<VAR>p</VAR>}} and {{math|<VAR>p</VAR><sup>⊥</sup>}} range |
|||
over [[Atomic formula|logical atoms]]. For reasons to be explained |
|||
below, the [[Logical connective|connectives]] ⊗, ⅋, 1, and |
|||
⊥ are called ''multiplicatives'', the connectives &, |
|||
⊕, ⊤, and 0 are called ''additives'', and the |
|||
connectives ! and ? are called ''exponentials''. We can further |
|||
employ the following terminology: |
|||
* ⊗ is called "multiplicative conjunction" or "times" (or sometimes "tensor") |
|||
* ⊕ is called "additive disjunction" or "plus" |
|||
* & is called "additive conjunction" or "with" |
|||
* ⅋ is called "multiplicative disjunction" or "par" |
|||
* ! is pronounced "of course" (or sometimes "bang") |
|||
* ? is pronounced "why not" |
|||
Binary connectives ⊗, ⊕, & and ⅋ are associative and commutative; 1 is the unit for ⊗, 0 is the unit for ⊕, ⊥ is the unit for ⅋ and ⊤ is the unit for &. |
|||
Каждое утверждение {{math|<VAR>A</VAR>}} в классической линейной логике имеет '''''двойственное''''' {{math|<VAR>A</VAR><sup>⊥</sup>}}, определяемое следующим образом: |
|||
{| border="1" cellpadding="5" cellspacing="0" style="margin:auto" |
{| border="1" cellpadding="5" cellspacing="0" style="margin:auto" |
||
|- |
|- |
||
Строка 69: | Строка 64: | ||
|} |
|} |
||
=== Содержательное толкование === |
|||
{| class="wikitable" style="float:right" |
|||
В линейной логике (в отличие от классической) посылки часто рассматриваются как расходуемые '''''ресурсы''''', поэтому выведенная или начальная формула может быть ограничена по числу использований. |
|||
|+ Classification of connectives |
|||
|- |
|||
! !! add !! mul !! exp |
|||
|- |
|||
! pos |
|||
| ⊕ 0 || ⊗ 1 || ! |
|||
|- |
|||
! neg |
|||
| & ⊤ || ⅋ ⊥ || ? |
|||
|} |
|||
Observe that {{math|(-)<sup>⊥</sup>}} is an [[Involution (mathematics)|involution]], i.e., {{math|<VAR>A</VAR><sup>⊥⊥</sup> {{=}} <VAR>A</VAR>}} for all propositions. {{math|<VAR>A</VAR><sup>⊥</sup>}} is also called the ''linear negation'' of {{math|<VAR>A</VAR>}}. |
|||
'''''Мультипликативная конъюнкция''''' ⊗ аналогична операции сложения [[Мультимножество|мультимножеств]] и может выражать объединение ресурсов. |
|||
The columns of the table suggest another way of classifying the connectives of linear logic, termed '''polarity''': the connectives negated in the left column (⊗, ⊕, 1, 0, !) are called ''positive'', while their duals on the right (⅋, &, ⊥, ⊤, ?) are called ''negative''; cf. table on the right. |
|||
Следует отметить, что {{math|(.)<sup>⊥</sup>}} является [[Инволюция (математика)|инволюцией]], то есть, {{math|<VAR>A</VAR><sup>⊥⊥</sup> {{=}} <VAR>A</VAR>}} для всех утверждений. {{math|<VAR>A</VAR><sup>⊥</sup>}} также называется '''''линейным отрицанием''''' {{math|<VAR>A</VAR>}}. |
|||
''Linear implication'' is not included in the grammar of connectives, but is definable in CLL using linear negation and multiplicative disjunction, by {{math|<VAR>A</VAR> ⊸ <VAR>B</VAR> :{{=}} <VAR>A</VAR><sup>⊥</sup> ⅋ <VAR>B</VAR>}}. The connective ⊸ is sometimes pronounced "[[lollipop]]", owing to its shape. |
|||
'''''Линейная импликация''''' играет большую роль в линейной логике, хотя она и не включена в грамматику связок. Может быть выражена через линейное отрицание и мультипликативную дизъюнкцию |
|||
: {{math|<VAR>A</VAR> ⊸ <VAR>B</VAR> :{{=}} <VAR>A</VAR><sup>⊥</sup> ⅋ <VAR>B</VAR>}}. |
|||
Связку ⊸ иногда называют «леденец на палочке» ({{lang-en|lollipop}}) из-за характерной формы. |
|||
Линейную импликацию можно использовать в выводе при наличии ресурсов в ее левой части, а в результате получаются ресурсы из правой линейной импликации. Данное преобразование задает [[Линейная функция|линейную функцию]], что и дало начало термину «Линейная логика»{{sfn|Ломазова|2004}}. |
|||
'''''Модальность «конечно»''''' (!) позволяет обозначить ресурс как неисчерпаемый. |
|||
Пример. Пусть D обозначает доллар, а C — плитку шоколада. Тогда покупку плитки шоколада можно обозначить как {{math|<VAR>D</VAR> ⊸ <VAR>C</VAR>}}. Покупку можно выразить следующим выводом: {{math|<VAR>D</VAR>⊗ !(<VAR>D</VAR> ⊸ <VAR>C</VAR>) ⊢ C⊗!(<VAR>D</VAR> ⊸ <VAR>C</VAR>)}}, то есть, что доллар и возможность купить на него шоколадку приводят к шоколадке, а возможность купить шоколадку сохраняется{{sfn|Ломазова|2004}}. |
|||
В отличие от классической и [[Интуиционистская логика|интуиционистской логик]], линейная логика имеет два вида конъюнкций, что позволяет выражать ограниченность ресурсов. Добавим к предыдущему примеру возможность покупки леденца L. Выразить возможность покупки шоколадки или леденца можно выразить с помощью '''''аддитивной конъюнкции'''''{{sfn|Lincoln|1992}}: |
|||
{{math|<VAR>D</VAR> ⊸ <VAR>L</VAR> & <VAR>C</VAR>}} |
|||
Разумеется, выбрать можно только что-то одно. Мультипликативная конъюнкция обозначает присутствие обоих ресурсов. Так, на два доллара можно купить и шоколадку, и леденец: |
|||
{{math|<VAR>D</VAR> ⊗ <VAR>D</VAR> ⊸ <VAR>L</VAR> ⊗ <VAR>C</VAR>}} |
|||
Мультипликативная дизъюнкция <VAR>A</VAR> ⅋ <VAR>B</VAR> может пониматься как «если не А, так B», а выражаемая через неё линейная импликация <VAR>A</VAR> ⊸ <VAR>B</VAR> в таком случае имеет смысл «может ли B быть выведена из A ровно один раз?»{{sfn|Lincoln|1992}} |
|||
'''''Аддитивная дизъюнкция''''' <VAR>A</VAR> ⊕ <VAR>B</VAR> обозначает возможность как A, так и B, но выбор не за вами{{sfn|Lincoln|1992}}. Например, беспроигрышную лотерую, где можно выиграть леденец или шоколадку, можно выразить с помощью аддитивной дизъюнкции: |
|||
{{math|<VAR>D</VAR> ⊸ <VAR>L</VAR> ⊕ <VAR>C</VAR>}} |
|||
== Фрагменты == |
|||
Помимо полной линейной логики находят применение её фрагменты{{sfn|Beffara|2013}}: |
|||
* LL: разрешены все связки |
|||
* MLL: только мультипликативы (⊗, ⅋) |
|||
* MALL: только мультипликативы и аддитивы (⊗, ⅋, ⊕, &) |
|||
* MELL: только мультипликативы и экспоненциалы (⊗, ⅋, !, ?) |
|||
Разумеется, этим списком не исчерпываются все возможные фрагменты. Например, возможны различные Хорн-фрагменты, которые используют линейную импликацию (по аналогии с [[Хорновский дизъюнкт|хорновскими дизъюнктами]]) в сочетаниях с различными связками.<ref name="автоссылка898">Max I. Kanovich. The complexity of Horn fragments of Linear Logic. Annals of Pure and Applied Logic 69 (1994) 195—241</ref> |
|||
Фрагменты логики интересуют исследователей с точки зрения [[Вычислительная сложность|сложности]] их вычислительной интерпретации. В частности, М. И. Канович доказал, что полный MLL-фрагмент является [[NP-полная задача|NP-полным]], а ⊕-хорновский фрагмент линейной логики с {{нп3|правило ослабления|правилом ослабления|en|Weakening (logic)}} ({{lang-en|weakening rule}}) [[PSPACE|PSPACE-полон]]. Это можно проинтерпретировать как то, что управление использованием ресурсов — трудная задача даже в простейших случаях.<ref name="автоссылка898" /> |
|||
== Представление в виде исчисления секвенций == |
|||
Один из способов определения линейной логики — это [[исчисление секвенций]]. Буквы Γ и ∆ обозначают списки предложений <math>A_1, ..., A_n</math>, и называются '''''контекстами'''''. В секвенции контекст помещается слева и справа от ⊢ («следует»), например: <math>\Gamma \vdash \Delta</math>. Ниже приведено исчисление секвенций для MLL в двустороннем формате{{sfn|Beffara|2013}}. |
|||
Структурное правило — перестановка. Задано соответственно левое и правое правила вывода: |
|||
<math>\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>\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>\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>\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>\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> |
|||
Аналогичные правила можно определить для полной линейной логики, её аддитивов и экспоненциалов. Обратите внимание, что в линейную логику '''не добавлены''' структурные правила ослабления и сокращения, так как в общем случае утверждения (и их копии) не могут произвольно появляться и исчезать в секвенциях, как это принято в классической логике. |
|||
== Примечания == |
== Примечания == |
||
Строка 92: | Строка 138: | ||
== Литература == |
== Литература == |
||
* {{книга|автор=Ломазова И. А.|часть=6.5. Вложенные сети Петри и Линейная логика|заглавие=Вложенные сети Петри: моделирование анализ распределенных систем с объектной структурой|место=М.|издательство=Научный мир|год=2004|страниц=208|страницы=175—185|isbn=5-89176-247-1|ref=Ломазова}} |
|||
* {{публикация|статья|автор=Patrick Lincoln|заглавие=Linear logic|издание=ACM SIGACT News|год=1992|месяц=5|номер=2|том=23|ref=Lincoln}} |
|||
* {{cite web|author=Emmanuel Beffara|title=Introduction to linear logic|url=https://hal.archives-ouvertes.fr/cel-01144229|date=2013|ref=Beffara}} |
|||
== Ссылки == |
== Ссылки == |
||
* [https://plato.stanford.edu/entries/logic-linear/ Linear Logic], Stanford Encyclopedia of Philosophy |
|||
{{Внешние ссылки}}{{Логика}} |
|||
[[Категория:Логика]] |
|||
[[Категория:Математическая логика]] |
Текущая версия от 08:14, 6 июня 2024
Линейная логика (англ. 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]
Представление в виде исчисления секвенций
[править | править код]Один из способов определения линейной логики — это исчисление секвенций. Буквы Γ и ∆ обозначают списки предложений , и называются контекстами. В секвенции контекст помещается слева и справа от ⊢ («следует»), например: . Ниже приведено исчисление секвенций для MLL в двустороннем формате[7].
Структурное правило — перестановка. Задано соответственно левое и правое правила вывода:
Тождество и сечение:
Мультипликативная конъюнкция:
Мультипликативная дизъюнкция:
Отрицание:
Аналогичные правила можно определить для полной линейной логики, её аддитивов и экспоненциалов. Обратите внимание, что в линейную логику не добавлены структурные правила ослабления и сокращения, так как в общем случае утверждения (и их копии) не могут произвольно появляться и исчезать в секвенциях, как это принято в классической логике.
Примечания
[править | править код]- ↑ 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.
- ↑ 1 2 Алгоритмические вопросы алгебры и логики /КАРТОЧКА ПРОЕКТА, ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ. Дата обращения:18.07.2021 . Дата обращения: 18 июля 2021. Архивировано 18 июля 2021 года.
- ↑ 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.
- ↑ 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 года.
- ↑ 1 2 Ломазова, 2004.
- ↑ 1 2 3 Lincoln, 1992.
- ↑ 1 2 Beffara, 2013.
- ↑ 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).
Ссылки
[править | править код]- Linear Logic, Stanford Encyclopedia of Philosophy