Icke-kommutativ logik
Icke-kommutativ logik är en förlängning av linjär logik som kombinerar de kommutativa konnektiviteten för linjär logik med de icke-kommutativa multiplikativa konnektiven i Lambek-kalkylen . Dess efterföljande kalkyl förlitar sig på strukturen av ordningsvariationer (en familj av cykliska ordningar som kan ses som en art av struktur ), och korrekthetskriteriet för dess bevisnät ges i termer av partiella permutationer . Den har också en denotationssemantik där formler tolkas av moduler över vissa specifika Hopf-algebror .
Icke-kommutativitet i logik
I förlängningen används termen icke-kommutativ logik också av ett antal författare för att hänvisa till en familj av substrukturella logiker där utbytesregeln är otillåten . Resten av denna artikel ägnas åt en presentation av denna acceptans av termen.
Den äldsta icke-kommutativa logiken är Lambek-kalkylen , som gav upphov till den klass av logik som kallas kategoriserad grammatik . Sedan publiceringen av Jean-Yves Girards linjära logik har det föreslagits flera nya icke-kommutativa logiker, nämligen David Yetters cykliska linjära logik, Christian Retorés pomsetlogik och de icke-kommutativa logiken BV och NEL .
Icke-kommutativ logik kallas ibland för ordnad logik, eftersom det är möjligt med de flesta föreslagna icke-kommutativa logiker att införa en total eller partiell ordning på formlerna i sekvenser. Detta är dock inte helt generellt eftersom vissa icke-kommutativa logiker inte stöder en sådan ordning, såsom Yetters cykliska linjära logik. Även om de flesta icke-kommutativa logiker inte tillåter försvagning eller sammandragning tillsammans med icke-kommutativitet, är denna begränsning inte nödvändig.
Lambek-kalkylen
Joachim Lambek föreslog den första icke-kommutativa logiken i sin 1958 uppsats Mathematics of Sentence Structure för att modellera de kombinatoriska möjligheterna för syntaxen för naturliga språk . Hans kalkyl har därmed blivit en av beräkningslingvistikens grundläggande formalismer .
Cyklisk linjär logik
David N. Yetter föreslog en svagare strukturell regel i stället för utbytesregeln för linjär logik, vilket gav cyklisk linjär logik. Sekvenser av cyklisk linjär logik bildar en ring och är därför invarianta under rotation, där regler med flera utgångspunkter limmar ihop sina ringar enligt formlerna som beskrivs i reglerna. Kalkylen stöder tre strukturella modaliteter, en självdubbel modalitet som tillåter utbyte, men fortfarande linjär, och de vanliga exponentialerna (? och !) av linjär logik, vilket gör att olinjära strukturella regler kan användas tillsammans med utbyte.
Pomset logik
Pomset-logik föreslogs av Christian Retoré i en semantisk formalism med två dubbla sekventiella operatorer som existerade tillsammans med den vanliga tensorprodukten och par-operatorerna för linjär logik, den första logiken föreslog att ha både kommutativa och icke-kommutativa operatorer. En sekventiell kalkyl för logiken gavs, men den saknade en cut-elimineringssats ; i stället etablerades kalkylens mening genom en denotationssemantik.
BV och NEL
Alessio Guglielmi föreslog en variant av Retorés kalkyl, BV, där de två icke-kommutativa operationerna kollapsas till en enda, självdual, operator, och föreslog en ny beviskalkyl, kalkylen av strukturer för att anpassa kalkylen . Den huvudsakliga nyheten i kalkylen av strukturer var dess genomgripande användning av djup inferens , som det hävdades är nödvändigt för kalkyler som kombinerar kommutativa och icke-kommutativa operatorer; denna förklaring överensstämmer med svårigheten att designa sekventiella system för pomset-logik som har cut-eliminering.
Lutz Straßburger utformade ett relaterat system, NEL, också i beräkningen av strukturer där linjär logik med mixregeln uppträder som ett delsystem.
Structads
generalisera begreppet sekvent i linje med Joyals kombinatoriska arter , vilket tillåter behandling av mer drastiskt icke-standardiserade logiker än de som beskrivits ovan, där till exempel "," av den efterföljande kalkylen är inte associativ .
Se även
externa länkar
- Icke-kommutativ logik I: det multiplikativa fragmentet av V. Michele Abrusci och Paul Ruet, Annals of Pure and Applied Logic 101(1), 2000.
- Logiska aspekter av beräkningslingvistik (PS) av Patrick Blackburn, Marc Dymetman, Alain Lecomte, Aarne Ranta, Christian Retoré och Eric Villemonte de la Clergerie.
- Artikel om kommutativ/icke-kommutativ linjär logik i strukturkalkylen : en forskningshemsida från vilken artiklarna som föreslår BV och NEL är tillgängliga.