[Algoritmi] Invarianti di un ciclo
Ciao a tutti! Ho un po' di confusione sugli invarianti di ciclo e gli appunti che ho preso a lezione non sono proprio coerenti con quello che c'è scritto sul libro. Innanzitutto il primo dubbio che ho è sulla definizione: non ho capito se l'invariante è una proprietà che deve valere alla fine di un ciclo, all'inizio di una iterazione o alla fine di una iterazione.
Vi riporto un semplicissimo esercizio che ho fatto da solo in modo che possiate vedere i miei errori.
Algoritmo arrayMax(A,n)
Input: array A di n interi A con 0$<=$i$<=$n
Output: massimo intero in A
currMax$larr$A[0]
for i$larr$1 to n-1 do {
if (currMax < A) then currMax$larr$A
}
return currMax
$S$: currMax = max{A[j] con 0$<=$j$<=$n-1}
$S_i$: currMax = max{A[j] con 0$<=$j$<=$i}
$S_0$: currMax = max{A[j] con 0$<=$j$<=$0} che è verificata perchè all'inizio del ciclo il valore di currMax sarà anche l'unico esaminato nell'array e quindi sarà il massimo.
$S_(i-1)$: currMax = max{A[j] con 0$<=$j$<=$i-1} che è verificata perchè alla fine dell'iterazione currMax contiene il massimo valore trovato nell'array fino a quel momento, sia che sia stata aggiornata o meno currMax.
Poichè $S_(i-1)$ è verificata, vale anche $S_i$.
Posto k=n-1, $S_k$: currMax = {A[j] con 0$<=$j$<=$k} che è verificata per la stessa motivazione di $S_(i-1)$
Poichè la proprietà vale per tutte le iterazioni allora vale $S$ per tutto il ciclo.
Grazie a chi mi risponderà!
Vi riporto un semplicissimo esercizio che ho fatto da solo in modo che possiate vedere i miei errori.
Algoritmo arrayMax(A,n)
Input: array A di n interi A con 0$<=$i$<=$n
Output: massimo intero in A
currMax$larr$A[0]
for i$larr$1 to n-1 do {
if (currMax < A) then currMax$larr$A
}
return currMax
$S$: currMax = max{A[j] con 0$<=$j$<=$n-1}
$S_i$: currMax = max{A[j] con 0$<=$j$<=$i}
$S_0$: currMax = max{A[j] con 0$<=$j$<=$0} che è verificata perchè all'inizio del ciclo il valore di currMax sarà anche l'unico esaminato nell'array e quindi sarà il massimo.
$S_(i-1)$: currMax = max{A[j] con 0$<=$j$<=$i-1} che è verificata perchè alla fine dell'iterazione currMax contiene il massimo valore trovato nell'array fino a quel momento, sia che sia stata aggiornata o meno currMax.
Poichè $S_(i-1)$ è verificata, vale anche $S_i$.
Posto k=n-1, $S_k$: currMax = {A[j] con 0$<=$j$<=$k} che è verificata per la stessa motivazione di $S_(i-1)$
Poichè la proprietà vale per tutte le iterazioni allora vale $S$ per tutto il ciclo.
Grazie a chi mi risponderà!
Risposte
"DavideF":
Ciao a tutti! Ho un po' di confusione sugli invarianti di ciclo e gli appunti che ho preso a lezione non sono proprio coerenti con quello che c'è scritto sul libro. Innanzitutto il primo dubbio che ho è sulla definizione: non ho capito se l'invariante è una proprietà che deve valere alla fine di un ciclo, all'inizio di una iterazione o alla fine di una iterazione.
[...]
Ciao DavideF
Innanzitutto cominciamo col fare chiarezza dicendo che l'invariante è una proprietà che deve valere prima di entrare nel ciclo (nella così detta inizializzazione), ad ogni iterazione dello stesso (così detta conservazione o mantenimento) ed infine dopo la sua conclusione (così detta terminazione).
"DavideF":
[...]
Vi riporto un semplicissimo esercizio che ho fatto da solo in modo che possiate vedere i miei errori.
Algoritmo arrayMax(A,n)
Input: array A di n interi A con 0$<=$i$<=$n
Output: massimo intero in A
currMax$larr$A[0]
for i$larr$1 to n-1 do {
if (currMax < A) then currMax$larr$A
}
return currMax
$S$: currMax = max{A[j] con 0$<=$j$<=$n-1}
$S_i$: currMax = max{A[j] con 0$<=$j$<=$i}
$S_0$: currMax = max{A[j] con 0$<=$j$<=$0} che è verificata perchè all'inizio del ciclo il valore di currMax sarà anche l'unico esaminato nell'array e quindi sarà il massimo.
$S_(i-1)$: currMax = max{A[j] con 0$<=$j$<=$i-1} che è verificata perchè alla fine dell'iterazione currMax contiene il massimo valore trovato nell'array fino a quel momento, sia che sia stata aggiornata o meno currMax.
Poichè $S_(i-1)$ è verificata, vale anche $S_i$.
Posto k=n-1, $S_k$: currMax = {A[j] con 0$<=$j$<=$k} che è verificata per la stessa motivazione di $S_(i-1)$
Poichè la proprietà vale per tutte le iterazioni allora vale $S$ per tutto il ciclo.
Grazie a chi mi risponderà!
Allora, ti do un consiglio iniziale: soprattutto le prime volte che hai da dimostrare la validità di un'invariante scrivila pure a parole così come ti viene. Solo dopo che hai individuato la proprietà corretta e sei convinto che valga (ci si convince solitamente prima in maniera intuitiva per poi passare ad una dimostrazione formale). Poi: cerca di utilizzare quanti meno indici possibili nella dimostrazione, utilizzando invece solo quelli presenti nel ciclo a cui ci riferiamo correntemente. Ad esempio nel nostro caso vogliamo possiamo esprimere (informalmente per ora) che "currMax contiene il massimo valore nella porzione di array che fino a quel momento abbiamo scansionato".
Ti ringrazio per i consigli, ho già le idee più chiare!
Allora cercherò di partire da un livello più discorsivo. L'ultima cosa che volevo sapere però era se la soluzione che ho dato io è corretta a livello di ragionamento e dimostrazione oppure se c'è qualche errore o manca qualcosa.
Allora cercherò di partire da un livello più discorsivo. L'ultima cosa che volevo sapere però era se la soluzione che ho dato io è corretta a livello di ragionamento e dimostrazione oppure se c'è qualche errore o manca qualcosa.
Fermo restando il fatto che si possono riscrivere tutte con un solo indice (per semplificare): $S_0$ (inizializzazione) è giusta, $S_i$ (conservazione o mantenimento che dir si voglia) va motivata e con $S_{i - 1}$ immagino tu volessi intendere $S_{n - 1}$ (terminazione, comunque motivata correttamente). $S_{k}$ pertanto non ti serve. In conclusione basta che riordini e risistemi tutto in maniera più semplificata.
Penso tu lo abbia intuito (e forse te lo avranno anche spiegato a lezione) che l'invariante è altro che un'altra versione del principio di induzione in matematica con una differenza: qui non vogliamo dimostrare la proprietà per un numero intero $n$ infinito ma finito.
Spero di esserti stato d'aiuto.
Penso tu lo abbia intuito (e forse te lo avranno anche spiegato a lezione) che l'invariante è altro che un'altra versione del principio di induzione in matematica con una differenza: qui non vogliamo dimostrare la proprietà per un numero intero $n$ infinito ma finito.
Spero di esserti stato d'aiuto.
In realtà con $S_(i-1)$ intendevo l'iterazione precedente all'i-esima. Il motivo per cui ho dimostrato quella è che sul mio libro trovo scritto questo:
" Per provare la correttezza di una certa espressione riferita ad un ciclo, si definisca $S$ come una serie di espressioni minori, $S_0$,$S_1$,...,$S_k$, dove:
1. La proposizione iniziale è vera prima che inizi il ciclo.
2. Se $S_(i-1)$ è vera prima dell'i-esima iterazione, allora $S_i$ sarà vera dopo l'i-esima iterazione.
3. L'ultima espressione, $S_k$, implica che l'espressione iniziale $S$ sia vera. "
Per questo motivo ho individuato la proprietà $S$ e ho dimostrato che vale $S_0$ (come al punto 1). Poi dal punto 2 io ho capito che dimostrato $S_(i-1)$, segue la validità di $S_i$ e quindi dimostrato $S_k$ (o $S_(n-1)$ che sia), come al punto 3, si è dimostrata la validità dell'intera proposizione.
Quindi non ho motivato $S_i$ perchè la sua validità dovrebbe seguire dalla dimostrazione di validità di $S_(i-1)$, almeno da quanto ho capito io... correggimi se sbaglio
Ti ringrazio ancora per l'aiuto che mi stai dando
" Per provare la correttezza di una certa espressione riferita ad un ciclo, si definisca $S$ come una serie di espressioni minori, $S_0$,$S_1$,...,$S_k$, dove:
1. La proposizione iniziale è vera prima che inizi il ciclo.
2. Se $S_(i-1)$ è vera prima dell'i-esima iterazione, allora $S_i$ sarà vera dopo l'i-esima iterazione.
3. L'ultima espressione, $S_k$, implica che l'espressione iniziale $S$ sia vera. "
Per questo motivo ho individuato la proprietà $S$ e ho dimostrato che vale $S_0$ (come al punto 1). Poi dal punto 2 io ho capito che dimostrato $S_(i-1)$, segue la validità di $S_i$ e quindi dimostrato $S_k$ (o $S_(n-1)$ che sia), come al punto 3, si è dimostrata la validità dell'intera proposizione.
Quindi non ho motivato $S_i$ perchè la sua validità dovrebbe seguire dalla dimostrazione di validità di $S_(i-1)$, almeno da quanto ho capito io... correggimi se sbaglio
Ti ringrazio ancora per l'aiuto che mi stai dando
In realtà ciò che è scritto nel tuo libro è del tutto equivalente a come è descritto nel libro di algoritmi e strutture dati che ho utilizzato a suo tempo, solo che assume una forma diversa e non ricalca molto il principio di induzione. Secondo me la modalità spiegata nel mio libro è soltanto più semplice, tutto qua.
Il punto $3$ della definizione del tuo libro secondo me va un po' parafrasato per essere capito a pieno. E' come se avessimo una catena di implicazioni $S_1 \Rightarrow S_2 \Rightarrow ... \Rightarrow S_k \Rightarrow S_1$ ed appunto $S_k$ è l'ultima che ti permette di "chiudere il cerchio" e completare la dimostrazione della validità dell'invariante. Ho omesso $S_0$ nella catena di implicazioni semplicemente perché è il caso base e va trattato a parte.
Pertanto seguendo questo ragionamento è corretto omettere la dimostrazione di $S_{i}$ se hai dimostrato correttamente $S_{i - 1}$.
Di nulla, figurati per l'aiuto
.
Il punto $3$ della definizione del tuo libro secondo me va un po' parafrasato per essere capito a pieno. E' come se avessimo una catena di implicazioni $S_1 \Rightarrow S_2 \Rightarrow ... \Rightarrow S_k \Rightarrow S_1$ ed appunto $S_k$ è l'ultima che ti permette di "chiudere il cerchio" e completare la dimostrazione della validità dell'invariante. Ho omesso $S_0$ nella catena di implicazioni semplicemente perché è il caso base e va trattato a parte.
Pertanto seguendo questo ragionamento è corretto omettere la dimostrazione di $S_{i}$ se hai dimostrato correttamente $S_{i - 1}$.
Di nulla, figurati per l'aiuto
.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo