Analiza algorytmu Euklidesa: Różnice pomiędzy wersjami
(→Dowód własności stop algorytmu Euklidesa) |
|||
Linia 86: | Linia 86: | ||
W algorytmie występuje pętla zewnętrzna i dwie po kolei pętle wewnętrzne. W każdym przypadku obliczenia pętli wewnętrznych są skończone. Wynika to wprost z aksjomatu (N3). | W algorytmie występuje pętla zewnętrzna i dwie po kolei pętle wewnętrzne. W każdym przypadku obliczenia pętli wewnętrznych są skończone. Wynika to wprost z aksjomatu (N3). | ||
Nieco trudniej jest zauważyć, że obliczenie pętli wewnętrznej jest także skończone. Wychodząc z drugiej pętli wewnętrznej osiągnęliśmy większą z dwu liczb ''n, m'' zaczynając od zera i dodając pracowicie jeden. | Nieco trudniej jest zauważyć, że obliczenie pętli wewnętrznej jest także skończone. Wychodząc z drugiej pętli wewnętrznej osiągnęliśmy większą z dwu liczb ''n, m'' zaczynając od zera i dodając pracowicie jeden. | ||
− | W każdym kolejnym wykonaniu instrukcji iterowanych w pętli zewnętrznej większa z liczb ''n,m'' jest zmniejszana bo <math>\color{blue} n \neq m</math>. Więc, po conajwyżej <math>\color{blue} max(n,m) </math> powtórzeniach pętli zewnętrznej, algorytm Euklidesa, w tej postaci, zatrzyma | + | W każdym kolejnym wykonaniu instrukcji iterowanych w pętli zewnętrznej większa z liczb ''n,m'' jest zmniejszana bo <math>\color{blue} n \neq m</math>. Więc, po conajwyżej <math>\color{blue} max(n,m) </math> powtórzeniach pętli zewnętrznej, algorytm Euklidesa, w tej postaci, zatrzyma się. |
+ | Ale po kolei: | ||
+ | Z aksjomatu (N3) wynika, że | ||
+ | |||
+ | <math>\{ r:=0; \mathbf{while} \ r\neq n\ \mathbf{do}\ r:=r+1\ \mathbf{od}\} | ||
+ | \ r=n </math> | ||
+ | |||
+ | Wykorzystując następującą regułę wnioskowania | ||
+ | |||
+ | <math>\frac{\alpha \Rightarrow \beta}{\mathbf{while}\ \beta\ \mathbf{do}\ K\ \mathbf{od}\ \neg \beta \Rightarrow \mathbf{while}\ \alpha\ \mathbf{do}\ K\ \mathbf{od}\ \neg \alpha} </math> | ||
+ | |||
+ | wnioskujemy, że | ||
+ | |||
+ | <math>\{ r:=0; \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od} \} | ||
+ | \ (r=n \lor r=m)</math> | ||
+ | |||
+ | Z założenia <math>n \neq m</math> wynika, że | ||
+ | |||
+ | <math>\{ r:=0; \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od} \} | ||
+ | \ (r=min{n, m})</math> | ||
+ | |||
+ | Udowodniliśmy więc, że | ||
+ | |||
+ | <math>\left \{\begin{array}{l} r:=0;\\ \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \end{array} \right \} | ||
+ | \ (r=min{n, m})</math> | ||
== Dowód poprawności algorytmu Euklidesa == | == Dowód poprawności algorytmu Euklidesa == |
Wersja z 17:04, 16 lut 2013
Należy udowodnić że algorytm zawsze kończy obliczenia.
Zacznijmy od obserwacji, że algorytm Euklidesa w niestandardowym modelu liczb naturalnych może nie zakończyć obliczeń.
Na jakich podstawach ma się oprzeć dowód własności stop algorytmu?
Algorytmiczne aksjomaty liczb naturalnych:
- (N1) [math]\color{blue} (\forall n) (n+1 \neq 0 ) [/math]
- (N2) [math]\color{blue} (\forall n)(\forall m)(n+1=m+1 \Rightarrow n=m)[/math]
- (N3) [math]\color{blue} (\forall n)[m:=0; \mathbf{while}\ m \neq n\ \mathbf{do}\ n:=n+1\ \mathbf{od}](m=n)[/math]
Możemy zdefiniować relacje mniejszości
Definicja
[math]\color{blue} x\lty\ \stackrel{df}{\equiv}\ \neg (x=y) \wedge \left[\begin{array}{l} r:=0; \\ \mathbf{while}\ r\neq x \land r \neq y \\ \mathbf{do} \\ \quad r:=r+1 \\ \mathbf{od} \end{array} \right](r=x)[/math] |
Definicja
[math]\color{blue} x\leq y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} r:=0; \\ \mathbf{while}\ r\neq x \land r \neq y \\ \mathbf{do} \\ \quad r:=r+1 \\ \mathbf{od} \end{array} \right](r=x)[/math] |
oraz operację odejmowania
Definicja
Jeśli [math]\color{blue} y \lt x [/math] to operacja odejmowania jest określona tak
[math]\color{blue} x \stackrel{.}{-}y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} r:=y;\ q:=0; \\ \mathbf{while}\ r \neq x \ \mathbf{do} \quad r:=r+1;\ q:=q+1 \ \mathbf{od}; \\ \end{array} \right] (wynik = q) [/math]
i operację dodawania
Definicja Operacja dodawania jest określona tak
[math]\color{blue} x + y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} r:=x;\ q:=0; \\ \mathbf{while}\ q \neq y \ \mathbf{do} \quad r:=r+1;\ q:=q+1 \ \mathbf{od}; \\ \end{array} \right] (wynik = r) [/math]
Lemat (aksjomat Archimedesa)
Jeśli [math] \color{blue} 0\ltn \lt m [/math] to [math]\color{blue} \left[\begin{array}{l} r:=n; \\ \mathbf{while}\ r \leq m \ \mathbf{do} \quad r:=r+n; \ \mathbf{od}; \\ \end{array} \right] (r\gtm) [/math]
Dowód własności stop algorytmu Euklidesa
Gdyby algorytm Euklidesa miał obliczenie nieskończone dla pewnych liczb naturalnych n i m to stanowiłoby to zaprzeczenie aksjomatu (N3) liczb naturalnych.
W algorytmie występuje pętla zewnętrzna i dwie po kolei pętle wewnętrzne. W każdym przypadku obliczenia pętli wewnętrznych są skończone. Wynika to wprost z aksjomatu (N3). Nieco trudniej jest zauważyć, że obliczenie pętli wewnętrznej jest także skończone. Wychodząc z drugiej pętli wewnętrznej osiągnęliśmy większą z dwu liczb n, m zaczynając od zera i dodając pracowicie jeden. W każdym kolejnym wykonaniu instrukcji iterowanych w pętli zewnętrznej większa z liczb n,m jest zmniejszana bo [math]\color{blue} n \neq m[/math]. Więc, po conajwyżej [math]\color{blue} max(n,m) [/math] powtórzeniach pętli zewnętrznej, algorytm Euklidesa, w tej postaci, zatrzyma się. Ale po kolei: Z aksjomatu (N3) wynika, że
[math]\{ r:=0; \mathbf{while} \ r\neq n\ \mathbf{do}\ r:=r+1\ \mathbf{od}\} \ r=n [/math]
Wykorzystując następującą regułę wnioskowania
[math]\frac{\alpha \Rightarrow \beta}{\mathbf{while}\ \beta\ \mathbf{do}\ K\ \mathbf{od}\ \neg \beta \Rightarrow \mathbf{while}\ \alpha\ \mathbf{do}\ K\ \mathbf{od}\ \neg \alpha} [/math]
wnioskujemy, że
[math]\{ r:=0; \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od} \} \ (r=n \lor r=m)[/math]
Z założenia [math]n \neq m[/math] wynika, że
[math]\{ r:=0; \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od} \} \ (r=min{n, m})[/math]
Udowodniliśmy więc, że
[math]\left \{\begin{array}{l} r:=0;\\ \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \end{array} \right \} \ (r=min{n, m})[/math]
Dowód poprawności algorytmu Euklidesa
Należy wykazać, że ...
- przejdź do algorytmu Euklidesa
-
- powrót do wybrane przykłady