Для установки нажмите кнопочку Установить расширение. И это всё.

Исходный код расширения WIKI 2 регулярно проверяется специалистами Mozilla Foundation, Google и Apple. Вы также можете это сделать в любой момент.

4,5
Келли Слэйтон
Мои поздравления с отличным проектом... что за великолепная идея!
Александр Григорьевский
Я использую WIKI 2 каждый день
и почти забыл как выглядит оригинальная Википедия.
Статистика
На русском, статей
Улучшено за 24 ч.
Добавлено за 24 ч.
Альтернативы
Недавние
Show all languages
Что мы делаем. Каждая страница проходит через несколько сотен совершенствующих техник. Совершенно та же Википедия. Только лучше.
.
Лео
Ньютон
Яркие
Мягкие

Из Википедии — свободной энциклопедии

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

Линейную логику отличает от классической логики то, что посылки логического вывода могут рассматриваться в ней как расходуемые ресурсы.

Описание

Синтаксис

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

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

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

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

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

DL & C

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

DDLC

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

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

DLC

Фрагменты

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

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

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

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

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

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

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

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

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

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

Отрицание:

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

Примечания

  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. Baez, John; Stay, Mike (2008). Bob Coecke, ed. “Physics, Topology, Logic and Computation: A Rosetta Stone” (PDF). New Structures of Physics.
  3. de Paiva, V. Dagstuhl Seminar 99341 on Linear Logic and Applications / V. de Paiva, J. van Genabith, E. Ritter. — 1999.
  4. 1 2 Ломазова, 2004.
  5. 1 2 3 Lincoln, 1992.
  6. 1 2 Beffara, 2013.
  7. 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).

Ссылки

Эта страница в последний раз была отредактирована 17 апреля 2021 в 04:12.
Основа этой страницы находится в Википедии. Текст доступен по лицензии CC BY-SA 3.0 Unported License. Нетекстовые медиаданные доступны под собственными лицензиями. Wikipedia® — зарегистрированный товарный знак организации Wikimedia Foundation, Inc. WIKI 2 является независимой компанией и не аффилирована с Фондом Викимедиа (Wikimedia Foundation).