Punti Fissi
Mappe tra insiemi parz. ordinati
Siano (P,P) e (Q,Q) due insiemi parzialmente ordinati. Una
funzione j da P a Q si dice:
monotona (preserva l’ordine) se
p1 P p2 jp1Q jp2
embedding se
p1 P p2 jp1Q jp2
isomorfismo se è un embedding suriettivo
Tino Cortesi
Tecniche di Analisi di Programmi
2
Esempi
b
d
a
c
j1a
j1d
j1b=j1c
j1 non è una funzione
monotona
j2d=j2e
j2b=j2c
j2a
j2 è una funzione
monotona, ma non è un
embedding:j2bQj2cma
non è vero che bPc
e
d
b
c
a
Tino Cortesi
Tecniche di Analisi di Programmi
3
Esempi
e
d
b
c
j3 è una funzione
monotona, ma non è un
embedding:j3bQj3cma
non è vero che bPc
j3e
j3c=j3d
j3a=j3b
a
j4d
d
b
c
a
Tino Cortesi
j4c
j4b
j2 è un embedding, ma non
è un isomorfismo.
j4a
Tecniche di Analisi di Programmi
4
Catene Convergenti
Ricordiamo che una sequenza (ln)nN di elementi di L è una
catena ascendente se
n  m  ln lm
Una sequenza (ln)nN converge se e solo se
$ n0N : "nN : n0  n ln0 = ln
Un insieme parzialmente ordinato (L,) soddisfa la condizione
sulle catene ascendenti se e solo se ogni catena ascendente di L
converge.
Tino Cortesi
Tecniche di Analisi di Programmi
5
Esempio
12
10
8
L’insieme ordinato dei
numeri pari non soddisfa la
condizione sulle catene
ascendenti
6
4
2
0
Tino Cortesi
Tecniche di Analisi di Programmi
6
Esempio
Questo insieme ha un
numero infinito di elementi
Non ha lunghezza finita
Soddisfa la condizione sulle
catene ascendenti
...
Tino Cortesi
Tecniche di Analisi di Programmi
7
Continuità
In Analisi, una funzione si dice continua se preserva i limiti.
Dati due ordini parziali (P,P) e (Q,Q), una funzione j da P a Q
si dice continua se per ogni insieme diretto S in P
jlubS=lub{ j(x) | xS }
(P,P)
j
S
Tino Cortesi
(Q,Q)
j(S)
Tecniche di Analisi di Programmi
8
Continuità
Non tutte le funzioni monotone sono continue.
Ad esempio,
j :NN
jS) = se S è finito,
N altrimenti
è monotona (se S1  S2 e S2 è finito, anche S1 è finito)
ma non è continua: se si prende l’insieme diretto
D = {X N | X è finito}
si ha:
lub {j(X) | X in D} = 
perché ogni X in D è finito
j(lub (D)) = N
perché D è infinito
Tino Cortesi
Tecniche di Analisi di Programmi
9
Punti Fissi
Sia f una funzione monotona f: (P,P) (P,P) su un insieme
parzialmente ordinato P.
Un elemento x di P si dice punto fisso di f se f(x)=x.
L’insieme dei punti fissi di f è un sottoinsieme di L chiamato
Fix(f):
Fix(f) ={ l L | f(l)=l}
Tino Cortesi
Tecniche di Analisi di Programmi
10
Punti fissi sui CPO
Sia f una funzione monotona f: (P,P) (P,P) su un insieme
completo parzialmente ordinato (CPO) P.
Sia a= n0 f n(^)
Se aFix(f) allora a= lfp(f)
Teorema di Kleene
Se f è continua allora il minimo punto fisso di f esiste ed è
uguale ad a.
Tino Cortesi
Tecniche di Analisi di Programmi
11
Punti fissi sui CPO
T
Fix(f) ={ l L | f(l)=l}
lfp(f) =
n0
fn(^)
f i(^)
^
Tino Cortesi
Tecniche di Analisi di Programmi
12
Punti Fissi sui reticoli completi
Sia f una funzione monotona f:LL su un reticolo completo
L.
Fix(f) è anch’esso un reticolo completo:
lfp(f) = glb(Fix(f))
gfp(f) = lub(Fix(f))
Fix(f)
Fix(f)
Teorema di Tarski:
Sia L un reticolo completo. Se f:LL è una funzione
monotona allora
lfp(f) = glb{ l L | f(l)  l }
gfp(f) = lub{ l L | l  f(l) }
Tino Cortesi
Tecniche di Analisi di Programmi
13
Punti fissi sui reticoli completi
Red(f) ={ l L | f(l) P l}
gfp(f) = lub{ l L | l  f(l) }
Fix(f) ={ l L | f(l)=l}
lfp(f) = glb{ l L | f(l)  l }
Ext(f) ={ l L | l P f(l)}
Tino Cortesi
Tecniche di Analisi di Programmi
14
Dimostriamo che se L è un reticolo completo lub{xL | x f(x)} è
un punto fisso di L (il greatest fix point).
Sia H={xL | x f(x)}, e sia a=lub(H). Dimostriamo che a=f(a).
Per ogni hH, h f(h), per definizione di H.
E vale anche h a (perché a è un upper bound di H).
Quindi h f(h) f(a): la prima relazione segue dal fatto che hH e la
seconda dalla monotonia di f.
Poiché h f(a) vale per ogni hH, f(a) è un upper bound dell’insieme H.
E poiché a è il lub(H), ne segue che a f(a).
Per dimostrare che a è un punto fisso, dobbiamo dimostrare che anche il
viceversa vale, ovvero che f(a) a.
Applichiamo f ad entrambi i termini dell’espressione a f(a) che abbiamo
dimostrato essere vera.
Per monotonia abbiamo che f(a)f(f(a).
Ma allora f(a)H, e quindi f(a) lub(H) = a, e quindi f(a) a.
Tino Cortesi
Tecniche di Analisi di Programmi
15
Esistenza di punti fissi nei CPO
Teorema I
Sia f: (P,P) (P,P) una funzione su un insieme completo
parzialmente ordinato P tale che per ogni x in P: x P f(x).
Allora f ha un punto fisso.
Teorema II
Sia f: (P,P) (P,P) una funzione monotona su un insieme
completo parzialmente ordinato P.
Allora f ha un punto fisso.
Tino Cortesi
Tecniche di Analisi di Programmi
16
Punti Fissi
Ci sono quindi tre risultati che garantiscono l’esistenza di punti
fissi:
1. Funzione continua su CPO
2. Funzione monotona su reticoli completi
3. Funzione monotona su CPO
I primi due hanno ipotesi più forti e offrono una formula per
calcolare il minimo punto fisso. Il terzo garantisce solo
l’esistenza di un punto fisso.
Tino Cortesi
Tecniche di Analisi di Programmi
17
Widening
Un operatore : (P,P) (P,P) si dice operatore di widening se
e solo se:
È un operatore di upper bound, ovvero l1,l2 P (l1,l2)
Per ogni catena (ln)n0, la catena
(ln)n0 = (l0’=l0, l1’=(l’0,l1),… )
converge dopo un numero finito di passi
Tino Cortesi
Tecniche di Analisi di Programmi
18
Esempio
Si consideri il reticolo completo
Int = {^}  {[a,b] | a  b & aZ{-}, bZ{+}}
dove l’ordinamento è l’inclusione tra intervalli.
Sia K un elemento fissato di Int
Definiamo l’operatore WK: (Int,Int)  Int
[min(a,c),max(b,d)] se [min(a,c),max(b,d)]  K
WK([a,b], [c,d]) =
[-, +]
altrimenti
Se K=[-2,4]: W[-2,4] è un operatore di widening
Alla catena
corrisponde la catena
Tino Cortesi
[0,0], [0,1], [0,2], [0,3], [0,4], [0,5], [0,6],…
[0,0], [0,1], [0,2], [0,3], [0,4], [-, +], [-, +],…
Tecniche di Analisi di Programmi
19
Esempio
Si consideri il reticolo completo
Int = {^}  {[a,b] | a  b & aZ{-}, bZ{+}}
dove l’ordinamento è l’inclusione tra intervalli.
Sia K un elemento fissato di Int
Definiamo l’operatore WK: (Int,Int)  Int
[min(a,c),max(b,d)] se [min(a,c),max(b,d)]  K
WK([a,b], [c,d]) =
[-, +]
altrimenti
Se K=[0, +]: W[0, +] non è un operatore di widening
Alla catena
corrisponde la catena
Tino Cortesi
[0,0], [0,1], [0,2], [0,3], [0,4], [0,5], [0,6],…
[0,0], [0,1], [0,2], [0,3], [0,4], [0,5], [0,6],…
che non converge!
Tecniche di Analisi di Programmi
20
Widening e punti fissi
lfp
widening
Tino Cortesi
Tecniche di Analisi di Programmi
21
Widening e punti fissi
Sia f una funzione monotona f: (P,P) (P,P) su un reticolo
completo, e dato un operatore di widening  su (P,P),
possiamo calcolare la catena ascendente:
f n=
^
se n=0
f n-1
se n>0 e f(f n-1) P f n-1
f(f n-1)  f n-1
altrimenti
Questa catena ascendente converge in un numero finito di
passi.
Tino Cortesi
Tecniche di Analisi di Programmi
22
Widening
T
f m= f m+1= …
Fix(f) ={ l L | f(l)=l}
lfp(f)
f 2
f 1
^
Tino Cortesi
Tecniche di Analisi di Programmi
23
A che serve tutto questo?
Abbiamo detto che l’approccio all’analisi di programmi che
consideriamo è basato sulla semantica
Semantica = assegnare ad ogni costrutto linguistico il suo
significato
Ogni semantica di un programma può essere espressa come
soluzione di un’equazione di minimo punto fisso.
Tino Cortesi
Tecniche di Analisi di Programmi
24
Sintassi e Semantica
Ci sono modi diversi per definire la semantica di un programma
scritto in un dato linguaggio di programmazione:
Semantica Operazionale:
la semantica di un costrutto linguistico viene espressa in termini dei
passi di computazione che possono aver luogo durante l’esecuzione del
programma
Semantica Assiomatica
la semantica viene definita indirettamente attraverso assiomi e regole
di una qualche logica
Semantica Denotazionale
fornisce modelli matematici ai linguaggi di programmazione: associa ad
ogni costrutto linguistico del programma un elemento di una struttura
matematica
Tino Cortesi
Tecniche di Analisi di Programmi
25