Lineaarinen logiikka

Lineaarinen logiikka ( englanniksi Linear Logic on alirakennelogiikka, jonka Jean - Yves Girard ehdotti klassisen ja intuitionistisen logiikan jalostukseksi , joka yhdistää edellisen kaksinaisuuden jälkimmäisen moniin rakentaviin ominaisuuksiin [1] , esiteltiin ja käytetään loogiseen päättelyyn, joka ottaa huomioon jonkin resurssin kulutuksen [2] ] . Vaikka logiikkaa on tutkittu myös sellaisenaan, lineaarisen logiikan ideat löytävät sovelluksia erilaisissa resurssiintensiivisissä sovelluksissa, mukaan lukien verkkoprotokollien verifiointi , ohjelmointikielet , peliteoria ( pelin semantiikka ) [2] ja kvanttifysiikka (koska lineaarista logiikkaa voidaan pitää kvanttiinformaatioteorian logiikkana ) [ 3] , kielitiede [4] .

Kuvaus

Syntaksi

Klassisen lineaarisen logiikan kieli ( englanniksi classic linear logic, CLL ) voidaan kuvata Backus-Naur-muodossa :

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

Missä

p ja p ⊥ ovat atomikaavoja ,

loogiset liitokset ja vakiot:

Symboli	Merkitys
⊗	kertova konjunktio ("tensori", eng. "tensor" )
⊕	additiivinen disjunktio
&	additiivinen konjunktio
⅋	kertova disjunktio ("par", englanniksi "par" )
!	modaalisuus " tietenkin "
?	modaali " miksi ei "
yksi	yksikkö ⊗
0	nolla arvolle ⊕
⊤	tyhjä arvolle &
⊥	yksikkö ⅋

Binäärikonnektiivit ⊗, ⊕, & ja ⅋ ovat assosiatiivisia ja kommutatiivisia .

Jokaisella klassisen lineaarisen logiikan lauseella A on duaali A ⊥ , joka määritellään seuraavasti:

( 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 ⊥ )

Merkittävä tulkinta

Lineaarisessa logiikassa (toisin kuin klassisessa logiikassa) tilat käsitellään usein kulutettavina resursseina , joten johdetun tai alkukaavan käyttökertoja voidaan rajoittaa.

Kertova konjunktio ⊗ on samanlainen kuin multiset yhteenlaskuoperaatio ja voi ilmaista resurssien liiton.

Huomaa, että (.) ⊥ on involuutio , eli A ⊥⊥ = A kaikille lauseille. A ⊥ kutsutaan myös A :n lineaariseksi negaatioksi .

Lineaarisella implikaatiolla on suuri rooli lineaarisessa logiikassa, vaikka se ei sisälly konnektiiviseen kielioppiin. Voidaan ilmaista lineaarisella negaatiolla ja multiplikatiivisella disjunktiolla

A ⊸ B := A ⊥ ⅋ B .

Nivelsitettä ⊸ kutsutaan joskus "tikkariksi" ( eng. lollipop ) sen ominaismuodon vuoksi.

Lineaarista implikaatiota voidaan käyttää tuotoksessa, kun sen vasemmalla puolella on resursseja ja tuloksena on resurssit oikeasta lineaarisesta implikaatiosta. Tämä muunnos määrittelee lineaarifunktion , josta syntyi termi "lineaarinen logiikka" [5] .

Modaliteetti "tietenkin" (!) antaa sinun määrittää resurssin ehtymättömäksi.

Esimerkki. Olkoon D dollari ja C suklaapatukka. Tällöin suklaapatukan ostoa voidaan merkitä D ⊸ C . Osto voidaan ilmaista seuraavasti: D ⊗ !( D ⊸ C ) ⊢ C⊗!( D ⊸ C ) , eli dollari ja mahdollisuus ostaa sen mukana suklaapatukka johtavat suklaapatukkaan, ja mahdollisuus ostaa suklaapatukka jää [5] .

Toisin kuin klassinen ja intuitionistinen logiikka , lineaarisessa logiikassa on kahdenlaisia konjunktioita, jotka mahdollistavat resurssien rajallisuuden ilmaisemisen. Lisätään edelliseen esimerkkiin mahdollisuus ostaa tikkari L. Mahdollisuus ostaa suklaapatukka tai tikkari voidaan ilmaista käyttämällä additiivinen konjunktio [6] :

D ⊸ L & C

Tietysti voit valita vain yhden. Kertova konjunktio tarkoittaa molempien resurssien läsnäoloa. Joten kahdella dollarilla voit ostaa sekä suklaapatukan että tikkarin:

D ⊗ D ⊸ L ⊗ C

Multiplikatiivinen disjunktio A ⅋ B voidaan ymmärtää "jos ei A, niin B", ja sen kautta ilmaistulla lineaarisella implikaatiolla A ⊸ B on merkitys "voidaanko B johtaa A:sta tasan kerran?" [6]

Additiivinen disjunktio A ⊕ B tarkoittaa sekä A:n että B:n mahdollisuutta, mutta valinta ei ole sinun [6] . Esimerkiksi win-win-arpajaiset, joissa voit voittaa tikkarin tai suklaapatukan, voidaan ilmaista käyttämällä additiivista disjunktiota:

D ⊸ L ⊕ C

Fragments

Täyden lineaarisen logiikan lisäksi sen fragmentteja käytetään [7] :

LL: kaikki linkit ovat sallittuja
MLL: vain kertoimet (⊗, ⅋)
MALL: vain kertoimet ja additiivit (⊗, ⅋, ⊕, &)
MELL: vain kertoimet ja eksponentiaalit (⊗, ⅋, !, ?)

Tämä luettelo ei tietenkään tyhjennä kaikkia mahdollisia fragmentteja. Esimerkiksi on olemassa useita Horn-fragmentteja, jotka käyttävät lineaarista implikaatiota (samanlainen kuin Horn-lauseet ) yhdistettynä erilaisten konnektiivien kanssa. [kahdeksan]

Logiikkafragmentit kiinnostavat tutkijoita niiden laskennallisen tulkinnan monimutkaisuuden vuoksi . Erityisesti M.I. Kanovich osoitti, että täydellinen MLL-fragmentti on NP-täydellinen ja lineaarisen logiikan ⊕- sarvifragmentti heikennyssäännöllä( englanniksi heikennyssääntö ) PSPACE-full . Tämän voidaan tulkita tarkoittavan, että resurssien käytön hallinta on vaikea tehtävä, jopa yksinkertaisimmissa tapauksissa. [kahdeksan]

Esitys peräkkäisenä laskentana

Yksi tapa määritellä lineaarinen logiikka on sekventiolaskenta . Kirjaimet Γ ja ∆ tarkoittavat lauseluetteloita , ja niitä kutsutaan konteksteiksi . Sarjassa konteksti sijoitetaan ⊢:n ("pitäisi") vasemmalle ja oikealle puolelle, esimerkiksi: . Alla on MLL:n laskenta kaksisuuntaisessa muodossa [7] . $A_{1},...,A_{n}$ $\Gamma \vdash \Delta$

Rakenteellinen sääntö - permutaatio. Vasen ja oikea päättelysäännöt on annettu vastaavasti:

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

Identiteetti ja osasto :

${\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 '))\;{\teksti{Leikkaa))$

Kertova konjunktio:

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

Multiplikatiivinen disjunktio:

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

Kielteisyys:

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

Samanlaiset säännöt voidaan määritellä täydelliselle lineaarilogiikalle, sen additiivisille ja eksponentiaaleille. Huomaa, että lineaariseen logiikkaan ei ole lisätty rakenteellisia heikentämisen ja vähentämisen sääntöjä , koska yleisessä tapauksessa lauseet (ja niiden kopiot) eivät voi ilmaantua ja kadota satunnaisesti sekvensseissä, kuten klassisessa logiikassa on tapana.

Muistiinpanot

↑ Girard, Jean-Yves (1987). "Lineaarinen logiikka" (PDF) . Teoreettinen tietojenkäsittelytiede . 50 (1): 1-102. DOI : 10.1016/0304-3975(87)90045-4 . HDL : 10338.dmlcz/120513 . Arkistoitu (PDF) alkuperäisestä 2021-05-06 . Haettu 24.03.2021 . Käytöstä poistettu parametri |deadlink=( ohje )
↑ 1 2 Algoritmisia algebran ja logiikan kysymyksiä / VENÄJÄN TIEDESÄÄTIÖN TUKEMA PROJEKTIKORTTI. Haettu: 18.07.2021 . Haettu 18. heinäkuuta 2021. Arkistoitu alkuperäisestä 18. heinäkuuta 2021. (määrätön)
↑ Baez, John ; Pysy, Mike (2008). Bob Coecke , toim. "Fysiikka, topologia, logiikka ja laskenta: Rosetta Stone" (PDF) . Fysiikan uudet rakenteet . Arkistoitu alkuperäisestä 2021-03-22 . Haettu 24.03.2021 . Käytöstä poistettu parametri |deadlink=( ohje )
↑ de Paiva, V. Dagstuhl Seminar 99341 on lineaarinen logiikka ja sovellukset / V. de Paiva, J. van Genabith, E. Ritter. — 1999. Arkistoitu 22. marraskuuta 2020 Wayback Machinessa
↑ 1 2 Lomazova, 2004 .
↑ 1 2 3 Lincoln, 1992 .
↑ 12. Beffara , 2013 .
↑ 1 2 Max I. Kanovich. Lineaarisen logiikan Horn-fragmenttien monimutkaisuus. Annals of Pure and Applied Logic 69 (1994) 195-241

Kirjallisuus

Lomazova I.A. 6.5. Sisäkkäiset Petri-verkot ja lineaarinen logiikka // Sisäkkäiset Petri-verkot: Hajautettujen järjestelmien mallintaminen ja analysointi objektirakenteella. - M . : Tieteellinen maailma, 2004. - S. 175-185. — 208 s. - ISBN 5-89176-247-1 .
Patrick Lincoln. Lineaarinen logiikka // ACM SIGACT -uutiset. - 1992. - V. 23, nro 2 (toukokuu).
Emmanuel Befarara. Johdatus lineaariseen logiikkaan (2013). (määrätön)

Linkit

Lineaarinen logiikka , Stanford Encyclopedia of Philosophy

Logiikka

Filosofia • Semantiikka • Syntaksi • Historia

Logiikkaryhmät

klassista logiikkaa	Aristoteelinen logiikka propositionaalinen logiikka Ensimmäisen asteen logiikka Toisen asteen logiikka korkeamman asteen logiikkaa
matemaattinen logiikka	joukko teoria Mallin teoria Lasketettavuuden teoria Todistusteoria ja konstruktiivinen matematiikka Lineaarinen logiikka muodollinen järjestelmä luonnollinen johtopäätös Sekvenssilaskenta Logiikan algebra Asiaankuuluva logiikka Deonttinen logiikka intuitionistinen logiikka Lambek-laskenta
Ei-klassinen logiikka	intuitionismi sumea logiikka Alirakennelogiikka logiikka Kuvauslogiikka Moniarvoinen logiikka Logiikka synteesi Sidontalogiikka Temporaalinen logiikka Modaalinen logiikka ( Hybridilogiikka ) episteeminen logiikka
Filosofinen logiikka	Kriittinen ajattelu epävirallista logiikkaa deduktiivinen päättely

Komponentit

Sieppaus (logiikka)
Todennäköisyys
lausunto
Vähennys / Induktio / Traduction
Todellisuus
induktiivinen päättely
päättely
boolen vakio
Totta
loogista seuraamista
Looginen muoto
Tarpeelliset ja riittävät olosuhteet
Kuvaus
Määritelmä
Korvaus
Paketti
Kiista ( antinomia )
Synteettinen arviointi / Analyyttinen arviointi
Linkki

Luettelo loogisista symboleista