Некоммутативная логика - Noncommutative logic

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

Некоммутативность в логике

В более широком смысле термин некоммутативная логика также используется рядом авторов для обозначения семейства субструктурная логика в которой правило обмена является недопустимый. Остальная часть этой статьи посвящена демонстрации принятия этого термина.

Самая старая некоммутативная логика - это Исчисление Ламбека, что дало начало классу логик, известному как категориальные грамматики. С момента публикации Жан-Ив Жирар с линейная логика было предложено несколько новых некоммутативных логик, а именно циклическая линейная логика Дэвида Йеттера, логика pomset Кристиана Реторе и некоммутативных логик BV и NEL.

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

Исчисление Ламбека

Основная статья: категориальная грамматика

Иоахим Ламбек предложил первую некоммутативную логику в своей статье 1958 г. Математика структуры предложения моделировать комбинаторные возможности синтаксиса естественных языков.[1] Таким образом, его исчисление стало одним из фундаментальных формализмов компьютерная лингвистика.

Циклическая линейная логика

Дэвид Н. Йеттер предложил более слабое структурное правило вместо правила обмена линейной логики, что привело к циклической линейной логике.[2] Секвенты циклической линейной логики образуют кольцо и, следовательно, инвариантны относительно вращения, когда правила с несколькими предпосылками склеивают свои кольца вместе по формулам, описанным в правилах. Исчисление поддерживает три структурных модальности: самодвойственную модальность, допускающую обмен, но все еще линейную, и обычные экспоненты (? И!) Линейной логики, позволяющие использовать нелинейные структурные правила вместе с обменом.

Логика Помсета

Логика Помсета была предложена Кристианом Реторе в семантическом формализме с двумя двойственными последовательными операторами, существующими вместе с обычным тензорным произведением и операторами par линейной логики, первая логика предлагала иметь как коммутативные, так и некоммутативные операторы.[3] Было дано последовательное исчисление логики, но в нем не было теорема исключения сечения; вместо этого смысл исчисления был установлен через денотационную семантику.

BV и NEL

Алессио Гульельми предложил вариант исчисления Реторе, BV, в котором две некоммутативные операции сворачиваются в один, самодвойственный оператор, и предложил новое исчисление доказательств, расчет конструкций для размещения исчисления. Основным новшеством исчисления структур было повсеместное использование глубокий вывод, что, как утверждалось, необходимо для исчислений, сочетающих коммутативные и некоммутативные операторы; это объяснение согласуется с трудностью разработки последовательных систем для логики pomset, у которых есть отсечение-исключение.

Лутц Страсбургер разработал родственную систему, NEL, также в исчислении структур, в которой линейная логика с правилом смешивания выступает в качестве подсистемы.

Structads

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

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

использованная литература

  1. ^ Ламбек, Иоахим (1958). «Математика структуры предложения». Американский математический ежемесячник. 65 (3): 154–170. CiteSeerX  10.1.1.538.885. Дои:10.2307/2310058. ISSN  0002-9890. JSTOR  2310058.
  2. ^ Йеттер, Дэвид Н. (1990). «Кванталы и (некоммутативная) линейная логика» (PDF). Журнал символической логики. 55 (1): 41–64. Дои:10.2307/2274953. HDL:10338.dmlcz / 140417. ISSN  0022-4812. JSTOR  2274953.
  3. ^ Реторе, Кристиан (1997-04-02). «Логика Помсета: некоммутативное расширение классической линейной логики». У Филиппа де Гроота; Дж. Роджер Хиндли (ред.). Типизированные лямбда-исчисления и приложения. Конспект лекций по информатике. 1210. Springer Berlin Heidelberg. С. 300–318. CiteSeerX  10.1.1.47.2354. Дои:10.1007/3-540-62688-3_43. ISBN  978-3-540-62688-6.

внешние ссылки

  1. Некоммутативная логика I: мультипликативный фрагмент Авторы: В. Мишель Абруски и Поль Руэт, Анналы чистой и прикладной логики 101 (1), 2000.
  2. Логические аспекты компьютерной лингвистики (ПК) Патрик Блэкберн, Марк Дайметман, Ален Леконт, Аарне Ранта, Кристиан Реторе и Эрик Вильемонте де ла Клержери.
  3. Статьи по коммутативной / некоммутативной линейной логике в исчислении структур: домашняя страница исследования, на которой доступны статьи, предлагающие BV и NEL.