Как я должен думать о проверочных сетях?

В своем ответе на этот вопрос , Стефан Хименес указал мне на алгоритм нормализации полиномиальное время для доказательств в линейной логике. В доказательстве в статье Жирара используются сети доказательств, которые являются аспектом линейной логики, о которой я на самом деле не очень много знаю.

Я уже пытался читать статьи о сетях доказательств (например , заметки о них Пьера-Луи Кюриена ), но на самом деле я их не понял. Итак, мой вопрос: как я должен думать о них? Под «как думать о них» я имею в виду неформальную интуицию, стоящую за ними (например, как они ведут себя в вычислительном отношении, или как они связаны с последовательностями), а также те теоремы о них, которые я должен доказать для себя, чтобы действительно получить их.

Отвечая на этот вопрос, вы можете предположить, что (1) я хорошо знаю теорию доказательств линейной логики (включая такие вещи, как, как идет доказательство исключения срезов, и в сфокусированной форме), (2) их категориальную семантику в терминах пространств когерентности или с помощью свертки Дня, и (3) самые основные зачатки строительства GoI.

Пруф-сети интересны в основном по трем причинам:

1) ИДЕНТИЧНОСТЬ ДОКАЗАТЕЛЬСТВ. Они дают ответ на вопрос «когда два доказательства одинаковы»? В исчислении секвенций у вас может быть много разных доказательств одного и того же предложения, которые различаются только потому, что в исчислении секвенций выстраивается порядок среди правил вывода, даже если в этом нет необходимости. Конечно, можно добавить отношение эквивалентности в доказательствах последовательного исчисления, но затем нужно показать, что исключение срезов ведет себя правильно на классах эквивалентности, а также необходимо обратиться к переписыванию по модулю, что является гораздо более техническим, чем простое переписывание. Сети доказательства решают проблему работы с классами эквивалентности, предоставляя синтаксис, в котором каждый класс эквивалентности свернут на одном объекте. Эта ситуация в любом случае немного идеалистическая, поскольку по многим причинам сети доказательств часто расширяются с некоторой формой эквивалентности.

2) НИКАКИХ КОММУТАТИВНЫХ ШАГОВ ВЫРЕЗАНИЯ. Исключение вырезов в контрольных сетях приобретает совершенно иной вид, чем в последовательных исчислениях, потому что коммутативные этапы вырезов исчезают Причина в том, что в сетях доказательств правила дедукции связаны только их причинной связью. Коммутативные случаи порождаются тем фактом, что одно правило может быть скрыто другим причинно не связанным правилом. Этого не может быть в сетях доказательств, где причинно не связанные правила находятся далеко друг от друга. Поскольку большинство случаев исключения среза являются коммутативными, можно получить поразительное упрощение устранения среза. Это было особенно полезно для изучения лямбда-исчислений с явными заменами (потому что экспоненты = явные замены). Опять же, эта ситуация идеализирована, поскольку некоторые представления сетей доказательств требуют коммутативных шагов. Тем не мение,

3) КРИТЕРИИ ПРАВИЛЬНОСТИ. Сети доказательств могут быть определены путем перевода последовательных доказательств исчисления, но обычно система сетей доказательств не принимается как таковая, если она не снабжена критерием корректности, то есть набором теоретико-графических принципов, характеризующих набор графов, полученных путем перевода доказательство последовательного исчисления. Причина, по которой требуется критерий корректности, заключается в том, что свободный графический язык, сгенерированный набором конструкторов сети доказательств (называемых ссылками), содержит «слишком много графов» в том смысле, что некоторые графы не соответствуют никаким доказательствам. Актуальность подхода критериев правильности обычно полностью не понимается. Это важно, потому что он дает неиндуктивные определения того, что является доказательством, предоставляя поразительно разные взгляды на природу вычетов. Тот факт, что характеристика не является индуктивной, обычно подвергается критике, хотя это именно то, что интересно. Конечно, его нелегко поддается формализации, но, опять же, в этом его сила: сети доказательств дают понимание, которое недоступно из-за обычной индуктивной перспективы доказательств и терминов. Фундаментальной теоремой для сетей доказательства является теорема секвенизации, которая говорит, что любой граф, удовлетворяющий критерию корректности, может быть индуктивно разложен как доказательство последовательного исчисления (перевод обратно в правильный граф).

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

$-A$$A$$-A$$A$

Жирар заметил, что естественный вывод именно таким образом асимметричен. Вот почему это совпадает с интуиционистской логикой. Сети доказательств представляют собой попытку Жирара изобрести симметричную форму естественного вывода.

Лучшее введение в эти идеи - в «Доказательствах и типах» Жирара. Если вы работаете через систему естественного вычета и последовательного исчисления для$\land\to$

$\Gamma \vdash A$$\vdash \Gamma^\perp, A$

Что-то я упустил в своем первоначальном ответе: сети доказательств - это способ написания доказательств, и мы знаем, что доказательства - это программы. Таким образом, доказательство сетей также способ написания программ.

Традиционная функциональная нотация для написания программ асимметрична, как и естественная дедукция. Таким образом, сети доказательств указывают на способ написания программ в симметричной форме. Вот как процесс исчисления входит в картину.

Другой способ представления симметрии - через логическое программирование, которое я исследовал в двух статьях: типизированное основание для программ направленной логики и аспекты логического программирования высшего порядка.

Я сосредотачиваюсь на том, как сети доказательства связаны с последовательным исчислением, оставляя более динамичный материал.

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

В основном это относится к части вашего вопроса «как они ведут себя вычислительно». Один из способов хорошо понять сети доказательств с вычислительной точки зрения - взглянуть на чуть более конкретные интерпретации (например, алгебраический процесс).

Вы можете быть заинтересованы в следующем:

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

• Статья Хонды и Лорана, в которой показано, как особый вид проверочных сетей, называемый поляризованными проверочными сетями, соответствует процессам с пи-исчислением и который упоминается выше Мартином Бергером: точное соответствие между типизированным пи-исчислением и поляризованным доказательством. сети

• (здесь я беззастенчиво рекламирую свою собственную работу) Проект: доказательство сетей в алгебраической форме процесса

Есть также некоторые работы, касающиеся сетей доказательства и лямбда-исчисления, которые также дают существенную интуицию. Например, следующие работы Делии Кеснер и Стефана Ленгранда:

• Операторы ресурсов для λ-исчисления

Вас также может заинтересовать этот тип работы (очень ориентированный на теоретические аспекты), который опирается на Proof Structures для подробного доказательства свойства сильной нормализации LL, выполненного Микеле Пагани и Лоренцо Тортора де Фалько.

• Свойство сильной нормализации для линейной логики второго порядка (эта статья содержит красивую карту важных теорем).

Вообще, какие теоремы нужно изучать? Ну, я вряд ли авторитет, но вы, возможно, захотите взглянуть на «секвенизацию» (относящуюся к сетям доказательства и последовательным проверкам; см. Оригинальную статью TCS о LL) и сильное доказательство нормализации (скорее, как и ожидалось, но многие важные Теоремы ПН связаны с этим [или используются для доказательства]).

Если вы знакомы с фокусировкой, вам может быть интересна эта статья Андреоли:

• Фокусирующие и проверочные сети в линейной и некоммутативной логике

Надеюсь это поможет. Опять же, эти ссылки действительно не являются исчерпывающими.

лучший, димитрис

Недавно была интересная работа по уточнению связи между сеткой доказательств и сфокусированными исчислениями, использованием «многоцелевых» вариантов, в которых может быть несколько левых отверстий одновременно, и изучением «максимально сфокусированных» доказательств. Если вы выберете правильное исчисление, максимально сфокусированные доказательства могут соответствовать сеткам доказательства MLL или, в классической логике, доказательствам расширения ( Изоморфизм между доказательствами расширения и мультифокусными последовательными доказательствами , Каустув Чаудхури, Стефан Хецль и Дейл Миллер, 2013)

Вы можете проверить мою статью « Обзор сетей доказательств и матриц для субструктурной логики» ".

Аннотация:

Эта статья представляет собой обзор двух видов «сжатых» схем доказательства, \ emph {matrix method} и \ emph {proof nets}, применительно к различным логикам, начиная от иерархии субструктур от классической вплоть до неассоциативная система Ламбека. Для последних предоставлен новый способ обработки проверочных сетей. Описания сетей доказательств и матриц приведены в единой записи на основе секвенций, так что свойства схем для различных логик можно легко сравнить.