Некоммутативная логика
Некоммутативная логика — это расширение линейной логики , которое сочетает в себе коммутативные связки линейной логики с некоммутативными мультипликативными связками исчисления Ламбека . Его секвенционное исчисление опирается на структуру многообразий порядков (семейство циклических порядков , которое можно рассматривать как разновидность структуры ), а критерий правильности его сетей доказательств дается в терминах частичных перестановок . Он также имеет денотационную семантику , в которой формулы интерпретируются модулями над некоторыми конкретными алгебрами Хопфа .
Некоммутативность в логике
[ редактировать ]В более широком смысле термин «некоммутативная логика» также используется рядом авторов для обозначения семейства субструктурных логик в которых правило обмена недопустимо , . Оставшаяся часть статьи посвящена изложению принятия этого термина.
Старейшей некоммутативной логикой является исчисление Ламбека , давшее начало классу логик, известному как категориальные грамматики . Со времени публикации Жан-Ива Жирара было линейной логики предложено несколько новых некоммутативных логик, а именно циклическая линейная логика Дэвида Йеттера, логика помсетов Кристиана Реторе и некоммутативные логики BV и NEL .
Некоммутативную логику иногда называют упорядоченной логикой, поскольку в большинстве предлагаемых некоммутативных логик можно наложить полный или частичный порядок на формулы в секвенциях. Однако это не является полностью общим, поскольку некоторые некоммутативные логики не поддерживают такой порядок, например циклическая линейная логика Йеттера. Хотя большинство некоммутативных логик не допускают ослабления или сжатия вместе с некоммутативностью, в этом ограничении нет необходимости.
Исчисление Ламбека
[ редактировать ]Иоахим Ламбек предложил первую некоммутативную логику в своей статье 1958 года «Математика структуры предложений» для моделирования комбинаторных возможностей синтаксиса естественных языков . [1] Таким образом, его исчисление стало одним из фундаментальных формализмов компьютерной лингвистики .
Циклическая линейная логика
[ редактировать ]Дэвид Н. Йеттер предложил более слабое структурное правило вместо правила обмена линейной логики, что привело к циклической линейной логике. [2] Секвенции циклической линейной логики образуют цикл и поэтому инвариантны относительно вращения, когда правила множественных предпосылок склеивают свои циклы вместе по формулам, описанным в правилах. Исчисление поддерживает три структурные модальности: самодвойственную модальность, допускающую обмен, но все же линейный, и обычные экспоненты (? и !) линейной логики, позволяющие использовать нелинейные структурные правила вместе с обменом.
Логика Pomset
[ редактировать ]Логика Помсетов была предложена Кристианом Реторе в семантическом формализме с двумя двойственными последовательными операторами, существующими вместе с обычным тензорным произведением и паритетными операторами линейной логики. В первой логике было предложено иметь как коммутативные, так и некоммутативные операторы. [3] Было дано секвенциальное исчисление логики, но в нем отсутствовала теорема об исключении разреза ; вместо этого смысл исчисления был установлен посредством денотационной семантики.
БВ и НЭЛ
[ редактировать ]Алессио Гульельми предложил вариант исчисления Реторе, BV, в котором две некоммутативные операции сведены в один самодвойственный оператор, и предложил новое исчисление доказательств - исчисление структур для размещения этого исчисления. Принципиальной новинкой исчисления структур было повсеместное использование глубокого вывода , который, как утверждалось, необходим для исчислений, сочетающих коммутативные и некоммутативные операторы; это объяснение согласуется с трудностью разработки секвенционных систем для логики помсетов, в которых есть исключение отсечения.
Лутц Страсбургер разработал родственную систему NEL также для исчисления структур, в которой линейная логика с правилом смешивания выступает в качестве подсистемы.
Структады
[ редактировать ]Структады — это подход к семантике логики, основанный на обобщении понятия секвенции в соответствии с Джояла комбинаторными видами , позволяющий обрабатывать более радикально нестандартные логики, чем описанные выше, где, например, «,» секвенциального исчисления не является ассоциативным .
См. также
[ редактировать ]Ссылки
[ редактировать ]- ^ Ламбек, Иоахим (1958). «Математика структуры предложения». Американский математический ежемесячник . 65 (3): 154–170. CiteSeerX 10.1.1.538.885 . дои : 10.2307/2310058 . ISSN 0002-9890 . JSTOR 2310058 .
- ^ Йеттер, Дэвид Н. (1990). «Кванталы и (некоммутативная) линейная логика». Журнал символической логики . 55 (1): 41–64. дои : 10.2307/2274953 . hdl : 10338.dmlcz/140417 . ISSN 0022-4812 . JSTOR 2274953 . S2CID 30626492 .
- ^ Реторе, Кристиан (2 апреля 1997 г.). «Логика Pomset: некоммутативное расширение классической линейной логики». У Филиппа де Гроота; Дж. Роджер Хиндли (ред.). Типизированные лямбда-исчисления и приложения . Конспекты лекций по информатике. Том. 1210. Шпрингер Берлин Гейдельберг. стр. 300–318. CiteSeerX 10.1.1.47.2354 . дои : 10.1007/3-540-62688-3_43 . ISBN 978-3-540-62688-6 .
Внешние ссылки
[ редактировать ]- Некоммутативная логика I: мультипликативный фрагмент В. Мишеля Абруски и Поля Рюэ, Annals of Pure and Applied Logic 101 (1), 2000.
- Логические аспекты компьютерной лингвистики Патрика Блэкберна, Марка Дайметмана, Алена Лекомта, Аарна Ранты, Кристиана Реторе и Эрика Вильмонте де ла Клержери.
- Статьи по коммутативной/некоммутативной линейной логике в исчислении структур : домашняя страница исследований, на которой доступны статьи, предлагающие BV и NEL.