Home

Federica EU

1/17

Aniello Murano » 8.Semantica denotazionale del comando while di IMP

Denotazione di Com

Ricordiamo la sintassi dei comandi Com di IMP

c ::= skip | X:=a | c0;c1 | if b then c₀ else c₁ | while b do c

La semantica denotazionale per c 2 Com è una funzione

C«c¬ : ∑ → ∑

La denotazione di c 2 Com (semantica denotazionale C«c¬ per c) è una relazione tra stati, definita per induzione sulla struttura dei comandi.
Si noti che la funzione di valutazione è parziale C«c¬ : ∑ → ∑ in quanto su alcuni comandi la funzione può non essere definita (per esempio sui loop infiniti)

Denotazione di Com II

C«skip¬ = {(σ, σ) | σ 2 ∑}

C«X:=a ¬ = {(σ, σ[n/X]) | σ 2 ∑ & A«a₀¬σ = n }

C«c0;c1¬ = C«c1¬ ± C«c0¬ (si noti l’inversione in accordo alla regola di composizione)

C«if b then c0 else c₁¬ = {(σ, σ’) | B«b¬σ = true & (σ, σ’) 2 C«c₀¬} [
{(σ, σ’) | B«b¬σ = false & (σ, σ’) 2 C«c₁¬}

Particolarmente difficile è invece la valutazione del comando while per il quale è necessario utilizzare i concetti matematici del punto fisso introdotti nella lezione precedente.

Denotazione del while

Dalla semantica operazionale (II lezione) abbiamo osservato che esiste la seguente equivalenza:

Sia w ´ while b do c allora: w » if b then c;w else skip

Possiamo allora scriver la semantica del comando while utilizzando le regole precedenti nel seguente modo:

C«w¬ = C«if b then c;w else skip¬ =

{(σ, σ’) | B«b¬σ = true & (σ, σ’) 2 C«w¬ ± C«c¬} [
{(σ, σ’) | B«b¬σ = false} =
{(σ, σ’) | 9 σ”. B«b¬σ = true & (σ, σ”) 2 C«c¬ & (σ”, σ’) 2 C«w¬} [
{(σ, σ’) | B«b¬σ = false}

Come si vede, il termine w compare in entrambi i lati dell’uguaglianza (equazione ricorsiva). Dunque C«w¬ non ha una soluzione immediata.

Risolvere questa funzione equivale a calcolare un punto fisso di una funzione C«w¬=f(C«w¬).

Alcune osservazioni su f(C[w])

C«w¬ = C«if b then c;w else skip¬ =
{(σ, σ’) | 9 σ”. B«b¬σ = true & (σ, σ”) 2 C«c¬ & (σ”, σ’) 2 C«w¬}
[ {(σ, σ) | B«b¬σ = false}

Risolvere questa equazione equivale a calcolare un punto fisso di una funzione C«w¬=f(C«w¬).
C«w¬ è una unzione parziale C«w¬: ∑ → ∑.
C«c¬ è una unzione parziale C«c¬: ∑ → ∑.
Dunque, f è ottenuta eseguendo prima C«c¬ e poi C«w¬. Per cui, f è una funzione f: (∑ → ∑) ! (∑ → ∑). Questa osservazione chiarirà il formalismo utilizzato nelle prossime diapositive.

Idea di valutazione con fixpoint

Valutazione di while con fixpoint II

Nella lezione precedente abbiamo parlato di ordinamento parziale tra funzioni:
date due funzioni parziali I,J : ∑ → ∑, con I · J indichiamo che J raffina I o che J estende I
Tornando alla funzione parziale di while, si potrebbe pensare che ad ogni iterazione di un while si può raffinare la conoscenza della sua valutazione
Caso base: prima che b sia valutata, la conoscenza su C«w¬ è
C0«w¬ := ? : ∑ → ∑, che denota la funzione non definita in nessun stato. Quindi C0«w¬ corrisponde a nessuna informazione.

Valutazione di while con fixpoint III

Si supponga adesso di valutare b “false” in uno stato σ. Dunque la denotazione del while ritorna {(σ,σ)},
Questo ci permette di raffinare la nostra conoscenza del while da C₀«w¬ ad una nuova funzione parziale C₁«w¬ : ∑ → ∑, che è una funzione identità sugli stati σ in cui b è valutata “false”
Se invece b è valutato “true” in σ, il comando c viene valutato in σ. Supponendo che la sua valutazione sia {(σ,σ’)}, il risultato del while è rimandato alla valutazione del while stesso su σ’.
Se conosciamo anche la valutazione di b in σ’ possiamo raffinare la nostra conoscenza sul valore del while in C2«w ¬. In pratica se b è valutato “false” in σ’, il while termina, altrimenti si valuta c in σ’ e si itera con la valutazione del while. Chiaramente C1«w¬ · C2«w¬.
Iterando il processo, abbiamo una σ-catena C0«w¬ · C1«w¬ · … · Ck«w¬ · … di raffinamenti e un ordine parziale dove ? = C0«w¬

Valutazione di while con fixpoint IV

Osservazioni sulla definizione di f

Osserviamo ancora come la definizione di f tramite le regole
- - ; ! (σ,σ) if B«b¬σ = false
  - (σ”,σ’) ! (σ,σ’) if B«b¬σ = true & C«c¬σ = σ”
- permette di valutare ricorsivamente il comando iterativo w in σ.

Consideriamo i seguenti scenari di denotazione di b:
b denotata false in σ, allora la denotazione di w è (σ,σ)
b vale true in σ, e false in σ”. Siccome al secondo ciclo si utilizza la prima regola di f, risulta (σ”,σ’) = (C«c¬σ, C«c¬σ). Dunque la denotazione di w è (σ, C«c¬σ), e corrisponde ad f applicata ad f al passo ricorsivo precedente cioè su: b valutata false in C«c¬σ”.
b vale k volte “true” partendo da σ, e false la k+1-ma volta. Allora si applica k volte la seconda regola di f e poi una sola volta la prima. Dunque la valutazione di w in questo caso è data dalla funzione f applicata su f al passo ricorsivo precedente cioè su: b valutata k-1 true partendo da σ, e poi false dopo k-1 volte.

Ultima osservazione su f

Nel libro di testo, la funzione f è riferita come “operatore ⌈”. In seguito anche noi utilizzeremo indistintamente f e ⌈, riferendoci allo stesso operatore definito in questa lezione.

Denotazione del comando while

Fixpoint per C[w]

La denotazione di w è data dalla soluzione della funzione ricorsiva f(C«w¬) = C«w¬. Questo equivale a calcolare il suo fixpoint
Siano f⁰(?) = ? = C₀«w¬ e f¹(?) = f(f₀(?)) = C₁«w¬, allora possiamo definire induttivamente
f^k(?) = f(f^k-1(?)) = C^k«w¬ come il risultato di k composizioni di f.
La funzione f è continua e dunque, esiste il fixpoint di f è corrisponde al “least upper bound” della catena.
Un modo alternativo per legare la valutazione del while “least upper bound” della catena fⁱ(?) è dato dal theorema di Tarski

Teorema di Tarski

Ricapitolando

Se ho un comando iterativo la cui denotazione è data una funzione ricorsiva di cui non so a priori il numero delle iterazioni, definisco un operatore di punto fisso, cioè una funzione (ricorsiva) il cui punto fisso è proprio la denotazione del comando.

Provo dunque a definire l’operatore tramite un insieme di regole

Se queste regole hanno premesse finite e positive, allora posso applicare il teorema di Tarski e concludere che la semantica del comando è il l.u.b. della catena ottenuta applicando iterativa-mente le regole che definiscono l’operatore.