Co to jest niezmiennik pętli?

Czytam „Wprowadzenie do algorytmu” CLRS. W rozdziale 2 autorzy wspominają o „niezmiennikach pętlowych”. Co to jest niezmiennik pętli?

Krótko mówiąc, niezmiennikiem pętli jest pewien predykat (warunek), który obowiązuje dla każdej iteracji pętli. Na przykład spójrzmy na prostą forpętlę, która wygląda następująco:

int j = 9;
for(int i=0; i<10; i++)  
  j--;

W tym przykładzie jest to prawda (dla każdej iteracji), że i + j == 9. Jest to również słabszy niezmiennik, który jest prawdą i >= 0 && i <= 10.

Podoba mi się ta bardzo prosta definicja: ( źródło )

Niezmiennik pętli jest warunkiem [wśród zmiennych programu], który z konieczności musi być prawdziwy bezpośrednio przed i po każdej iteracji pętli. (Zauważ, że nie mówi to nic o jej prawdzie lub fałszu w połowie iteracji).

Sam niezmiennik pętli niewiele robi. Jednak biorąc pod uwagę odpowiedni niezmiennik, można go wykorzystać do udowodnienia poprawności algorytmu. Prosty przykład w CLRS prawdopodobnie dotyczy sortowania. Na przykład niech niezmiennik pętli będzie mniej więcej taki, że na początku pętli isortowane są pierwsze wpisy tej tablicy. Jeśli możesz udowodnić, że jest to niezmiennik pętli (tzn. Że zachowuje się przed i po każdej iteracji pętli), możesz użyć tego, aby udowodnić poprawność algorytmu sortowania: przy zakończeniu pętli niezmiennik pętli jest nadal spełniony , a licznik ijest długością tablicy. Dlatego pierwsze iwpisy są sortowane, co oznacza, że ​​cała tablica jest sortowana.

Jeszcze prostszy przykład: niezmienniki pętli, poprawność i wyprowadzanie programu .

Sposób, w jaki rozumiem niezmiennik pętli, to systematyczne, formalne narzędzie do wnioskowania o programach. Wykonujemy jedno stwierdzenie, na którym koncentrujemy się, aby udowodnić prawdziwość, i nazywamy to niezmiennikiem pętli. To organizuje naszą logikę. Chociaż równie dobrze możemy nieformalnie spierać się o poprawność jakiegoś algorytmu, użycie niezmiennika pętli zmusza nas do bardzo uważnego myślenia i zapewnia, że ​​nasze rozumowanie jest hermetyczne.

Jest jedna rzecz, o której wiele osób nie zdaje sobie sprawy od razu, mając do czynienia z pętlami i niezmiennikami. Mylą się między niezmiennikiem pętli a warunkową pętlą (warunek kontrolujący zakończenie pętli).

Jak zauważają ludzie, niezmiennik pętli musi być prawdziwy

1. przed rozpoczęciem pętli
2. przed każdą iteracją pętli
3. po zakończeniu pętli

(chociaż może to być tymczasowo fałszywe podczas treści pętli). Z drugiej strony warunek pętli musi być fałszywy po zakończeniu pętli, w przeciwnym razie pętla nigdy się nie zakończy.

Zatem niezmienna pętla i warunek pętli muszą być różnymi warunkami.

Dobrym przykładem niezmiennika złożonej pętli jest wyszukiwanie binarne.

bsearch(type A[], type a) {
start = 1, end = length(A)

    while ( start <= end ) {
        mid = floor(start + end / 2)

        if ( A[mid] == a ) return mid
        if ( A[mid] > a ) end = mid - 1
        if ( A[mid] < a ) start = mid + 1

    }
    return -1

}

Warunkowa pętla wydaje się więc dość prosta - kiedy start> koniec pętla się kończy. Ale dlaczego pętla jest poprawna? Czym jest niezmiennik pętli, który dowodzi jego poprawności?

Niezmiennikiem jest logiczne zdanie:

if ( A[mid] == a ) then ( start <= mid <= end )

To stwierdzenie jest logiczną tautologią - zawsze jest prawdziwe w kontekście konkretnej pętli / algorytmu, który próbujemy udowodnić . I dostarcza użytecznych informacji o poprawności pętli po jej zakończeniu.

Jeśli wrócimy, ponieważ znaleźliśmy element w tablicy, wówczas instrukcja jest wyraźnie prawdziwa, ponieważ jeśli A[mid] == awtedy aznajduje się w tablicy i midmusi znajdować się między początkiem a końcem. A jeśli wygaśnięciem pętli bo start > endwtedy nie może być tak, że liczba start <= mid a mid <= end , a więc wiemy, że oświadczenie A[mid] == amusi być fałszywe. Jednak w rezultacie ogólne zdanie logiczne jest nadal prawdziwe w sensie zerowym. (W logice stwierdzenie, czy (fałsz), a następnie (coś) jest zawsze prawdziwe.)

A co z tym, co powiedziałem o warunkowej pętli, która musi być fałszywa, gdy pętla się kończy? Wygląda na to, że gdy element zostanie znaleziony w tablicy, wówczas warunek pętli jest prawdziwy, gdy pętla się kończy !? Tak naprawdę nie jest, ponieważ domniemana pętla warunkowa jest naprawdę, while ( A[mid] != a && start <= end )ale skracamy rzeczywisty test, ponieważ sugerowana jest pierwsza część. Ten warunek jest wyraźnie fałszywy po pętli, niezależnie od tego, w jaki sposób pętla się kończy.

Poprzednie odpowiedzi definiowały niezmiennik pętli w bardzo dobry sposób.

Poniżej autorzy CLRS zastosowali niezmiennik pętli, aby udowodnić poprawność sortowania wstawianego.

Algorytm sortowania wstawianego (jak podano w książce):

INSERTION-SORT(A)
    for j ← 2 to length[A]
        do key ← A[j]
        // Insert A[j] into the sorted sequence A[1..j-1].
        i ← j - 1
        while i > 0 and A[i] > key
            do A[i + 1] ← A[i]
            i ← i - 1
        A[i + 1] ← key

Niezmiennik pętli w tym przypadku: Tablica podrzędna [1 do j-1] jest zawsze sortowana.

Teraz sprawdźmy to i udowodnijmy, że algorytm jest poprawny.

Inicjalizacja : Przed pierwszą iteracją j = 2. Podtablica [1: 1] to tablica do przetestowania. Ponieważ ma tylko jeden element, jest sortowany. W ten sposób niezmiennik jest spełniony.

Konserwacja : Można to łatwo zweryfikować, sprawdzając niezmiennik po każdej iteracji. W takim przypadku jest spełniony.

Zakończenie : Na tym etapie udowodnimy poprawność algorytmu.

Kiedy pętla się kończy, wówczas wartość j = n + 1. Znowu niezmiennik pętli jest spełniony. Oznacza to, że podgrupa [1 do n] powinna być posortowana.

To właśnie chcemy zrobić z naszym algorytmem. Dlatego nasz algorytm jest poprawny.

Oprócz wszystkich dobrych odpowiedzi, sądzę, że świetny przykład z How to Think About Al Algorytmy autorstwa Jeffa Edmondsa może bardzo dobrze zilustrować tę koncepcję:

PRZYKŁAD 1.2.1 „Algorytm dwóch palców Find-Max”

1) Dane techniczne: Instancja wejściowa składa się z listy L (1..n) elementów. Dane wyjściowe składają się z indeksu i takiego, że L (i) ma maksymalną wartość. Jeśli istnieje wiele wpisów o tej samej wartości, zwracany jest dowolny z nich.

2) Podstawowe kroki: Ty decydujesz o metodzie dwoma palcami. Prawy palec przesuwa się po liście.

3) Miara postępu: Miarą postępu jest to, jak daleko wzdłuż listy znajduje się twój prawy palec.

4) Niezmiennik pętli: Niezmiennik pętli stwierdza, że ​​lewy palec wskazuje jeden z największych wpisów napotkanych do tej pory przez prawy palec.

5) Główne kroki: podczas każdej iteracji przesuwasz prawy palec w dół o jeden wpis na liście. Jeśli prawy palec wskazuje teraz na wpis większy niż lewy, przesuń lewy palec, aby był prawym palcem.

6) Rób postępy: robisz postępy, ponieważ prawy palec przesuwa jeden wpis.

7) Zachowaj niezmiennik pętli: wiesz, że niezmiennik pętli został utrzymany w następujący sposób. Dla każdego kroku nowym lewym palcem jest Max (stary lewy palec, nowy element). Niezmiennikiem pętli jest Max (Max (krótsza lista), nowy element). Matematycznie jest to Max (dłuższa lista).

8) Ustanowienie niezmiennika pętli: Początkowo niezmiennik pętli ustala się, wskazując oba palce na pierwszy element.

9) Warunek wyjścia: Skończysz, gdy prawy palec zakończy przeglądanie listy.

10) Zakończenie: W końcu wiemy, że problem został rozwiązany w następujący sposób. Zgodnie z warunkami wyjścia prawy palec napotkał wszystkie wpisy. Niezmiennikiem pętli lewy palec wskazuje maksymalnie na nich. Zwróć ten wpis.

11) Zakończenie i czas działania: Wymagany czas to pewna stała wielokrotność długości listy.

12) Przypadki specjalne: Sprawdź, co się stanie, gdy jest wiele wpisów o tej samej wartości lub gdy n = 0 lub n = 1.

13) Szczegóły kodowania i implementacji: ...

14) Dowód formalny: poprawność algorytmu wynika z powyższych kroków.

Należy zauważyć, że niezmiennik pętli może pomóc w projektowaniu algorytmów iteracyjnych, jeśli weźmie się pod uwagę twierdzenie, które wyraża ważne relacje między zmiennymi, które muszą być prawdziwe na początku każdej iteracji i po zakończeniu pętli. Jeśli tak się stanie, obliczenia są na drodze do skuteczności. Jeśli false, to algorytm zawiódł.

Niezmienny w tym przypadku oznacza warunek, który musi być spełniony w pewnym punkcie każdej iteracji pętli.

W programowaniu kontraktowym niezmiennik jest warunkiem, który musi być spełniony (na podstawie umowy) przed i po wywołaniu dowolnej metody publicznej.

Znaczenie niezmiennika nigdy się nie zmienia

W tym przypadku niezmiennik pętli oznacza „Zmiana, która zdarza się w zmiennej w pętli (przyrost lub spadek), nie zmienia warunku pętli, tzn. Warunek jest satysfakcjonujący”, dlatego pojawiła się koncepcja niezmiennika pętli

Właściwość niezmiennika pętli jest warunkiem, który obowiązuje dla każdego kroku wykonania pętli (tj. Dla pętli, podczas gdy pętle itp.)

Jest to niezbędne w przypadku dowodu niezmiennika pętli, w którym można wykazać, że algorytm działa poprawnie, jeśli na każdym etapie jego wykonywania właściwość niezmiennika pętli jest zachowana.

Aby algorytm był poprawny, niezmiennik pętli musi mieć wartość:

Inicjalizacja (początek)

Konserwacja (każdy krok po)

Wypowiedzenie (po zakończeniu)

Służy to do oceny wielu rzeczy, ale najlepszym przykładem są chciwe algorytmy ważonego przechodzenia przez wykres. Aby chciwy algorytm mógł uzyskać optymalne rozwiązanie (ścieżka na wykresie), musi osiągnąć połączenie wszystkich węzłów w ścieżce o możliwie najniższej masie.

Zatem niezmienną właściwością pętli jest to, że wybrana ścieżka ma najmniejszą wagę. Na początku nie dodaliśmy żadnych krawędzi, więc ta właściwość jest prawdziwa (w tym przypadku nie jest fałszywa). Na każdym kroku podążamy za najniższą krawędzią wagi (krok zachłanny), więc znów wybieramy ścieżkę o najniższej wadze. Na koniec znaleźliśmy ścieżkę o najniższej ważonej wartości, więc nasza właściwość jest również prawdziwa.

Jeśli algorytm tego nie robi, możemy udowodnić, że nie jest on optymalny.

Trudno jest śledzić, co dzieje się z pętlami. Pętle, które nie kończą się lub kończą bez osiągnięcia celu, jest częstym problemem w programowaniu komputerowym. Niezmienniki pętli pomagają. Niezmiennik pętli to formalne oświadczenie dotyczące relacji między zmiennymi w twoim programie, które zachowuje wartość prawą tuż przed uruchomieniem pętli (ustanawianie niezmiennika) i jest ponownie prawdziwe na dole pętli, za każdym razem przez pętlę (utrzymanie niezmiennika ). Oto ogólny wzorzec użycia niezmienników pętli w kodzie:

... // niezmiennik pętli musi być prawdziwy,
podczas gdy (WARUNEK TESTU) {
// góra pętli
...
// dolna część pętli
// niezmiennik pętli musi być prawdziwy tutaj
}
// Terminination + Loop Invariant = Cel
...
Pomiędzy górą i dołem pętli zapewne poczyniono postępy w kierunku osiągnięcia celu pętli. Może to zakłócić (uczynić fałszem) niezmiennikiem. Punktem niezmienników pętli jest obietnica, że ​​niezmiennik zostanie przywrócony przed każdym powtórzeniem treści pętli. Są dwie zalety tego:

Praca nie jest przenoszona do następnego przejścia w skomplikowany sposób zależny od danych. Każde przejście przez pętlę jest niezależne od wszystkich innych, przy czym niezmienny służy do łączenia przejść w działającą całość. Rozumowanie, że pętla działa, sprowadza się do rozumowania, że ​​niezmiennik pętli jest przywracany przy każdym przejściu przez pętlę. To dzieli skomplikowane ogólne zachowanie pętli na małe proste kroki, z których każdy można rozpatrywać osobno. Warunek testowy pętli nie jest częścią niezmiennika. To właśnie powoduje zakończenie pętli. Rozważamy osobno dwie rzeczy: dlaczego pętla powinna się kiedykolwiek kończyć i dlaczego pętla osiąga swój cel po zakończeniu. Pętla zakończy się, jeśli za każdym razem przez pętlę zbliżysz się do spełnienia warunku zakończenia. Często łatwo jest to zapewnić: np przesuwanie licznika przeciwnego o jeden, aż osiągnie ustaloną górną granicę. Czasami uzasadnienie wypowiedzenia jest trudniejsze.

Niezmiennik pętli powinien zostać utworzony, aby po osiągnięciu warunku zakończenia i niezmienniku prawdziwym, cel został osiągnięty:

niezmiennik + zakończenie => cel
Praktyka polega na tworzeniu niezmienników, które są proste i odnoszą się do wszystkich celów, z wyjątkiem zakończenia. Najlepiej używać symboli matematycznych do wyrażania niezmienników pętli, ale gdy prowadzi to do zbyt skomplikowanych sytuacji, polegamy na czystej prozie i zdrowym rozsądku.

Niestety nie mam uprawnień do komentowania.

@Tom Petricek, jak wspomniałeś

Słabszym niezmiennikiem, który jest również prawdziwy, jest to, że i> = 0 i& i <10 (ponieważ jest to warunek kontynuacji!) ”

Jak to jest niezmiennik pętli?

Mam nadzieję, że się nie mylę, o ile rozumiem ^[1] , Niezmiennik Pętli będzie prawdziwy na początku pętli (Inicjalizacja), będzie prawdą przed i po każdej iteracji (Konserwacja) i będzie również prawdą po zakończenie pętli (Zakończenie) . Ale po ostatniej iteracji i staje się 10. Zatem warunek i> = 0 i& i <10 staje się fałszem i kończy pętlę. Narusza to trzecią właściwość (zakończenie) niezmiennika pętli.

[1] http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html

Niezmiennikiem pętli jest wzór matematyczny, taki jak (x=y+1). W tym przykładzie, xoraz ystanowią dwie zmienne w pętli. Biorąc pod uwagę zmieniającą się zachowanie tych zmiennych całej wykonanie kodu, to jest prawie niemożliwe, aby przetestować wszystkie możliwe xi ywartości i sprawdzić, czy wytwarzają one żadnego błędu. Powiedzmy, że xjest liczbą całkowitą. Liczba całkowita może przechowywać 32-bitowe miejsce w pamięci. Jeśli liczba ta przekroczy, nastąpi przepełnienie bufora. Musimy więc mieć pewność, że podczas wykonywania kodu nigdy nie przekroczy tej przestrzeni. w tym celu musimy zrozumieć ogólną formułę, która pokazuje związek między zmiennymi. W końcu po prostu staramy się zrozumieć zachowanie programu.

Krótko mówiąc, jest to warunek PĘTLI, który jest prawdziwy w każdej iteracji pętli:

for(int i=0; i<10; i++)
{ }

W tym możemy powiedzieć, że stan i jest i<10 and i>=0

Niezmiennik pętli jest twierdzeniem, które jest prawdziwe przed i po wykonaniu pętli.

W wyszukiwaniu liniowym (zgodnie z ćwiczeniem podanym w książce) musimy znaleźć wartość V w danej tablicy.

To proste jak skanowanie tablicy od 0 <= k <długości i porównanie każdego elementu. Jeśli znaleziono V lub jeśli skanowanie osiąga długość tablicy, po prostu zakończ pętlę.

Zgodnie z moim zrozumieniem w powyższym problemie

Niezmienniki pętli (inicjalizacja): V nie występuje w iteracji k-1. Już pierwsza iteracja, będzie to -1 stąd możemy powiedzieć, że V nie znaleziono na pozycji -1

Utrzymanie: W następnej iteracji V nie znaleziono w k-1 jest prawdą

Terminacja: Jeśli V znalezione w pozycji k lub k osiągnie długość tablicy, zakończ pętlę.