Dowodzenie własności stopu
Kryterium liczników iteracji Kryterium malejących wielkości
Załóżmy, że dany jest algorytm:
M:{
l=c;
while(p)do {
K;
l=l+1;
} }
Dobieramy teraz dwie wielkości:
takie, że l<= oraz takie,
które wyjaśnia zależność między wartościami zmiennych w chwili sprawdzania warunku
(niezmiennika) p.
Kryterium liczników iteracji
Jeżeli:
1) i >=l jest w algorytmie M niezmiennikiem instrukcji iteracyjnej „while” przy warunku początkowym ,
2) K ma własność stopu względem i p,
to M oraz „while(p)do K” mają własność stopu względem .
zmienna l jest licznikiem iteracji, służy do
obliczania liczby wykonań instrukcji iterowanej K
Przykład 3.
void dzielenie1 (int x,y)
{ //1: 0<=x i 0<y
int q,r;
q=0;
r=x;
while(y<=r) //p: x=q*y+r i 0<=r i 0<y {
q=q+1;
r=r-y;
};
} //: x=q*y+r i 0<=r<y.
!!
M:{
l=c;
while(p)do {
K;
l=l+1;
} }
Zmienna
q
pełni rolę licznika iteracji.void dzielenie1 (int x,y)
{ //1: 0<=x i 0<y
int q,r;
q=0;
r=x;
while(y<=r) //p: x=q*y+r i 0<=r i 0<y {
q=q+1;
r=r-y;
};
} //: x=q*y+r i 0<=r<y.
M:{
l=c;
while(p)do {
K;
l=l+1;
} }
Określmy : x/y oraz : x=q*y+r i r>=0 i 0<y.
Pokażemy, że i q<=x/y jest niezmiennikiem instrukcji iteracyjnej.
Przy wejściu do instrukcji mamy: q=0, r=x, x>=0, y>0, czyli zachodzi
i q<=x/y oraz r>=y.
Wtedy dostajemy nowe wartości: q’=q+1 i r’=r-y.
void dzielenie1 (int x,y)
{ //1: 0<=x i 0<y
int q,r;
q=0;
r=x;
while(y<=r) //p: x=q*y+r i 0<=r i 0<y {
q=q+1;
r=r-y;
};
} //: x=q*y+r i 0<=r<y.
M:{
l=c;
while(p)do {
K;
l=l+1;
} }
: x/y oraz : x=q*y+r i r>=0 i 0<y.
Łatwo pokazać, że te nowe zmienne spełniają warunek , a nierówność q<=x/y wynika z , bo:
Ćwiczenie!
x=q*y+r, y>0 q=x/y-r/y, y>0 (r>=0,y>0) q<=x/y
Stosując teraz kryterium liczników iteracji wnioskujemy, że algorytm ma własność stopu względem 1. Ponadto nierówność q<=x/y podaje
ograniczenie na liczbę wykonywanych iteracji.
Załóżmy, że dany jest algorytm:
M:{
i=w+1;
while(p)do {
i=w;
K;
} }
Dobieramy teraz trzy wielkości:
i oraz w będące liczbami całkowitymi i takie, które wyjaśnia zależność między
wartościami zmiennych w chwili sprawdzania warunku
(niezmiennika) p.
Kryterium malejących wielkości Jeżeli:
1) i i>w, i w>=0 jest w algorytmie M niezmiennikiem
instrukcji iteracyjnej „while” przy warunku początkowym , 2) K ma własność stopu względem i p,
to M oraz „while(p)do K” mają własność stopu względem .
Metodę malejących wielkości stosuje się, gdy w algorytmie zwiększanie wartości następuje w sposób nieregularny, czyli niekoniecznie o 1.
Zamiast szacować wzrost rozpatruje się jednak te wielkości, które
zmniejszają swoje wartości w trakcie wykonywania algorytmu i dla których istnieją wartości ograniczające je z dołu.
Przykład 4.
void dzielenie2 (int x,y)
{ //2: 0<=x i 0<y
int q,r; int i;
q=0;
r=x; i=r+1;
while(y<=r) //p: x=q*y+r i 0<=r i 0<y {
q=q+1; i=r;
r=r-y;
};
} //: x=q*y+r i 0<=r<y.
M:{
i=w+1;
while(p)do {
i=w;
K;
} }
Zmienna r pełni rolę w. Wprowadzamy też pomocniczą zmienną i.
void dzielenie2 (int x,y)
{ //2: 0<=x i 0<y
int q,r; int i;
q=0;
r=x; i=r+1;
while(y<=r) //p: x=q*y+r i 0<=r i 0<y {
q=q+1; i=r;
r=r-y;
};
} //: x=q*y+r i 0<=r<y.
M:{
i=w+1;
while(p)do {
i=w;
K;
} }
Ustalamy : y>0 i (i=r+1 ∨ i=r+y).
Przy wejściu do instrukcji „while” warunek jest spełniony, bo i=r+1.
void dzielenie2 (int x,y)
{ //2: 0<=x i 0<y
int q,r; int i;
q=0;
r=x; i=r+1;
while(y<=r) //p: x=q*y+r i 0<=r i 0<y {
q=q+1; i=r;
r=r-y;
};
} //: x=q*y+r i 0<=r<y.
M:{
i=w+1;
while(p)do {
i=w;
K;
} }
: y>0 i (i=r+1 ∨ i=r+y).
Warunek zachowuje się przy każdym wykonaniu instrukcji
iterowanej, bo jeśli i’ i r’ są nowymi wartościami, to i’=r oraz r’=r-y, czyli i’=r’+y.
Zatem jest niezmiennikiem iteracji.
Ponieważ r>=0, to cały warunek i r<i , i r>=0 jest niezmiennikiem iteracji.
Na podstawie kryterium malejących wielkości mamy własność stopu względem 2.
Klasyfikować równania rekurencyjne możemy ze względu na:
Sposób, w jaki połączone są wyrazy,
Rodzaj współczynników,
Ilość użytych wyrazów poprzednich.
Typ rekurencji Przykład
I rzędu liniowe nieliniowe II rzędu liniowe
nieliniowe
o zmiennych współczynnikach p-tego rzędu
pełnego rzędu połówkowe
1 1
1
1 1
an
n
n n
a
na a
1 )
1 (
2
2 1
2 2
1
2 1
n n
n
n n
n n
n n
n
a n
na a
a a
a a
a a
a
n a
a
a a
a a
n a
a a
a f a
n n
n n
n
p n n
n n
2
1 2
2 1
2
1, , , )
(
rozwiązania
dokładne
pierwszego rzędu
liniowe wyższych
rzędów
jednorodne
niejednorodne
oszacowania asymptotyczne
podstawianie
iteracje
rekurencja uniwersalne
Przykład.
Schemat
postępowania
(a)
Komentarz: