Logika nieprzemienna

Logika nieprzemienna jest rozszerzeniem logiki liniowej , które łączy spójniki przemienne logiki liniowej z nieprzemiennymi spójnikami multiplikatywnymi rachunku Lambeka . Jego rachunek sekwencyjny opiera się na strukturze rozmaitości rzędów (rodzina rzędów cyklicznych , które można postrzegać jako rodzaj struktury ), a kryterium poprawności jego siatek dowodowych jest podane w postaci częściowych permutacji . Posiada również semantyka denotacyjna , w której formuły są interpretowane przez moduły w oparciu o określone algebry Hopfa .

Nieprzemienność w logice

Co za tym idzie, termin logika nieprzemienna jest również używany przez wielu autorów w odniesieniu do rodziny logik podstrukturalnych , w których reguła wymiany jest niedopuszczalna . Dalsza część artykułu poświęcona jest prezentacji tej akceptacji tego terminu.

Najstarszą logiką nieprzemienną jest rachunek Lambeka , który dał początek klasie logik zwanej gramatyką kategorialną . Od czasu opublikowania logiki liniowej Jeana-Yvesa Girarda zaproponowano kilka nowych logik nieprzemiennych, a mianowicie cykliczną logikę liniową Davida Yettera, logikę pomset Christiana Retoré oraz nieprzemienne logiki BV i NEL .

Logika nieprzemienna jest czasami nazywana logiką uporządkowaną, ponieważ w większości proponowanych logik nieprzemiennych możliwe jest narzucenie całkowitego lub częściowego porządku formułom w sekwencjach. Jednak nie jest to w pełni ogólne, ponieważ niektóre nieprzemienne logiki nie obsługują takiego porządku, na przykład cykliczna logika liniowa Yettera. Chociaż większość logik nieprzemiennych nie dopuszcza osłabienia lub skrócenia wraz z nieprzemiennością, to ograniczenie nie jest konieczne.

Rachunek Lambeka

Główny artykuł: gramatyka kategorialna

Joachim Lambek zaproponował pierwszą logikę nieprzemienną w swoim artykule Mathematics of Sentence Structure z 1958 roku , aby modelować kombinatoryczne możliwości składni języków naturalnych . Jego rachunek różniczkowy stał się w ten sposób jednym z podstawowych formalizmów lingwistyki komputerowej .

Cykliczna logika liniowa

David N. Yetter zaproponował słabszą regułę strukturalną zamiast reguły wymiany logiki liniowej, uzyskując cykliczną logikę liniową. Sekwencje cyklicznej logiki liniowej tworzą pierścień, a więc są niezmienne podczas rotacji, gdzie reguły wieloprzesłankowe sklejają swoje pierścienie według wzorów opisanych w regułach. Rachunek obsługuje trzy modalności strukturalne, samodualną modalność umożliwiającą wymianę, ale nadal liniową, oraz zwykłe wykładniki (? i!) Logiki liniowej, umożliwiające stosowanie nieliniowych reguł strukturalnych wraz z wymianą.

Logika Pomseta

Logika Pomseta została zaproponowana przez Christiana Retoré w formalizmie semantycznym z dwoma podwójnymi operatorami sekwencyjnymi istniejącymi razem ze zwykłym iloczynem tensorowym i operatorami par logiki liniowej, pierwsza logika, w której zaproponowano posiadanie zarówno operatorów przemiennych, jak i nieprzemiennych. Podano rachunek sekwencyjny dla logiki, ale brakowało w nim twierdzenia o eliminacji cięcia ; zamiast tego sens rachunku różniczkowego został ustalony za pomocą semantyki denotacyjnej.

BV i NEL

Alessio Guglielmi zaproponował odmianę rachunku różniczkowego Retoré, BV, w której dwie nieprzemienne operacje są sprowadzone do jednego, samodualnego operatora, i zaproponował nowatorski rachunek dowodowy, rachunek struktur do uwzględnienia rachunku różniczkowego . Główną nowością rachunku struktur było jego wszechobecne stosowanie głębokiego wnioskowania , które, jak argumentowano, jest konieczne w przypadku rachunków łączących operatory przemienne i nieprzemienne; to wyjaśnienie jest zgodne z trudnością projektowania systemów sekwencyjnych dla logiki pomset, które mają eliminację odcięcia.

Lutz Straßburger opracował pokrewny system, NEL, również w rachunku struktur, w którym logika liniowa z regułą mieszania pojawia się jako podsystem.

Struktady

Struktady to podejście do semantyki logiki, które opiera się na uogólnieniu pojęcia sekwencji na wzór gatunków kombinatorycznych Joyala , umożliwiając traktowanie bardziej drastycznie niestandardowych logik niż te opisane powyżej, gdzie na przykład „,” rachunku sekwencyjnego nie jest asocjacyjna .

Zobacz też

• System typów uporządkowanych , system typów podstrukturalnych
• Logika kwantowa

Linki zewnętrzne

1. Logika nieprzemienna I: fragment multiplikatywny autorstwa V. Michele Abrusci i Paula Rueta, Annals of Pure and Applied Logic 101 (1), 2000.
2. Logiczne aspekty lingwistyki komputerowej (PS) autorstwa Patricka Blackburna, Marca Dymetmana, Alaina Lecomte'a, Aarne Ranty, Christiana Retoré i Erica Villemonte de la Clergerie.
3. Artykuły na temat przemiennej / nieprzemiennej logiki liniowej w rachunku struktur : strona internetowa badań, na której dostępne są artykuły proponujące BV i NEL.