Lineáris logika

Lineáris logika ( az angol Linear Logic egy szubstrukturális logika, amelyet Jean -Yves Girard javasolt a klasszikus és intuíciós logika finomításaként , amely az előbbi kettősségét az utóbbi számos konstruktív tulajdonságával ötvözi [1] , bevezetve és felhasználva valamilyen erőforrás felhasználását figyelembe vevő logikai érveléshez [2] ] . Bár a logikát önmagában is tanulmányozták, a lineáris logika ötletei számos erőforrás-igényes alkalmazásban találnak alkalmazást, beleértve a hálózati protokoll - ellenőrzést , a programozási nyelveket , a játékelméletet ( játékszemantikát ) [2] és a kvantumfizikát (mert a lineáris logika a kvantuminformáció-elmélet logikájának tekinthető ) [3] , a nyelvészet [4] .

Leírás

Szintaxis

A klasszikus lineáris logika nyelve ( angolul classic linear logic, CLL ) Backus-Naur formában írható le :

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

Ahol

p és p ⊥ atomi képletek,

logikai összefüggések és konstansok:

Szimbólum	Jelentése
⊗	multiplikatív kötőszó ("tenzor", angol "tenzor" )
⊕	additív diszjunkció
&	additív kötőszó
⅋	multiplikatív diszjunkció ("par", angol "par" )
!	modalitás " természetesen "
?	modalitás " miért ne "
egy	mértékegysége ⊗
0	nulla ⊕ esetén
⊤	null &
⊥	mértékegysége ⅋

A ⊗, ⊕, & és ⅋ bináris konnektívuma asszociatív és kommutatív .

A klasszikus lineáris logikában minden A állításnak van egy duális A ⊥ , amelyet a következőképpen definiálunk:

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

Értelmes értelmezés

A lineáris logikában (a klasszikus logikától eltérően) a premisszák gyakran elhasználható erőforrásokként vannak kezelve , így a származtatott vagy kezdeti képlet felhasználási száma korlátozható.

A ⊗ multiplikatív kötőszó hasonló a többhalmazos összeadási művelethez , és kifejezheti az erőforrások egyesülését.

Figyeljük meg, hogy (.) ⊥ involúció , azaz A ⊥⊥ = A minden állításra. A ⊥ -t A lineáris negációjának is nevezik .

A lineáris implikáció nagy szerepet játszik a lineáris logikában, bár nem szerepel a konnektív nyelvtanban. Lineáris negációval és multiplikatív diszjunkcióval fejezhető ki

A ⊸ B := A ⊥ ⅋ B .

A szalagot ⊸ jellegzetes alakja miatt néha "nyalókának" ( eng. lollipop ) is nevezik.

A lineáris implikáció akkor használható a kimenetben, ha annak bal oldalán vannak erőforrások, és az eredmény a jobb oldali lineáris implikációból származó erőforrások. Ez a transzformáció egy lineáris függvényt határoz meg , amelyből a "lineáris logika" [5] kifejezés született .

A „természetesen” (!) modalitás lehetővé teszi, hogy egy erőforrást kimeríthetetlennek jelöljünk.

Példa. Legyen D egy dollár, C pedig egy csokoládé. Ekkor egy csokoládé vásárlását D ⊸ C -vel jelölhetjük . A vásárlást a következőképpen fejezhetjük ki: D ⊗ !( D ⊸ C ) ⊢ C⊗!( D ⊸ C ) , vagyis hogy a dollár és az azzal való tábla csokoládévásárlás lehetősége egy csokoládéhoz vezet, és a csokoládé vásárlási lehetőség marad [5] .

A klasszikus és intuicionista logikával ellentétben a lineáris logikának kétféle kötőszója van, amelyek lehetővé teszik az erőforrások korlátozottságának kifejezését. Adjuk hozzá az előző példához a nyalóka L vásárlásának lehetőségét. A tábla csokoládé vagy nyalóka vásárlásának lehetőségét additív kötőszóval fejezhetjük ki [6] :

D ⊸ L & C

Természetesen csak egyet választhat. A multiplikatív kötőszó mindkét erőforrás jelenlétét jelzi. Tehát két dollárért vásárolhat egy csokit és egy nyalókát is:

D ⊗ D ⊸ L ⊗ C

Az A ⅋ B multiplikatív diszjunkció felfogható úgy, hogy „ha nem A, akkor B”, a rajta keresztül kifejezett A ⊸ B lineáris implikáció pedig „levezethető-e B-ből A-ból pontosan egyszer?” [6]

Az A ⊕ B additív diszjunkció mind A, mind B lehetőségét jelöli, de a választás nem a tiéd [6] . Például egy win-win lottó, ahol nyalókát vagy csokit nyerhet, kifejezhető additív diszjunkcióval:

D ⊸ L ⊕ C

Töredékek

A teljes lineáris logika mellett töredékeit használják [7] :

LL: minden hivatkozás engedélyezett
MLL: csak szorzók (⊗, ⅋)
MALL: csak szorzók és additívek (⊗, ⅋, ⊕, &)
MELL: csak szorzók és exponenciálisok (⊗, ⅋, !, ?)

Természetesen ez a lista nem merít ki minden lehetséges töredéket. Például vannak különféle Horn-töredékek, amelyek lineáris implikációt használnak (hasonlóan a Horn-tagmondatokhoz ) különféle konnektívumokkal kombinálva. [nyolc]

A logika töredékei számítási értelmezésük összetettsége miatt érdekesek a kutatók számára. Konkrétan M. I. Kanovich bebizonyította, hogy egy teljes MLL-fragment NP-teljes , és egy lineáris logika ⊕-kürt töredéke egy gyengítési szabállyal .( angol gyengítési szabály ) PSPACE-full . Ez úgy értelmezhető, hogy az erőforrás-felhasználás kezelése a legegyszerűbb esetekben is nehéz feladat. [nyolc]

Ábrázolás szekvenciális kalkulusként

A lineáris logika meghatározásának egyik módja a szekvenciális számítás . A Γ és ∆ betűk mondatlistákat jelölnek , és kontextusnak nevezzük . Egy sorozatban a kontextus a ⊢ ("kell") bal és jobb oldalán helyezkedik el, például: . Az alábbiakban látható az MLL szekvenciális számítása kétirányú formátumban [7] . $A_{1},...,A_{n}$ $\Gamma \vdash \Delta$

Szerkezeti szabály – permutáció. A bal és a jobb oldali következtetési szabályok a következők:

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

Identitás és szakasz :

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

Multiplikatív kötőszó:

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

Multiplikatív diszjunkció:

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

Tagadás:

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

Hasonló szabályok definiálhatók a teljes lineáris logikára, annak additívumaira és exponenciálisaira. Megjegyzendő, hogy a gyengítés és a redukció strukturális szabályait nem adták hozzá a lineáris logikához , mivel általában az utasítások (és azok másolatai) nem jelenhetnek meg és nem tűnhetnek el véletlenszerűen egymás után, ahogy az a klasszikus logikában megszokott.

Jegyzetek

↑ Girard, Jean-Yves (1987). "Lineáris logika" (PDF) . Elméleti számítástechnika . 50 (1): 1-102. DOI : 10.1016/0304-3975(87)90045-4 . HDL : 10338.dmlcz/120513 . Archivált (PDF) az eredetiből ekkor: 2021-05-06 . Letöltve: 2021-03-24 . Elavult használt paraméter |deadlink=( súgó )
↑ 1 2 Algoritmikus algebrai és logikai kérdések / AZ OROSZ TUDOMÁNYOS ALAPÍTVÁNY ÁLTAL TÁMOGATOTT PROJEKTkártya. Letöltve: 2021.07.18 . Letöltve: 2021. július 18. Az eredetiből archiválva : 2021. július 18. (határozatlan)
↑ Baez, John ; Maradj, Mike (2008). Bob Coecke , szerk. „Fizika, topológia, logika és számítás: Rosetta-kő” (PDF) . A fizika új struktúrái . Archiválva az eredetiből, ekkor: 2021-03-22 . Letöltve: 2021-03-24 . Elavult használt paraméter |deadlink=( súgó )
↑ de Paiva, V. Dagstuhl Seminar 99341 on lineáris logika és alkalmazások / V. de Paiva, J. van Genabith, E. Ritter. — 1999. Archiválva : 2020. november 22. a Wayback Machine -nél
↑ 1 2 Lomazova, 2004 .
↑ 1 2 3 Lincoln, 1992 .
↑ 12 Beffara , 2013 .
↑ 1 2 Max I. Kanovich. A Lineáris Logika Horn-töredékeinek összetettsége. Annals of Pure and Applied Logic 69 (1994) 195-241

Irodalom

Lomazova I. A. 6.5. Beágyazott Petri hálók és lineáris logika // Beágyazott Petri hálók: Elosztott rendszerek modellezése és elemzése objektumstruktúrával. - M . : Tudományos világ, 2004. - S. 175-185. — 208 p. - ISBN 5-89176-247-1 .
Patrick Lincoln. Lineáris logika // ACM SIGACT News. - 1992. - V. 23., 2. szám (május).
Emmanuel Befarara. Bevezetés a lineáris logikába (2013). (határozatlan)

Linkek

Lineáris logika , Stanford Encyclopedia of Philosophy

Logikák

Filozófia • Szemantika • Szintaxis • Történelem

Logikai csoportok

klasszikus logika	Arisztotelészi logika propozíciós logika Elsőrendű logika Másodrendű logika magasabb rendű logika
matematikai logika	halmazelmélet Modellelmélet Kiszámíthatóság elmélet Bizonyításelmélet és konstruktív matematika Lineáris logika formális rendszer természetes következtetés Sorozatszámítás Logikai algebra Releváns logika Deontikus logika intuicionista logika Lambek kalkulus
Nem klasszikus logika	intuicionizmus zavaros logika Szubstrukturális logika logika Leírás logika Többértékű logika Logikai szintézis Kötési logika Időbeli logika Modális logika ( Hibrid logika ) episztemikus logika
Filozófiai logika	Kritikus gondolkodás informális logika deduktív érvelés

Alkatrészek

Logikai szimbólumok listája