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

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

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

• 1 Связи, двойственность и полярность
  • 1.1 Синтаксис
• 2 Последовательность представление исчисления
  • 2.1 Множители
  • 2.2 Добавки
  • 2.3 Экспоненты
• 3 Замечательные формулы
• 4 Кодирование классической / интуиционистской логики в линейной логике
• 5 Интерпретация ресурсов
• 6 Другие системы доказательств
  • 6.1 Сети доказательства
• 7 Семантика
  • 7.1 Алгебраическая семантика
• 8 Разрешимость / сложность вывода
• 9 Варианты
• 10 См. Также
• 11 Ссылки
• 12 Дополнительная литература
• 13 Внешние ссылки

Синтаксис

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

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

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

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

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

Обратите внимание, что (-) является инволюцией, т. Е. A= Aдля всех предложений. Aтакже называется линейным отрицанием A.

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

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

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

Теперь мы даем правила вывода, описывающие, как строить доказательства секвенций.

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

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, A 1, A 2, Δ

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, A 2, A 1, Δ

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

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

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$A, A

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, A $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$A, Δ $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, Δ

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

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

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

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

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, A $⊢\; \{\; \backslash \; displaystyle\; \backslash \; vdash\}$Δ, B $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, Δ, A⊗ B

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, A, B $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, A⅋ B

и для их единиц:

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$1

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, ⊥

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

Добавки

Правила для аддитивного соединения () и дизъюнкции (⊕):

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, A $⊢\; \{\; \backslash \; displaystyle\; \backslash \; vdash\}$Γ, B $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, AB

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, A $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, A⊕ B

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, B $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, A⊕ B

и их единицы измерения:

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ, ⊤

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

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

Экспоненты

Экспоненты используются для предоставления контролируемого доступа к ослаблению и сжатию. В частности, мы добавляем структурные правила ослабления и сжатия для предложений? 'D:

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ,? A

$⊢\; \{\; \backslash \; displaystyle\; \backslash \; vdash\}$Γ,? A,? A $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ,? A

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

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$? Γ, A $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$? Γ,! A

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\; \}$Γ, A $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$Γ,? A

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

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

Дистрибутивность

$A\; \otimes \; (B\; \oplus \; C)\; \equiv \; (A\; \otimes \; B)\; \oplus \; (A\; \otimes \; C)\; \{\backslash \; Displaystyle\; A\; \backslash \; otimes\; (B\; \backslash \; oplus\; C)\; \backslash \; Equiv\; (A\; \backslash \; otimes\; B)\; \backslash \; oplus\; (A\; \backslash \; otimes\; C)\}$

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

$!\; (A\; и\; B)!\; А!\; B\; \{\backslash \; displaystyle\; \backslash ,!\; (A\; \backslash \; B)\; \backslash \; Equiv\; \backslash ,!\; A\; \backslash \; otimes\; \backslash ,!\; B\}$

(Здесь $A\; \equiv \; B\; =\; (A\; ⊸\; B)\; (B\; ⊸\; A)\; \{\backslash \; displaystyle\; A\; \backslash \; Equiv\; B\; \backslash \; quad\; =\; \backslash \; quad\; (A\; \backslash \; multimap\; B)\; \backslash \; (B\; \backslash \; multimap\; A)\}$.)

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

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

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

(A⊗ (B⅋ C)) ⊸ ((A⊗ B) ⅋ C)

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

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

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

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

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

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

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

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

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

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

Сети доказательств

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

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

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$A, B, C, D $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$A⅋ B, C, D $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$A⅋ B, C⅋ D

$⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$A, B, C, D $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$A, B, C⅋ D $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$A⅋ B, C⅋ D

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

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

Отношение следование в полной CLL неразрешимо. При рассмотрении фрагментов CLL проблема решения имеет разную сложность:

• Мультипликативная линейная логика (MLL): только мультипликативные связки. Вывод MLL является NP-полным, даже ограничиваясь предложениями Хорна в чисто импликативном фрагменте или безатомными формулами.
• Мультипликативно-аддитивная линейная логика (MALL): только мультипликативы и добавки (т. е. без экспоненты). Вывод MALL PSPACE-complete.
• Мультипликативно-экспоненциальная линейная логика (MELL): только мультипликативы и экспоненты. Путем сокращения проблемы достижимости для сетей Петри, следствие MELL должно быть не менее EXPSPACE-hard, хотя сама разрешимость имеет статус давно открытой проблемы. В 2015 году доказательство разрешимости было опубликовано в журнале TCS, но позже было показано, что оно ошибочно.
• Аффинная линейная логика (то есть линейная логика с ослаблением, расширение, а не фрагмент), как было показано в 1995 году, разрешима.

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

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

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

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

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

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

• Средства массовой информации, относящиеся к линейной логике на Wikimedia Commons
• A Linear Logic Prover (llprover), доступный для использования в Интернете по адресу: Naoyuki Tamura / Департамент CS / Университет Кобе / Япония