Czym jest niezmiennik w algorytmach? Mam taką definicję "Mówimy, że warunek g jest niezmiennikim instrukcji I w algorytmie K w wyróżnionym jej miejscu przy warunku wejściowym , jeżeli dla każdego obliczenia K spełniającego warunek początkowy , za każdym razem, gdy obliczenie dochodzi do wyróżnionego miejsca instrukcji I, bieżące wartości zmiennych spełniają warunek g." ale nie do końca wszystko rozumiem.
0
1
Tu trochę info: https://pl.wikipedia.org/wiki/Niezmiennik_p%C4%99tli
Jak sama nazwa wskazuje jest to asercja, która w danym momencie algorytmu jest na pewno spełniona. Jako przykład program w Pythonie liczący pierwiastek w integerach:
def square(n):
# n >=0 warunek wstępny
x = 0
while (x + 1) * (x + 1) <= n:
# 0 <= x * x <= n - niezmiennik
x += 1
return x
Niezmiennik jest spełniony nawet przed pętlą (x = 0). Warunkiem końcowym (warunek sukcesu algorytmu) jest zaś: n <(x + 1)^2. Dokładniej jest to:
0 <= x * x <= n AND n <(x + 1)^2.
0
Czyli niezmiennik to jest coś co przy każdym obiegu pętli będzie prawdą?
1
Tak, 0 <= x * x <= n będzie spełnione zawsze, nawet w momencie końca pętli, jak podałem:
0 <= x * x <= n AND n <(x + 1)^2
W tym stanie prawdą będzie zdanie: zaprzeczenie warunku pętli while i niezmiennik. Bo tak zresztą jest to skonstruowane.
0
Zawsze w sensie aż do przerwania pętli a nie w takim sensie jak ?
x^2 > 0
1
Zawsze, przed obiegiem pętli (tyle mogę napisać na pewno), nawet po zakończeniu też, co można łatwo sprawdzić:
def square(n):
# n >=0 warunek wstępny
x = 0
while (x + 1) * (x + 1) <= n:
# 0 <= x * x <= n - niezmiennik
assert(0 <= x * x <= n)
x += 1
assert(0 <= x * x <= n)
return x
0
W necie jest cała masa nieprawdziwych materiałów o niezmiennikach.
Niezmiennik jest to takie zdanie (warunek), które spełnia implikację:
Jeżeli warunek był spełniony przed blokiem instrukcji, to będzie także spełniony po bloku instrukcji.
Niezmiennik pętli jest to niezmiennik umieszczony w pętli, gdzie blokiem instrukcji jest jeden pełny przebieg pętli.
W związku z tym:
- Każde zdanie prawdziwe (asercja) jest niezmiennikiem każdej pętli.
- Każde zdanie fałszywe jest niezmiennikiem każdej pętli (bo spełnia implkację fałsz -> fałsz).
- Jeżeli pętla nie zmienia jakiejś zmiennej (tzn. dana zmienna jest stałą danej pętli), to niezmiennikiem tej pętli będzie każde zdanie typu: "ta zmienna = jakaś stała".
Niezmiennik pętli nie musi być prawdziwy przed pętlą. W trakcie działania pętli niezmiennik może się zmienić z fałszywego na prawdziwy. Ale jeżeli chociaż raz był prawdziwy, to będzie już prawdziwy na zawsze. Pętla może go tylko naprawić a nie może go zepsuć.
Wielu ludzi myli niezmienniki pętli z asercjami. Niezmiennik można przedstawić jako asercję, jeżeli zapisze się go jako implikację w stosunku do jego poprzedniej wartości.
# na początku
invariant_last = False
# gdzieś w pętli
if invariant_last:
assert check_invariant() # asercja implikacji: invariant_last -> check_invariant()
invariant_last = check_invariant()
Czy dany warunek jest niezmiennikiem, można wydedukować na podstawie samej pętli, analizując tylko jedną jej iterację, abstrahując od wartości początkowych, parametrów, argumentów, środowiska i wszystkiego innego. Oznacza to, że niezmienniki można sprawdzać "szybko", nie iterując pętli wiele razy.
Po co są niezmienniki pętli? Żeby udowodnić, że pętla robi to, co do niej należy.
Jeżeli mamy pętlę
i mamy jakieś warunki początkowe
i mamy warunek jej zakończenia...
Oraz mamy niezmiennik tej pętli
i jest on również spełniony dla warunków początkowych, czyli można go przed pętlą wstawić do asercji...
To po zakończeniu pętli tenże niezmiennik będzie dalej prawdziwy, pomimo zmienionych wartości zmiennych
i jeszcze w dodatku prawdziwy będzie warunek zakończenia pętli.
Z powyższych faktów można udowodnić poprawność danego programu z pętlą.
Przykład: Potęgowanie.
def power(base, exponent):
result = 1
n = 0
while n < exponent:
result *= base
n += 1
return result
Mamy tutaj pętlę o następującym ciele:
result *= base
n += 1
Niezmiennikiem tej pętli będzie następujący warunek:
result == base**n
Jeżeli warunek ten będzie fałszywy, to trudno, ale dalej jest on niezmiennikiem pętli. Natomiast jeżeli jest prawdziwy, to jeden przebieg pętli go nie zepsuje. Jeden przebieg pętli zwiększa n o 1 oraz mnoży result przez base, przez co result dalej ma wartość base podniesioną do potęgi n, przy nowej wartości n. Mogliśmy to stwierdzić, analizując jeden tylko przebieg tej pętli (dwie instrukcje). Nie potrzebujemy ani wartości początkowych, ani nie musimy "rozwijać" pętli, tzn. iterować po niej.
Skoro już mamy niezmiennik, to analizujemy dalej.
Ten sam warunek jest prawdziwy przed pętlą. To dobrze, bo pozostanie prawdziwy po pętli, niezależnie od ilości przebiegów.
def power(base, exponent):
result = 1
n = 0
assert result == base**n # łatwo to sprawdzić dla bieżących wartości result, base i n.
while n != exponent:
invariant(result == base**n) # jak ustaliliśmy wcześniej, ten warunek jest niezmiennikiem tej pętli
result *= base
n += 1
assert result == base**n # ten warunek jest tutaj spełniony, ponieważ był prawdziwy przed pętlą i jest jej niezmiennikiem, czyli pętla go nie zepsuła
assert n == exponent # pętla się zakończyła, więc spełniony jest warunek jej zakończenia (negacja warunku kontynuacji w instrukcji while)
assert result == base**exponent # na podstawie powyższych dedukujemy, że pod koniec programu zmienna result ma wartość taką, jaka nam się podoba
return result
Znajomość niezmiennika pętli pozwoliła nam w kilku asercjach udowodnić poprawność programu z pętlą, bez rozwijania tejże pętli. Wyobraźcie sobie program, gdzie pętla wykonuje miliard iteracji. Sprawdzanie takiego programu bez znajomości niezmiennika wymagałoby wykonania po kolei każdej iteracji pętli. Niezmienniki pozwalają nam przeprowadzić dowód miliard razy szybciej.
0
haael napisał(a):
Niezmiennik pętli nie musi być prawdziwy przed pętlą. W trakcie działania pętli niezmiennik może się zmienić z fałszywego na prawdziwy. Ale jeżeli chociaż raz był prawdziwy, to będzie już prawdziwy na zawsze. Pętla może go tylko naprawić a nie może go zepsuć.
Jeden dodatek jeszcze -- prawdziwość i fałszywość niezmienników sprawdzamy tylko przed i po danym bloku/pętli/instrukcji -- w trakcie, na chwilę, może zostać "zepsuty", o ile
w tej samej iteracji zostanie naprawiony.
Na przykład:
int a = 1;
int b = 2;
while(a < 10) {
++a;
// **
++b;
}
Niezmiennikiem tej pętli jest a < b, bo przed każdym obrotem i po każdym obrocie jest prawdziwy, więc i prawdziwa jest odpowiednia implikacja, ale w linijce oznaczonej // ** jest nieprawdziwy.