Линейная логика — это субструктурная логика, предложенная Жан-Ивом Жираром как усовершенствование классической и интуиционистской логики , объединяющая двойственность первой со многими конструктивными свойствами последней. [1] Хотя логика также изучалась сама по себе, в более широком смысле идеи линейной логики оказали влияние на такие области, как языки программирования , семантика игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовых вычислений ). теория информации ), [2] , а также лингвистика , [3] особенно из-за ее акцента на ограниченности ресурсов, двойственности и взаимодействии.
Линейная логика допускает множество различных представлений, объяснений и интуиций.С точки зрения теории доказательства , оно вытекает из анализа классического секвенциального исчисления , в котором использование ( структурных правил ) сжатия и ослабления тщательно контролируется. С практической точки зрения это означает, что логический вывод больше не является просто постоянно расширяющимся набором устойчивых «истин», но также и способом манипулирования ресурсами , которые не всегда можно дублировать или выбрасывать по своему желанию. С точки зрения простых денотационных моделей линейную логику можно рассматривать как уточнение интерпретации интуиционистской логики путем замены декартовых (замкнутых) категорий симметричными моноидальными (замкнутыми) категориями или интерпретацию классической логики путем замены булевых алгебр C *-алгебрами . [ нужна цитата ]
Язык классической линейной логики (CLL) определяется индуктивно с помощью обозначения BNF.
Здесь p и p⊥ пробегают логические атомы . По причинам, которые будут объяснены ниже, связки ⊗, ⅋, 1 и ⊥ называются мультипликативами , связки &, ⊕, ⊤ и 0 называются аддитивами , а связки ! и ? называются экспонентами . Далее мы можем использовать следующую терминологию:
Бинарные связки ⊗, ⊕, & и ⅋ ассоциативны и коммутативны; 1 — единица измерения ⊗, 0 — единица измерения ⊕, ⊥ — единица измерения ⅋, а ⊤ — единица измерения &.
Каждое предложение A в CLL имеет двойственное A ⊥ , определенное следующим образом:
Заметим, что (-) ⊥ является инволюцией , т. е. A ⊥⊥ = A для всех предложений. A ⊥ также называется линейным отрицанием A .
Столбцы таблицы предлагают другой способ классификации связок линейной логики, называемыйполярность : отрицательные связки в левом столбце (⊗, ⊕, 1, 0, !) называютсяположительными, а их двойственные справа (⅋, &, ⊥, ⊤, ?) называютсяотрицательными; ср. стол справа.
Линейная импликация не включена в грамматику связок, но в CLL ее можно определить с помощью линейного отрицания и мультипликативной дизъюнкции по формуле A ⊸ B := A ⊥ ⅋ B . Соединительный союз ⊸ иногда произносится как «леденец» из-за его формы.
Один из способов определения линейной логики — это секвенциальное исчисление . Мы используем буквы Γ и Δ для ранжирования списков предложений A 1 , ..., An , также называемых контекстами . Секвенция помещает контекст слева и справа от турникета , записываемый Γ Δ . Интуитивно секвенция утверждает, что конъюнкция Γ влечет за собой дизъюнкцию Δ (хотя мы имеем в виду «мультипликативную» конъюнкцию и дизъюнкцию, как поясняется ниже). Жирар описывает классическую линейную логику, используя только односторонние секвенции (где левый контекст пуст), и мы следуем здесь этому более экономичному изложению. Это возможно, поскольку любое помещение слева от турникета всегда можно перенести на другую сторону и дуализировать.
Теперь мы дадим правила вывода , описывающие, как строить доказательства секвенций. [4]
Во-первых, чтобы формализовать тот факт, что нас не волнует порядок предложений внутри контекста, мы добавляем структурное правило обмена :
Обратите внимание, что мы не добавляем структурные правила ослабления и сокращения, поскольку нас заботит отсутствие предложений в секвенции и количество присутствующих копий.
Далее мы добавляем начальные секвенции и разрезы :
Правило отсечения можно рассматривать как способ составления доказательств, а начальные секвенции служат единицами композиции . В определенном смысле эти правила избыточны: поскольку ниже мы вводим дополнительные правила для построения доказательств, мы будем сохранять то свойство, что произвольные начальные секвенции могут быть получены из атомарных начальных секвенций и что всякий раз, когда секвенция доказуема, ей можно дать разрез. бесплатное доказательство. В конечном счете, это свойство канонической формы (которое можно разделить на полноту атомарных начальных секвенций и теорему об исключении разреза , порождающую понятие аналитического доказательства ) лежит в основе приложений линейной логики в информатике, поскольку оно позволяет логике быть используется при поиске доказательств и в качестве лямбда-исчисления с учетом ресурсов .
Теперь мы объясним связки, приведя логические правила . Обычно в секвенциальном исчислении для каждой связки даются как «правые правила», так и «левые правила», по существу описывая два способа рассуждения о предложениях, включающих эту связку (например, проверка и фальсификация). В одностороннем представлении вместо этого используется отрицание: правые правила для связки (скажем, ⅋) эффективно играют роль левых правил для ее двойственной (⊗). Итак, следует ожидать определенной «гармонии» между правилом(ами) для связки и правилом(ами) для ее двойственного.
Правила мультипликативного конъюнкции (⊗) и дизъюнкции (⅋):
и для их подразделений:
Заметим, что правила мультипликативной конъюнкции и дизъюнкции допустимы для простой конъюнкции и дизъюнкции в классической интерпретации (т. е. они являются допустимыми правилами в LK ).
Правила аддитивной конъюнкции (&) и дизъюнкции (⊕):
и для их подразделений:
Заметим, что правила аддитивной конъюнкции и дизъюнкции снова допустимы в классической интерпретации. Но теперь мы можем объяснить основу мультипликативного/аддитивного различия в правилах для двух разных вариантов конъюнкции: для мультипликативной связки (⊗) контекст заключения ( Γ, Δ ) расщепляется между посылками, тогда как для аддитивной падежной связки (&) контекст заключения ( Γ ) целиком переносится в обе посылки.
Экспоненты используются для обеспечения контролируемого доступа к ослаблению и сокращению. В частности, мы добавляем структурные правила ослабления и сжатия для предложений ?'d: [5]
и используйте следующие логические правила:
Можно заметить, что правила для экспонент следуют другой схеме, чем правила для других связок, напоминая правила вывода, управляющие модальностями в последовательных формализациях исчисления нормальной модальной логики S4 , и что больше нет такой явной симметрии между двойники! и ?. Эту ситуацию исправляют альтернативные представления CLL (например, LU-представление).
Помимо описанных выше двойственностей Де Моргана , некоторые важные эквивалентности в линейной логике включают:
По определению A ⊸ B как A ⊥ ⅋ B , последние два закона дистрибутивности также дают:
(Здесь A ≣ B есть ( A ⊸ B ) & ( B ⊸ A ) .)
Отображение, которое не является изоморфизмом, но играет решающую роль в линейной логике:
Линейные распределения являются фундаментальными в теории доказательств линейной логики. Последствия этого отображения были впервые исследованы в [6] и названы «слабым распределением». В последующих работах оно было переименовано в «линейное распределение», чтобы отразить фундаментальную связь с линейной логикой.
Следующие формулы дистрибутивности, как правило, не являются эквивалентностью, а являются лишь импликацией:
Как интуиционистскую, так и классическую импликацию можно восстановить из линейной импликации путем вставки экспонент: интуиционистская импликация кодируется как ! A ⊸ B , а классическую импликацию можно закодировать как !? А ⊸ ? Б или ! А ⊸?! B (или множество альтернативных возможных переводов). [7] Идея состоит в том, что экспоненты позволяют нам использовать формулу столько раз, сколько нам нужно, что всегда возможно в классической и интуиционистской логике.
Формально существует перевод формул интуиционистской логики в формулы линейной логики таким образом, чтобы гарантировать доказуемость исходной формулы в интуиционистской логике тогда и только тогда, когда переведенная формула доказуема в линейной логике. Таким образом , используя отрицательный перевод Гёделя – Генцена , мы можем встроить классическую логику первого порядка в линейную логику первого порядка.
Лафонт (1993) впервые показал, как интуиционистскую линейную логику можно объяснить как логику ресурсов, предоставив таким образом логическому языку доступ к формализмам, которые можно использовать для рассуждений о ресурсах внутри самой логики, а не, как в классической логике, путем средствами нелогических предикатов и отношений. Классический пример торгового автомата Тони Хоара (1985) можно использовать для иллюстрации этой идеи.
Предположим, мы представляем наличие шоколадного батончика атомарным предложением candy , а наличие доллара — 1 долларом . Чтобы констатировать тот факт, что за доллар вы сможете купить одну шоколадку, мы могли бы написать импликацию $1 ⇒ конфета . Но в обычной (классической или интуиционистской) логике из A и A ⇒ B можно заключить A ∧ B. Итак, обычная логика приводит нас к мысли, что мы можем купить шоколадку и сохранить свой доллар! Конечно, мы можем избежать этой проблемы, используя более сложные кодировки, [ необходимы пояснения ] , хотя обычно такие кодировки страдают от проблемы с кадрами . Однако отказ от ослабления и сжатия позволяет линейной логике избежать такого рода ложных рассуждений даже при наличии «наивного» правила. Вместо $1 ⇒ candy мы выражаем свойство торгового автомата как линейную импликацию $1 ⊸ candy . Из $1 и этого факта мы можем сделать вывод о конфетах , но не о $1 ⊗ конфетах . В общем, мы можем использовать предложение линейной логики A ⊸ B , чтобы выразить обоснованность преобразования ресурса A в ресурс B.
На примере торгового автомата рассмотрим «ресурсные интерпретации» других мультипликативных и аддитивных связок. (Экспоненты предоставляют средства для объединения этой интерпретации ресурса с обычным понятием устойчивой логической истины .)
Мультипликативный союз ( A ⊗ B ) обозначает одновременное появление ресурсов, которые будут использоваться по указанию потребителя. Например, если вы покупаете жевательную резинку и бутылку безалкогольного напитка, вы запрашиваете жевательную резинку ⊗ . Константа 1 обозначает отсутствие какого-либо ресурса и поэтому функционирует как единица ⊗.
Аддитивный союз ( А и Б ) представляет собой альтернативное возникновение ресурсов, выбор которых контролирует потребитель. Если в торговом автомате есть пачка чипсов, шоколадный батончик и банка безалкогольного напитка, каждая из которых стоит один доллар, то за эту цену вы можете купить ровно один из этих продуктов. Таким образом, мы пишем $1 ⊸ ( конфеты , чипсы и напитки ) . Мы не пишем 1 доллар ⊸ ( конфеты ⊗ чипсы ⊗ напиток ) , что означало бы, что одного доллара достаточно для покупки всех трех продуктов вместе. Однако из $1 ⊸ ( конфеты , чипсы и напитки ) мы можем правильно вывести $3 ⊸ ( конфеты ⊗ чипсы ⊗ напиток ) , где $3 := $1 ⊗ $1 ⊗ $1 . Единицу ⊤ аддитивного соединения можно рассматривать как мусорную корзину для ненужных ресурсов. Например, мы можем написать $3 ⊸ ( конфеты ⊗ ⊤) , чтобы выразить, что за три доллара вы можете получить шоколадный батончик и некоторые другие вещи, не вдаваясь в подробности (например, чипсы и напиток, или 2 доллара, или 1 доллар и фишки). , и т. д.).
Аддитивная дизъюнкция ( A ⊕ B ) представляет собой альтернативное появление ресурсов, выбором которых управляет машина. Например, предположим, что торговый автомат разрешает азартные игры: вставьте доллар, и автомат сможет выдать шоколадный батончик, пачку чипсов или безалкогольный напиток. Мы можем выразить эту ситуацию как 1 доллар ⊸ ( конфеты ⊕ чипсы ⊕ напиток ) . Константа 0 представляет собой продукт, который невозможно произвести, и, таким образом, служит единицей ⊕ (машина, которая может производить А или 0, так же хороша, как и машина, которая всегда производит А , потому что ей никогда не удастся произвести 0). Таким образом, в отличие от предыдущего, мы не можем вывести из этого 3 доллара ⊸ ( конфеты ⊗ чипсы ⊗ напиток ) .
Сети доказательств, представленные Жан-Ивом Жираром , были созданы во избежание бюрократии , то есть всего того, что делает два вывода разными с логической точки зрения, но не с «моральной» точки зрения.
Например, эти два доказательства «морально» идентичны:
Цель сетей доказательств — сделать их идентичными, создав их графическое представление.
Отношение следования в полной CLL неразрешимо . [8] При рассмотрении фрагментов CLL проблема решения имеет различную сложность:
Многие варианты линейной логики возникают в результате дальнейшего изменения структурных правил:
Рассмотрены различные интуиционистские варианты линейной логики. Когда оно основано на представлении последовательного исчисления с одним выводом, как в ILL (интуиционистская линейная логика), связки ⅋, ⊥ и ? отсутствуют, а линейная импликация трактуется как примитивная связка. В FILL (полная интуиционистская линейная логика) связки ⅋, ⊥ и ? присутствуют, линейная импликация является примитивной связкой и, как и в интуиционистской логике, все связки (кроме линейного отрицания) независимы. Существуют также расширения линейной логики первого и высшего порядка, формальное развитие которых несколько стандартно (см. Логика первого порядка и Логика высшего порядка ).
{{cite conference}}: Отсутствует или пусто |title=( помощь )
СМИ, связанные с линейной логикой, на Викискладе?