Logica dinamica

La logica dinamica è un'estensione della logica modale originariamente definita per il ragionamento di programmi e in seguito applicata a compiti più generali e complessi derivati dalla linguistica, dalla filosofia, dall'intelligenza artificiale e da altri campi.

La logica modale è caratterizzata dagli operatori modali ${\displaystyle \Box }$p (box p), indica che p è necessariamente vero, e ${\displaystyle \Diamond }$p (diamond p) indica che p è possibile. La logica dinamica estende questa possibilità associando ad ogni azione a gli operatori modali [a] e <a>, così da renderla una logica multimodale. Il significato di [a]p è che in seguito all'esecuzione di un'azione a è necessario che valga p, quindi, ad a deve seguire p. Il significato di <a>p è che in seguito all'esecuzione di a è possibile che valga p, quindi, ad a può seguire p. Questi operatori sono correlati con [a]p ≡ ¬<a>¬ p e <a>p ≡ ¬[a]¬ p, analogamente alla relazione tra i quantificatori esistenziali e universali.

La logica dinamica permette di comporre azioni a partire da azioni più piccole. Si potrebbero utilizzare operatori di controllo di base di qualsiasi linguaggio di programmazione per tale scopo; gli operatori delle espressioni regolari di Kleene sono una buona scelta per la logica modale. Date le azioni a e b, l'azione composta a∪b, la scelta, anche scritta come a+b o a|b, è eseguita eseguendo l'azione a o l'azione b. L'azione composta a;b, sequenza, è eseguita eseguendo prima a e successivamente b. L'azione composta a*, iterazione, è eseguita eseguendo a zero o più volte, in sequenza. L'azione costante 0 o BLOCK non effettua nulla e non termina, mentre l'azione 1 o SKIP o NOP definibile con 0*, non effettua nulla ma termina.

Questi operatori possono essere assiomatizzati nella logica dinamica come segue, prendendo come già data una pratica assiomatizzazione di logica modale includendo tali assiomi per gli operatori modali, come l'assioma citato in precedenza [a]p = <a> p e le due regole di inferenza modus ponens (p, p→q${\displaystyle \vdash }$q) e la necessità (p ${\displaystyle \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

L'assioma A1 fa la promessa a vuoto che quando BLOCK termina, p varrà, anche se p è la proposizione falso (A1 estrae l'essenza della nozione di congelare l'inferno). A2 dice che [NOP] agisce sulle proposizioni come la funzione identità, ovvero, trasforma p in se stessa. A3 dice che se eseguendo una scelta fra a e b viene causata p, allora sia a sia b' devono causare p. A4 dice che se eseguendo la sequenza composta da a e b si giunge a p, l'esecuzione di a deve condurre a una situazione in cui l'esecuzione di b conduca a p. A5 è l'evidente risultato dell'applicazione di A2, A3 e A4 all'equazione a* = 1?a;a* dell'algebra di Kleene. A6 asserisce che se p vale ora, e indipendentemente da quante volte si esegue a permane il caso che la verità di p dopo tali esecuzioni si mantiene dopo un'ulteriore esecuzione di a, allora p deve rimanere vera indipendentemente dalle esecuzioni di a. A6 è riconoscibile come l'induzione matematica con l'azione n:=n+1 di incrementare n generalizzato dalle arbitrarie azioni a.

L'assioma modale logico [a]p = <a> p permette la derivazione dei seguenti sei teoremi corrispondenti ai succitati assiomi.

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 asserisce l'impossibilità di accettare qualsiasi cosa con il verificarsi di BLOCK. T2 afferma ancora che NOP non cambia niente, tenendo a mente che NOP è sia deterministico e termina dove [1] e <1> hanno la stessa forza. T3 dice che se la scelta di a o b può portare a p, allora sia a sia b possono portare a p. T4 è analogo ad A4. T5 si spiega come A5. T6 asserisce che se è possibile causare p eseguendo a sufficientemente a lungo, allora o p è vero ora oppure è possibile eseguire ripetutamente a per causare una situazione in cui p è (ancora) falso ma un'ulteriore esecuzione di a può causare p. Box e diamond sono completamente simmetrici riguardo a quale dei due è preso come primitiva. Un'assiomatizzazione alternativa potrebbe prendere i teoremi T1-T6 come assiomi, dai quali si possono derivare A1-A6 come teoremi. La differenza tra implicazione e inferenza è la stessa nella logica dinamica come in qualsiasi altra logica: laddove l'implicazione p→q asserisce che se p è vero allora lo è anche q, l'inferenza p${\displaystyle \vdash }$q afferma che se p è valida lo è anche q. Comunque la natura dinamica della logica dinamica sposta questa distribuzione fuori dal reame delle assiomatizzazioni astratte dentro l'esperienza del senso comune di situazioni concrete. La regola di inferenza p${\displaystyle \vdash }$[a]p per esempio è corretta perché la sua premessa afferma che p è sempre vera, quindi non importa dove a può portare, p alla fine sarà vera. L'implicazione p→[a]p invece non è sempre valida perché l'attuale verità di p non garantisce della verità di p dopo l'esecuzione di a. Per esempio p?[a]p sarà vera in qualsiasi situazione dove p è falsa, o in qualsiasi situazione in cui [a]p è vera, ma l'affermazione x=1 → [x:=x+1]x=1 è falsa in qualsiasi situazione dove x ha valore 1, e quindi non è valida.

Come per la logica modale, le regole di inferenza, modus ponens e necessità sono sufficienti anche per la logica dinamica come le sole regole primitive di cui ha bisogno, come osservato prima. Comunque come è d'uso in logica ulteriori regole possono essere derivate da queste con l'aiuto degli assiomi. Un esempio dimostrativo di queste regole derivate in logica dinamica è che prendendo a calci una volta la TV rotta non è possibile aggiustarla, quindi prendendola a calci ripetutamente diviene ancora più impossibile ripararla. Scrivendo k per l'azione del prendere a calci la TV e b per la proposizione che la TV è rotta, la logica dinamica esprime questa inferenza come b?[k]b ${\displaystyle \vdash }$ b→[k*]b, avendosi come premessa b → [k]b e come conclusione b → [k*]b. Il significato di [k]b è che è garantito che dopo aver preso a calci la TV, essa è rotta. Quindi la premessa b → [k]b significa che se la TV è rotta, dopo averla presa un'altra volta a calci essa sarà ancora rotta. k* denota l'azione di prendere a calci la TV zero o più volte. Quindi la conclusione b ?[k*]b che se la TV è rotta, allora dopo averla presa a calci zero o più volte sarà ancora rotta. Se non fosse così, allora dopo il penultimo calcio la TV sarebbe nella condizione in cui dandogli un altro calcio si aggiusterebbe, ma la premessa lo esclude in ogni circostanza.

L'inferenza b→[k]b ${\displaystyle \vdash }$ b→[k*]b è corretta. Comunque l'implicazione (b→[k]b) → (b?[k*]b) non è valida perché possiamo facilmente trovare una situazione in cui b→[k]b vale ma b→[k*]b no. In qualsiasi controesempio di tal genere b deve valere ma [k*]b deve essere falsa, mentre [k]b deve essere comunque vera. Ma questo può avvenire in qualsiasi situazione in cui la TV è rotta ma può essere aggiustata con due calci. L'implicazione fallisce perché richiede solo che b→[k]b valga ora, laddove l'inferenza riesce perché richiede che b→[k]b valga in tutte le situazioni, non solo in quella corrente.

Un esempio di implicazione valida è la proposizione x≥3 → [x:=x+1]x≥4 . Afferma infatti che se x è maggiore o uguale a 3, allora dopo aver incrementato x, xdeve essere maggiore o uguale a 4. Nel caso di azioni deterministiche a per cui è garantita la terminazione, come x:=x+1, deve e dovrebbe hanno la stessa forza, cioè [a] e <a> hanno lo stesso significato. Di conseguenza la precedente proposizione è equivalente a x≥3 → <x:=x+1>x≥4, la quale asserisce che se x è maggiore o uguale a 3 allora dopo aver eseguito x:=x+1, x potrebbe essere maggiore o uguale a 4.

La forma generale di una dichiarazione di assegnazione è x := e dove x è una variabile ed e è un'espressione costruita tramite costanti e variabili con qualsiasi operazione fornita dal linguaggio, come addizione e moltiplicazione. L'assioma di Hoare per l'assegnazione non è dato come un singolo assioma ma piuttosto come uno schema di assiomi.

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

Questo è uno schema nel senso che Φ(x) può essere istanziata con qualsiasi formulaΦ contenente zero o più istanze della variabile x. Il significato di Φ(e) è Φ con quelle ricorrenze di x che ricorrono liberamente in Φ, cioè non limitate da quantificatori come in ∀x, rimpiazzato da e. Per esempio si può instanziare A7 con [x:=e](x=y²) ≡ e=y², o con [x:=e](b=c+x) ≡ b=c+e. Tale schema assiomatico produce un numero infinito di assiomi di forma comune scritta come un'espressione finita che connoti tale forma.

L'istanza [x:=x+1]x≥4 ≡ x+1 ≥ 4 di A7 ci consente di calcolare meccanicamente che l'esempio [x:=x+1]x≥4 incontrato pochi paragrafi fa è equivalente a x+1 ≥ 4, , che a sua volta è equivalente a x≥3 tramite l'algebra elementare.

Un esempio che illustra l'assegnamento in combinazione con * è la proposizione <(x:=x+1)*>x=7. Qui si afferma che è possibile, incrementando x a sufficienza, fare sì che valga 7. Questo certamente non è sempre vero, per esempio se all'inizio x è 8, o 6,5, segue che questa proposizione non è un teorema di logica dinamica. Se x è comunque di tipo intero, allora questa proposizione è vera se e solo se all'inizio x è al massimo 7, cioè un altro modo per dire x≤7.

L'induzione matematica può essere ottenuta come l'istanza di A6 in cui la proposizione p è istanziata come Φ(n), l'azione a come n:=n+1, e n come 0. Le prime due di queste tre istanziazioni sono immediate, convertendo A6 in (Φ(n) ʌ [(n:=n+1)*] (Φ(n)→[n:=n+1]Φ(n))) → [(n:=n+1)*]Φ(n). Comunque l'apparentemente semplice sostituzione con 0 di n non è così semplice perché porta alla luce la cosiddetta opacità referenziale della logica modale nel caso in cui una modalità può interferire con una sostituzione.

Quando sostituiamo Φ(n) per p, noi stavamo pensando al simbolo proposizionale p come designatore rigido rispetto alla modalità [n:=n+1], il che significa che è la stessa proposizione dopo aver incrementato n come prima, anche se l'incrementare di n può aver impatto sulla verità. Similmente, l'azione a resta la stessa dopo aver incrementato n, anche se tale incremento significa che sarà eseguita in un ambiente differente. Invece n stesso non è un designatore rigido rispetto alla modalità [n:=n+1]; infatti, se prima dell'incremento denota 3, dopo denota 4. Quindi in A6 non possiamo sostituire 0 per n dovunque.

Un modo per gestire l'opacità delle modalità è quello di eliminare queste ultime. A questo fine, si espande [(n:=n+1)*]Φ(n) come una congiunzione infinita [(n:=n+1)⁰]Φ(n) ʌ [(n:=n+1)¹]Φ(n) ʌ [(n:=n+1) ²]Φ(n) ʌ …, cioè la congiunzione su tutte le i di [(n:=n+1) ⁱ]Φ(n). Ora, applicando A4 si trasforma [(n:=n+1)ⁱ]Φ(n) in [n:=n+1][n:=n+1]…Φ(n) con i modalità. Quindi applicando l'assioma di Hoare i volte si produce Φ(n+i), poi si semplifica questa congiunzione infinita a ∀iΦ(n+i). Questa riduzione completa deve essere applicata a entrambe le istanze di [(n:=n+1)*] in A6, giungendo a (Φ(n) ʌ ∀i(Φ(n+i)→[n:=n+1]Φ(n+i))) → ∀iΦ(n+i). La modalità rimanente può essere ora eliminata con un ulteriore uso dell'assioma di Hoare per ottenere (Φ(n) ʌ ∀i(Φ(n+i)→Φ(n+i+1))) → ∀iΦ(n+i).

Senza modalità opache si può ora sostituire 0 a n nel modo usuale della logica del primo ordine per ottenere il celebre assioma di Giuseppe Peano (Φ(0) ʌ ∀i(Φ(i)→Φ(i+1))) → ∀iΦ(i), che prende il nome di Induzione matematica.

Una sottigliezza su cui abbiamo sorvolato qui è che ∀i dovrebbe essere interpretato come variare nell'intervallo dei numeri naturali, dove i è l'apice nell'espansione di a* come l'unione di aⁱ in tutti i numeri naturali i. L'importanza di orientarsi tra queste informazioni tipografiche diventa chiaro se n è di tipo intero, o perfino reale, per entrambi i quali A6 è un assioma perfettamente valido. Come nel caso in discussione se n è una variabile reale e Φ(n) è il predicato n è un numero naturale, allora l'assioma A6 dopo le prime due sostituzioni, cioè (Φ(n) ʌ ∀i(Φ(n+i)→Φ(n+i+1))) → ∀iΦ(n+i), è ancora valido, cioè vero, in ogni stato indipendentemente dal valore di n in tale stato, per esempio quando n è del tipo numero naturale. Se in un dato stato n è un numero naturale allora l'antecedente dell'implicazione principale di A6 vale, ma allora anche n+i è un numero naturale, e quindi vale anche il conseguente. Se n non è un numero naturale allora l'antecedente è falso, quindi A6 rimane vero indipendentemente dalla verità del conseguente. Si può rinforzare A6 a un'equivalenza p ∧ [a*](p → [a]p) ≡ [a*]p senza alcun impatto sugli elementi, essendo l'altra direzione dimostrabile da A5, da cui si vede che se l'antecedente di A6 diventa falso da qualche parte, allora il conseguente deve essere falso.

La logica dinamica associa a ogni proposizione p un'azione p? chiamata test. Quando vale p, il test p? agisce come NOP, senza cambiare nulla ma permettendo all'azione di proseguire. Quando p è falso, p? agisce come BLOCK. I test possono essere assiomatizzati nel modo seguente.

A8. [p?]q ≡ p→q

Il corrispondente teorema per <p?> è;

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

Il costrutto se p allora a altrimenti b si realizza in logica dinamica come (p?;a)∪(~p?;b). Questa azione esprime una scelta cauta: se vale p allora p?;a è equivalente ad a, laddove ~p?;b è equivalente a BLOCK, e a∪BLOCK è equivalente ad a. Ne segue che quando p è vero l'esecutore dell'azione può prendere solo il ramo sinistro, e quando p è falso quello destro.

Il costrutto mentre p esegui a si realizza come (p?;a)*;~p?. Si esegue p?;a zero o più volte e successivamente si esegue ~p?. Per tutto il tempo in cui p rimane vero, la~p? finale impedisce all'esecutore di terminare l'iterazione prematuramente, ma non appena diventa falso, ulteriori iterazioni del corpo p sono bloccate e l'esecutore allora non ha altra scelta che uscire attraverso il test~p?.

La proposizione di assegnamento casuale x:=? denota l'azione non deterministica di porre x a un valore arbitrario. [x:=?]p allora dice che p vale indipendentemente da quale valore abbia x, invece <x:=?>p dice che è possibile assegnare a x un valore che renda vero p. [x:=?] quindi ha lo stesso significato del quantificatore universale ∀x, mentre <x:=?> similmente corrisponde al quantificatore esistenziale ∃x. Quindi, la Logica del primo ordine può essere interpretata come la logica dinamica dei programmi di forma x:=?.

La logica modale è perlopiù interpretata in termini di semantiche del mondo possibile o strutture di Kripke. Queste semantiche portano naturalmente alla logica dinamica interpretando i mondi come stati di un computer applicati alla verifica di programmi, o stati del nostro ambiente nelle applicazioni di linguistica, IA, ecc. Un ruolo per le semantiche del mondo possibile è quello di formalizzare le nozioni intuitive di verità e validità, che a loro volta conducono alle nozioni di correttezza e completezza da definire nei sistemi di assiomi. Una regola di inferenza è corretta quando la validità delle sue premesse implica la validità della sua conclusione. Un sistema assiomatico è corretto quando tutti i suoi assiomi sono validi e le sue regole di inferenza sono corrette. Un sistema assiomatico è completo quando ogni formula valida è derivabile come teorema di quel sistema. Questi concetti si applicano a tutti i sistemi di logica inclusa quella dinamica.

La logica ordinaria o Logica del primo ordine ha due tipi di termini, rispettivamente asserzioni e dati. Come si può osservare dagli esempi precedenti, la logica dinamica aggiunge un terzo tipo di termini denotanti azioni. L'asserzione di logica dinamica [x:=x+1]x≥4 contiene tutti e tre i tipi: x, x+1, e 4 sono dati, x:=x+1 è un'azione, e x≥4 e[x:=x+1]x≥4 sono asserzioni. La Logica proposizionale è derivata dalla Logica del primo ordine omettendo i termini dati e ragiona solo attraverso proposizioni astratte, che possono essere semplici variabili proposizionali o atomi o proposizioni composte costruite con connettivi logici come and, or, not.

La logica proposizionale dinamica, o PDL, fu derivata dalla logica dinamica nel 1977 da Michael Fischer e Richard Ladner. La PDL miscela le idee alla base della logica proposizionale e della logica dinamica aggiungendo le azioni e omettendo i dati; ne segue che i termini della PDL sono azioni e proposizioni. L'esempio precedente della TV è espresso in PDL, mentre il successivo esempio relativo a x:=x+1 è in logica dinamica del primo ordine. PDL sta alla logica dinamica (del primo ordine) come la logica proposizionale sta alla logica di primo ordine.

Fischer e Ladner dimostrarono nel loro lavoro del 1977 che la soddisfacibilità della PDL era di complessità computazionale al massimo di tempo esponenziale non deterministico, e perlomeno di tempo esponenziale deterministico nel caso peggiore. Questo intervallo fu colmato nel 1978 da Vaughan Pratt, che dimostrò che la decidibilità della PDL in un tempo esponenziale deterministico. Nel 1977 Krister Segerberg propose una completa assiomatizzazione della PDL, precisamente ogni completa assiomatizzazione della logica modale K insieme con gli assiomi A1-A6 suddetti. Le prove di completezza per gli assiomi di Segerberg furono trovate da Gabbay, Parikh (1978), Pratt (1979), Kozen e Parikh (1981).

La logica dinamica fu sviluppata da Vaughan Pratt nel 1974 in alcune note di una lezione sulla verifica dei programmi come approccio per assegnare un significato alla Logica di Hoare esprimendo la formula di Hoare p{a}q come p→[a]q. L'approccio fu successivamente pubblicato nel 1976 come un sistema logico con pieni diritti. Il sistema è paragonabile al sistema di A. Salwicki di Logica Algoritmica e alla nozione di Edsger Dijkstra di trasformatore predicativo di più debole precondizione wp(a,p) con [a]p corrispondente al Dijkstrano wlp(a,p) di più debole precondizione liberale. Tali logiche comunque non esprimono alcuna connessione sia con la logica modale, con le semantiche di Kripke, con espressioni regolari, o con il calcolo delle relazioni binarie; la logica dinamica può quindi essere vista come un raffinamento della logica algoritmica e dei trasformatori predicativi che li collegano con le semantiche assiomatiche e di Kripke della logica modale così come ai calcoli delle relazioni binarie e le espressioni regolari.

La logica di Hoare, la logica algoritmica, le precondizioni più deboli e la logica dinamica sono tutte adeguate per discutere e ragionare sul comportamento sequenziale. Estendere queste logiche al comportamento concorrente è stato comunque problematico. Ci sono vari approcci ma tutti mancano dell'eleganza del caso sequenziale. Al contrario, il sistema di Logica temporale di Amir Pnueli del 1977, altra variante di logica modale che condivide molte caratteristiche comuni con la logica dinamica, differisce da tutte le succitate logiche per essere ciò che Pnueli ha caratterizzato come una logica endogena, essendo le altre logiche esogene . Con ciò Pnueli intese che le asserzioni della logica temporale sono interpretate in un contesto comportamentale universale in cui una singola situazione globale cambia col passare del tempo, laddove le asserzioni delle altre logiche vengono fatte esternamente alle azioni multiple delle quali parlano. Il vantaggio dell'approccio endogeno è che non fa ipotesi fondamentali su che cosa causa cosa con il passare del tempo. Invece una formula di logica temporale può parlare di due parti non correlate del sistema, perché in quanto non correlate evolvono tacitamente in parallelo. In effetti l'ordinaria congiunzione logica di asserzioni temporali è l'operatore di composizione concorrente della logica temporale. La semplicità di questo approccio alla concorrenza ha fatto sì che logica temporale sia la logica modale d'elezione per ragionare sui sistemi concorrenti, con i loro problemi di sincronizzazione, interferenza, indipendenza, punto morto, punto vivo, imparzialità, eccetera.

Questi aspetti della concorrenza possono apparire essere meno centrali in Linguistica, Filosofia e Intelligenza Artificiale, aree in cui la logica dinamica s'incontra più spesso attualmente.

Per un trattamento completo della logica dinamica si veda il libro di David Harel et. al. sotto citato.

• V.R. Pratt, "Semantical Considerations on Floyd-Hoare Logic", Proc. 17th Annual IEEE Symposium on Foundations of Computer Science, 1976, 109-121.
• D. Harel, D. Kozen, and J. Tiuryn, "Dynamic Logic". MIT Press, 2000 (450 pp).
• D. Harel, "Dynamic Logic", In D. Gabbay and F. Guenthner, (eds.), Handbook of Philosophical Logic, volume II: Extensions of Classical Logic, capitolo 10, pagine 497-604. Reidel, Dordrecht, 1984.

• Logica matematica
• Logica modale
• Logica proposizionale dinamica

• (EN) Nicolas Troquard & Philippe Balbiani, Propositional Dynamic Logic, in Edward N. Zalta (a cura di), Stanford Encyclopedia of Philosophy, Center for the Study of Language and Information (CSLI), Università di Stanford.
• Vaughan R. Pratt, Semantical Considerations on Floyd-Hoare Logic (PDF), su boole.stanford.edu. (original paper on dynamic logic)

Portale Matematica: accedi alle voci di Teknopedia che trattano di matematica