Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

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 f0(?) = ? = C0«w¬ e f1(?) = f(f0(?)) = C1«w¬, allora possiamo definire induttivamente
  • fk(?) = f(fk-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 fi(?) è 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 ´ a1 + a2.
  • Se (σ, n) 2 A«a1 + a2 ¬ allora esistono (σ, n1) 2 A«a1¬ & (σ, n2) 2 A«a2¬ tale che n=n1+n2. Allora per induzione < a1, σ> ! n1 e < a2, σ > ! n2, dunque < a1 + a2, σ > ! n.
  • Se < a1 + a2, σ > ! n allora esiste una derivazione con sottoderivazioni < a1, σ > ! n1 e < a2, σ > ! n2 tale che n=n1+n2. Allora, per induzione (σ, n1) 2 A«a1¬ & (σ, n2) 2 A«a2¬, dunque (σ, n) 2 A«a2 +a2¬.
  • Per a ´ a1 - a2 e a ´ a1 * a2 ragionamento analogo al precedente.

Equivalenza per Bexp


Equivalenza per Bexp


  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion