Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
vuoi
o PayPal
tutte le volte che vuoi
Semantica concreta
Considereremo un linguaggio pseudo-funzionale di base piuttosto che un linguaggio imperativo nello stile While.
Iniziamo da un linguaggio molto limitato, che permette unicamente di moltiplicare interi.
Exp ::= n | e*e
La semantica di questo linguaggio si può descrivere mediante una funzione definita da:
ηZ: Exp !η = n
η(n) *e ) = )£η(e )η(e η(e1 2 1 2 8
Semantica astratta
Possiamo considerare un'astrazione della semantica concreta (semantica astratta) che calcola solo il segno delle espressioni
Exp {-,0,+}!σ: a - 0 +£
- se n<0
- + 0 -= 0 se n=0
σ(n) 0 0 0 0
+ se n>0
+ - 0 +*e ) = ) )a£σ(e σ(e σ(e1 2 1 2 9
Correttezza
Possiamo dimostrare che questa astrazione è corretta, ovvero che prevede correttamente il segno delle espressioni.
La dimostrazione è per induzione strutturale sull'espressione e semplicemente utilizza le proprietà
della moltiplicazione tra interi (il prodotto di due positivi è positivo, etc.). Per ogni espressione e ∈ Exp: < 0 = -, η(e) σ(e) = 0 = 0, η(e) σ(e) > 0 = +, η(e) σ(e) Una prospettiva diversa • Possiamo associare ad ogni valore astratto l'insieme di valori concreti che esso rappresenta: P(Z) γ: {-,0,+} Z = {x² | x < 0} γ(-) = {0} γ(0) Z = {x² | x > 0} γ(+) = {0} Concretizzazione • La funzione di concretizzazione mappa un valore γ astratto in un insieme di valori concreti • Indichiamo con D il dominio concreto dei valori e con A il dominio astratto A σ γ Exp η(e)² γ(σ(e)) η D {•} P(D) Interpretazione Astratta • Abbiamo specificato una interpretazione astratta. - Computazioni astratte in un dominio astratto - In questo caso, il dominio astratto è {+,0,-}. • La semantica astratta è corretta - È un'approssimazione della semanticaconcretaη(e) µ γ(σ(e))• La funzione di concretizzazione stabilisce la relazione tra il concetto di approssimazione nei due domini concreto ed astratto 13Aggiungiamo -• Aggiungiamo al nostro tiny language l'operatore unario di cambiamento di segnoExp e ::= n | e*e | -e3= -η(e)η(-e) = - dove - (-) = +, - (0) = 0, - (+) = -a a a aσ(-e) σ(e) 14Aggiungiamo +• Aggiungere l'addizione è più complesso, in quanto il dominio astratto non è chiuso rispetto a questa operazione+a - 0 ++ e ) = ) + )η(e η(e η(e1 2 1 2 - - - ?+ e ) = ) + )aσ(e σ(e σ(e 0 - 0 +1 2 1 2 + ? + +• A quale valore astratto corrisponde il risultato della somma di due numeri interi con segno opposto? 15Soluzione• Aggiungiamo un nuovo valore astratto che rappresenta un qualsiasi numero intero+a - 0 + >- - - > >Z=γ(>) 0 - 0 + >+ + +> >> > > > > 16Estendere lealtre operazioni• Avendo aggiunto un elemento al dominio astratto, ènecessario estendere le operazioni astratte giàdefinitea - 0 + - (-) = +, - (0) = 0,a a£ > - (+) = -, - (>) =a a >- + 0 - >0 0 0 0 0+ - 0 + >0> > > > 17
EsempiIn alcuni casi c’è perdita di informazione dovuta alle operazioni• - 3) = 0η((1+2) -3) = (+ + +) + - = + + - =a a a >σ((1+2)+In altri casi non c’è perdita di informazione• + 6) = 26η((5*4) + 6) = (+ +) + + = + + + = +a a a£σ((5*4) 18
Aggiungiamo la divisione• Aggiungere la divisione intera / non crea problemi, eccetto il caso delladivisione per 0• Se dividiamo un insieme di interi per 0 che risultato otteniamo?L’insieme vuoto. Quindi la semantica concreta assumera` i propri valoriZ,sul powerset di cioe` ! P(Z)η:Exp• L’insieme vuoto di interi è rappresentato da un nuovo elemento ⊥astratto rispetto al quale
si devono estendere le altre operazioni/ - 0 +a > ⊥ + x = = x +a a- + 0 - > ? ? ?⊥γ(?)=; x = = xa a0 ? £ ? £ ?? ⊥ ⊥ ⊥ ⊥ - (?) =a ?+ - 0 + > ⊥0> > > > ⊥⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 19Il dominio astratto• Il dominio astratto è un poset incui l’ordine parziale rappresenta >la nozione di approssimazione/precisione• L’ordine parziale è coerente con 0- +la funzione di concretizzazione:x y· , µγ(x) γ(y) ?• Ogni sottoinsieme ha un lub edun glb: è quindi un reticolocompleto 20La funzione di astrazione• Alla funzione di concretizzazione corrisponde unaγfunzione di astrazione α.• La funzione mappa un insieme S di valori concretiαnel piu` preciso valore astratto che rappresenta S.• Nel nostro esempio se S =? ; Z- se S S;, µ≠ <0A = 0 se S = {0}!α:P(Z) α(S) Z+ se S S;,
µ≠ >0altrimenti> 21Definizione Generale• Una Interpretazione Astratta consiste in:– Un dominio astratto A ed un dominio concreto C– A e C reticoli completi. L’ordine riflette la precisione/approssimazione (più piccolo = più preciso)– Funzioni di concretizzazione e di astrazione monotone, cheformano una inserzione di Galois.– Operazioni astratte che astraggono correttamente su A lasemantica concreta su C.
• Inserzione di Galois: funzioni monotone e taliα:C!A γ:A!Cche: C. c8c 2 · γ(α(c))CA. a =8a 2 α(γ(a)) 22Altro esempio(x) =γ sign , se x =; ?• >{y2Z|y>0}, se x = +• {y2Z|y≥0}, se x = 0+ 0- 0+• {0}, se x = 0• 0{y2Z|y≤0}, se x = 0- - +• {y2Z|y<0}, se x = -• se x =Z, >• ?= glb diα (S)sign se S = ({0,1,3})= 0+α?, ∅• sign-, se S {z2Z|z < 0} (0+) ⊇ {0,1,3}, {3,5,2}, ...⊆• γ sign0-
GC e` una Galois insertion (GI) seγ)vale una delle seguenti condizioni equivalenti: 1) suriettivaα 2) iniettivaγ 3) = a8a2A. α(γ(a)) 25Aggiunzioni(α, C, A, aggiunzione seγ)1) A e C poset 2) A (astrazione)!α:C 3) : A C (concretizzazione)!γ 4) a c8c2C. 8a2A. · , ·α(c) γ(a) CFATTO: (α,C,A,γ) GC (α,C,A,γ) aggiunzione, 26Galois Insertion: proprieta`(α, C, A, GC e` una Galois insertion (GI) seγ)vale una delle seguenti condizioni equivalenti: 1) suriettivaα 2) iniettivaγ 3) = a8a2A. α(γ(a))GI tra reticoli completiγ)(1) = | cÆ{a2A ·α(c) γ(a)}C(2) = | a}Ç{c2C ·γ(a) α(c) A(3) QUINDI: determina e viceversaα γ(4) preserva i lub’sα(5) preserva i glb’sγ(6) ) = e ) =? >α(? γ(>C A A C(7) se una funzione tra reticoli completi preserva i lub’s alloraC Aα : !posso definire la come in (2) che forma con una GIγ α(8) se una funzione preserva i glb’s allora posso definire laA Cγ : α!come in (1) che forma con una GIγ 27Galois Insertion: proprieta`Come "trasformare" una GC (α, C, A, in una GI eliminando i valoriγ)astratti "inutili"?Semplicemente considero come dominio astratto "ridotto" (reduced)A = e considero le restrizioni delle medesime funzioni dired α(C)astrazione e concretizzazione:: C A dove (c) =red red red!α α α(c): A C dove (a) =red red red!γ γ γ(a)Banalmente,(α , C, A , ) e' diventata una GI con lo stesso red γ"potere espressivo" della GC di partenza. 28Astrazioni come chiusure• Il dominio astratto specificato come una GI (α,C,A,γ) induce una partizione del dominio concreto:c c ) = )» , α(c α(c1 2 1 2• Per ogni classe di equivalenza [c] esiste il lub, cioe' »ogni classe di equivalenza ha un rappresentante canonico• La funzione C che mappa un valore concreto cρ:C!a questo rappresentante [c] e' un operatore di Ç c »chiusura su C 29Chiusure• Un operatore : C C su un poset C e'!ρuna chiusura se:– e' monotonaρ– e' crescente: x ·ρ ρ(x)– e' idempotente: =ρ ρ(ρ(x)) ρ(x)• uco(C) denota l'insieme di tutte le chiusuresu C 30Chiusure e GI• Una GI (α,C,A,γ) induce una chiusura :C!CρAdefinita come: [c],(c) = {x2C | =Ç Çρ
γ±α(c) α(x)·α(c)} cA C »• Una chiusura C su un reticolo completo C!ρ:Cinduce una GI (ρ,C,img (C),id)ρ• Queste due trasformazioni sono una l’inversadell&r γ±α(c) α(x)·α(c)} cA C »• Una chiusura C su un reticolo completo C!ρ:Cinduce una GI (ρ,C,img (C),id)ρ• Queste due trasformazioni sono una l’inversadell&r