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
Isomorfismo
j’
j
i
g
g’
h
f
d
h’
i’
d’
e’
f’
e
a
a’
c
Tino Cortesi
b’
b
Tecniche di Analisi di Programmi
c’
5
Monotona? Embedding? Isomorfismo?
j da (Z, ) a (Z, ), definita come segue: j(x)=x+1
j da ((S), ) a
1
0
, definita come segue:
j(U)=1 se U contiene almeno un elemento, j()=0.
j da ((Z), ) a ((Z), ) , definita come segue:
j(U)={1} se 1 U
j(U)={2} se 2 U e 1 non appartiene a U
j(U)= altrimenti
Tino Cortesi
Tecniche di Analisi di Programmi
6
Teorema (Dedekind)
Per ogni insieme parzialmente ordinato E esiste un embedding
in un reticolo completo L tale che i lub ed i glb che esistono in E
sono preservati in L.
La dimostrazione generalizza il metodo d Dedekind per ottenere
l’insieme dei numeri reali a partire dai numeri razionali.
Tino Cortesi
Tecniche di Analisi di Programmi
7
Catene Ascendenti e Discendenti
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 (ACC) se e solo se ogni catena
ascendente di L converge.
Dualmente si definisce la condizione sulle catene discendenti
DCC
Tino Cortesi
Tecniche di Analisi di Programmi
8
Esempio
12
10
8
6
4
L’insieme ordinato dei
numeri pari non soddisfa la
condizione sulle catene
ascendenti
Ma soddisfa la condizione
sulle catene discendenti
2
0
Tino Cortesi
Tecniche di Analisi di Programmi
9
Esempio
Questo insieme ha un
numero infinito di elementi
Ha altezza finita
Soddisfa la condizione sulle
catene ascendenti e sulle
catene discendenti
...
Tino Cortesi
Tecniche di Analisi di Programmi
10
Esempio
...
...
...
Questo insieme ha un
numero infinito di elementi
Ha altezza finita
Soddisfa la condizione sulle
catene ascendenti e sulle
catene discendenti
...
Tino Cortesi
Tecniche di Analisi di Programmi
11
Esempio
...
...
...
...
Tino Cortesi
Questo insieme ha un
numero infinito di elementi
Non ha altezza finita
NON soddisfa la condizione
sulle catene ascendenti ACC
Soddidfa la condizione sulle
catene discendenti DCC
Tecniche di Analisi di Programmi
12
Reticoli e ACC
Se P è un reticolo, ha un bottom element e soddisfa ACC, allora
è un reticolo completo
Dimostrazione
Sia (P,P) un reticolo che ha un bottom element e soddisfa ACC.
Dimostriamo che per ogni sottoinsieme non vuoto X di P esiste
un sottoinsieme finito F di X tale che lub(F)=lub(X).
Consideriamo
Y={lub(H) | H è un sottoinsieme non vuoto e finito di X}
Poiché X è non vuoto, anche Y è non vuoto, ed essendo un
sottoinsieme di P, che soddisfa ACC, ha un elemento massimale
m.
Tino Cortesi
Tecniche di Analisi di Programmi
13
Quindi m = lub(F) per un qualche sottoinsieme finito F  X.
Prendiamo ora xX. Abbiamo che lub(F {x}) Y e che
m=lub(F) lub(F {x})  m, poiché m è massimale in Y.
Quindi per la proprietà antisimmetrica, m=lub(F)=lub(F {x}).
Questo implica in particolare che x  m, per definizione di lub, e poiché
questo vale per ogni xX, m è un upper bound di X.
Consideriamo ora un altro upper bound u di X. Allora u è un upper
bound anche di F, perché F  X, e quindi m=lub(F)  u.
Questo prova che m è il least upper bound di X, ovvero che
lub(X)=m=lub(F).
Se P ha un elemento bottom e soddisfa ACC, lub(X) esiste per ogni
sottoinsieme non vuoto X di P, quindi P è un reticolo completo.
T
Si dimostra anche che Se P è un reticolo che non ha catene
infinite, allora è completo
Tino Cortesi
Tecniche di Analisi di Programmi
14
Continuità
In Analisi Matematica, una funzione si dice continua se preserva
i limiti. Sui posets possiamo esprimere una proprietà simile.
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
15
Continuità
Se P e Q sono CPO, le proiezioni p1: PxQ P e p2: PxQ Q
definite da: p1(x,y)=x, p2(x,y)=y
sono relazioni continue
Dimostrarlo per esercizio!
Tino Cortesi
Tecniche di Analisi di Programmi
16
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
17
Punti Fissi
Sia f una funzione 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
18
Esempio
f
d
c
b
Fix(f)={b,c}
a
Tino Cortesi
Tecniche di Analisi di Programmi
19
Minimo e Massimo punto fisso
Sia f una funzione f: (P,P) (P,P) su un insieme parzialmente
ordinato P.
Un elemento x di Fix(f) si dice minimo punto fisso di f, se per
ogni yP, se y=f(y), allora xPy.
Se il minimo punto fisso di una funzione esiste, è unico, e lo si
denota con lfp(f).
Un elemento x di Fix(f) si dice massimo punto fisso di f, se per
ogni yP, se y=f(y), allora yPx.
Se il massimo punto fisso di una funzione esiste, è unico, e lo si
denota con gfp(f).
Tino Cortesi
Tecniche di Analisi di Programmi
20
Esempio
f
d
lfp(f)={c}
gfp(f)={d}
c
b
a
Tino Cortesi
Tecniche di Analisi di Programmi
21
Esempio
Consideriamo l’insieme dei naturali positivi, e la funzione fact(k)
definita da:
fact(k) = 1
se k=0
fact(k) = k*fact(k-1) se k>0
Ad ogni funzione f dagli interi positivi agli interi positivi
possiamo associare una nuova funzione f’ definita come segue:
f’(k) = 1
se k=0
f’(k) = k*f(k-1) se k>0
In altre parole abbiamo una funzione
F:(N0 N0)  (N0 N0) definita da: F(f)=f’.
fact è un punto fisso di questa funzione F. Infatti F(fact)=fact.
Tino Cortesi
Tecniche di Analisi di Programmi
22
Esempio
xn+1 = cos xn con valore iniziale x1 = -1.
La funzione converge a 0.73908513…, il punto dove il grafico
della funzione cos interseca la retta y = x.
Tino Cortesi
Tecniche di Analisi di Programmi
23
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
24
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
25
Esempio
Abbiamo visto prima che fact è punto fisso del funzionale F. Si può
dimostrare che F è continua nel CPO delle funzioni N0 N0.
Abbiamo che:
F(^)={(0,1)}
F({(0,1)})= {(0,1),(1,1)}
F({(0,1),(1,1)})={(0,1),(1,1),(2,2)}
…
Questa sequenza approssima sempre più fact, che infatti
costituisce il least upper bound di essa.
Tino Cortesi
Tecniche di Analisi di Programmi
26
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
27
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
28
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
29
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
30
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
31
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
32
Esempio
Si consideri il reticolo completo
Int = {^}  {[a,b] | a  b & aZ{-}, bZ{+}}
dove l’ordinamento è l’inclusione tra intervalli.
Sia K=[-k,k] con 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
33
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
34
Widening e punti fissi
lfp
widening
Tino Cortesi
Tecniche di Analisi di Programmi
35
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
36
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
37
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
38
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
39
Esercizio
Per la seguente funzione f: N0 N0, costruisci un funzionale
F:(N0 N0)  (N0 N0) i cui punti fissi soddisfino la
specifica. Dimostra che F è monotona, e descrivi F(^), F(F(^)),
F(F(F(^))) e n0 F n(^)
f(k) = 1
se k =1
(2k -1)+f(k-1) altrimenti
Tino Cortesi
Tecniche di Analisi di Programmi
40
Esercizio
Sia S il CPO di tutte le stringhe che si possono costruire
sull’alfabeto {0,1}.
Data una stringa u ed una stringa v, denotiamo con uv la stringa
ottenuta concatenando le due stringhe.
Sia F:S S la funzione definita da F(u)=01u
Qual è l’unica soluzione dell’equazione di punt fisso F(u)=u?
Verificare che questa è proprio la soluzione che si ottiene
n
prendendo la stringa vuota e costruendo
n0F ()
Tino Cortesi
Tecniche di Analisi di Programmi
41