Линейная логика () — субструктурная логика, предложенная как уточнение классической и интуиционистской логики, объединяющая двойственность первой со многими конструктивными свойствами последней, введена и используется для логических рассуждений, учитывающих расход некоторого ресурса. Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для верификации сетевых протоколов, языки программирования, теория игр (игровая семантика) и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации), лингвистика .
Описание
Синтаксис Язык классической линейной логики () может быть описан в форме Бэкуса — Наура:
Где
и — атомарные формулы,
логические связки и константы: Символ Значение ⊗ мультипликативная конъюнкция («тензор», ) ⊕ аддитивная дизъюнкция & аддитивная конъюнкция ⅋ мультипликативная дизъюнкция («пар», ) ! модальность «конечно» () ? модальность «почему нет» () 1 единица для ⊗ 0 нуль для ⊕ ⊤ нуль для & ⊥ единица для ⅋
Бинарные связки ⊗, ⊕, & и ⅋ ассоциативны и коммутативны.
Каждое утверждение в классической линейной логике имеет двойственное , определяемое следующим образом:
Содержательное толкование В линейной логике (в отличие от классической) посылки часто рассматриваются как расходуемые ресурсы, поэтому выведенная или начальная формула может быть ограничена по числу использований.
Мультипликативная конъюнкция ⊗ аналогична операции сложения мультимножеств и может выражать объединение ресурсов.
является инволюцией, то есть, для всех утверждений. также называется линейным отрицанием .
Линейная импликация играет большую роль в линейной логике, хотя она и не включена в грамматику связок. Может быть выражена через линейное отрицание и мультипликативную дизъюнкцию
.
Связку ⊸ иногда называют «леденец на палочке» () из-за характерной формы.
Линейную импликацию можно использовать в выводе при наличии ресурсов в ее левой части, а в результате получаются ресурсы из правой линейной импликации. Данное преобразование задает линейную функцию, что и дало начало термину «Линейная логика».
Модальность «конечно» (!) позволяет обозначить ресурс как неисчерпаемый.
Пример. Пусть D обозначает доллар, а C — плитку шоколада. Тогда покупку плитки шоколада можно обозначить как . Покупку можно выразить следующим выводом: , то есть, что доллар и возможность купить на него шоколадку приводят к шоколадке, а возможность купить шоколадку сохраняется.
В отличие от классической и интуиционистской логик, линейная логика имеет два вида конъюнкций, что позволяет выражать ограниченность ресурсов. Добавим к предыдущему примеру возможность покупки леденца L. Выразить возможность покупки шоколадки или леденца можно выразить с помощью аддитивной конъюнкции:
Разумеется, выбрать можно только что-то одно. Мультипликативная конъюнкция обозначает присутствие обоих ресурсов. Так, на два доллара можно купить и шоколадку, и леденец:
Мультипликативная дизъюнкция A ⅋ B может пониматься как «если не А, так B», а выражаемая через неё линейная импликация A ⊸ B в таком случае имеет смысл «может ли B быть выведена из A ровно один раз?»
Аддитивная дизъюнкция A ⊕ B обозначает возможность как A, так и B, но выбор не за вами. Например, беспроигрышную лотерую, где можно выиграть леденец или шоколадку, можно выразить с помощью аддитивной дизъюнкции:
Фрагменты Помимо полной линейной логики находят применение её фрагменты:
LL: разрешены все связки MLL: только мультипликативы (⊗, ⅋) MALL: только мультипликативы и аддитивы (⊗, ⅋, ⊕, &) MELL: только мультипликативы и экспоненциалы (⊗, ⅋, !, ?)
Разумеется, этим списком не исчерпываются все возможные фрагменты. Например, возможны различные Хорн-фрагменты, которые используют линейную импликацию (по аналогии с хорновскими дизъюнктами) в сочетаниях с различными связками.Max I. Kanovich. The complexity of Horn fragments of Linear Logic. Annals of Pure and Applied Logic 69 (1994) 195—241
Фрагменты логики интересуют исследователей с точки зрения сложности их вычислительной интерпретации. В частности, М. И. Канович доказал, что полный MLL-фрагмент является NP-полным, а ⊕-хорновский фрагмент линейной логики с () PSPACE-полон. Это можно проинтерпретировать как то, что управление использованием ресурсов — трудная задача даже в простейших случаях.
Представление в виде исчисления секвенций Один из способов определения линейной логики — это исчисление секвенций. Буквы Γ и ∆ обозначают списки предложений , и называются контекстами. В секвенции контекст помещается слева и справа от ⊢ («следует»), например: . Ниже приведено исчисление секвенций для MLL в двустороннем формате.
Структурное правило — перестановка. Задано соответственно левое и правое правила вывода:
Тождество и сечение:
Мультипликативная конъюнкция:
Мультипликативная дизъюнкция:
Отрицание:
Аналогичные правила можно определить для полной линейной логики, её аддитивов и экспоненциалов. Обратите внимание, что в линейную логику не добавлены структурные правила ослабления и сокращения, так как в общем случае утверждения (и их копии) не могут произвольно появляться и исчезать в секвенциях, как это принято в классической логике.
Примечания
Литература
Ссылки Linear Logic, Stanford Encyclopedia of Philosophy
Категория:Логика Категория:Математическая логика