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
 
I corsi di Scienze Matematiche Fisiche e Naturali
 
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