Logika liniowa

W logice matematycznej, a dokładniej w teorii dowodu , logika liniowa , wymyślona przez logika Jeana-Yvesa Girarda w 1986 roku, jest systemem formalnym, który z logicznego punktu widzenia rozkłada i analizuje logikę klasyczną i intuicjonistyczną oraz of view, to system typów dla rachunku lambda pozwalający na określenie pewnych zastosowań zasobów.

Logika klasyczna nie bada najbardziej podstawowych aspektów rozumowania. Jego strukturę można rozłożyć na bardziej elementarne systemy formalne, które opisują drobniejsze etapy dedukcji; w szczególności można zainteresować się logiką, w której nie istnieją pewne reguły logiki klasycznej. Takie logiki nazywane są logikami podstrukturalnymi . Jedną z tych logik podstrukturalnych jest logika liniowa; brakuje w nim w szczególności reguły kontrakcji logiki klasycznej, która mówi z grubsza, że jeśli możemy przeprowadzić rozumowanie z tą samą hipotezą przywołaną dwukrotnie, możemy zrobić to samo rozumowanie bez powielania tej hipotezy i reguły osłabiającej co pozwala wyeliminować ze wszystkich hipotez niewykorzystaną hipotezę w rozumowaniu.

Wizja programowa i wizja geometryczna

Logika liniowa może być rozumiana przez korespondencję Curry-Howarda jako system pisania dla programów wyższego rzędu ( typowany rachunek lambda ), umożliwiający wyrażenie sposobu, w jaki zarządzają swoimi zasobami, w szczególności faktu, że zasób jest zużyty liniowo , to znaczy raz i tylko raz podczas wykonywania programu.

Logika liniowa promuje „geometryczny” pogląd na składnie formalne poprzez kultywowanie analogii z algebrą liniową (przestrzenie spójne) i wprowadzanie nowych reprezentacji dowodów / programów za pomocą wykresów ( sieci dowodowe ), a nawet operatorów ( geometria). Interakcja ). Pozwoliło to również Girardowi zaproponować logiczne podejście do złożoności algorytmicznej (lekka i elementarna logika liniowa). Odniosła duży sukces, zwłaszcza w informatyce teoretycznej , niewątpliwie dzięki wielu oryginalnym narzędziom, które wprowadza oraz ponieważ rozbija logikę intuicjonistyczną i klasyczną, zapewniając w ten sposób ujednolicone ramy do ich badania.

Geneza logiki liniowej

Logika liniowa powstała z badania denotacyjnego modelu terminów rachunku lambda typowanego , tj. Poprzez korespondencję Curry-Howarda , dowody logiki intuicjonistycznej. Jest to w rzeczywistości poprzez opracowanie modelu przestrzeni spójnych że Girard zauważył, że możemy zdefiniować pojęcie liniowej funkcji (w pewnym sensie bardzo blisko do funkcji liniowej między przestrzeniami wektor), co sprawia, że możliwe do rozłożenia funkcji z w w ogólnym nieliniowa funkcja in i liniowa funkcja in ( jest to spójna przestrzeń, której konstrukcja przypomina algebrę tensorową). Właściwość tę podsumowuje wzór założycielski logiki liniowej: $W$ $b$ $W$ $!W$ $!W$ $b$ $!W$ $W$

A \ rightarrow B = \,! A \ multimap B

gdzie lewy człon oznacza przestrzeń funkcji w, a prawy człon oznacza przestrzeń funkcji liniowych in . $W$ $b$ $!W$ $b$

Składnia

Sekwencje

Dzięki negacji, która jest integralną częścią systemu, możemy (i nie pozbawiamy się jej) przedstawiać sekwencje, umieszczając wszystkie zdania po prawej stronie znaku . Na przykład zamiast reguły z poprzednikiem i następcą takim jak , piszemy regułę tylko z następcą podobnym . Wśród diadycznych reguł dedukcji (tych, które mają dwie przesłanki) wyróżniamy dwa typy reguł: $\ vdash$ $A \ vdash B$ $\ vdash A ^ {\ bot}, B$

z multiplikatywne reguły w takich zasadach oba Sequent lokale mają różne następców których jeden dołącza się do wniosku o regułę. na przykład

{\ frac {\ vdash \ Gamma, A \ quad \ vdash B, \ Delta} {\ vdash \ Gamma, A \ odot B, \ Delta}}

że dodatek zasady , w takich zasad dwa Sequent lokale mają taki sam sukces oprócz propozycji których odsetki nas, co znajdujemy w konkluzji. na przykład

{\ frac {\ vdash \ Gamma, A \ quad \ vdash \ Gamma, B} {\ vdash \ Gamma, A \ \ odot \ B}}

Złącza

Złącza klasycznej zdaniowej logiki liniowej (CLL) to:

oznaczona negacja liniowa ; $A ^ {\ bot}$
koniunkcja i multiplikatywna dysjunkcja : tensor ( ) i by ( ); $\ otimes$ $\ wp$
koniunkcja i dysjunkcja addytywna : the with (&) i plus ( ); $\ oplus$
strzałka liniowa jest zdefiniowana za pomocą liniowej negacji i multiplikatywnej dysjunkcji . $A \ multimap B = A ^ {\ perp} \ wp B$

Dodajemy modalności

! co oznacza tyle razy, ile się chce , co też oczywiście wymawia się ;
? co jest w pewnym sensie dwojaką! i że ogłaszamy, dlaczego nie .

Istnieją dwie główne składnie pisania dowodów: rachunek ciągów i sieci dowodów . Twierdzenie o sekwencjonowaniu zapewnia, że możemy przetłumaczyć dowolny dowód z jednej składni na drugą. Obie składnie spełniają twierdzenie o eliminacji przerw .

Sieci dowodowe to hipergrafy, których wierzchołki są formułami połączonymi hiper-krawędziami reprezentującymi reguły logiczne. Tworzą one bardzo syntetyczną składnię wyposażoną w wiele właściwości geometrycznych, ale trudną do zdefiniowania, więc łatwiej jest podejść do logiki liniowej od strony rachunku całkowego do ciągów.

Obliczanie ciągów liniowych

Obliczanie ciągów liniowych uzyskuje się z klasycznego obliczania ciągów, usuwając strukturalne zasady kurczenia się i osłabiania . Ta delecja prowadzi do duplikacji łączników koniunkcyjnych i rozłącznych.

Grupa tożsamości

{\ frac {} {\ vdash A, A ^ {\ bot}}} ({\ mbox {aksjomat}}) \ qquad \ qquad \ qquad {\ frac {\ vdash \ Gamma, A \ quad \ vdash A ^ { \ bot}, \ Delta} {\ vdash \ Gamma, \ Delta}} ({\ mbox {cutoff}})

Grupa multiplikatywna

{\ frac {\ vdash \ Gamma, A \ quad \ vdash B, \ Delta} {\ vdash \ Gamma, A \ otimes B, \ Delta}} (\ otimes) \ qquad \ qquad \ qquad {\ frac {\ vdash \ Gamma, A, B} {\ vdash \ Gamma, A \ wp B}} (\ wp)

Grupa dodatków

{\ frac {\ vdash \ Gamma, A \ quad \ vdash \ Gamma, B} {\ vdash \ Gamma, A \ \ & \ B}} (\ &) \ qquad \ qquad \ qquad {\ frac {\ vdash \ Gamma, A_ {i}} {\ vdash \ Gamma, A_ {1} \ oplus A_ {2}}} (\ oplus _ {i})

Grupa wykładnicza

{\ frac {\ vdash \ Gamma ,? A ,? A} {\ vdash \ Gamma ,? A}} ({\ mbox {contraction}}) \ qquad \ qquad \ qquad {\ frac {\ vdash \ Gamma, A } {\ vdash \ Gamma ,? A}} ({\ mbox {dereliction}})

{\ frac {\ vdash \ Gamma} {\ vdash \ Gamma ,? A}} ({\ mbox {osłabienie}}) \ qquad \ qquad \ qquad {\ frac {\ vdash? \ Gamma, A} {\ vdash? \ Gamma ,! A}} ({\ mbox {promocja}})

Kilka niezwykłych wzorów liniowych

Oto niektóre z głównych możliwych do udowodnienia wzorów (na przykład w rachunku ciągów) w logice liniowej. W dalszej części symbol reprezentuje równoważność liniową : $\ equiv$

$A \ equiv B \ quad = \ quad (A \ multimap B) \ & (B \ multimap A)$

Prawa De Morgana

{\ begin {aligned} (A ^ {\ perp}) ^ {\ perp} & \ equiv A \\ (A \ otimes B) ^ {\ perp} & \ equiv A ^ {\ perp} \, \ wp \ , B ^ {\ perp} \\ (A \ oplus B) ^ {\ perp} & \ equiv A ^ {\ perp} \, \ & \, B ^ {\ perp} \\ (! A) ^ {\ perp} & \ equiv \,? A ^ {\ perp} \ end {aligned}}

Dystrybucja

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

Izomorfizm wykładniczy

\,! (A \ & B) \ equiv \,! A \ otimes \,! B

Zauważ, że dzięki prawom De Morgana każda z tych równoważności ma podwójną, na przykład negacja dlaczego nie jest przebiegiem negacji, par rozkłada się na z ...

Wreszcie, oto ważna tautologia liniowa, która jednak nie jest równoważnością:

Półrozdzielczość

(A \ otimes (B \, \ wp \, C)) \ multimap ((A \ otimes B) \, \ wp \, C)

Interpretacja wzorów

Z tradycyjnego punktu widzenia, gdzie logikę postrzega się jako naukę o prawdzie lub jako analizę języka, logika liniowa z jej dwoma spójnikami, dwoma dysjunkcjami, jej wykładniczymi modalnościami , może wydawać się trochę ezoteryczna. Jest znacznie lepiej rozumiana dzięki korespondencji Curry-Howarda.

Naturalną interpretacją formuł logiki liniowej jest postrzeganie ich jako typów , to znaczy formalnych opisów zachowań programów na wejściu / wyjściu. Podobnie jak logika intuicjonistyczna (a dokładniej formalizacja logiki intuicjonistycznej), logika liniowa jest konstruktywna w sensie Curry-Howarda, tj. (Formalne) dowody LL można postrzegać jako programy, których dane wejściowe są wpisywane za pomocą formuł hipotez i wyników poprzez wnioskowanie formuły. Logika liniowa różni się jednak od logiki intuicjonistycznej w jednym zasadniczym punkcie: ma negację, która spełnia wszystkie symetrie, które znajdujemy w logice klasycznej pod nazwą praw De Morgana : negacja jest inwolutywna, negacja `` koniunkcji jest dysjunkcja negacji itp. Ponadto, w porównaniu z logiką intuicjonistyczną, LL dodaje dodatkowy stopień wyrazistości, umożliwiając określenie dokładnych relacji między danymi wejściowymi i wyjściowymi programu.

Jeśli weźmiemy na przykład pod uwagę wzór , implikuje liniowo , z tradycyjnego punktu widzenia, wyraża on, że można wyprowadzić tę właściwość , używając hipotezy raz i tylko raz . To ograniczenie może wydawać się arbitralne i prawdopodobnie najlepiej je zrozumieć, transponując je za pomocą Curry-Howarda do zdania: program typu przyjmuje dane wejściowe typu i używa ich dokładnie raz, aby obliczyć wynik typu . Taki program może więc zaoszczędzić na przydzielaniu określonej przestrzeni pamięci, w której zapisuje wartość swojego wejścia, a dokładniej taki program zużywa swoje dane wejściowe podczas obliczeń (zazwyczaj automat skończony całkowicie zużywa jeden i tylko jeden raz wpisane hasło ). $A \ multimap B$ $W$ $b$ $b$ $W$ $A \ multimap B$ $W$ $b$

W tym kontekście liniowa negacja wzoru nie ma tak naprawdę prostej interpretacji zgodnie z tradycyjnym punktem widzenia. Z drugiej strony jest dobrze rozumiany jako typ : program typu to program, który daje wynik typu ; program typu to program, który liniowo wykorzystuje dane wejściowe typu . Zatem negacja liniowa wyraża dwoistość między danymi wejściowymi i wyjściowymi i lepiej rozumiemy, że jest ona niekolektywna: wyjście typu jest wejściem typu . $ani)$ $W$ $W$ $W$ $ani)$ $W$ $ani)$ $W$

Możemy podać inne ramy interpretacyjne, takie jak pojęcie zasobów. W tym kontekście idempotentny charakter łączników algebry Boole'a stwarza problemy. Na przykład idempotencja przekłada się na wzór: $\ vee$

{\ Displaystyle A \ vee A \ equiv A}

Oznacza to, że każdy zasób może zostać zduplikowany. $W$

Ta idempotencja uniemożliwia rozważenie po prostu ilościowych aspektów zasobów.

Ta właściwość oznacza również, że fakt jest wieczną prawdą. To kolejna z wielkich słabości logicznego paradygmatu, jeśli chodzi o reprezentowanie dynamicznych systemów, które mają niewiele prawd wiecznych, ale wiele prawd przelotnych, takich jak stany systemu.

Niektóre złączy liniowych , i zostały określone przez Girard odrzucając tę właściwość . $\ otimes$ $\ wp$ $\ multimap$

W tym kontekście operatory multiplikatywne, a także znajdują proste i naturalne znaczenie: ${\ displaystyle nil}$

kółko przekreślone (czasami nazywany produkt tensor ): oznacza koniunkcję zasobów i ; $A \ otimes B$ $W$ $b$
par : oznacza, że zasoby i są użyteczne, ale nie wspólnie; $\ wp$ $W$ $b$
WPŁYW liniowy : oznacza przemianę w . jest konsumowany i przekształcany w . Pojęcie to ma zasadnicze znaczenie dla reprezentacji systemów dynamicznych; $A \ multimap B$ $W$ $b$ $W$ $b$
$ani)$ ma prostą interpretację: chodzi o potrzebę . To znaczy . $W$ $-W$

Uwagi i odniesienia

Ponieważ nie mamy reguły kontrakcji, musimy wyraźnie kontrolować powielanie zdań.

Bibliografia

J.-Y. Girard, Logika liniowa, Teoretyczna Informatyka nr 50, 1987
Advances in Linear Logic, London Mathematical Society Lecture Notes Series nr 222, Cambridge University Press, 1995
Linear Logic in Computer Science, London Mathematical Society Notatki do wykładów, seria nr 316, Cambridge University Press, 2004