Lineární logika - Linear logic

Lineární logika je substrukturální logika navržená Jeanem-Yvesem Girardem jako zdokonalení klasické a intuicionistické logiky , která spojuje dualitu prvního s mnoha konstrukčními vlastnostmi logiky druhé. Ačkoli logika byla také studována kvůli sobě, v širším smyslu myšlenky z lineární logiky ovlivnily oblasti, jako jsou programovací jazyky , sémantika her a kvantová fyzika (protože na lineární logiku lze pohlížet jako na logiku kvantové teorie informací ) , stejně jako lingvistika , zejména kvůli svému důrazu na omezenost zdrojů, dualitu a interakci.

Lineární logika je vhodná pro mnoho různých prezentací, vysvětlení a intuic. Důkazně teoreticky pochází z analýzy klasického sekvenčního počtu, ve které jsou pečlivě kontrolována použití ( strukturálních pravidel ) kontrakce a oslabení . Provozně to znamená, že logická dedukce už není jen o stále se rozšiřující sbírce perzistentních „pravd“, ale také o způsobu manipulace se zdroji, které nelze vždy duplikovat nebo je libovolně zahodit. Z hlediska jednoduché denotační modely , mohou být lineární logika viděn jako rafinace výkladu intuitionistic logika nahrazením kartézských (uzavřené) kategorie od symetrické monoidal (uzavřený) kategorie nebo výkladu klasické logiky nahrazením booleovské algebry od C * -algebras .

Spojky, dualita a polarita

Syntax

Jazyk klasické lineární logiky (CLL) je induktivně definován notací BNF

$A$	:: =	$p ∣ p ⊥$
	$∣$	$A \otimes A ∣ A \oplus A$
	$∣$	$A & A ∣ A ⅋ A$
	$∣$	$1 ∣ 0 ∣ ⊤ ∣ ⊥$
	$∣$	$! A ∣? A$

Zde se $p$ a $p ⊥$ pohybují nad logickými atomy . Z důvodů, které budou vysvětleny níže, se spojky ⊗, ⅋, 1 a ⊥ nazývají multiplikáty , spojky &, ⊕, ⊤ a 0 se nazývají přísady a spojky! a ? se nazývají exponenciály . Můžeme dále používat následující terminologii:


Symbol	název
⊗	multiplikativní spojka	krát	tenzor
⊕	aditivní disjunkce	Plus
&	aditivní spojení	s
⅋	multiplikativní disjunkce	par
!	samozřejmě	prásk
?	proč ne

Binární spojky ⊗, ⊕, & a ⅋ jsou asociativní a komutativní; 1 je jednotka pro ⊗, 0 je jednotka pro ⊕, ⊥ je jednotka pro ⅋ a ⊤ je jednotka pro &.

Každý návrh $A$ v CLL má duální $A ⊥$ , definovaný následovně:

$(p) ⊥ = p ⊥$			$(p ⊥) ⊥ = p$
$(A \otimes B) ⊥ = A ⊥ ⅋ B ⊥$			$(A ⅋ B) ⊥ = A ⊥ \otimes B ⊥$
$(A \oplus B) ⊥ = A ⊥ & B ⊥$			$(A & B) ⊥ = A ⊥ \oplus B ⊥$
$(1) ⊥ = ⊥$			$(⊥) ⊥ = 1$
$(0) ⊥ = ⊤$			$(⊤) ⊥ = 0$
$(! A) ⊥ =? (A ⊥)$			$(? A) ⊥ =! (A ⊥)$

Klasifikace spojek
	přidat	mul	zk
poz	⊕ 0	⊗ 1	!
neg	& ⊤	⅋ ⊥	?

Všimněte si, že $(-) ⊥$ je involuce , tj. $A ⊥⊥ = A$ pro všechna tvrzení. $⊥$ je také nazýván lineární negaci a $A$ .

Sloupce tabulky naznačují další způsob klasifikace spojek lineární logiky, nazývaný polarita : spojky negované v levém sloupci (⊗, ⊕, 1, 0 ,! ) Se nazývají kladné , zatímco jejich duály vpravo (⅋, &, ⊥, ⊤,?) Se nazývají záporné ; srov. stůl vpravo.

Lineární implikace není součástí gramatiky spojek, ale je definovatelná v CLL použitím lineární negaci a multiplikativní disjunkce, od $A ⊸ B : = ⊥ ⅋ B$ . Spojovací ⊸ je kvůli svému tvaru někdy vyslovováno jako „ lízátko “.

Prezentace postupného počtu

Jedním ze způsobů definování lineární logiky je sekvenční počet . Pomocí písmen $Γ$ a $Δ$ $procházíme$ seznam výroků $A 1, ..., A n$ , nazývaných také kontexty . Sequent umístí kontext levé a pravé straně turniketu , které ${\ displaystyle \ vdash}$ . Sekvence intuitivně tvrdí, že konjunkce $Γ$ znamená disjunkci $Δ$ (ačkoli máme na mysli „multiplikativní“ konjunkci a disjunkci, jak je vysvětleno níže). Girard popisuje klasickou lineární logiku pomocí pouze jednostranných sekvencí (kde je kontext levé ruky prázdný) a my zde sledujeme ekonomičtější prezentaci. To je možné, protože jakékoli prostory nalevo od turniketu lze vždy přesunout na druhou stranu a dualizovat.

Nyní dáváme odvozovací pravidla popisující, jak vytvářet důkazy sekvencí.

Za prvé, abychom formalizovali skutečnost, že se nestaráme o pořadí výroků v kontextu, přidáme strukturální směnné pravidlo :

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

Všimněte si toho, že nepřidáváme strukturální pravidla oslabení a smrštění, protože nám záleží na absenci propozic v sekvenci a na počtu přítomných kopií.

Dále přidáme počáteční sekvence a střihy :

{\ displaystyle \ vdash}

${\ displaystyle \ vdash}$			${\ displaystyle \ vdash}$

${\ displaystyle \ vdash}$

Pravidlo střihu lze považovat za způsob skládání důkazů a počáteční jednotky slouží jako jednotky pro kompozici. V určitém smyslu jsou tato pravidla nadbytečná: jelikož níže uvedeme další pravidla pro vytváření důkazů, zachováme vlastnost, že libovolné počáteční sekvence lze odvodit z atomových počátečních sekvencí, a že kdykoli je sekvence prokazatelná, lze ji omezit- důkaz zdarma. Tato vlastnost kanonické formy (kterou lze rozdělit na úplnost počátečních atomových sekvencí a větu o eliminaci řezu , vyvolávající představu analytického důkazu ) nakonec stojí za aplikacemi lineární logiky v informatice, protože umožňuje logiku používá se v důkazním vyhledávání a jako lambda kalkul s vědomím zdrojů .

Nyní vysvětlíme spojky zadáním logických pravidel . Typicky v sekvenčním počtu jeden dává jak „pravá pravidla“, tak „levá pravidla“ pro každé pojivo, v podstatě popisuje dva způsoby uvažování o propozicích zahrnujících toto pojivo (např. Ověření a falšování). V jednostranné prezentaci se místo toho používá negace: pravá pravidla pro pojivo (řekněme ⅋) účinně hrají roli levých pravidel pro jeho dvojí (⊗). Měli bychom tedy očekávat určitou „harmonii“ mezi pravidly pro spojovací prvek a pravidly pro jeho dvojí.

Multiplikáty

Pravidla pro multiplikativní spojku (⊗) a disjunkci (⅋):

${\ displaystyle \ vdash}$			${\ displaystyle \ vdash}$

${\ displaystyle \ vdash}$

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

a pro jejich jednotky:



${\ displaystyle \ vdash}$

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

Všimněte si, že pravidla pro multiplikativní spojky a disjunkce jsou přípustná pro prostou spojku a disjunkci podle klasické interpretace (tj. Jsou to přípustná pravidla v LK ).

Aditiva

Pravidla pro aditivní spojení (&) a disjunkce (⊕):

${\ displaystyle \ vdash}$			${\ displaystyle \ vdash}$

${\ displaystyle \ vdash}$

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

a pro jejich jednotky:



${\ displaystyle \ vdash}$

(žádné pravidlo pro

0

)

Všimněte si, že pravidla pro aditivní spojení a disjunkce jsou opět přípustná podle klasické interpretace. Nyní však můžeme vysvětlit základ pro multiplikativní/aditivní rozlišení v pravidlech pro dvě různé verze konjunkce: pro multiplikativní pojivo (⊗) je kontext závěru ( $Γ, Δ$ ) rozdělen mezi premisy, zatímco pro aditivní případ spojovací (&) je kontext závěru ( $Γ$ ) přenesen celý do obou prostor.

Exponenciály

Exponenciály se používají k zajištění kontrolovaného přístupu k oslabení a smrštění. Konkrétně přidáme strukturální pravidla oslabení a smrštění pro? Návrhů:

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

a použijte následující logická pravidla:

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

Dalo by se poznamenat, že pravidla pro exponenciály se řídí jiným vzorem než pravidla pro ostatní spojky, připomínající odvozovací pravidla upravující modality v postupných formalizacích kalkulu normální modální logiky S4, a že již neexistuje tak jasná symetrie mezi duály! a ?. Tato situace je napravena v alternativních prezentacích CLL (např. Prezentace LU ).

Pozoruhodné vzorce

Kromě De Morganových dualit popsaných výše, některé důležité ekvivalence v lineární logice zahrnují:

Distribuce

A \otimes (B \oplus C) ≣ (A \otimes B) \oplus (A \otimes C)

(A \oplus B) \otimes C ≣ (A \otimes C) \oplus (B \otimes C)

A ⅋ (B & C) ≣ (A ⅋ B) & (A ⅋ C)

(A & B) ⅋ C ≣ (A ⅋ C) & (B ⅋ C)

Podle definice $A ⊸ B$ jako $A ⊥ ⅋ B$ , poslední dva zákony distribuce také dávají:

A ⊸ (B & C) ≣ (A ⊸ B) & (A ⊸ C)

(A \oplus B) ⊸ C ≣ (A ⊸ C) & (B ⊸ C)

(Zde $A ≣ B$ je $(A ⊸ B) & (B ⊸ A)$ .)

Exponenciální izomorfismus

! (A & B) ≣! A \otimes! B

? (A \oplus B) ≣? A ⅋? B

Lineární rozdělení

Mapa, která není izomorfismem, přesto hraje zásadní roli v lineární logice, je:

(A \otimes (B ⅋ C)) ⊸ ((A \otimes B) ⅋ C)

Lineární distribuce jsou zásadní v teorii důkazů lineární logiky. Důsledky této mapy byly nejprve prozkoumány a nazvány „slabou distribucí“. V další práci byl přejmenován na „lineární distribuci“, aby odrážel základní spojení s lineární logikou.

Jiné důsledky

Následující vzorce distribuce nejsou obecně ekvivalencí, pouze implikací:

! A \otimes! B ⊸! (A \otimes B)

! A \oplus! B ⊸! (A \oplus B)

? (A ⅋ B) ⊸? A ⅋? B

? (A & B) ⊸? A &? B

(A & B) \otimes C ⊸ (A \otimes C) & (B \otimes C)

(A & B) \oplus C ⊸ (A \oplus C) & (B \oplus C)

(A ⅋ C) \oplus (B ⅋ C) ⊸ (A \oplus B) ⅋ C

(A & C) \oplus (B & C) ⊸ (A \oplus B) & C

Kódování klasické/intuitivní logiky v lineární logice

Intuicionistickou i klasickou implikaci lze z lineární implikace získat vložením exponenciálů: intuicionistická implikace je kódována jako $! ⊸ B$ , zatímco klasický důsledek mohou být kódovány jako $? A ⊸? B$ nebo $! A ⊸ ?! B$ (nebo různé alternativní možné překlady). Myšlenka je taková, že exponenciály nám umožňují použít vzorec tolikrát, kolikrát potřebujeme, což je v klasické a intuicionistické logice vždy možné.

Formálně existuje překlad vzorců intuitionistické logiky do vzorců lineární logiky způsobem, který zaručuje, že původní vzorec je v intuicionistické logice prokazatelný právě tehdy, když je přeložený vzorec prokazatelný v lineární logice. Pomocí negativního překladu Gödel – Gentzen můžeme tedy vložit klasickou logiku prvního řádu do lineární logiky prvního řádu.

Interpretace zdrojů

Lafont (1993) nejprve ukázal, jak lze intuicionalistickou lineární logiku vysvětlit jako logiku zdrojů, a poskytnout tak logickému jazyku přístup k formalismům, které lze použít k úvahám o zdrojích v samotné logice, nikoli, jako v klasické logice, prostředky nelogických predikátů a vztahů. K ilustraci této myšlenky lze použít klasický příklad automatu Tonyho Hoareho (1985).

Předpokládejme, že reprezentujeme cukroví podle atomových $bonbónů$ a dolar o $1$ dolar . Abychom uvedli skutečnost, že za dolar vám koupíme jednu tyčinku, můžeme napsat implikaci $1 $ \Rightarrow cukroví$ . Ale v běžném (klasickém nebo intuitionistic) logiky, z $A$ a $A \Rightarrow B$ lze dovodit $A \land B$ . Běžná logika nás tedy vede k přesvědčení, že si můžeme koupit tyčinku a udržet si dolar! Tomuto problému se samozřejmě můžeme vyhnout použitím sofistikovanějších kódování, ačkoli typicky takováto kódování trpí problémem rámce . Odmítnutí oslabení a smrštění však umožňuje lineární logice vyhnout se tomuto druhu falešného uvažování i při „naivním“ pravidle. Spíše než $1 $ \Rightarrow cukroví$ vyjadřujeme vlastnost prodejního automatu jako lineární implikaci $1 $ ⊸ cukroví$ . Od $1 $$ a této skutečnosti můžeme uzavřít $bonbóny$ , ale ne $1 $ \otimes bonbóny$ . Obecně platí, že můžeme použít lineární logický návrh $⊸$ $B$ vyjádřit platnosti transformaci zdrojů $A$ do zdrojů $B$ .

Na příkladu automatu zvažte „interpretace prostředků“ ostatních multiplikativních a aditivních spojek. (Exponenciály poskytují prostředky pro kombinaci této interpretace zdrojů s obvyklým pojmem trvalé logické pravdy .)

Multiplikativní spojka $(A \otimes B)$ označuje současný výskyt zdrojů, které mají být použity podle pokynů spotřebitele. Například, pokud si koupíte žvýkačku a láhev nealkoholického nápoje, pak žádáte $dásní \otimes nápoj$ . Konstanta 1 označuje nepřítomnost jakéhokoli zdroje, a proto funguje jako jednotka ⊗.

Aditivní spojka $(A & B)$ představuje alternativní výskyt zdrojů, jejichž výběr spotřebitel kontroluje. Pokud je v automatu balíček čipů, tyčinka a plechovka nealkoholického nápoje, každý za jeden dolar, pak za tuto cenu můžete koupit přesně jeden z těchto produktů. Tak píšeme $$ 1 ⊸ (bonbony & čipy & nápoj)$ . Nemáme ani psát $$ 1 ⊸ (candy \otimes čipy \otimes nápoj)$ , což by znamenalo, že jeden dolar vystačí na koupi všech tří produktů dohromady. Nicméně, od $$ 1 ⊸ (bonbony & chips a nápoj)$ , můžeme správně odvodit $$ 3 ⊸ (candy \otimes čipy \otimes nápoj)$ , kde $$ 3 : = $ 1 \otimes $ 1 \otimes $ 1$ . Jednotku ⊤ aditivní konjunkce lze považovat za odpadkový koš pro nepotřebné zdroje. Například můžeme napsat $3 $ (bonbóny \otimes ⊤),$ abychom vyjádřili, že se třemi dolary můžete získat tyčinku a další věci, aniž byste byli konkrétnější (například chipsy a drink nebo 2 $ nebo 1 $ a chipy , atd.).

Aditivní disjunkce $(A \oplus B)$ představuje alternativní výskyt zdrojů, jejichž výběr kontroluje stroj. Předpokládejme například, že automat umožňuje hazardní hry: vložte dolar a automat může vydat bonbón, balíček čipů nebo nealkoholický nápoj. Tuto situaci můžeme vyjádřit jako $1 $ ⊸ (bonbóny \oplus chipsy \oplus nápoj)$ . Konstanta 0 představuje produkt, který nelze vyrobit, a slouží tedy jako jednotka ⊕ (stroj, který může produkovat $A$ nebo $0,$ je stejně dobrý jako stroj, který vždy produkuje $A,$ protože nikdy nebude schopen vyrobit 0). Na rozdíl od výše uvedeného z toho nemůžeme odvodit $3 $ ⊸ (bonbóny \otimes čipy \otimes nápoj)$ .

Multiplikativní disjunkce $( ⅋ B),$ je mnohem obtížnější lesku, pokud jde o interpretaci zdrojů, i když může kódovat zpět do lineární nepřímo, a to buď jako $A ⊥ ⊸ B$ nebo $B ⊥ ⊸ A$ .

Další důkazní systémy

Důkazní sítě

Představený Jeanem-Yvesem Girardem byly vytvořeny důkazní sítě, aby se zabránilo byrokracii , to jsou všechny věci, které odlišují dvě derivace z logického hlediska, ale ne z hlediska „morálního“.

Například tyto dva důkazy jsou „morálně“ totožné:

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

{\ displaystyle \ vdash}

Cílem důkazních sítí je udělat je identickými vytvořením jejich grafického znázornění.

Sémantika

Algebraická sémantika

Rozhodnutelnost/složitost implikace

Vztah zapříčiněný plně CLL je nerozhodnutelný . Při zvažování fragmentů CLL má problém s rozhodováním různou složitost:

Multiplikativní lineární logika (MLL): pouze multiplikativní spojovací prvky. Zapojení MLL je NP-úplné , dokonce se omezuje na klauzule Horn v čistě implikačním fragmentu nebo na vzorce bez atomů.
Lineární logika multiplikativní aditivní (MALL): pouze multiplikativní a aditivní (tj. Bez exponenciálu). Zapojení MALL je kompletní pro PSPACE .
Multiplikativní-exponenciální lineární logika (MELL): pouze multiplikativní a exponenciální. Snížením problému s dosažitelností u Petriho sítí musí být zapojení MELL přinejmenším EXPSPACE , i když samotná rozhodovatelnost má status dlouhodobě otevřeného problému. V roce 2015 byl v časopise TCS publikován důkaz o rozhodnutelnosti , ale později se ukázalo, že je chybný.
V roce 1995 se ukázalo, že afinní lineární logika (tj. Lineární logika s oslabením, spíše rozšíření než fragment) je rozhodnutelná.

Varianty

Mnoho variací lineární logiky vzniká dalším pohráváním se strukturálními pravidly:

Afinní logika , která zakazuje kontrakci, ale umožňuje globální oslabení (rozhodnutelné rozšíření).
Přísná logika nebo relevantní logika , která zakazuje oslabení, ale umožňuje globální kontrakci.
Nekomutativní logika nebo uspořádaná logika, která kromě blokování oslabování a smršťování odstraňuje pravidlo směny. V uspořádané logice se lineární implikace dále dělí na levou implikaci a pravou implikaci.

Byly zvažovány různé intuicionistické varianty lineární logiky. Když jsou založeny na sekvenční prezentaci kalkulu s jedním závěrem, jako v ILL (Intuitionistic Linear Logic), spojky ⅋, ⊥ a? chybí a lineární implikace je považována za primitivní pojivo. Ve FILL (Full Intuitionistic Linear Logic) spojky ⅋, ⊥ a? jsou přítomny, lineární implikace je primitivní pojivem a podobně jako v intuitistické logice jsou všechny spojky (kromě lineární negace) nezávislé. Existují také rozšíření lineární logiky prvního a vyššího řádu, jejichž formální vývoj je poněkud standardní (viz logika prvního řádu a logika vyššího řádu ).

Viz také

Reference

Další čtení

Girard, Jean-Yves. Lineární logika , Theoretical Computer Science, sv. 50, č. 1, s. 1–102, 1987.
Girard, Jean-Yves, Lafont, Yves a Taylor, Paul. Důkazy a typy . Cambridge Press, 1989.
Hoare, CAR, 1985. Komunikace sekvenčních procesů . Prentice-Hall International. ISBN 0-13-153271-5
Lafont, Yves, 1993. Úvod do lineární logiky . Přednášky z Letní školy TEMPUS o algebraických a kategoriálních metodách z informatiky , Brno, Česká republika.
Troelstra, AS Přednášky o lineární logice . CSLI (Centrum pro studium jazyka a informací) Přednášky č. 29. Stanford, 1992.
AS Troelstra , H. Schwichtenberg (1996). Základní teorie důkazu . V sérii Cambridge Tracts in Theoretical Computer Science , Cambridge University Press, ISBN 0-521-77911-1 .
Di Cosmo, Roberto a Danos, Vincent. Lineární logický primer .
Úvod do lineární logiky (Postscript) od Patricka Lincolna
Úvod do lineární logiky od Torbena Braunera
Chuť lineární logiky od Philipa Wadlera
Lineární logika podle Roberto Di Cosmo a Dale Miller . Stanfordská encyklopedie filozofie (podzim 2006), Edward N. Zalta (ed.).
Přehled lineárního logického programování od Dale Miller . In Linear Logic in Computer Science , edited by Ehrhard, Girard, Ruet, and Scott. Cambridge University Press. London Mathematical Society Lecture Notes, Volume 316, 2004.
Lineární logika Wiki

externí odkazy

Média související s lineární logikou na Wikimedia Commons
Linear Logic Prover (llprover) , dostupný pro použití online, od: Naoyuki Tamura / Dept of CS / Kobe University / Japan

Languages

In other projects