Punti Fissi

Tino Cortesi Tecniche di Analisi di Programmi 2

Mappe tra insiemi parz. ordinati

Siano (P,P) e (Q,Q) due insiemi parzialmente ordinati. Una funzione da P a Q si dice:

monotona (preserva l’ordine) sep1 P p2 p1Q p2

embedding sep1 P p2 p1Q p2

isomorfismo se è un embedding suriettivo

Tino Cortesi Tecniche di Analisi di Programmi 3

Esempi1 non è una funzione monotona

2 è una funzione monotona, ma non è un embedding:2bQ2cma non è vero che bPc

1a 1d

1b1c

d

a

b

c

b

a

c

d

e

2d2e 2b2c 2a

Tino Cortesi Tecniche di Analisi di Programmi 4

Esempi3 è una funzione monotona, ma non è un embedding:3bQ3cma non è vero che bPc

2 è un embedding, ma non è un isomorfismo. b

a

c

d

b

a

c

d

e

3e 3c3d 3a3b

4d

4c 4b

4a

Tino Cortesi Tecniche di Analisi di Programmi 5

Catene ConvergentiRicordiamo che una sequenza (ln)nN di elementi di L è una catena ascendente se

n m ln lm

Una sequenza (ln)nN converge se e solo se

n0N : nN : 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 6

Esempio

L’insieme ordinato dei numeri pari non soddisfa la condizione sulle catene ascendenti

0

2

4

6

8

10

12

Tino Cortesi Tecniche di Analisi di Programmi 7

Esempio

Questo insieme ha un numero infinito di elementiNon ha lunghezza finitaSoddisfa la condizione sulle catene ascendenti

...

Tino Cortesi Tecniche di Analisi di Programmi 8

ContinuitàIn Analisi, una funzione si dice continua se preserva i limiti.Dati due ordini parziali (P,P) e (Q,Q), una funzione da P a Q si dice continua se per ogni insieme diretto S in P

lubSlub{ (x) | xS }

S(S)

(P,P) (Q,Q

)

Tino Cortesi Tecniche di Analisi di Programmi 9

ContinuitàNon tutte le funzioni monotone sono continue. Ad esempio,

:NNS)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 {(X) | X in D} = perché ogni X in D è finito(lub (D)) = N perché D è infinito

Tino Cortesi Tecniche di Analisi di Programmi 10

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 11

Punti fissi sui CPOSia f una funzione monotona f: (P,P) (P,P) su un insieme completo parzialmente ordinato (CPO) P.Sia = n0 f n()

Se Fix(f) allora = lfp(f)Teorema di Kleene Se f è continua allora il minimo punto fisso di f esiste ed è uguale ad .

Tino Cortesi Tecniche di Analisi di Programmi 12

Punti fissi sui CPO

Fix(f) ={ l L | f(l)=l}

lfp(f) = n0 fn()

T

f i()

Tino Cortesi Tecniche di Analisi di Programmi 13

Punti Fissi sui reticoli completi

Sia f una funzione monotona f:LL su un reticolo completo L.

Fix(f) è anch’esso un reticolo completo:

lfp(f) = glb(Fix(f)) Fix(f)gfp(f) = lub(Fix(f)) Fix(f)

Teorema di Tarski:Sia L un reticolo completo. Se f:LL è 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 14

Punti fissi sui reticoli completi

Fix(f) ={ l L | f(l)=l}

Red(f) ={ l L | f(l) P l}

Ext(f) ={ l L | l P f(l)}

lfp(f) = glb{ l L | f(l) l }

gfp(f) = lub{ l L | l f(l) }

Tino Cortesi Tecniche di Analisi di Programmi 15

Dimostriamo che se L è un reticolo completo lub{xL | x f(x)} è un punto fisso di L (il greatest fix point).

Sia H={xL | x f(x)}, e sia a=lub(H). Dimostriamo che a=f(a).

Per ogni hH, 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 hH e la seconda dalla monotonia di f.Poiché h f(a) vale per ogni hH, 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 16

Esistenza di punti fissi nei CPO

Teorema ISia 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 IISia 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 17

Punti Fissi

Ci sono quindi tre risultati che garantiscono l’esistenza di punti fissi:

1. Funzione continua su CPO2. Funzione monotona su reticoli completi3. 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 18

WideningUn 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)n0, la catena

(ln)n0 = (l0’=l0, l1’=(l’0,l1),… )

converge dopo un numero finito di passi

Tino Cortesi Tecniche di Analisi di Programmi 19

EsempioSi consideri il reticolo completo

Int = {} {[a,b] | a b & aZ{-}, bZ{+}}dove l’ordinamento è l’inclusione tra intervalli. Sia K un elemento fissato di IntDefiniamo l’operatore K: (Int,Int) Int

[min(a,c),max(b,d)] se [min(a,c),max(b,d)] K

K([a,b], [c,d]) = [-, +] altrimenti

Se K=[-2,4]: [-2,4] è un operatore di widening

Alla catena [0,0], [0,1], [0,2], [0,3], [0,4], [0,5], [0,6],…corrisponde la catena [0,0], [0,1], [0,2], [0,3], [0,4], [-, +], [-, +],…

Tino Cortesi Tecniche di Analisi di Programmi 20

EsempioSi consideri il reticolo completo

Int = {} {[a,b] | a b & aZ{-}, bZ{+}}dove l’ordinamento è l’inclusione tra intervalli. Sia K un elemento fissato di IntDefiniamo l’operatore K: (Int,Int) Int

[min(a,c),max(b,d)] se [min(a,c),max(b,d)] KK([a,b], [c,d]) =

[-, +] altrimenti

Se K=[0, +]: [0, +] non è un operatore di widening

Alla catena [0,0], [0,1], [0,2], [0,3], [0,4], [0,5], [0,6],…corrisponde la catena [0,0], [0,1], [0,2], [0,3], [0,4], [0,5], [0,6],…

che non converge!

Tino Cortesi Tecniche di Analisi di Programmi 21

Widening e punti fissi

lfp

widening

Tino Cortesi Tecniche di Analisi di Programmi 22

Widening e punti fissiSia 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:

se n=0

f n= f n-1se 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 23

Widening

Fix(f) ={ l L | f(l)=l}

lfp(f)

T

f 2

f 1

f m= f m+1= …

…

Tino Cortesi Tecniche di Analisi di Programmi 24

A che serve tutto questo?

Abbiamo detto che l’approccio all’analisi di programmi che consideriamo è basato sulla semanticaSemantica = assegnare ad ogni costrutto linguistico il suo significatoOgni semantica di un programma può essere espressa come soluzione di un’equazione di minimo punto fisso.

Tino Cortesi Tecniche di Analisi di Programmi 25

Sintassi e SemanticaCi 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 programmaSemantica Assiomaticala semantica viene definita indirettamente attraverso assiomi e regole di una qualche logica

Semantica Denotazionalefornisce modelli matematici ai linguaggi di programmazione: associa ad ogni costrutto linguistico del programma un elemento di una struttura matematica