Линейная логика - Linear logic

«⅋» перенаправляется сюда. Об EP см. ⅋ (EP).

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

Линейная логика поддается множеству различных представлений, объяснений и интуиций.Теоретически доказательство, он основан на анализе классических последовательное исчисление в каком использовании ( структурные правила ) сокращение и ослабление тщательно контролируются. С практической точки зрения это означает, что логическая дедукция - это уже не просто постоянно расширяющаяся коллекция устойчивых «истин», но также способ манипулирования Ресурсы которые не всегда можно скопировать или выбросить по желанию. С точки зрения простого денотационные модели, линейную логику можно рассматривать как уточнение интерпретации интуиционистской логики путем замены декартовы (закрытые) категории к симметричные моноидальные (замкнутые) категории, или интерпретация классической логики путем замены Булевы алгебры к C * -алгебры.^{[нужна цитата ]}

Связи, двойственность и полярность

Синтаксис

Язык классическая линейная логика (CLL) индуктивно определяется Обозначение BNF

А	::=	п ∣ п^⊥
	∣	А ⊗ А ∣ А ⊕ А
	∣	А & А ∣ А ⅋ А
	∣	1 ∣ 0 ∣ ⊤ ∣ ⊥
	∣	!А ∣ ?А

Здесь п и п^⊥ диапазон логические атомы. По причинам, которые будут объяснены ниже, связки ⊗, ⅋, 1 и называются мультипликативысвязки &, ⊕, ⊤ и 0 называются добавки, и связные! и ? называются экспоненты. Мы можем использовать следующую терминологию:

• ⊗ называется "мультипликативным соединением" или "умножением" (или иногда "тензором")
• ⊕ называется «аддитивная дизъюнкция» или «плюс»
• & называется "аддитивным соединением" или "с"
• ⅋ называется «мультипликативная дизъюнкция» или «номинал»
• ! произносится как "конечно" (или иногда "бах")
• ? произносится "почему бы и нет"

Бинарные связки ⊗, ⊕, & и ⅋ ассоциативны и коммутативны; 1 - единица для, 0 - единица для, ⊥ - единица для, ⊤ - единица для &.

Каждое предложение А в CLL имеет двойной А^⊥, определяется следующим образом:

(п)^⊥ = п^⊥			(п^⊥)^⊥ = п
(А ⊗ B)^⊥ = А^⊥ ⅋ B^⊥			(А ⅋ B)^⊥ = А^⊥ ⊗ B^⊥
(А ⊕ B)^⊥ = А^⊥ & B^⊥			(А & B)^⊥ = А^⊥ ⊕ B^⊥
(1)^⊥ = ⊥			(⊥)^⊥ = 1
(0)^⊥ = ⊤			(⊤)^⊥ = 0
(!А)^⊥ = ?(А^⊥)			(?А)^⊥ = !(А^⊥)

Классификация связок

	Добавить	мул	exp
позиция	⊕ 0	⊗ 1	!
негр	& ⊤	⅋ ⊥	?

Заметьте, что (-)^⊥ является инволюция, т.е. А^⊥⊥ = А по всем предложениям. А^⊥ также называется линейное отрицание из А.

Столбцы таблицы предлагают другой способ классификации связок линейной логики, называемый полярность: связки, инвертированные в левом столбце (⊗, ⊕, 1, 0,!), называются положительный, а их двойники справа (⅋, &, ⊥, ⊤,?) называются отрицательный; ср. таблица справа.

Линейное следствие не включен в грамматику связок, но может быть определен в CLL с использованием линейного отрицания и мультипликативной дизъюнкции посредством А ⊸ B := А^⊥ ⅋ B. Соединительное слово ⊸ иногда произносится как "леденец ", благодаря своей форме.

Последовательное представление исчисления

Один из способов определения линейной логики - это как последовательное исчисление. Используем буквы Γ и Δ перебрать список предложений А₁, ..., А_п, также называемый контексты. А последовательный помещает контекст слева и справа от турникет, написано Γ ${\displaystyle \vdash }$ Δ. Интуитивно секвенция утверждает, что соединение Γ влечет за собой дизъюнкция Δ (хотя мы имеем в виду «мультипликативное» соединение и дизъюнкцию, как объясняется ниже). Жирар описывает классическую линейную логику, используя только односторонний sequents (где левый контекст пуст), и здесь мы следуем более экономичному представлению. Это возможно потому, что любое помещение слева от турникета всегда можно переместить на другую сторону и сдвоить.

Теперь мы даем правила вывода описывая, как строить доказательства секвенций.^[4]

Во-первых, чтобы формализовать тот факт, что нас не волнует порядок предложений внутри контекста, мы добавляем структурное правилообмен:

${\displaystyle \vdash }$ Γ, A1, А2, Δ

${\displaystyle \vdash }$ Γ, A2, А1, Δ

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

Далее мы добавляем начальные последовательности и порезы:

${\displaystyle \vdash }$ А, А^⊥

${\displaystyle \vdash }$ Γ, А       ${\displaystyle \vdash }$ А^⊥, Δ ${\displaystyle \vdash }$ Γ, Δ

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

Теперь мы объясняем связки, давая логические правила. Обычно в последовательном исчислении один дает и «правые правила», и «левые правила» для каждой связки, по существу описывая два способа рассуждения о предложениях, включающих эту связку (например, проверка и фальсификация). В одностороннем представлении вместо этого используется отрицание: правые правила для связки (скажем, ⅋) эффективно играют роль левых правил для ее двойственного (⊗). Итак, следует ожидать определенного "гармония" между правилом (ями) для связки и правилом (ями) для двойственного.

Мультипликативы

Правила мультипликативной конъюнкции (⊗) и дизъюнкции (⅋):

${\displaystyle \vdash }$ Γ, А       ${\displaystyle \vdash }$ Δ, B ${\displaystyle \vdash }$ Γ, Δ, А ⊗ B

${\displaystyle \vdash }$ Γ, А, B ${\displaystyle \vdash }$ Γ, А ⅋ B

и для их агрегатов:

${\displaystyle \vdash }$ 1

${\displaystyle \vdash }$ Γ ${\displaystyle \vdash }$ Γ, ⊥

Обратите внимание, что правила мультипликативной конъюнкции и дизъюнкции допустимый объяснять соединение и дизъюнкция в классической интерпретации (т.е. они являются допустимыми правилами в LK ).

Добавки

Правила аддитивной конъюнкции (&) и дизъюнкции (⊕):

${\displaystyle \vdash }$ Γ, А       ${\displaystyle \vdash }$ Γ, B ${\displaystyle \vdash }$ Γ, А & B

${\displaystyle \vdash }$ Γ, А ${\displaystyle \vdash }$ Γ, А ⊕ B

${\displaystyle \vdash }$ Γ, B ${\displaystyle \vdash }$ Γ, А ⊕ B

и для их агрегатов:

${\displaystyle \vdash }$ Γ, ⊤

(нет правила для 0)

Заметим, что правила аддитивной конъюнкции и дизъюнкции снова допустимы в классической интерпретации. Но теперь мы можем объяснить основу различия мультипликативного / аддитивного в правилах для двух разных версий конъюнкции: для мультипликативной связки (⊗) контекст заключения (Γ, Δ) делится между предпосылками, тогда как для связки аддитивного падежа (&) контекст заключения (Γ) целиком переносится в оба помещения.

Экспоненты

Показательные числа используются для предоставления контролируемого доступа к ослаблению и сокращению. В частности, мы добавляем структурные правила ослабления и сжатия для предложений?^[5]

${\displaystyle \vdash }$ Γ ${\displaystyle \vdash }$ Γ,?А

${\displaystyle \vdash }$ Γ,?А, ?А ${\displaystyle \vdash }$ Γ,?А

и используйте следующие логические правила:

${\displaystyle \vdash }$ ? Γ, А ${\displaystyle \vdash }$ ? Γ,!А

${\displaystyle \vdash }$ Γ, А ${\displaystyle \vdash }$ Γ,?А

Можно заметить, что правила для экспонент следуют шаблону, отличному от правил для других связок, напоминая правила вывода, управляющие модальностями в формализации секвенциального исчисления нормальная модальная логика S4, и что между дуалами больше нет такой четкой симметрии! и ?. Эта ситуация исправляется в альтернативных представлениях ХЛЛ (например, LU презентация).

Замечательные формулы

В добавок к Двойственности де Моргана Как описано выше, некоторые важные эквиваленты в линейной логике включают:

Распределительность

${\displaystyle A\otimes (B\oplus C)\equiv (A\otimes B)\oplus (A\otimes C)}$

Экспоненциальный изоморфизм

${\displaystyle \,!(A\&B)\equiv \,!A\otimes \,!B}$

(Здесь ${\displaystyle A\equiv B\quad =\quad (A\multimap B)\&(B\multimap A)}$.)

Предположим, что ⅋ - это любой из бинарных операторов times, plus, with или par (но не линейная импликация). Следующее, как правило, не эквивалентно, а лишь подразумевается:

Линейные распределения

Карта, которая не является изоморфизмом, но играет решающую роль в линейной логике:

(А ⊗ (B ⅋ C)) ⊸ ((А ⊗ B) ⅋ C)

Линейные распределения являются фундаментальными в теории доказательства линейной логики. Последствия этой карты были впервые исследованы в ^[6] и называется «слабым распределением». В последующей работе оно было переименовано в «линейное распределение», чтобы отразить фундаментальную связь с линейной логикой.

Кодирование классической / интуиционистской логики в линейной логике

Как интуиционистская, так и классическая импликация может быть восстановлена ​​из линейной импликации путем вставки экспонент: интуиционистская импликация кодируется как !А ⊸ B, а классическая импликация может быть закодирована как !?А ⊸ ?B или же !А ⊸ ?!B (или множество альтернативных возможных переводов).^[7] Идея состоит в том, что экспоненты позволяют нам использовать формулу столько раз, сколько нам нужно, что всегда возможно в классической и интуиционистской логике.

Формально существует перевод формул интуиционистской логики в формулы линейной логики таким способом, который гарантирует доказуемость исходной формулы в интуиционистской логике тогда и только тогда, когда переведенная формула доказуема в линейной логике. С использованием Негативный перевод Гёделя – Гентцена, таким образом, мы можем встроить классическую логику первого порядка в линейную логику первого порядка.

Истолкование ресурса

Лафон (1993) впервые показал, как интуиционистская линейная логика может быть объяснена как логика ресурсов, таким образом предоставляя логическому языку доступ к формализмам, которые можно использовать для рассуждений о ресурсах внутри самой логики, а не, как в классической логике, с помощью средства нелогических предикатов и отношений. Тони Хоар Классический пример торгового автомата (1985) может быть использован для иллюстрации этой идеи.

Предположим, мы представляем конфету с помощью атомарного предложения конфеты, и имея доллар $1. Чтобы констатировать тот факт, что за доллар можно купить один шоколадный батончик, мы могли бы написать следующий вывод: $1 ⇒ конфеты. Но в обычной (классической или интуиционистской) логике от А и А ⇒ B можно сделать вывод А ∧ B. Итак, обычная логика приводит нас к мысли, что мы можем купить шоколадный батончик и сохранить свои деньги! Конечно, мы можем избежать этой проблемы, используя более сложные кодировки,^{[требуется разъяснение ]} хотя обычно такие кодировки страдают от проблема с рамой. Однако отказ от ослабления и сжатия позволяет линейной логике избегать такого рода ложных рассуждений даже с «наивным» правилом. Скорее, чем $1 ⇒ конфеты, мы выражаем свойство торгового автомата как линейный значение $1 ⊸ конфеты. Из $1 и по этому факту можно сделать вывод конфеты, но нет $1 ⊗ конфеты. В общем, мы можем использовать предложение линейной логики А ⊸ B чтобы выразить обоснованность преобразования ресурса А в ресурс B.

На примере торгового автомата рассмотрим «ресурсные интерпретации» других мультипликативных и аддитивных связок. (Экспоненты предоставляют средства для объединения этой интерпретации ресурса с обычным понятием постоянного логическая правда.)

Мультипликативное соединение (А ⊗ B) обозначает одновременное появление ресурсов, которые будут использоваться по указанию потребителя. Например, если вы покупаете жевательную резинку и бутылку безалкогольного напитка, вы запрашиваете камедь ⊗ напиток. Константа 1 означает отсутствие какого-либо ресурса и, следовательно, функционирует как единица измерения.

Аддитивное соединение (А & B) представляет собой альтернативное появление ресурсов, выбор которых контролирует потребитель. Если в автомате есть пачка чипсов, шоколадный батончик и банка безалкогольных напитков, каждая из которых стоит один доллар, то по этой цене вы можете купить ровно один из этих продуктов. Таким образом, мы пишем $1 ⊸ (конфеты & чипсы & напиток). Мы делаем нет записывать $1 ⊸ (конфеты ⊗ чипсы ⊗ напиток), что означало бы, что одного доллара достаточно для покупки всех трех продуктов вместе. Однако из $1 ⊸ (конфеты & чипсы & напиток), мы можем правильно вывести $3 ⊸ (конфеты ⊗ чипсы ⊗ напиток), куда $3 := $1 ⊗ $1 ⊗ $1. Единицу аддитивной связи ⊤ можно рассматривать как корзину для ненужных ресурсов. Например, мы можем написать $3 ⊸ (конфеты ⊗ ⊤) Чтобы выразить это, за три доллара вы можете получить шоколадный батончик и некоторые другие вещи, не вдаваясь в подробности (например, чипсы и напиток, или 2 доллара, или 1 доллар и чипсы и т. д.).

Аддитивная дизъюнкция (А ⊕ B) представляет собой альтернативное возникновение ресурсов, выбором которых управляет машина. Например, предположим, что торговый автомат разрешает азартные игры: вставьте доллар, и автомат может выдать шоколадный батончик, пачку чипсов или безалкогольный напиток. Мы можем выразить эту ситуацию как $1 ⊸ (конфеты ⊕ чипсы ⊕ напиток). Константа 0 представляет продукт, который невозможно произвести, и, таким образом, служит единицей ⊕ (машина, которая может производить А или же 0 так же хороша, как машина, которая всегда производит А потому что ему никогда не удастся произвести 0). Итак, в отличие от вышеизложенного, мы не можем вывести $3 ⊸ (конфеты ⊗ чипсы ⊗ напиток) из этого.

Мультипликативная дизъюнкция (А ⅋ B) с точки зрения интерпретации ресурса труднее подвести, хотя мы можем закодировать обратно в линейную импликацию, либо как А^⊥ ⊸ B или же B^⊥ ⊸ А.

Другие системы доказательства

Доказательства сети

Основная статья: Доказательство сети

Представлен Жан-Ив Жирар были созданы сети доказательств, чтобы избежать бюрократия, вот и все, что делает два вывода разными с логической точки зрения, но не с «моральной» точки зрения.

Например, эти два доказательства идентичны «морально»:

${\displaystyle \vdash }$ А, B, C, D ${\displaystyle \vdash }$ А ⅋ B, C, D ${\displaystyle \vdash }$ А ⅋ B, C ⅋ D

${\displaystyle \vdash }$ А, B, C, D ${\displaystyle \vdash }$ А, B, C ⅋ D ${\displaystyle \vdash }$ А ⅋ B, C ⅋ D

Цель сетей доказательства - сделать их идентичными, создав их графическое представление.

Семантика

Алгебраическая семантика

Смотрите также: Quantale

Разрешимость / сложность вывода

В логическое следствие отношение в полном CLL неразрешимый.^[8] При рассмотрении фрагментов ХЛЛ проблема решения имеет разную сложность:

• Мультипликативная линейная логика (MLL): только мультипликативные связки. MLL следствие НП-полный, даже ограничиваясь Роговые оговорки в чисто импликативном фрагменте,^[9] или к безатомным формулам.^[10]
• Мультипликативно-аддитивная линейная логика (MALL): только мультипликативные и аддитивные (т. Е. Без экспоненты). Влечет за собой МОЛЛ PSPACE-полный.^[8]
• Мультипликативно-экспоненциальная линейная логика (MELL): только мультипликативы и экспоненты. Путем сокращения от проблемы достижимости для Сети Петри,^[11] Влияние MELL должно быть не менее EXPSPACE-жесткий, хотя сама разрешимость имеет статус давно открытой проблемы. В 2015 г. в журнале опубликовано доказательство разрешимости. TCS,^[12] но позже было показано, что он ошибочен.^[13]
• В 1995 году было показано, что аффинная линейная логика (то есть линейная логика с ослаблением, расширение, а не фрагмент) разрешима.^[14]

Варианты

Многие вариации линейной логики возникают в результате дальнейшего изменения структурных правил:

• Аффинная логика, который запрещает сжатие, но допускает глобальное ослабление (разрешимое расширение).
• Строгая логика или же соответствующая логика, который запрещает ослабление, но допускает глобальное сжатие.
• Некоммутативная логика или упорядоченная логика, которая устраняет правило обмена в дополнение к запрету ослабления и сжатия. В упорядоченной логике линейная импликация подразделяется на левую и правую.

Рассмотрены различные интуиционистские варианты линейной логики. Когда основано на представлении последовательного исчисления с одним выводом, как в ILL (интуиционистская линейная логика), связки ⅋, ⊥ и? отсутствуют, и линейная импликация рассматривается как примитивная связка. В FILL (полная интуиционистская линейная логика) связки ⅋, ⊥ и? присутствуют, линейная импликация является примитивной связкой, и, как и в интуиционистской логике, все связки (кроме линейного отрицания) независимы. Существуют также расширения первого и более высокого порядка линейной логики, формальное развитие которых в некоторой степени стандартно ( видеть логика первого порядка и логика высшего порядка ).

Смотрите также

• Философский портал

• Система линейного типа, а система субструктурного типа
• Логика единства (LU)
• Доказательства сети
• Геометрия взаимодействия
• Семантика игры
• Интуиционистская логика
• Логика вычислимости
• Ludics
• Пространства Чу
• Тип уникальности
• Программирование линейной логики

Рекомендации

1. Жирар, Жан-Ив (1987). «Линейная логика» (PDF). Теоретическая информатика. 50 (1): 1–102. Дои:10.1016/0304-3975(87)90045-4. HDL:10338.dmlcz / 120513.
2. Баэз, Джон; Останься, Майк (2008). Боб Кук (ред.). "Физика, топология, логика и вычисления: розеттский камень" (PDF). Новые структуры физики.
3. де Пайва, В.; van Genabith, J .; Риттер, Э. (1999). Дагштульский семинар 99341 по линейной логике и приложениям (PDF).
4. Girard (1987), стр.22, Def.1.15
5. Girard (1987), стр.25-26, Def.1.21
6. Дж. Робин Кокетт и Роберт Сили "Слабо распределительные категории" Журнал чистой и прикладной алгебры 114 (2) 133-173, 1997
7. Ди Космо, Роберто. Учебник по линейной логике. Примечания к курсу; Глава 2.
8. Этот результат и обсуждение некоторых из приведенных ниже фрагментов см .: Линкольн, Патрик; Митчелл, Джон; Щедров, Андре; Шанкар, Натараджан (1992). "Решающие задачи для предложенной линейной логики". Анналы чистой и прикладной логики. 56 (1–3): 239–311. Дои:10.1016 / 0168-0072 (92) 90075-Б.
9. Канович, Макс И. (1992-06-22). «Программирование рупора в линейной логике является NP-полным». Седьмой ежегодный симпозиум IEEE по логике в компьютерных науках, 1992. LICS '92. Труды. Седьмой ежегодный симпозиум IEEE по логике в компьютерных науках, 1992. LICS '92. Ход работы. С. 200–210. Дои:10.1109 / LICS.1992.185533.
10. Линкольн, Патрик; Винклер, Тимоти (1994). "Мультипликативная линейная логика только с константами является NP-полной". Теоретическая информатика. 135: 155–169. Дои:10.1016/0304-3975(94)00108-1.
11. Gunter, C.A .; Гехлот, В. (1989). Десятая международная конференция по применению и теории сетей Петри. Ход работы. С. 174–191. Отсутствует или пусто | название = (помощь)
12. Бимбо, Каталин (13 сентября 2015 г.). «Разрешимость интенсионального фрагмента классической линейной логики». Теоретическая информатика. 597: 1–17. Дои:10.1016 / j.tcs.2015.06.019. ISSN  0304-3975.
13. Штрасбургер, Лутц (10 мая 2019 г.). «О проблеме решения для MELL». Теоретическая информатика. 768: 91–98. Дои:10.1016 / j.tcs.2019.02.022. ISSN  0304-3975.
14. Копылов, А. П. (1995-06-01). «Разрешимость линейной аффинной логики». Десятый ежегодный симпозиум IEEE по логике в компьютерных науках, 1995 г. LICS '95. Труды. Десятый ежегодный симпозиум IEEE по логике в компьютерных науках, 1995 г. LICS '95. Ход работы. С. 496–504. CiteSeerX  10.1.1.23.9226. Дои:10.1109 / LICS.1995.523283.

дальнейшее чтение

• Жирар, Жан-Ив. Линейная логика, Теоретическая информатика, Том 50, № 1, стр. 1–102, 1987.
• Жирар, Жан-Ив, Лафон, Ив, и Тейлор, Поль. Доказательства и типы. Cambridge Press, 1989.
• Хоар, К. А. Р., 1985. Связь последовательных процессов. Prentice-Hall International. ISBN  0-13-153271-5
• Лафон, Ив, 1993. Введение в линейную логику. Конспект лекций Летней школы ТЕМПУС на Алгебраические и категориальные методы в компьютерных науках, Брно, Чехия.
• Троэльстра, А. Лекции по линейной логике. CSLI (Центр изучения языка и информации) Лекционные заметки № 29. Стэнфорд, 1992.
• A. S. Troelstra, Х. Швичтенберг (1996). Основная теория доказательств. Последовательно Кембриджские трактаты по теоретической информатике, Издательство Кембриджского университета, ISBN  0-521-77911-1.
• Ди Космо, Роберто, и Данос, Винсент. Учебник по линейной логике.
• Введение в линейную логику (Постскриптум) автор Патрик Линкольн
• Введение в линейную логику Торбен Браунер
• Вкус линейной логики Филип Вадлер
• Линейная логика к Роберто Ди Космо и Дейл Миллер. Стэнфордская энциклопедия философии (издание осень 2006 г.), Эдвард Н. Залта (ред.).
• Обзор линейного логического программирования к Дейл Миллер. В Линейная логика в информатикепод редакцией Эрхарда, Жирара, Рюэ и Скотта. Издательство Кембриджского университета. Конспект лекций Лондонского математического общества, том 316, 2004 г.
• Линейная логика вики

внешняя ссылка

• СМИ, связанные с Линейная логика в Wikimedia Commons
• Программа доказательства линейной логики (доказатель), доступно для использования в Интернете по адресу: Naoyuki Tamura / Департамент CS / Университет Кобе / Япония