Logică dinamică

Logica dinamică este o extensie a logicii modale definită inițial pentru raționamentul programului și aplicată ulterior sarcinilor mai generale și complexe derivate din lingvistică, filosofie, inteligență artificială și alte domenii.

Limba

Logica modală este caracterizată de operatori modali $\Box$ ${\ displaystyle \ Box}$ $\Cutie$ p (caseta p), indică faptul că p este neapărat adevărat și $\Diamond$ ${\ displaystyle \ Diamond}$ $\ Diamond$ p (diamant p) indică faptul că p este posibil. Logica dinamică extinde această posibilitate prin asocierea fiecărei acțiuni cu operatorii modali [a] și <a> , astfel încât să o facă o logică multimodală . Înțelesul lui [a] p este că, în urma executării unei acțiuni a, este necesar ca p să fie valid, prin urmare, ad a trebuie să urmeze p . Înțelesul lui <a> p este că, în urma executării a , este posibil ca p să fie valid, prin urmare, ad a poate urma p . Acești operatori sunt corelați cu [a] p ≡ ¬ <a> ¬ p și <a> p ≡ ¬ [a] ¬ p , similar cu relația dintre cuantificatorii existențiali și universali.

Logica dinamică vă permite să compuneți acțiuni pornind de la acțiuni mai mici. Puteți utiliza operatorii de control de bază ai oricărui limbaj de programare în acest scop; Operatorii de expresie regulată ai lui Kleene sunt o alegere bună pentru logica modală. Având în vedere acțiunile a și b , acțiunea compusă a∪b , alegerea , scrisă și ca a + b sau a | b , se realizează prin executarea acțiunii a sau a acțiunii b . Acțiunea compusă a; b , secvență , se realizează executând mai întâi a și apoi b . Acțiunea constă dintr- o *, iterație, este efectuată prin efectuarea de zero sau de mai multe ori, în ordine. Acțiunea constantă 0 sau BLOCK nu face nimic și nu se termină, în timp ce acțiunea 1 sau SKIP sau NOP definibile cu 0 * , nu face altceva decât să se termine.

Axiome

Acești operatori pot fi axiomatizați în logica dinamică după cum urmează, luând deja o axiomatizare practică a logicii modale prin includerea unor astfel de axiome pentru operatorii modali, cum ar fi axioma menționată anterior [a] p = <a> p și cele două reguli ale modului inferența ponens ( p , p → q $\vdash$ ${\ displaystyle \ vdash}$ $\ vdash$ q ) și necesitate ( p $\vdash$ ${\ displaystyle \ vdash}$ $\ vdash$ [a] p ).

A1. [0] p

A2. [1] p ≡ p

A3. [a∪b] p ≡ [a] p ∧ [b] p

A4. [a; b] p ≡ [a] [b] p

A5. [a *] p ≡ p ∧ [a] [a *] p

A6. p ∧ [a *] (p → [a] p) → [a *] p

Axioma A1 face promisiunea goală că, atunci când BLOCK se termină, p va ține, chiar dacă p este propoziția falsă (A1 extrage esența noțiunii de îngheț iad). A2 spune că [NOP] acționează pe propoziții precum funcția de identitate, adică transformă p în sine. A3 spune că în cazul în care efectuează o alegere între a și b este cauzată p, atunci atât a și b „trebuie să provoace p. A4 spune că în cazul în care execută secvența compusă dintr - o și b conduce la p, executarea unei trebuie să conducă la o situație în care executarea b conduce la p. A5 este rezultatul evident al aplicării A2, A3 și A4 la ecuația a * = 1? A; a * a algebrei lui Kleene . A6 afirmă că , dacă p este acum în valoare, și indiferent de cât de multe ori executați rămășițele cazul în care p adevăr , după astfel de execuții este reținut , după o altă variantă de realizare a unui, atunci p trebuie să rămână valabil , indiferent de performanțele unui. A6 este recunoscută ca inducție matematică cu acțiunea n: = n + 1 a incrementării n generalizate de acțiunile arbitrare a .

Urmări

Axioma modală logică [a] p = <a> p permite derivarea următoarelor șase teoreme corespunzătoare axiomelor menționate mai sus.

T1. ¬ <0> p

T2. <1> p ≡ p

T3. <a∪b> p ≡ <a> p ∨ <b> p

T4. <a; b> p ≡ <a> <b> p

T5. <a *> p ≡ p ∨ <a> <a *> p

T6. <a *> p → p ∨ <a *> (¬p ∧ <a> p)

T1 afirmă incapacitatea de a accepta orice cu apariția BLOCK . T2 afirmă încă că NOP nu schimbă nimic, ținând cont de faptul că NOP este determinist și se termină acolo unde [1] și <1> au aceeași forță. T3 spune că în cazul în care alegerea a sau b poate duce la p, atunci atât a și b poate duce la p. T4 este analog cu A4. T5 se explică ca A5. T6 afirmă că , dacă este posibil să cauza p rulând o suficient de lung, atunci fie p este adevărat acum sau este posibil să se execute în mod repetat , o să provoace o situație în care p este (încă) de execuție false , dar în continuare a unei poate provoca p. Cutia și diamantul sunt complet simetrice cu privire la care dintre cele două este luată ca primitivă. O axiomatizare alternativă ar putea lua teoremele T1-T6 ca axiome, din care A1-A6 poate fi derivat ca teoreme. Diferența dintre implicație și inferență este aceeași în logica dinamică ca în orice altă logică: unde implicația p → q afirmă că, dacă p este adevărat, atunci este și q , inferența p $\vdash$ ${\ displaystyle \ vdash}$ $\ vdash$ q afirmă că dacă p este valid, este și q . Cu toate acestea, natura dinamică a logicii dinamice mută această distribuție din domeniul axiomatizărilor abstracte în experiența de bun simț a situațiilor concrete. Regula inferenței p $\vdash$ ${\ displaystyle \ vdash}$ $\ vdash$ [a] p , de exemplu , este corect , deoarece premisa afirmă că p este întotdeauna adevărat, așa că nu contează în cazul în care o poate duce, p va fi în cele din urmă adevărat. Implicația p → [a] p pe de altă parte nu este întotdeauna valabilă deoarece adevărul real al lui p nu garantează adevărul lui p după executarea unui . De exemplu, p? [A] p va fi adevărat în orice situație în care p este fals sau în orice situație în care [a] p este adevărat, dar afirmația x = 1 → [x: = x + 1] x = 1 it este fals în orice situație în care x are valoarea 1 și, prin urmare, nu este valid.

Reguli de deducție derivate

Ca și în cazul logicii modale, regulile de inferență, modus ponens și necesitate sunt, de asemenea, suficiente pentru logica dinamică ca singure reguli primitive de care are nevoie, așa cum s-a menționat mai sus. Totuși, așa cum este obișnuit în logică, reguli suplimentare pot fi derivate din acestea cu ajutorul axiomelor. Un exemplu demonstrativ al acestor reguli derivate din logica dinamică este că lovirea cu piciorul a televizorului spart o dată nu o poate remedia, așa că lovirea cu piciorul în mod repetat face chiar mai imposibilă rezolvarea acestuia. Scriind k pentru acțiunea de a da cu piciorul la televizor și b pentru propunerea că televizorul este rupt, logica dinamică exprimă această deducție ca b? [K] b $\vdash$ ${\ displaystyle \ vdash}$ $\ vdash$ b → [k *] b , având b → [k] b ca premisă și b → [k *] b ca concluzie. Înțelesul lui [k] b este că este garantat că după lovirea televizorului, acesta este rupt. Deci, premisa b → [k] b înseamnă că, dacă televizorul este rupt, după ce l-a lovit din nou, acesta va fi rupt. k * denotă acțiunea de a lovi cu piciorul televizorul de zero sau de mai multe ori. Deci, concluzia b? [K *] b că, dacă televizorul este rupt, atunci după ce l-a lovit de zero sau de mai multe ori, acesta va fi rupt. Dacă acest lucru nu ar fi fost cazul, atunci după penultima lovitură, televizorul ar fi în situația în care să i se ofere o altă lovitură, însă premisa îl exclude în toate circumstanțele.

Inferația b → [k] b $\vdash$ ${\ displaystyle \ vdash}$ $\ vdash$ b → [k *] b este corect. Cu toate acestea, implicația (b → [k] b) → (b? [K *] b) nu este validă, deoarece putem găsi cu ușurință o situație în care b → [k] b este valabil, dar b → [k *] b nu. În orice astfel de contraexemplu, b trebuie să păstreze, dar [k *] b trebuie să fie fals, în timp ce [k] b trebuie să fie adevărat. Dar acest lucru se poate întâmpla în orice situație în care televizorul este rupt, dar poate fi remediat cu două lovituri. Implicația eșuează, deoarece necesită doar că b → [k] b este valabil acum, în timp ce inferența reușește, deoarece necesită ca b → [k] b să fie valabilă în toate situațiile, nu doar în cea actuală.

Un exemplu de implicație validă este propoziția x≥3 → [x: = x + 1] x≥4 . Într-adevăr, afirmă că dacă x este mai mare sau egal cu 3, atunci după creșterea lui x , x trebuie să fie mai mare sau egal cu 4. În cazul acțiunilor deterministe a pentru care este garantată încheierea, cum ar fi x: = x + 1 , e trebuie să aibă aceeași forță, adică [a] și <a> să aibă aceeași semnificație. În consecință, propoziția anterioară este echivalentă cu x≥3 → <x: = x + 1> x≥4 , care afirmă că, dacă x este mai mare sau egal cu 3, atunci după ce ați efectuat x: = x + 1 , x ar putea fi mai mare mai mare sau egal cu 4.

Misiune

Forma generală a unei declarații de atribuire este x: = e unde x este o variabilă și e este o expresie construită din constante și variabile cu orice operație furnizată de limbă, cum ar fi adunarea și multiplicarea. Axioma lui Hoare pentru atribuire nu este dată ca o singură axiomă, ci mai degrabă ca o schemă de axiome.

A7. [x: = e] Φ (x) ≡ Φ (e)

Acesta este un model în sensul că Φ (x) poate fi instanțiat cu orice formulă Φ conținând zero sau mai multe instanțe ale variabilei x . Înțelesul lui Φ (e) este Φ cu acele recurențe ale lui x care apar liber în Φ , adică nu sunt limitate de cuantificatori ca în ∀x , înlocuiți cu e . De exemplu, A7 poate fi instanțiat cu [x: = e] (x = y²) ≡ e = y² , sau cu [x: = e] (b = c + x) ≡ b = c + e . Această schemă axiomatică produce un număr infinit de axiome de formă comună scrise ca o expresie finită care conotează această formă.

Instanța [x: = x + 1] x≥4 ≡ x + 1 ≥ 4 din A7 ne permite să calculăm mecanic că exemplul [x: = x + 1] x≥4 întâlnit acum câteva paragrafe este echivalent cu x + 1 ≥ 4 , care la rândul său este echivalent cu x≥3 prin algebră elementară .

Un exemplu care ilustrează atribuirea în combinație cu * este propoziția <(x: = x + 1) *> x = 7. Aici se afirmă că este posibil, prin creșterea x suficient, pentru a face în valoare de 7. Acest lucru cu siguranță nu este întotdeauna adevărat, de exemplu , dacă la începutul x este 8, sau 6,5, rezultă că această propunere nu este o teoremă de dinamică logică. Dacă x este oricum de tip întreg, atunci această propoziție este adevărată dacă și numai dacă la început x este cel mult 7, acesta este un alt mod de a spune x≤7 .

Inducția matematică poate fi obținută ca instanță a lui A6 în care propoziția p este instanțiată ca Φ (n) , acțiunea a ca n: = n + 1 și n ca 0 . Primele două dintre aceste trei instanțe sunt imediate, transformând A6 în (Φ (n) ʌ [(n: = n + 1) *] (Φ (n) → [n: = n + 1] Φ (n))) → [(n: = n + 1) *] Φ (n) . Cu toate acestea, înlocuirea aparent simplă 0 a lui n nu este atât de simplă, deoarece scoate la lumină așa-numita opacitate referențială a logicii modale în cazul în care o modalitate poate interfera cu o substituție.

Când înlocuim Φ (n) pentru p, ne gândeam simbolul propozitional p ca designator rigid în ceea ce privește modalitatea [n: = n + 1], ceea ce înseamnă că este aceeași propoziție după incrementare n ca mai înainte, chiar dacă creșterea cu n poate avea impact asupra adevărului. În mod similar, acțiunea a rămâne aceeași după incrementarea n , chiar dacă acel increment înseamnă că va fi efectuat într-un mediu diferit. Pe de altă parte, n însuși nu este un designator rigid în ceea ce privește modalitatea [n: = n + 1] ; de fapt, dacă înainte de creștere denotă 3, după ce denotă 4. Deci, în A6 nu putem înlocui 0 cu n nicăieri.

O modalitate de a gestiona opacitatea modurilor este eliminarea modurilor. În acest scop, extindeți [(n: = n + 1) *] Φ (n) ca o conjuncție infinită [(n: = n + 1) ⁰ ] Φ (n) ʌ [(n: = n + 1) ¹ ] Φ (n) ʌ [(n: = n + 1) ² ] Φ (n) ʌ… , care este conjuncția pentru toți i din [(n: = n + 1) ⁱ ] Φ (n) . Acum, aplicând A4 transformam [(n: = n + 1) ^i] Φ (n) în [n: = n + 1] [n: = n + 1] ... Φ (n) cu modalitățile. Deci aplicând axioma lui Hoare i ori producem Φ (n + i) , atunci simplificăm această conjuncție infinită la ∀iΦ (n + i) . Această reducere completă trebuie aplicată ambelor instanțe ale lui [(n: = n + 1) *] în A6, rezultând (Φ (n) ʌ ∀i (Φ (n + i) → [n: = n + 1] Φ (n + i))) → ∀iΦ (n + i) . Modul rămas poate fi acum eliminat cu o altă utilizare a axiomei lui Hoare pentru a obține (Φ (n) ʌ ∀i (Φ (n + i) → Φ (n + i + 1))) → ∀iΦ (n + i) .

Fără modalități opace putem înlocui acum 0 cu n în modul obișnuit al logicii de prim ordin pentru a obține celebra axiomă a lui Giuseppe Peano (Φ (0) ʌ ∀i (Φ (i) → Φ (i + 1))) → ∀ iΦ (i) , care ia numele de Inducție matematică .

O subtilitate pe care am trecut-o cu vederea aici este că ∀i ar trebui interpretat ca diferind în intervalul numerelor naturale, unde i este vârful în expansiunea a * ca uniunea a ⁱ în toate numerele naturale i . Importanța orientării între aceste informații tipografice devine clară dacă n este de tip întreg , sau chiar real , pentru care A6 este o axiomă perfect validă. Ca și în cazul în discuție dacă n este o variabilă reală și Φ (n) este predicatul n este un număr natural , atunci axioma A6 după primele două substituții, adică (Φ (n) ʌ ∀i (Φ (n + i) → Φ (n + i + 1))) → ∀iΦ (n + i) , este încă valabil, adică adevărat, în orice stare indiferent de valoarea lui n în acea stare, de exemplu când n este natural tipul de număr . Dacă într-o stare dată n este un număr natural, atunci antecedentul implicației principale a lui A6 se menține, dar atunci n + i este, de asemenea, un număr natural, și, prin urmare, valabil și consecința. Dacă n nu este un număr natural, atunci antecedentul este fals, deci A6 rămâne adevărat, indiferent de adevărul rezultatului. A6 poate fi întărit la o echivalență p ∧ [a *] (p → [a] p) ≡ [a *] p fără niciun impact asupra elementelor, cealaltă direcție fiind demonstrabilă de A5, din care vedem că dacă l antecedent din A6 devine fals undeva, atunci consecința trebuie să fie falsă.

Test

Logica dinamică asociază fiecare propunere p cu o acțiune p? numit test. Când este p , testul p? acționează ca un NOP , fără a schimba nimic, dar permite ca acțiunea să continue. Când este p fals, p? acționează ca un BLOC . Testele pot fi axiomatizate în felul următor.

A8. [p?] q ≡ p → q

Teorema corespunzătoare pentru <p?> Este;

„ T8. <p?> q ≡ p∧q

Construcția dacă p atunci a altfel b este realizată în logică dinamică ca (p ?; A) ∪ (~ p ?; B) . Această acțiune exprimă o alegere prudentă: dacă p ține atunci p ?; A este echivalent cu a , unde ~ p ?; B este echivalent cu BLOCK și a∪BLOCK este echivalent cu a . Rezultă că atunci când p este adevărat, executorul acțiunii poate lua doar ramura stângă, iar când p este fals, cea dreaptă.

Construcția în timp ce p execută a se realizează ca (p ?; A) *; ~ p? . Rulați p ?; Până la zero sau mai multe ori și apoi faceți ~ p? . Atâta timp cât p rămâne adevărat, ~ p? final îl împiedică pe executant să termine încheierea prematură a iterației, dar de îndată ce devine falsă, iterațiile ulterioare ale corpului p sunt blocate și executantul nu are de ales decât să iasă prin testul ~ p? .

Cuantificarea ca atribuire aleatorie

Propunerea de alocare aleatorie x: =? denotă acțiunea nedeterministă a setării x la o valoare arbitrară. [x: =?] p apoi spune că p se menține indiferent de ce valoare are x , în schimb <x: =?> p spune că este posibil să se atribuie lui x o valoare care face ca p să fie adevărat. [x: =?] are deci aceeași semnificație ca cuantificatorul universal ∀x , în timp ce <x: =?> corespunde în mod similar cuantificatorului existențial ∃x . Prin urmare, logica de ordinul întâi poate fi interpretată ca logica dinamică a programelor de forma x: =? .

Semantica lumii posibile

Logica modală este interpretată mai ales în termeni de semantică mondială posibilă sau structuri Kripke. Aceste semantice conduc în mod natural la logica dinamică prin interpretarea lumilor ca stări ale unui computer aplicat verificării programelor sau stări ale mediului nostru în aplicații de lingvistică, AI etc. Un rol pentru semantica lumii posibile este de a formaliza noțiunile intuitive de adevăr și validitate, care la rândul lor duc la noțiunile de corectitudine și completitudine care trebuie definite în sistemele de axiome. O regulă de inferență este corectă atunci când validitatea premiselor sale implică validitatea încheierii sale. Un sistem axiomatic este corect atunci când toate axiomele sale sunt valide și regulile sale de inferență sunt corecte. Un sistem axiomatic este complet atunci când orice formulă validă este derivabilă ca teoremă a sistemului respectiv. Aceste concepte se aplică tuturor sistemelor de logică, inclusiv dinamice.

Logică propozițională dinamică (PDL)

Logica obișnuită sau logica de primă ordine are două tipuri de termeni, declarații și, respectiv, date. După cum se poate vedea din exemplele anterioare, logica dinamică adaugă un al treilea tip de termeni care denotă acțiuni. Declarația logică dinamică [x: = x + 1] x≥4 conține toate cele trei tipuri: x , x + 1 și 4 sunt date, x: = x + 1 este o acțiune și x≥4 și [x: = x + 1] x≥4 sunt afirmații. Logica propozițională este derivată din logica primului ordin, omiind termenii și motivele date numai prin propoziții abstracte, care pot fi simple variabile propoziționale sau atomi sau propoziții compuse construite cu conectivități logice precum și, sau, nu.

Logica propozițională dinamică, sau PDL, a fost derivată din logica dinamică în 1977 de Michael Fischer și Richard Ladner. PDL amestecă ideile din spatele logicii propoziționale și logicii dinamice prin adăugarea de acțiuni și omiterea datelor; rezultă că termenii PDL sunt acțiuni și propoziții. Exemplul anterior al televizorului este exprimat în PDL, în timp ce următorul exemplu referitor la x: = x + 1 este în logica dinamică de ordinul întâi. PDL este logica dinamică (de ordinul întâi), așa cum logica propozițională este logica de ordinul întâi.

Fischer și Ladner au demonstrat în lucrarea lor din 1977 că satisfacția PDL a fost de complexitate de calcul la cel mai nedeterminist timp exponențial și cel puțin de timp exponențial determinist în cel mai rău moment. Acest decalaj a fost eliminat în 1978 de Vaughan Pratt, care a demonstrat că decizibilitatea PDL într-un timp exponențial determinist. În 1977, Krister Segerberg a propus o axiomatizare completă a PDL, tocmai orice axiomatizare completă a logicii modale K împreună cu axiomele A1-A6 menționate anterior. Dovezile de completitudine pentru axiomele lui Segerberg au fost găsite de Gabbay, Parikh (1978), Pratt (1979), Kozen și Parikh (1981).

Istorie

Logica dinamică a fost dezvoltată de Vaughan Pratt în 1974 în unele note ale unei prelegeri despre verificarea programului ca o abordare de atribuire a sensului Logicii lui Hoare prin exprimarea formulei lui Hoare p {a} q ca p → [a] q . Abordarea a fost publicată ulterior în 1976 ca un sistem logic cu drepturi depline. Sistemul este comparabil cu sistemul de logică algoritmică al lui A. Salwicki și noțiunea lui Edsger Dijkstra de transformator predicativ de precondiție mai slabă wp (a, p) cu [a] p corespunzătoare Dijkstrano wlp (a, p) de precondiție liberală mai slabă. Cu toate acestea, aceste logici nu exprimă nicio legătură nici cu logica modală, cu semantica Kripke, cu expresii regulate, nici cu calculul relațiilor binare; logica dinamică poate fi deci văzută ca un rafinament al logicii algoritmice și al transformatoarelor predicative care le leagă de semantica axiomatică și Kripke a logicii modale, precum și de calculele relațiilor binare și ale expresiilor regulate.

Provocarea concurenței

Logica lui Hoare, logica algoritmică, condițiile prealabile mai slabe și logica dinamică sunt toate adecvate pentru a discuta și a argumenta comportamentul secvențial. Cu toate acestea, extinderea acestor logici la un comportament concurent a fost problematică. Există diverse abordări, dar tuturor le lipsește eleganța cazului secvențial. Dimpotrivă, sistemul de logică temporală al lui Amir Pnueli din 1977, o altă variantă a logicii modale care împărtășește multe caracteristici comune cu logica dinamică, diferă de toate logica menționată mai sus pentru a fi ceea ce Pnueli a caracterizat ca o logică endogenă , celelalte fiind logici exogene . Prin aceasta, Pnueli a înțeles că afirmațiile logicii temporale sunt interpretate într-un context comportamental universal în care o singură situație globală se schimbă odată cu trecerea timpului, în timp ce afirmațiile celorlalte logici sunt făcute extern acțiunilor multiple despre care vorbesc. Avantajul abordării endogene este că nu face presupuneri fundamentale despre ceea ce cauzează ceea ce în timp. Pe de altă parte, o formulă a logicii temporale poate vorbi despre două părți ale sistemului fără legătură, deoarece, ca neînrudite, ele evoluează tacit în paralel. Într-adevăr, conjuncția logică obișnuită a afirmațiilor temporale este operatorul compoziției simultane a logicii temporale. Simplitatea acestei abordări a concurenței a însemnat că logica temporală este logica modală de alegere pentru raționamentul sistemelor concurente, cu problemele lor de sincronizare, interferență, independență, impas, punct ascuțit, imparțialitate etc.

Aceste aspecte ale competiției pot părea a fi mai puțin centrale în lingvistică , filosofie și inteligență artificială , domenii în care logica dinamică este cel mai adesea întâlnită astăzi.

Pentru un tratament complet al logicii dinamice vezi cartea lui David Harel et. la. mentionat mai jos.

Bibliografie

VR Pratt, „Considerații semantice asupra logicii Floyd-Hoare”, Proc. 17 Simpozion anual IEEE privind fundamentele științei computerizate, 1976, 109-121.
D. Harel, D. Kozen și J. Tiuryn, „Dynamic Logic”. MIT Press, 2000 (450 pp).
D. Harel, „Dynamic Logic”, În D. Gabbay și F. Guenthner, (eds.), Handbook of Philosophical Logic , volumul II: Extensions of Classical Logic, capitolul 10, paginile 497-604. Reidel, Dordrecht, 1984.

Elemente conexe

linkuri externe

( EN ) Nicolas Troquard și Philippe Balbiani, Logică dinamică propozițională , în Edward N. Zalta (ed.), Stanford Encyclopedia of Philosophy , Centre for the Study of Language and Information (CSLI), Universitatea Stanford .
Vaughan R. Pratt, Semantical Considerations on Floyd-Hoare Logic ( PDF ), pe boole.stanford.edu . (lucrare originală despre logica dinamică)