Logica liniară

Logica liniară ( logica liniară engleză este o logică substructurală, propus de Jean -Yves Girard ca o rafinare a logicii clasice și intuiționiste , combinând dualitatea primei cu multe proprietăți constructive ale celei din urmă [1] , introdus și folosit pentru raționamentul logic care ține cont de consumul unei anumite resurse [2] ] . Deși logica a fost, de asemenea, studiată în sine, ideile logicii liniare își găsesc aplicații într-o varietate de aplicații mari consumatoare de resurse, inclusiv verificarea protocolului de rețea , limbaje de programare , teoria jocurilor ( semantica jocului ) [2] și fizica cuantică (pentru că logica liniară poate fi considerată ca logica teoriei informației cuantice ) [3] , lingvistică [4] .

Descriere

Sintaxă

Limbajul logicii liniare clasice ( logica liniară clasică engleză , CLL ) poate fi descris în forma Backus-Naur :

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

Unde

p și p ⊥ sunt formule atomice ,

conective logice și constante:

Simbol	Sens
⊗	conjuncție multiplicativă („tensor”, ing. „tensor” )
⊕	disjuncție aditivă
&	conjuncție aditivă
⅋	disjuncție multiplicativă ("par", engleză "par" )
!	modalitate " desigur "
?	modalitatea "de ce nu "
unu	unitate pentru ⊗
0	zero pentru ⊕
⊤	nul pentru &
⊥	unitate pentru ⅋

Conectivele binare ⊗, ⊕, & și ⅋ sunt asociative și comutative .

Fiecare afirmație A din logica liniară clasică are un dual A ⊥ definit după cum urmează:

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

Interpretare semnificativă

În logica liniară (spre deosebire de logica clasică), premisele sunt adesea tratate ca resurse consumabile , astfel încât formula derivată sau inițială poate fi limitată în numărul de utilizări.

Conjuncția multiplicativă ⊗ este similară operației de adunare multimulți și poate exprima uniunea resurselor.

Rețineți că (.) ⊥ este o involuție , adică A ⊥⊥ = A pentru toate afirmațiile. A ⊥ se mai numește și negația liniară a lui A .

Implicația liniară joacă un rol important în logica liniară, deși nu este inclusă în gramatica conjunctivă. Poate fi exprimat în termeni de negație liniară și disjuncție multiplicativă

A ⊸ B := A ⊥ ⅋ B .

Ligamentul ⊸ este uneori numit „acadea” ( ing. acadea ) din cauza formei sale caracteristice.

O implicație liniară poate fi utilizată în ieșire atunci când există resurse pe partea stângă, iar rezultatul sunt resursele din implicația liniară dreaptă. Această transformare definește o funcție liniară , care a dat naștere termenului de „logică liniară” [5] .

Modalitatea „desigur” (!) vă permite să desemnați o resursă ca fiind inepuizabilă.

Exemplu. Fie D un dolar și C o baton de ciocolată. Apoi achiziționarea unui baton de ciocolată poate fi notat cu D ⊸ C . Achiziția poate fi exprimată astfel: D ⊗ !( D ⊸ C ) ⊢ C⊗!( D ⊸ C ) , adică dolarul și capacitatea de a cumpăra o baton de ciocolată cu el duc la o baton de ciocolată, iar oportunitatea de a cumpăra un baton de ciocolată rămâne [5] .

Spre deosebire de logica clasică și intuiționistă , logica liniară are două tipuri de conjuncții, ceea ce permite limitarea resurselor să fie exprimată. Să adăugăm la exemplul anterior posibilitatea de a cumpăra o acadea L. Posibilitatea de a cumpăra o ciocolată sau o acadea poate fi exprimată folosind o conjuncție aditivă [6] :

D ⊸ L & C

Desigur, puteți alege doar unul. O conjuncție multiplicativă denotă prezența ambelor resurse. Deci, pentru doi dolari puteți cumpăra atât un baton de ciocolată, cât și o acadea:

D ⊗ D ⊸ L ⊗ C

Disjuncția multiplicativă A ⅋ B poate fi înțeleasă ca „dacă nu A, atunci B”, iar implicația liniară A ⊸ B exprimată prin ea are semnificația „B poate fi dedus din A exact o dată?” [6]

Disjuncția aditivă A ⊕ B denotă posibilitatea atât a lui A cât și a lui B, dar alegerea nu este a ta [6] . De exemplu, o loterie câștig-câștig în care puteți câștiga o acadea sau un baton de ciocolată poate fi exprimată folosind disjuncția aditivă:

D ⊸ L ⊕ C

Fragmente

Pe lângă logica liniară completă, fragmentele sale sunt folosite [7] :

LL: toate linkurile sunt permise
MLL: numai multiplicative (⊗, ⅋)
MALL: numai multiplicative și aditivi (⊗, ⅋, ⊕, &)
MELL: numai multiplicative și exponențiale (⊗, ⅋, !, ?)

Desigur, această listă nu epuizează toate fragmentele posibile. De exemplu, există diverse fragmente Horn care folosesc implicația liniară (similar cu clauzele Horn ) în combinație cu diverse conjunctive. [opt]

Fragmente de logică sunt de interes pentru cercetători în ceea ce privește complexitatea interpretării lor computaționale. În special, M.I. Kanovich a demonstrat că un fragment MLL complet este NP-complet și un fragment ⊕-Horn al unei logici liniare cu o regulă de slăbire( regulă de slăbire engleză ) PSPACE-full . Acest lucru poate fi interpretat ca însemnând că gestionarea utilizării resurselor este o sarcină dificilă, chiar și în cele mai simple cazuri. [opt]

Reprezentarea ca un calcul secvent

O modalitate de a defini logica liniară este calculul secvenţial . Literele Γ și ∆ reprezintă liste de propoziții și sunt numite contexte . Într-o secvență, contextul este plasat la stânga și la dreapta lui ⊢ ("ar trebui"), de exemplu: . Mai jos este calculul succesiv pentru MLL în format bidirecțional [7] . $A_{1},...,A_{n}$ $\Gamma \vdash \Delta$

Regulă structurală – permutare. Regulile de inferență din stânga și din dreapta sunt date, respectiv:

${\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}}$

Identitate și secțiune :

${\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{Cut))$

Conjuncția multiplicativă:

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

Disjuncția multiplicativă:

${\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}}$

Negare:

${\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}}$

Reguli similare pot fi definite pentru logica liniară completă, aditivii și exponențialele acesteia. Rețineți că regulile structurale de slăbire și reducere nu au fost adăugate la logica liniară , deoarece, în cazul general, enunțurile (și copiile lor) nu pot apărea și dispărea aleatoriu în secvențe, așa cum este obișnuit în logica clasică.

Note

↑ Girard, Jean-Yves (1987). „Logica liniară” (PDF) . Informatica teoretica . 50 (1): 1-102. DOI : 10.1016/0304-3975(87)90045-4 . HDL : 10338.dmlcz/120513 . Arhivat (PDF) din original pe 2021-05-06 . Preluat 2021-03-24 . Parametrul depreciat folosit |deadlink=( ajutor )
↑ 1 2 Întrebări algoritmice de algebră și logică / CARTEA DE PROIECT SUSȚINUTĂ DE FUNDAȚIA RUSĂ DE ȘTIINȚĂ. Preluat: 18.07.2021 . Preluat la 18 iulie 2021. Arhivat din original la 18 iulie 2021. (nedefinit)
↑ Baez, Ioan ; Stai, Mike (2008). Bob Coecke , ed. „Fizică, topologie, logică și calcul: o piatră Rosetta” (PDF) . Structuri noi ale fizicii . Arhivat din original pe 22.03.2021 . Preluat 2021-03-24 . Parametrul depreciat folosit |deadlink=( ajutor )
↑ de Paiva, V. Dagstuhl Seminar 99341 on Linear Logic and Applications / V. de Paiva, J. van Genabith, E. Ritter. — 1999. Arhivat 22 noiembrie 2020 la Wayback Machine
↑ 1 2 Lomazova, 2004 .
↑ 1 2 3 Lincoln, 1992 .
↑ 12 Beffara , 2013 .
↑ 1 2 Max I. Kanovich. Complexitatea fragmentelor Horn ale logicii liniare. Analele logicii pure și aplicate 69 (1994) 195-241

Literatură

Lomazova I. A. 6.5. Rețele Petri imbricate și logica liniară // Rețele Petri imbricate: modelarea și analiza sistemelor distribuite cu o structură de obiect. - M . : Lumea științifică, 2004. - S. 175-185. — 208 p. - ISBN 5-89176-247-1 .
Patrick Lincoln. Logica liniară // ACM SIGACT News. - 1992. - V. 23, nr 2 (mai).
Emmanuel Befarara. Introducere în logica liniară (2013). (nedefinit)

Link -uri

Logica liniară , Stanford Encyclopedia of Philosophy

Logici

Filosofie • Semantică • Sintaxă • Istorie

Grupuri logice

logica clasica	logica aristotelică Logica propozițională Logica de ordinul întâi Logica de ordinul doi logica de ordin superior
logica matematica	teoria multimilor Teoria modelului Teoria computabilității Teoria dovezilor și matematică constructivă Logica liniară sistem formal concluzie firească Calcul de secvență Algebra logicii Logica relevanta Logica deontică logica intuiționistă calculul Lambek
Logica non-clasică	intuitionism logica fuzzy Logica substructurala logica Logica descrierii Logica cu mai multe valori Sinteza logica Logica obligatorie Logica temporală Logica modală ( logica hibridă ) logica epistemică
Logica filozofică	Gândire critică logica informala motiv dedus

Componente

Lista simbolurilor booleene