Aniello Murano » 9.Equivalenza delle semantiche operazionale e denotazionale di Aexp e Bexp di IMP

Riepilogo

Definizione di un Linguaggio Formale

Un linguaggio formale, qual è un linguaggio di programmazione, deve essere definito in modo chiaro, preciso e completo,
Una specifica chiara precisa e completa è necessaria sia per chi deve costruire compilatori e/o interpreti del linguaggio, sia per chi deve scrivere programmi.
Descrivere con precisione un linguaggio significa definirne con precisione sintassi e semantica.
La sintassi specifica sia la struttura lessicale del linguaggio (come costruire le parole a partire dai caratteri dell’alfabeto) sia le regole per la costruzione delle frasi (programmi sintatticamente corretti).
La semantica specifica il significato delle frasi (programmi).

Semantiche considerate

Nelle lezioni precedenti abbiamo introdotto il linguaggio imperativo IMP e per questo linguaggio abbiamo mostrato una Sintassi basata su regole di composizione (BNF) e due tipi di semantiche:
Semantica operazionale:
- associa alle frasi del linguaggio operazioni eseguite da una macchina astratta.
Semantica denotazionale:
- associa alle frasi del linguaggio funzioni matematiche.
Semantica assiomatica (solo accennata):
- associa alle frasi del linguaggio formule logiche.

Semantica denotazionale

Al linguaggio IMP sono associate le seguenti funzioni:
- A: Aexp ! (Σ ! N);
- B: Bexp ! (Σ ! {true, false}),
- C: Com ! (Σ !Σ )
Per esempio, se la denotazione di X è data da (σ, σ(X)), la valutazione di X in uno stato σ è data da A«X¬(σ)= σ(X)
Per i comandi, questo ragionamento può dare luogo a difficoltà.
Per esempio, sia w ´ while b do c. Abbiamo visto che C«w¬ = {(σ,σ’) | B«b¬σ = true & (σ,σ’) 2 C«w¬ ± C«c¬} [ {(σ,σ) | B«b¬σ = false} non da la denotazione di w, perché C«w¬ è una funzione ricorsiva.
In pratica, la denotazione di w è data dalla sua denotazione al prossimo ciclo concatenata alla denotazione del comando c.
Questo ragionamento suggerisce una funzione continua f: (Σ ! Σ) ! (Σ ! Σ) il cui fixpoint (corrispondente all’eventuale termine del ciclo while) fornisce la denotazione di w.

Denotazione del comando while

Sia C«w¬ =

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

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

C«w¬ è una funzione ricorsiva e la sua soluzione è data dal punto fisso di una funzione f(C«w¬) = C«w¬. Tale funzione è definita dal seguente schema di regole

Vedi figura.

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(?)) = Ck«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

Dato un insieme definito da un insieme di regole, se
1. Le premesse delle regole sono positive. Cioè non hanno forma ¬α/β
2. Le premesse delle regole sono in numero finito allora l’operatore f è continuo.
Se le condizioni del Teorema di Tarski sono soddisfatte allora (vedi figura).
È possibile provare che la regola 1 da sola garantisce univocamente la monotonicità di f.
È utile notare che il risultato ottenuto sfrutta il fatto che f è una funzione tra potenze di insiemi (insiemi di possibili coppie di stati) e l’insieme potenza con la relazione di inclusione è un c.p.o.

Ricapitolando

Se ho un comando iterativo la cui denotazione è data una funzione ricorsiva, provo a definire un insieme di regole per la funzione.
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 la funzione.

Schema delle prossime lezioni

In questa lezione: Equivalenza della semantica operazionale e denotazionale di Aexp e Bexp + Esercitazione su semantiche dei comandi.
Prossima lezione: Equivalenza della semantica operazionale e denotazionale di Com + Esercitazione.
Lezione successiva: Esercitazione alla prova di verifica.

Equivalenza delle semantiche

In questa lezione mostriamo l’equivalenza della semantica operazionale con quella denotazionale per il linguaggio IMP.
Per provare l’equivalenza delle due semantiche occorre dimostrare che:
- per ogni a 2 Aexp, (σ, n) 2 A«a¬ , < a, σ > ! n (questa lezione);
- per ogni b 2 Bexp, (σ, t) 2 B«b¬ , < b, σ > ! t (questa lezione);
- per ogni c 2 Com, (σ, σ’) 2 C«c¬ , < c, σ > ! σ’ (prossima lezione).

Equivalenza per Aexp

Dimostriamo per induzione strutturale che per ogni a 2 Aexp vale la proprietà P(a)

(σ, n) 2 A«a¬ , < a, σ > ! n

Sia a ´ m. Allora (σ, n) 2 A«m¬ , m = n , < m, σ > ! n
Sia a ´ X. Allora (σ, n) 2 A«X ¬ , n = σ(X) , < X, σ > ! n
Sia a ´ a₁+ a₂.
Se (σ, n) 2 A«a1 + a2 ¬ allora esistono (σ, n₁) 2 A«a1¬ & (σ, n₂) 2 A«a2¬ tale che n=n1+n2. Allora per induzione < a₁, σ> ! n₁ e < a₂, σ > ! n2, dunque < a₁ + a₂, σ > ! n.
Se < a₁ + a₂, σ > ! n allora esiste una derivazione con sottoderivazioni < a₁, σ > ! n₁ e < a₂, σ > ! n₂ tale che n=n₁+n₂. Allora, per induzione (σ, n₁) 2 A«a₁¬ & (σ, n₂) 2 A«a₂¬, dunque (σ, n) 2 A«a₂ +a₂¬.
Per a ´ a₁- a₂ e a ´ a₁ * a₂ ragionamento analogo al precedente.