Loop Invariants in Python

Un ciclo invariante è semplicemente qualcosa che è vero su ogni iterazione del ciclo. Ad esempio, prendi un ciclo while banale:

while x <= 5:
  x = x + 1

Qui il ciclo invariante sarebbe quello x ≤ 6 . Ovviamente, nella vita reale, gli invarianti di loop saranno più complicati: trovare il ciclo invariante in generale è qualcosa di un'arte e non può essere fatto facilmente algoritmicamente (per quanto ne so).

Quindi, perché è utile? Bene, a un livello grossolano, è positivo per il debug: se si identifica un invariante importante, è facile verificare che sia valido anche quando si modifica un codice. Potresti semplicemente aggiungere una dichiarazione di asserzione di qualche tipo:

while x <= 5:
  x = x + 1
  assert x <= 6

Più precisamente, questi invarianti ci aiutano a capire come si comportano i loop. Qui entra in gioco la semantica assiomatica e la logica di Hoare. (Questa parte della risposta è un po 'più avanzata ed esoterica, quindi non preoccuparti troppo.) Nel caso in cui sei arrugginito sulla notazione: ⇒ significa " implica ", ∧ significa" e "e ¬ significa" non ".

L'idea di base è che vogliamo un modo sistematico per dimostrare le proprietà del nostro codice. Il modo in cui ci avviciniamo a questo è guardando le precondizioni e le post-condizioni nel codice. Cioè, vogliamo dimostrare che se alcune condizioni A contengono prima eseguiamo il nostro codice, alcune condizioni B contengono dopo lo eseguiamo. Generalmente lo scriviamo come:

{A} code {B}

In generale, questo è piuttosto semplice. Puoi capire intuitivamente come provare qualcosa come {x = 0} x = x + 1 {x = 1} . Puoi farlo sostituendo x + 1 per x nella post-condizione, dandoti una formula logica di x = 0 ⇒ x + 1 = 1 che è ovviamente vera. Questo è il modo in cui gestisci il compito in generale: sostituisci semplicemente il nuovo valore per la variabile nella post-condizione.

Altri costrutti come più istruzioni di seguito e istruzioni if sono piuttosto intuitive.

Tuttavia, come lo fai per i loop? Questa è una domanda difficile perché non si conosce (in generale) quante volte un ciclo verrà iterato. È qui che entrano gli invarianti di loop. Stiamo osservando un ciclo come:

while cond: code

Ci sono due possibilità qui. Se cond è False , allora è banale: il ciclo non fa nulla, quindi otteniamo solo A ⇒ B . Ma cosa succede se il ciclo viene effettivamente eseguito? Questo è dove abbiamo bisogno dell'invariant.

L'idea dietro l'invariante è che tiene sempre dentro il loop. Quando sei all'interno del ciclo while, cond è sempre true. Quindi otteniamo un'affermazione del genere:

{A ∧ cond} code {A}

Questo scrive solo ciò di cui avevamo bisogno formalmente: dato che A (il ciclo invariante) e cond si tengono all'inizio del corpo del ciclo, A deve essere mantenuto alla fine. Se possiamo provarlo per il corpo del ciclo, sappiamo che A sarà valido indipendentemente dal numero di volte in cui il ciclo viene eseguito. Quindi, data la dichiarazione di cui sopra è vero, possiamo dedurre:

{A} while cond: code {A}

come bonus aggiuntivo, poiché il ciclo while è appena terminato, sappiamo che cond deve essere falso. Quindi possiamo effettivamente scrivere il risultato completo come:

{A} while cond: code {A ∧ ¬cond}

Quindi usiamo queste regole per provare qualcosa sul mio esempio sopra. Quello che vogliamo dimostrare è:

{x ≤ 0} while x <= 5: x = x + 1 {x = 6}

Cioè, vogliamo mostrare che se iniziamo con un piccolo x , alla fine del ciclo x sarà sempre 6. Questo è piuttosto banale, ma costituisce un buon esempio illustrativo. Quindi il primo passo è trovare un ciclo invariante. In questo caso, l'invariante sarà x ≤ 6 . Ora dobbiamo dimostrare che questo è in realtà un ciclo invariante:

{x ≤ 5 ∧ x ≤ 6} x = x + 1 {x ≤ 6}

Cioè, se x è minore o uguale a 5, x è minore o uguale a 6 dopo aver eseguito x = x + 1 . Possiamo farlo usando la regola di sostituzione sopra descritta, ma è comunque abbastanza ovvio.

Quindi, sapendo questo, possiamo dedurre la regola per l'intero ciclo:

{x ≤ 6} while x <= 5: x = x + 1 {x ≤ 6 ∧ ¬(x ≤ 5)}

Quindi questo ci dice che, alla fine del ciclo, x è sia maggiore che 5 e minore o uguale a 6. Questo semplifica fino a x = 6 . Dal momento che x ≤ 6 ogni volta che x ≤ 0 , abbiamo dimostrato la nostra affermazione iniziale.

Ora, questo potrebbe sembrare un sacco di ostentazione per dimostrare qualcosa di molto ovvio. Dopo tutto, qualsiasi programmatore potrebbe averti detto il valore di x alla fine di questo ciclo! Tuttavia, l'idea importante è che questo metodo si adatta a cicli più complicati che potrebbero non essere immediatamente evidenti. Ma se riesci a trovare un invariante per tale ciclo, puoi utilizzarlo per dimostrare proprietà più interessanti.

In ogni caso, spero che non sia stato troppo confuso e ti ho dato una buona idea del perché gli invarianti di loop sono importanti ad un livello più fondamentale.

Ho trovato una spiegazione molto buona, che include un esempio di utilizzo, qui:

link

L'esempio con biglie rosse e blu nel barattolo spiegava totalmente il trucco. Proverò a sintetizzare in modo che la risposta sia conforme alle regole dello stack (alcune parti potrebbero essere un copia-incolla dell'originale).

-Supponiamo che ci sia un barattolo e contenga una certa quantità N di biglie ROSSE o BLU (N > = 1).

-Sei anche una quantità illimitata di biglie ROSSE sul lato.

PROCEDURE:

while (N > 1):
   pick any two marbles from the jar 

   if (marbles have same colour):
      remove marbles
      put 1 RED marble in the jar

   else:  // marble have different colour
      remove picked RED marble 
      put picked BLUE marble back

Esaminando questa procedura puoi vedere che N diminuisce di uno ad ogni iterazione. Quindi, se sai che all'inizio il barattolo conteneva N biglie, dopo i loop N-1 ne conterrà solo 1. Questo è un argomento intuitivo ma informale che "il ciclo termina dopo un numero infinito di iterazioni".

Supponiamo che la quantità di biglie ROSSO e BLU nel barattolo sia inizialmente nota. Proviamo a prevedere il colore dell'ultimo marmo nel vaso alla fine della procedura.

Formalmente, stiamo cercando di trovare una funzione

f: N × N --> {BLUE, RED}, 

domain: set of ordered pairs of natural numbers, 

range: is the set {BLUE, RED}) 

che soddisfa la seguente condizione:

For all K and M (such that at least one of them is non-zero), 
if we begin with K RED marbles and M BLUE marbles in the jar, 
then the last marble remaining in the jar is necessarily of color f(K,M).

Il modo per identificare questa funzione è trovare prima un invariante del ciclo che funzioni sulla quantità di biglie BLU nel vaso.

Considerazione di una ripetizione del ciclo e del suo effetto sul numero di biglie BLU:

Case 1: both marbles have same colour:
    subcase 1.1: marbles are BLUE (number of BLUE marble decreases by 2)
    subcase 1.2: marbles are RED (number of BLUE marble stays the same)

Case 2: marbles have different colour: (number of BLUE marble stays the same)

Possiamo apprezzare come una singola iterazione del ciclo non abbia alcun effetto sulla parità del numero di biglie BLU. M rimarrà pari o dispari (a seconda dello stato iniziale) come conseguenza dell'iterazione.

Questa proprietà è valida per qualsiasi numero di iterazioni.

Let us denote:
 Big_K the number of BLUE marbles in the jar at the beginning 
 small_k the number of BLUE marbles currently in the jar

then an invariant of the loop is:

  small_k is odd if and only if Big_K is odd

This can be also expressed in a different way:

  (both Big_K and small_k are odd) or (both Big_K and small_k are even)

Supponiamo che il numero di biglie BLU inizialmente nel vaso, Big_K, fosse dispari. "Ricorda che poiché un loop invariante tiene alla fine di ogni iterazione, si tiene, in particolare, alla fine dell'ultima iterazione."

Quindi l'ultimo marmo nel barattolo deve essere BLU, perché altrimenti small_k = 0 (pari). Allo stesso modo, se Big_K fosse pari, l'ultimo marmo deve essere ROSSO, perché altrimenti k = 1 (dispari).

La funzione f è la seguente:

f(Big_K,M) = { RED   if Big_K is even
            { BLUE  if Big_K is odd

tutto il credito va a Robert McCloskey link per la sua utilissima spiegazione su Loop Invariants