Lineær logik

Lineær logik ( engelsk Linear Logic er en substrukturel logik, foreslået af Jean -Yves Girard som en forfining af klassisk og intuitionistisk logik , der kombinerer førstnævntes dualitet med mange konstruktive egenskaber ved sidstnævnte [1] , introduceret og brugt til logisk ræsonnement, der tager højde for forbruget af en eller anden ressource [2] ] . Selvom logik også er blevet undersøgt i sig selv, finder ideerne om lineær logik applikationer i en række ressourcekrævende applikationer, herunder netværksprotokolverifikation , programmeringssprog , spilteori ( spilsemantik ) [ 2] og kvantefysik (fordi lineær logik kan betragtes som kvanteinformationsteoriens logik ) [3] , lingvistik [4] .

Beskrivelse

Syntaks

Sproget i klassisk lineær logik ( engelsk klassisk lineær logik, CLL ) kan beskrives i Backus-Naur-formen :

A ::= p ∣ p ⊥ | A ⊗ A ∣ A ⊕ A | A & A ∣ A ⅋ A | 1 ∣ 0 ∣ ⊤ ∣ ⊥ | ! A∣ ? EN

Hvor

p og p ⊥ er atomformler ,

logiske forbindelser og konstanter:

Symbol	Betyder
⊗	multiplikativ konjunktion ("tensor", eng. "tensor" )
⊕	additiv disjunktion
&	additiv konjunktion
⅋	multiplikativ disjunktion ("par", engelsk "par" )
!	modalitet " selvfølgelig "
?	modalitet " hvorfor ikke "
en	enhed for ⊗
0	nul for ⊕
⊤	null for &
⊥	enhed til ⅋

De binære bindeled ⊗, ⊕, & og ⅋ er associative og kommutative .

Hvert udsagn A i klassisk lineær logik har en dobbelt A ⊥ defineret som følger:

( p ) ⊥ = p ⊥			( p ⊥ ) ⊥ = s
( A ⊗ B ) ⊥ = A ⊥ ⅋ B ⊥			( A ⅋ B ) ⊥ = A ⊥ ⊗ B ⊥
( A ⊕ B ) ⊥ = A ⊥ & B ⊥			( A & B ) ⊥ = A ⊥ ⊕ B ⊥
(1) ⊥ = ⊥			(⊥) ⊥ = 1
(0) ⊥ = ⊤			(⊤) ⊥ = 0
(! A ) ⊥ = ?( A ⊥ )			(? A ) ⊥ = !( A ⊥ )

Meningsfuld fortolkning

I lineær logik (i modsætning til klassisk logik) behandles lokalerne ofte som forbrugsressourcer , så den afledte eller indledende formel kan begrænses i antallet af anvendelser.

Den multiplikative konjunktion ⊗ ligner multisæt additionsoperationen og kan udtrykke foreningen af ressourcer.

Bemærk at (.) ⊥ er en involution , det vil sige A ⊥⊥ = A for alle udsagn. A ⊥ kaldes også den lineære negation af A .

Lineær implikation spiller en stor rolle i lineær logik, selvom den ikke er inkluderet i den bindende grammatik. Kan udtrykkes i form af lineær negation og multiplikativ disjunktion

A ⊸ B := A ⊥ ⅋ B .

Ledbåndet ⊸ kaldes undertiden "slikkepind" ( eng. slikkepind ) på grund af dets karakteristiske form.

En lineær implikation kan bruges i output, når der er ressourcer på dens venstre side, og resultatet er ressourcerne fra den højre lineære implikation. Denne transformation definerer en lineær funktion , som gav anledning til udtrykket "Lineær logik" [5] .

Modaliteten "selvfølgelig" (!) giver dig mulighed for at udpege en ressource som uudtømmelig.

Eksempel. Lad D være en dollar og C være en chokoladebar. Så kan køb af en chokoladebar betegnes som D ⊸ C . Købet kan udtrykkes således: D ⊗ !( D ⊸ C ) ⊢ C⊗!( D ⊸ C ) , det vil sige, at dollaren og muligheden for at købe en chokoladebar med den fører til en chokoladebar, og mulighed for at købe en chokoladebar er tilbage [5] .

I modsætning til klassisk og intuitionistisk logik har lineær logik to slags konjunktioner, som tillader begrænsningen af ressourcer at blive udtrykt. Lad os tilføje til det foregående eksempel muligheden for at købe en slikkepind L. Muligheden for at købe en chokoladebar eller en slikkepind kan udtrykkes ved hjælp af en additiv konjunktion [6] :

D ⊸ L & C

Du kan selvfølgelig kun vælge én. En multiplikativ konjunktion angiver tilstedeværelsen af begge ressourcer. Så for to dollars kan du købe både en chokoladebar og en slikkepind:

D ⊗ D ⊸ L ⊗ C

Den multiplikative disjunktion A ⅋ B kan forstås som "hvis ikke A, så B", og den lineære implikation A ⊸ B udtrykt gennem den har betydningen "kan B udledes fra A nøjagtigt én gang?" [6]

Den additive disjunktion A ⊕ B betegner muligheden for både A og B, men valget er ikke dit [6] . For eksempel kan et win-win lotteri, hvor du kan vinde en slikkepind eller en chokoladebar, udtrykkes ved hjælp af additiv disjunktion:

D ⊸ L ⊕ C

Fragmenter

Ud over fuld lineær logik bruges dens fragmenter [7] :

LL: alle links er tilladt
MLL: kun multiplikativer (⊗, ⅋)
MALL: kun multiplikativer og additiver (⊗, ⅋, ⊕, &)
MELL: kun multiplikativer og eksponentialer (⊗, ⅋, !, ?)

Selvfølgelig udtømmer denne liste ikke alle mulige fragmenter. For eksempel er der forskellige Horn-fragmenter, der bruger lineær implikation (svarende til Horn-sætninger ) i kombination med forskellige bindeled. [otte]

Fragmenter af logik er af interesse for forskere med hensyn til kompleksiteten af deres beregningsfortolkning. Især M.I. Kanovich beviste, at et komplet MLL-fragment er NP-komplet , og et ⊕-Horn-fragment af en lineær logik med en svækkelsesregel( Engelsk svækkelsesregel ) PSPACE-fuld . Dette kan tolkes til at betyde, at styring af ressourceforbrug er en vanskelig opgave, selv i de mest simple tilfælde. [otte]

Repræsentation som en sekventiel beregning

En måde at definere lineær logik på er sekventeregningen . Bogstaverne Γ og ∆ står for sætningslister og kaldes sammenhænge . I en sekvens placeres konteksten til venstre og højre for ⊢ ("bør"), for eksempel: . Nedenfor er den sekvente beregning for MLL i to-vejs format [7] . $A_{1},...,A_{n}$ $\Gamma \vdash \Delta$

Strukturel regel - permutation. Venstre og højre inferensregler er givet henholdsvis:

${\cfrac {\Gamma ,A,B,\Gamma '\vdash \Delta }{\Gamma ,B,A,\Gamma '\vdash \Delta ))\;{\text{exL))\qquad {\cfrac {\Gamma \vdash \Delta ,A,B,\Delta '}{\Gamma \vdash \Delta ,B,A,\Delta '}}\;{\text{exR}}$

Identitet og sektion :

${\cfrac {\cdot }{A\vdash A}}\;{\text{I}}\qquad {\cfrac {\Gamma \vdash \Sigma ,A,\Delta \qquad \Gamma ',A ,\Sigma '\vdash \Delta '}{\Gamma ,\Gamma ',\Sigma '\vdash \Sigma ,\Delta ,\Delta '))\;{\text{Klip))$

Multiplikativ konjunktion:

${\cfrac {\Gamma ,A,B\vdash \Delta }{\Gamma ,A\otimes B\vdash \Delta ))\;\nogle gange {\text{L))\qquad {\cfrac {\ Gamma \vdash A,\Delta \qquad \Gamma '\vdash B,\Delta '}{\Gamma ,\Gamma '\vdash A\otimes B,\Delta ,\Delta '))\;\nogle gange {\tekst{ R}}$

Multiplikativ disjunktion:

${\cfrac {\Gamma ,A\vdash \Delta \qquad \Gamma ',B\vdash \Delta '}{\Gamma ,\Gamma ',A{\text{⅋))B\vdash \Delta , \Delta '}}\;{\text{⅋L}}\qquad {\cfrac {\Gamma \vdash A,B,\Delta }{\Gamma \vdash A{\text{⅋}}B,\Delta } }\;{\text{⅋R}}$

Negation:

${\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,A^{\bot }\vdash \Delta }}\;\bot {\text{L}}\qquad {\cfrac {\ Gamma ,A\vdash \Delta }{\Gamma \vdash A^{\bot },\Delta }}\;\bot {\text{R}}$

Lignende regler kan defineres for komplet lineær logik, dens additiver og eksponentialer. Bemærk, at strukturelle regler for svækkelse og reduktion ikke er blevet tilføjet til lineær logik , da udsagn (og deres kopier) i det generelle tilfælde ikke kan optræde og forsvinde tilfældigt i sekvenser, som det er sædvanligt i klassisk logik.

Noter

↑ Girard, Jean-Yves (1987). "Lineær logik" (PDF) . Teoretisk datalogi . 50 (1): 1-102. DOI : 10.1016/0304-3975(87)90045-4 . HDL : 10338.dmlcz/120513 . Arkiveret (PDF) fra originalen 2021-05-06 . Hentet 2021-03-24 . Forældet parameter brugt |deadlink=( hjælp )
↑ 1 2 Algoritmiske spørgsmål om algebra og logik / PROJEKTKORT STØTTET AF RUSSIAN SCIENCE FOUNDATION. Hentet: 18/07/2021 . Hentet 18. juli 2021. Arkiveret fra originalen 18. juli 2021. (ubestemt)
↑ Baez, John ; Bliv, Mike (2008). Bob Coecke , red. "Fysik, topologi, logik og beregning: En Rosetta-sten" (PDF) . Fysikkens nye strukturer . Arkiveret fra originalen 2021-03-22 . Hentet 2021-03-24 . Forældet parameter brugt |deadlink=( hjælp )
↑ de Paiva, V. Dagstuhl Seminar 99341 om lineær logik og applikationer / V. de Paiva, J. van Genabit, E. Ritter. — 1999. Arkiveret 22. november 2020 på Wayback Machine
↑ 1 2 Lomazova, 2004 .
↑ 1 2 3 Lincoln, 1992 .
↑ 12 Beffara , 2013 .
↑ 1 2 Max I. Kanovich. Kompleksiteten af hornfragmenter af lineær logik. Annals of Pure and Applied Logic 69 (1994) 195-241

Litteratur

Lomazova I. A. 6.5. Nestede petri-net og lineær logik // Nestede petri-net: modellering og analyse af distribuerede systemer med en objektstruktur. - M . : Scientific world, 2004. - S. 175-185. — 208 s. - ISBN 5-89176-247-1 .
Patrick Lincoln. Lineær logik // ACM SIGACT News. - 1992. - V. 23, nr. 2 (maj).
Emmanuel Befarara. Introduktion til lineær logik (2013). (ubestemt)

Links

Linear Logic , Stanford Encyclopedia of Philosophy

Logik

Filosofi • Semantik • Syntaks • Historie

Logiske grupper

klassisk logik	Aristotelisk logik propositionel logik Første ordens logik Anden ordens logik højere ordens logik
matematisk logik	mængdeteori Modelteori Beregnelighedsteori Bevisteori og konstruktiv matematik Lineær logik formelt system naturlig konklusion Sekvensberegning Algebra af logik Relevant logik Deontisk logik intuitionistisk logik Lambek regning
Ikke-klassisk logik	intuitionisme sløret logik Substrukturel logik logik Beskrivelseslogik Flerværdilogik Logisk syntese Bindende logik Tidsmæssig logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritisk tænkning uformel logik deduktiv ræsonnement

Komponenter

Bortførelse (logik)
Sandsynlighed
udmelding
Fradrag / Induktion / Traduktion
Virkelighed
Induktiv begrundelse
slutning
boolsk konstant
Rigtigt
logisk følge
Logisk form
Nødvendige og tilstrækkelige betingelser
Beskrivelse
Definition
Substitution
Pakke
Kontrovers ( Antinomy )
Syntetisk dømmekraft / Analytisk dømmekraft
Link

Liste over booleske symboler