Линейная логика - Linear logic
Линейная логика - это субструктурная логика, предложенная Жан-Ивом Жираром как уточнение классической и интуиционистской логики , объединяющая дуальности первой со многими конструктивными свойствами последней. Хотя логика также изучалась сама по себе, в более широком смысле идеи линейной логики оказали влияние в таких областях, как языки программирования , семантика игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации ). , а также лингвистику , особенно из-за ее упора на ограниченность ресурсов, двойственность и взаимодействие.
Линейная логика поддается множеству различных представлений, объяснений и интуиций. Теоретически это доказательство вытекает из анализа классического секвенциального исчисления, в котором использование ( структурных правил ) сжатия и ослабления тщательно контролируется. С практической точки зрения это означает, что логическая дедукция - это уже не просто постоянно расширяющаяся коллекция устойчивых «истин», но также способ манипулирования ресурсами, которые не всегда могут быть скопированы или выброшены по желанию. С точкой зрения простых денотационных моделей , линейная логика может рассматриваться как уточнение интерпретации интуиционистской логики, заменив декартова (закрытую) категорию с помощью симметричных моноидального (закрытого) категории , или интерпретацию классической логики, заменяя булевы алгебры с помощью C * -алгебры .
Связи, двойственность и полярность
Синтаксис
Язык классической линейной логики (CLL) определяется индуктивно с помощью обозначения BNF
А | знак равно | п ∣ п ⊥ |
∣ | А ⊗ А ∣ А ⊕ А | |
∣ | А & А ∣ А ⅋ А | |
∣ | 1 ∣ 0 ∣ ⊤ ∣ ⊥ | |
∣ | ! А ∣? А |
Здесь р и р ⊥ пробегают логические атомы . По причинам, которые будут объяснены ниже, связки ⊗, ⅋, 1 и ⊥ называются мультипликативными , связки &, ⊕, ⊤ и 0 называются аддитивными , а связки! и ? называются экспонентами . В дальнейшем мы можем использовать следующую терминологию:
Символ | Имя | ||
---|---|---|---|
⊗ | мультипликативная конъюнкция | раз | тензор |
⊕ | аддитивная дизъюнкция | плюс | |
& | аддитивное соединение | с | |
⅋ | мультипликативная дизъюнкция | номинал | |
! | конечно | хлопнуть | |
? | почему бы нет |
Бинарные связки ⊗, ⊕, & и ⅋ ассоциативны и коммутативны; 1 - единица для, 0 - единица для, ⊥ - единица для ⅋, ⊤ - единица для &.
Каждое предложение A в CLL имеет двойственный 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 ⊥ ) |
добавлять | мул | exp | |
---|---|---|---|
позиция | ⊕ 0 | ⊗ 1 | ! |
негр | & ⊤ | ⅋ ⊥ | ? |
Заметим , что (-) ⊥ является инволюцией , т.е. ⊥⊥ = для всех предложений. ⊥ также называется линейное отрицание из A .
Столбцы таблицы предлагают другой способ классификации связок линейной логики, называемый полярностью : связки, отрицаемые в левом столбце (⊗, ⊕, 1, 0,!), Называются положительными , а их двойственные справа (⅋, &, ⊥, ⊤,?) Называются отрицательными ; ср. таблица справа.
Линейный вывод не входит в грамматике связок, но определим в CLL с использованием линейной отрицании и мультипликативной дизъюнкции, от A ⊸ B : = ⊥ ⅋ Б . Соединительный элемент ⊸ иногда произносится как « леденец » из-за его формы.
Последовательное представление исчисления
Один из способов определения линейной логики - это последовательное исчисление . Мы используем буквы Γ и ∆, чтобы пробегать по списку предложений A 1 , ..., A n , также называемых контекстами . Секвенции помещают контекст слева и справа от турникета , написанного Г Д . Интуитивно секвенция утверждает, что конъюнкция Γ влечет за собой дизъюнкцию ∆ (хотя мы имеем в виду «мультипликативную» конъюнкцию и дизъюнкцию, как объясняется ниже). Жирар описывает классическую линейную логику, используя только односторонние секвенции (где левый контекст пуст), и мы следуем здесь более экономичному представлению. Это возможно потому, что любое помещение слева от турникета всегда можно переместить на другую сторону и сдвоить.
Теперь мы дадим правила вывода, описывающие, как строить доказательства секвенций.
Во-первых, чтобы формализовать тот факт, что нас не волнует порядок предложений внутри контекста, мы добавляем структурное правило обмена :
Γ, A 1 , A 2 , Δ |
Γ, A 2 , A 1 , Δ |
Обратите внимание, что мы не добавляем структурные правила ослабления и сокращения, потому что мы действительно заботимся об отсутствии предложений в секвенции и количестве имеющихся копий.
Затем мы добавляем начальные секвенции и разрезы :
|
|
Правило вырезания можно рассматривать как способ составления доказательств, а начальные последовательности служат единицами для композиции. В определенном смысле эти правила являются избыточными: по мере того, как мы вводим дополнительные правила для построения доказательств ниже, мы сохраняем свойство, согласно которому произвольные начальные секвенции могут быть получены из атомарных начальных секвенций, и что всякий раз, когда секвенция доказуема, ей можно дать разрез. бесплатное доказательство. В конечном итоге это свойство канонической формы (которое можно разделить на полноту атомарных начальных секвенций и теорему об исключении разрезов , порождающую понятие аналитического доказательства ) лежит в основе приложений линейной логики в информатике, поскольку оно позволяет логике быть используется в поисковом поиске и в качестве лямбда-исчисления с учетом ресурсов .
Теперь мы объясняем связки, давая логические правила . Обычно в исчислении последовательностей для каждой связки даются и «правые правила», и «левые правила», по сути описывая два способа рассуждений о предложениях, содержащих эту связку (например, проверка и фальсификация). В одностороннем представлении вместо этого используется отрицание: правые правила для связки (скажем,) эффективно играют роль левых правил для ее двойственного (⊗). Итак, мы должны ожидать определенной «гармонии» между правилом (ями) для связки и правилом (ями) для ее дуального.
Мультипликативы
Правила мультипликативной конъюнкции (⊗) и дизъюнкции (⅋):
|
|
и для их агрегатов:
|
|
Обратите внимание, что правила мультипликативной конъюнкции и дизъюнкции допустимы для простой конъюнкции и дизъюнкции в классической интерпретации (т. Е. Они допустимые правила в LK ).
Добавки
Правила аддитивной конъюнкции (&) и дизъюнкции (⊕):
|
|
|
и для их агрегатов:
|
(нет правила для 0 ) |
Заметим, что правила аддитивной конъюнкции и дизъюнкции снова допустимы в классической интерпретации. Но теперь мы можем объяснить основу мультипликативного / аддитивного различия в правилах для двух разных версий конъюнкции: для мультипликативной связки (⊗) контекст заключения ( Γ, ∆ ) разбивается между предпосылками, тогда как для связки аддитивного случая (&) контекст заключения ( Γ ) целиком переносится в обе посылки.
Экспоненты
Экспоненты используются для предоставления контролируемого доступа к ослаблению и сокращению. В частности, мы добавляем структурные правила ослабления и сжатия для предложений?
|
|
и используйте следующие логические правила:
|
|
Можно заметить, что правила для экспонент следуют шаблону, отличному от правил для других связок, напоминая правила вывода, управляющие модальностями в формализации секвенциального исчисления нормальной модальной логики S4, и что больше нет такой четкой симметрии между двойники! и ?. Эта ситуация исправляется в альтернативных представлениях CLL (например, в представлении LU ).
Замечательные формулы
В дополнение к двойственности Де Моргана, описанной выше, некоторые важные эквивалентности в линейной логике включают:
- Распределительность
A ⊗ ( B ⊕ C ) ≣ ( A ⊗ B ) ⊕ ( A ⊗ C ) |
( A ⊕ B ) ⊗ C ≣ ( A ⊗ C ) ⊕ ( B ⊗ C ) |
A ⅋ ( B и C ) ≣ ( A ⅋ B ) и ( A ⅋ C ) |
( A и B ) ⅋ C ≣ ( A ⅋ C ) и ( B ⅋ C ) |
По определению A ⊸ B как A ⊥ ⅋ B последние два закона дистрибутивности также дают:
A ⊸ ( B и C ) ≣ ( A ⊸ B ) и ( A ⊸ C ) |
( A ⊕ B ) ⊸ C ≣ ( A ⊸ C ) и ( B ⊸ C ) |
(Здесь A ≣ B означает ( A ⊸ B ) & ( B ⊸ A ) .)
- Экспоненциальный изоморфизм
! ( A и B ) ≣! А ! B |
? ( A ⊕ B ) ≣? А ⅋? B |
- Линейные распределения
Карта, которая не является изоморфизмом, но играет решающую роль в линейной логике:
( A ⊗ ( B ⅋ C )) ⊸ (( A ⊗ B ) ⅋ C ) |
Линейные распределения являются фундаментальными в теории доказательств линейной логики. Последствия этой карты были впервые исследованы и названы «слабым распределением». В последующей работе оно было переименовано в «линейное распределение», чтобы отразить фундаментальную связь с линейной логикой.
- Прочие последствия
Следующие формулы дистрибутивности в общем случае не эквивалентны, а только импликации:
! А ! B ⊸! ( A ⊗ B ) |
! А ! B ⊸! ( A ⊕ B ) |
? ( A ⅋ B ) ⊸? А ⅋? B |
? ( A и B ) ⊸? А &? B |
( A и B ) ⊗ C ⊸ ( A ⊗ C ) и ( B ⊗ C ) |
( A и B ) ⊕ C ⊸ ( A ⊕ C ) и ( B ⊕ C ) |
( A ⅋ C ) ⊕ ( B ⅋ C ) ⊸ ( A ⊕ B ) ⅋ C |
( A и C ) ⊕ ( B и C ) ⊸ ( A ⊕ B ) и C |
Кодирование классической / интуиционистской логики в линейной логике
Как интуиционистская, так и классическая импликация могут быть восстановлены из линейной импликации путем вставки экспонент: интуиционистская импликация кодируется как ! A ⊸ B , а классическая импликация может быть закодирована как !? А ⊸? B или ! А ⊸?! B (или множество альтернативных возможных переводов). Идея состоит в том, что экспоненты позволяют нам использовать формулу столько раз, сколько нам нужно, что всегда возможно в классической и интуиционистской логике.
Формально существует перевод формул интуиционистской логики в формулы линейной логики таким образом, чтобы гарантировать доказуемость исходной формулы в интуиционистской логике тогда и только тогда, когда переведенная формула доказуема в линейной логике. Таким образом, используя отрицательный перенос Гёделя – Генцена , мы можем встроить классическую логику первого порядка в линейную логику первого порядка.
Истолкование ресурса
Лафон (1993) впервые показал, как интуиционистская линейная логика может быть объяснена как логика ресурсов, таким образом предоставляя логическому языку доступ к формализмам, которые можно использовать для рассуждений о ресурсах внутри самой логики, а не, как в классической логике, с помощью средства нелогических предикатов и отношений. Для иллюстрации этой идеи можно использовать классический пример торгового автомата Тони Хоара (1985).
Предположим, что мы представляем конфету с помощью атомарного предложения конфеты и доллар с помощью 1 доллара . Чтобы констатировать тот факт, что за доллар можно купить один шоколадный батончик, мы могли бы написать импликацию $ 1 ⇒ конфеты . Но в обычной (классической или интуиционистской) логики, от A и A ⇒ B можно заключить A ∧ B . Итак, обычная логика приводит нас к мысли, что мы можем купить шоколадный батончик и сохранить свои деньги! Конечно, мы можем избежать этой проблемы, используя более сложные кодировки, хотя обычно такие кодировки страдают проблемой фреймов . Однако отказ от ослабления и сжатия позволяет линейной логике избегать такого рода ложных рассуждений даже с «наивным» правилом. Вместо $ 1 ⇒ конфеты , мы выражаем собственность торгового автомата в качестве линейного следования $ 1 ⊸ конфеты . От $ 1 и этот факт, мы можем заключить , конфеты , но не $ 1 ⊗ конфеты . В общем, мы можем использовать линейное логическое суждение ⊸ B , чтобы выразить законность преобразования ресурса A в ресурсе B .
На примере торгового автомата рассмотрим «ресурсные интерпретации» других мультипликативных и аддитивных связок. (Экспоненты предоставляют средства для объединения этой ресурсной интерпретации с обычным понятием постоянной логической истины .)
Мультипликативная конъюнкция ( A ⊗ B ) обозначает одновременное появление ресурсов, которые будут использоваться в соответствии с указаниями потребителя. Например, если вы покупаете палку резины и бутылку безалкогольного напитка, то вы запрашиваете камеди ⊗ напиток . Константа 1 обозначает отсутствие какого-либо ресурса и, таким образом, функционирует как единица измерения.
Аддитивная конъюнкция ( A и B ) представляет собой альтернативное появление ресурсов, выбор которых контролирует потребитель. Если в торговом автомате есть пачка чипсов, шоколадный батончик и банка безалкогольных напитков, каждая из которых стоит один доллар, то по этой цене вы можете купить ровно один из этих продуктов. Таким образом , мы пишем $ 1 ⊸ ( конфеты & чипсы & напиток ) . Мы не пишем $ 1 ⊸ ( конфеты ⊗ чипсы ⊗ напиток ) , что означает, что одного доллара достаточно для покупки всех трех продуктов вместе. Тем не менее, от $ 1 ⊸ ( конфеты и чипсы и напитки ) , мы можем правильно вывести $ 3 ⊸ ( конфеты ⊗ чипы ⊗ напиток ) , где $ 3 : = $ 1 ⊗ $ 1 ⊗ $ 1 . Блок ⊤ аддитивной связи можно рассматривать как мусорную корзину для ненужных ресурсов. Например, мы можем написать $ 3 ⊸ ( конфеты ⊗ ⊤), чтобы выразить, что с тремя долларами вы можете получить шоколадный батончик и некоторые другие вещи, не вдаваясь в подробности (например, чипсы и напиток, или 2 доллара, или 1 доллар и чипсы. , так далее.).
Аддитивная дизъюнкция ( A ⊕ B ) представляет собой альтернативное вхождение ресурсов, выбор которых контролирует машина. Например, предположим, что торговый автомат разрешает азартные игры: вставьте доллар, и автомат может выдать шоколадный батончик, пачку чипсов или безалкогольный напиток. Мы можем выразить эту ситуацию как $ 1 ⊸ ( конфеты ⊕ чипсы ⊕ напиток ) . Константа 0 представляет продукт, который невозможно произвести, и, таким образом, служит единицей (машина, которая может производить A или 0 , так же хороша, как машина, которая всегда производит A, потому что ей никогда не удастся произвести 0). Таким образом , в отличие от выше, мы не можем вывести $ 3 ⊸ ( конфеты ⊗ Щепа ⊗ напиток ) от этого.
Мультипликативная дизъюнкция ( ⅋ Б ) более трудно глянец с точкой зрения интерпретации ресурса, хотя мы можем кодировать обратно в линейную импликацию, либо как A ⊥ ⊸ B или B ⊥ ⊸ A .
Другие системы доказательства
Доказательства сети
Представленные Жан-Ивом Жираром , сети доказательств были созданы, чтобы избежать бюрократии , то есть всего того, что делает два вывода разными с логической точки зрения, но не с «моральной» точки зрения.
Например, эти два доказательства идентичны «морально»:
|
|
Цель сетей доказательства - сделать их идентичными, создав их графическое представление.
Семантика
Алгебраическая семантика
Разрешимость / сложность вывода
Отношение следования в полной CLL неразрешимо . При рассмотрении фрагментов ХЛЛ проблема решения имеет разную сложность:
- Мультипликативная линейная логика (MLL): только мультипликативные связки. Вывод MLL является NP-полным , даже ограничиваясь предложениями Горна в чисто импликативном фрагменте или безатомными формулами.
- Мультипликативно-аддитивная линейная логика (MALL): только мультипликативные и аддитивные (т. Е. Без экспоненциальной зависимости). Влечение ТЦ является PSPACE-полным .
- Мультипликативно-экспоненциальная линейная логика (MELL): только мультипликативы и экспоненты. Путем редукции из проблемы достижимости для сетей Петри вывод MELL должен быть по крайней мере EXPSPACE-трудным , хотя сама разрешимость имеет статус давней открытой проблемы. В 2015 году доказательство разрешимости было опубликовано в журнале TCS , но позже было показано, что оно ошибочное.
- В 1995 году было показано, что аффинная линейная логика (то есть линейная логика с ослаблением, расширение, а не фрагмент) разрешима.
Варианты
Многие вариации линейной логики возникают в результате дальнейшего изменения структурных правил:
- Аффинная логика , запрещающая сжатие, но допускающая глобальное ослабление (разрешимое расширение).
- Строгая логика или соответствующая логика , запрещающая ослабление, но допускающая глобальное сокращение.
- Некоммутативная логика или упорядоченная логика, которая удаляет правило обмена в дополнение к запрету ослабления и сжатия. В упорядоченной логике линейная импликация подразделяется на левую и правую.
Рассмотрены различные интуиционистские варианты линейной логики. Если основано на представлении последовательного исчисления с одним выводом, как в ILL (интуиционистская линейная логика), связки ⅋, ⊥ и? отсутствуют, и линейная импликация рассматривается как примитивная связка. В FILL (полная интуиционистская линейная логика) связки ⅋, ⊥ и? присутствуют, линейная импликация является примитивной связкой, и, подобно тому, что происходит в интуиционистской логике, все связки (кроме линейного отрицания) независимы. Существуют также расширения первого и более высокого порядка линейной логики, формальное развитие которых в некоторой степени стандартно (см. Логику первого и высшего порядка ).
Смотрите также
- Система типов Линейной , A субструктурного типа системы
- Логика единства (LU)
- Доказательства сети
- Геометрия взаимодействия
- Семантика игры
- Интуиционистская логика
- Логика вычислимости
- Ludics
- Пространства Чу
- Тип уникальности
- Программирование линейной логики
использованная литература
дальнейшее чтение
- Жирар, Жан-Ив. Линейная логика , Теоретическая информатика, Том 50, № 1, стр. 1–102, 1987.
- Жирар, Жан-Ив, Лафон, Ив и Тейлор, Поль. Доказательства и типы . Cambridge Press, 1989.
- Хоар, ЦАР, 1985. Связь последовательных процессов . Prentice-Hall International. ISBN 0-13-153271-5
- Лафон, Ив, 1993. Введение в линейную логику . Конспект лекций Летней школы TEMPUS по алгебраическим и категориальным методам в компьютерных науках , Брно, Чешская Республика.
- Трельстра А.С. Лекции по линейной логике . CSLI (Центр изучения языка и информации) Конспект лекций № 29. Стэнфорд, 1992.
- AS Troelstra , Х. Швихтенберг (1996). Основная теория доказательств . В серии « Кембриджские трактаты по теоретической информатике» , издательство Кембриджского университета, ISBN 0-521-77911-1 .
- Ди Космо, Роберто, и Данос, Винсент. Учебник по линейной логике .
- Введение в линейную логику (постскриптум) Патрика Линкольна
- Введение в линейную логику Торбена Браунера
- Вкус линейной логики Филипа Вадлера
- Линейная логика от Roberto Di Cosmo и Дейл Миллер . Стэнфордская энциклопедия философии (издание осень 2006 г.), Эдвард Н. Залта (ред.).
- Обзор линейной логики программирования по Дейл Миллер . В Linear Logic in Computer Science , под редакцией Ehrhard, Girard, Ruet и Scott. Издательство Кембриджского университета. Конспект лекций Лондонского математического общества, том 316, 2004 г.
- Линейная логика вики
внешние ссылки
- СМИ, связанные с линейной логикой на Викискладе?
- Программа для доказательства линейной логики , доступная для использования в Интернете по адресу : Naoyuki Tamura / Dept of CS / Kobe University / Japan