Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

Некоммутативность в логике [ править ]

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

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

Внешние ссылки [ править ]

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