Analiza algorytmu Euklidesa: Różnice pomiędzy wersjami
(→Dowód własności stop algorytmu Euklidesa) |
|||
(Nie pokazano 18 pośrednich wersji utworzonych przez tego samego użytkownika) | |||
Linia 2: | Linia 2: | ||
Należy udowodnić że algorytm zawsze kończy obliczenia. | Należy udowodnić że algorytm zawsze kończy obliczenia. | ||
− | Zacznijmy od obserwacji, że algorytm Euklidesa w [[niestandardowy model liczb naturalnych|niestandardowym modelu liczb naturalnych]] może nie zakończyć obliczeń. (Lub, ujmując to inaczej - jest taka [[niestandardowy model liczb naturalnych|klasa K]] w której ten algorytm nie kończy obliczeń.) | + | Dowodu nie da się przeprowadzić opierając się na aksjomatach Peano. Zacznijmy od obserwacji, że algorytm Euklidesa w [[niestandardowy model liczb naturalnych|niestandardowym modelu liczb naturalnych]] może nie zakończyć obliczeń. (Lub, ujmując to inaczej - jest taka [[niestandardowy model liczb naturalnych|klasa K]] w której ten algorytm nie kończy obliczeń.) |
− | Na jakich podstawach ma się oprzeć dowód własności stop algorytmu? | + | Na jakich więc podstawach ma się oprzeć dowód własności stop algorytmu? |
− | + | Okaże się, że wystarczą trzy następujące: | |
Algorytmiczne aksjomaty liczb naturalnych: | Algorytmiczne aksjomaty liczb naturalnych: | ||
− | :(N1) <math>\color{blue} (\forall n) (n+1 \neq 0 ) </math> | + | :(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> | + | :(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}\ | + | :(N3) <math>\color{blue} { (\forall n)[m:=0; \mathbf{while}\ m \neq n\ \mathbf{do}\ m:=m+1\ \mathbf{od}](m=n) } </math> |
Możemy zdefiniować relacje mniejszości | Możemy zdefiniować relacje mniejszości | ||
Linia 19: | Linia 19: | ||
| '''Definicja''' | | '''Definicja''' | ||
− | <math>\color{blue} x<y\ \stackrel{df}{\equiv}\ \neg (x=y) \wedge \left[\begin{array}{l} | + | <math>\color{blue} {x < y\ \stackrel{df}{\equiv}\ \neg (x=y) \wedge \left[\begin{array}{l} |
r:=0; \\ | r:=0; \\ | ||
\mathbf{while}\ r\neq x \land r \neq y \\ | \mathbf{while}\ r\neq x \land r \neq y \\ | ||
Linia 25: | Linia 25: | ||
\quad r:=r+1 \\ | \quad r:=r+1 \\ | ||
\mathbf{od} | \mathbf{od} | ||
− | \end{array} \right](r=x)</math> | + | \end{array} \right](r=x)} </math> |
| | | | ||
|'''Definicja''' | |'''Definicja''' | ||
− | <math>\color{blue} x\leq y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} | + | <math>\color{blue} { x\leq y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} |
r:=0; \\ | r:=0; \\ | ||
\mathbf{while}\ r\neq x \land r \neq y \\ | \mathbf{while}\ r\neq x \land r \neq y \\ | ||
Linia 35: | Linia 35: | ||
\quad r:=r+1 \\ | \quad r:=r+1 \\ | ||
\mathbf{od} | \mathbf{od} | ||
− | \end{array} \right](r=x)</math> | + | \end{array} \right](r = x) } </math> |
|} | |} | ||
oraz operację odejmowania | oraz operację odejmowania | ||
Linia 41: | Linia 41: | ||
'''Definicja''' | '''Definicja''' | ||
− | Jeśli <math>\color{blue} y < x </math> to operacja odejmowania jest określona tak | + | Jeśli <math>\color{blue}{ y < x }</math> to operacja odejmowania jest określona tak |
− | <math>\color{blue} x \stackrel{.}{-}y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} | + | :<math>\color{blue}{ x \stackrel{.}{-}y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} |
r:=y;\ q:=0; \\ | r:=y;\ q:=0; \\ | ||
\mathbf{while}\ r \neq x \ | \mathbf{while}\ r \neq x \ | ||
Linia 50: | Linia 50: | ||
\mathbf{od}; \\ | \mathbf{od}; \\ | ||
\end{array} \right] | \end{array} \right] | ||
− | (wynik = q) | + | (wynik = q)} |
</math> | </math> | ||
− | + | '''Lemat''' | |
+ | |||
+ | :(N3') <math> \quad \color{blue}{ (\forall n \neq 0)[ \mathbf{while}\ n \neq 0\ \mathbf{do}\ n:=n \stackrel{_\centerdot}{-}1\ \mathbf{od}](n=0)}</math> | ||
+ | |||
'''Definicja''' | '''Definicja''' | ||
Operacja dodawania jest określona tak | Operacja dodawania jest określona tak | ||
− | <math>\color{blue} x + y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} | + | :<math>\color{blue}{ x + y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} |
r:=x;\ q:=0; \\ | r:=x;\ q:=0; \\ | ||
\mathbf{while}\ q \neq y \ | \mathbf{while}\ q \neq y \ | ||
Linia 65: | Linia 68: | ||
\mathbf{od}; \\ | \mathbf{od}; \\ | ||
\end{array} \right] | \end{array} \right] | ||
− | (wynik = r) | + | (wynik = r) } |
</math> | </math> | ||
− | '''Lemat''' ( | + | '''Lemat''' (zasada Archimedesa) |
− | Jeśli <math> \color{blue} 0<n < m </math> to | + | Jeśli <math> \color{blue}{ 0 < n < m }</math> to |
− | <math>\color{blue} \left[\begin{array}{l} | + | :<math>\color{blue}{ \left[\begin{array}{l} |
r:=n; \\ | r:=n; \\ | ||
\mathbf{while}\ r \leq m \ | \mathbf{while}\ r \leq m \ | ||
Linia 79: | Linia 82: | ||
\mathbf{od}; \\ | \mathbf{od}; \\ | ||
\end{array} \right] | \end{array} \right] | ||
− | (r>m) | + | (r> m) } |
</math> | </math> | ||
Linia 93: | Linia 96: | ||
Z aksjomatu (N3) wynika, że | Z aksjomatu (N3) wynika, że | ||
− | <math>\{ r:=0; \mathbf{while} \ r\neq n\ \mathbf{do}\ r:=r+1\ \mathbf{od}\} | + | :<math>\{ r:=0; \mathbf{while} \ r \neq n\ \mathbf{do}\ r:=r+1\ \mathbf{od}\} |
\ r=n </math> | \ r=n </math> | ||
Wykorzystując następującą regułę wnioskowania | 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> | + | :<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 | wnioskujemy, że | ||
− | <math>\{ r:=0; \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od} \} | + | :<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> | \ (r=n \lor r=m)</math> | ||
Z założenia <math>n \neq m</math> wynika, że | 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} \} | + | :<math>\{ r:=0; \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od} \} |
\ (r=min(n, m))</math> | \ (r=min(n, m))</math> | ||
Udowodniliśmy więc, że | Udowodniliśmy więc, że | ||
− | <math>\left \{\begin{array}{l} \mathbf{if}\ n\neq m\\ | + | :<math>\left \{\begin{array}{l} \mathbf{if}\ n\neq m\\ |
\mathbf{then} \\ | \mathbf{then} \\ | ||
− | \quad r:=0;\\\quad \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ | + | \quad r:=0;\\\quad \mathbf{while} \ r \neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ |
\quad \mathbf{then}\\ | \quad \mathbf{then}\\ | ||
− | \qquad n\_mniejsze:=true;\ | + | \qquad n\_mniejsze:=true;\ maks:=m\\\quad \mathbf{else}\\ |
− | \qquad n\_mniejsze:=false;\ | + | \qquad n\_mniejsze:=false;\ maks:=n\\\quad \mathbf{fi};\\ |
\mathbf{fi} \end{array} \right \} | \mathbf{fi} \end{array} \right \} | ||
− | \ ((r=n \land n<m)\lor (r=m \land m>n )\land | + | \ ((r=n \land n< m)\lor (r=m \land m> n )\land maks=\mathrm{max}(n,m))</math> |
Jeszcze raz korzystamy z aksjomatu (N3) | Jeszcze raz korzystamy z aksjomatu (N3) | ||
− | <math>\{ r:=0; \mathbf{while} \ r\neq | + | :<math>\{ r:=0; \mathbf{while} \ r\neq maks \ \mathbf{do}\ r:=r+1\ \mathbf{od}\} |
− | \ r= | + | \ r=maks </math> |
− | <math>\left \{\begin{array}{l} \mathbf{if}\ n\neq m\\ | + | :<math>\left \{\begin{array}{l} \mathbf{if}\ n\neq m\\ |
\mathbf{then} \\ | \mathbf{then} \\ | ||
\quad r:=0;\\ \quad \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ | \quad r:=0;\\ \quad \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ | ||
\quad \mathbf{then}\\ | \quad \mathbf{then}\\ | ||
− | \qquad n\_mniejsze:=true;\ | + | \qquad n\_mniejsze:=true;\ maks:=m\\ \quad \mathbf{else}\\ |
− | \qquad n\_mniejsze:=false;\ | + | \qquad n\_mniejsze:=false;\ maks:=n\\ \quad \mathbf{fi};\\ |
\quad r:=0;\\ | \quad r:=0;\\ | ||
− | \quad \mathbf{while} \ r\neq | + | \quad \mathbf{while} \ r\neq maks \ \mathbf{do}\ r:=r+1\ \mathbf{od} \\ |
\mathbf{fi} \end{array} \right \} | \mathbf{fi} \end{array} \right \} | ||
− | \ ( r= | + | \ ( r=maks \land maks=\mathrm{max}(n,m))</math> |
Skorzystam z prawa przerwania i wznowienia podróży | Skorzystam z prawa przerwania i wznowienia podróży | ||
− | <math>\left \{\begin{array}{l} | + | :<math>\left \{\begin{array}{l} |
r:=0;\\ \mathbf{while} \ r\neq \mathrm{max}(n,m) \\ \mathbf{do}\\ | r:=0;\\ \mathbf{while} \ r\neq \mathrm{max}(n,m) \\ \mathbf{do}\\ | ||
\quad r:=r+1 \\ | \quad r:=r+1 \\ | ||
Linia 150: | Linia 153: | ||
\quad r:=r+1\\ | \quad r:=r+1\\ | ||
\mathbf{od}; \\ | \mathbf{od}; \\ | ||
− | \mathbf{if}\ r=n\\ | + | \mathbf{if}\ r= n\\ |
\mathbf{then}\\ | \mathbf{then}\\ | ||
\quad n\_mniejsze:=true;\\ | \quad n\_mniejsze:=true;\\ | ||
− | \quad | + | \quad maks:=m\\ |
\mathbf{else}\\ | \mathbf{else}\\ | ||
\quad n\_mniejsze:=false;\\ | \quad n\_mniejsze:=false;\\ | ||
− | \quad | + | \quad maks:=n\\ \mathbf{fi};\\ |
− | \mathbf{while} \ r\neq | + | \mathbf{while} \ r\neq maks \\ \mathbf{do}\\ |
\quad r:=r+1\\ \mathbf{od} \\ | \quad r:=r+1\\ \mathbf{od} \\ | ||
\end{array} \right \} | \end{array} \right \} | ||
Linia 164: | Linia 167: | ||
by uzyskać | by uzyskać | ||
− | <math>\left \{\begin{array}{l} \mathbf{if}\ n\neq m\\ | + | :<math>\left \{\begin{array}{l} \mathbf{if}\ n\neq m\\ |
\mathbf{then} \\ | \mathbf{then} \\ | ||
\quad r:=0;\\ \quad \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ | \quad r:=0;\\ \quad \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ | ||
\quad \mathbf{then}\\ | \quad \mathbf{then}\\ | ||
− | \qquad n\_mniejsze:=true;\ | + | \qquad n\_mniejsze:=true;\ maks:=m\\ \quad \mathbf{else}\\ |
− | \qquad n\_mniejsze:=false;\ | + | \qquad n\_mniejsze:=false;\ maks:=n\\ \quad \mathbf{fi};\\ |
\quad q:=0 \\ | \quad q:=0 \\ | ||
− | \quad \mathbf{while} \ r\neq | + | \quad \mathbf{while} \ r\neq maks \\ \quad \mathbf{do}\\ |
\qquad r:=r+1;\ q:=q+1\\ \quad \mathbf{od} \\ | \qquad r:=r+1;\ q:=q+1\\ \quad \mathbf{od} \\ | ||
\mathbf{fi} \end{array} \right \} | \mathbf{fi} \end{array} \right \} | ||
− | \left( \begin{array}{l} ( r= | + | \left( \begin{array}{l} ( r=maks \land maks=\mathrm{max}(n,m)) \land \\ |
((n\_mniejsze \land q=m-n)\lor(\neg n\_mniejsze \land q=n-m))\end{array} \right) </math> | ((n\_mniejsze \land q=m-n)\lor(\neg n\_mniejsze \land q=n-m))\end{array} \right) </math> | ||
Linia 183: | Linia 186: | ||
co pozwala mi udowodnić następującą implikację | co pozwala mi udowodnić następującą implikację | ||
− | <math>\color{red} | + | :<math>(\color{red} { \mathrm{max}(n,m) = l } \color{black}) {\Rightarrow \left \{\begin{array}{l} \mathbf{if}\ n\neq m\\ |
\mathbf{then} \\ | \mathbf{then} \\ | ||
\quad r:=0;\\ \quad \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ | \quad r:=0;\\ \quad \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ | ||
\quad \mathbf{then}\\ | \quad \mathbf{then}\\ | ||
− | \qquad n\_mniejsze:=true;\ | + | \qquad n\_mniejsze:=true;\ maks:=m\\ \quad \mathbf{else}\\ |
− | \qquad n\_mniejsze:=false;\ | + | \qquad n\_mniejsze:=false;\ maks:=n\\ \quad \mathbf{fi};\\ |
\quad q:=0 \\ | \quad q:=0 \\ | ||
− | \quad \mathbf{while} \ r\neq | + | \quad \mathbf{while} \ r\neq maks \\ \quad \mathbf{do}\\ |
\qquad r:=r+1;\ q:=q+1\\ \quad \mathbf{od}; \\ | \qquad r:=r+1;\ q:=q+1\\ \quad \mathbf{od}; \\ | ||
\quad \mathbf{if}\ n\_mniejsze\ \mathbf{then}\ m:=q\ \mathbf{else}\ n := q \ \mathbf{fi}; \\ | \quad \mathbf{if}\ n\_mniejsze\ \mathbf{then}\ m:=q\ \mathbf{else}\ n := q \ \mathbf{fi}; \\ | ||
− | \mathbf{fi} \end{array} \right \} | + | \mathbf{fi} \end{array} \right \} } |
− | \ ( \color{red} max(n,m)<l | + | \ ( \color{red} { \mathrm{max}(n,m))< l })</math> |
− | + | Zastosujemy lemat (N3'). Powiada on, dla każdego n, powtarzając odejmowanie 1 otrzymamy w końcu 0. Z tego powodu pętla zewnętrzna musi zakończyć swe obliczenia: nie można zmniejszać bez końca wartości <math>max(n,m)</math>. Przy okazji uzyskaliśmy, bardzo niedoskonałe, oszacowanie górne kosztu algorytmu <math>O(max(n,m)^2)</math>. | |
== Dowód poprawności algorytmu Euklidesa == | == Dowód poprawności algorytmu Euklidesa == | ||
− | Należy wykazać, że wynik algorytmu Euklidesa to największy wspólny dzielnik. | + | Należy wykazać, że wynik algorytmu Euklidesa dla danych ''x'' i ''y'' to największy wspólny dzielnik. |
Z postaci programu widać, że wynik jest największą liczbą <math>n</math>, mniejszą od <math>max(x,y)</math> taką, że ... | Z postaci programu widać, że wynik jest największą liczbą <math>n</math>, mniejszą od <math>max(x,y)</math> taką, że ... | ||
− | <math>n|x</math> i <math>n|y</math>. | + | <math>n | x</math> i <math>n | y</math>. |
Algorytm wyznacza ciąg par <math>\{\langle n_i, m_i \rangle\} </math> taki, że | Algorytm wyznacza ciąg par <math>\{\langle n_i, m_i \rangle\} </math> taki, że | ||
:<math>\langle n_1,m_1 \rangle = \langle x,y \rangle </math> | :<math>\langle n_1,m_1 \rangle = \langle x,y \rangle </math> | ||
− | :<math>\langle n_{i+1},m_{i+1} \rangle = \begin{cases} \langle n_{i}-m_{i},m_{i} \rangle & \text{gdy}\ n_i>m_i \\ | + | :<math>\langle n_{i+1},m_{i+1} \rangle = \begin{cases} \langle n_{i}-m_{i},m_{i} \rangle & \text{gdy}\ n_i> m_i \\ |
− | \langle n_{i},m_{i}-n_i \rangle & \text{gdy}\ n_i<m_i \\ | + | \langle n_{i},m_{i}-n_i \rangle & \text{gdy}\ n_i< m_i \\ |
\mbox{niezdefiniowany} & \text{gdy}\ n_i=m_i | \mbox{niezdefiniowany} & \text{gdy}\ n_i=m_i | ||
\end{cases}</math> | \end{cases}</math> | ||
Linia 215: | Linia 218: | ||
:<math>\mathrm{NWD}( n_{i+1},m_{i+1})= \mathrm{NWD}( n_{i},m_{i}) </math> | :<math>\mathrm{NWD}( n_{i+1},m_{i+1})= \mathrm{NWD}( n_{i},m_{i}) </math> | ||
− | Ciąg wartości <math>\mathrm{max}( n_{i},m_{i}) </math> jest ciągiem ściśle malejącym. | + | Ciąg wartości <math>\mathrm{max}( n_{i},m_{i}) </math> jest ciągiem ściśle malejącym, ograniczonym od dołu przez 1. |
::::::::przejdź do [[algorytm Euklidesa|algorytmu Euklidesa]] | ::::::::przejdź do [[algorytm Euklidesa|algorytmu Euklidesa]] | ||
: | : | ||
− | ::::::::powrót do [[wybrane przykłady]] | + | :::::::::::::::::powrót do [[wybrane przykłady]] |
Aktualna wersja na dzień 20:05, 23 sie 2015
Należy udowodnić że algorytm zawsze kończy obliczenia.
Dowodu nie da się przeprowadzić opierając się na aksjomatach Peano. Zacznijmy od obserwacji, że algorytm Euklidesa w niestandardowym modelu liczb naturalnych może nie zakończyć obliczeń. (Lub, ujmując to inaczej - jest taka klasa K w której ten algorytm nie kończy obliczeń.)
Na jakich więc podstawach ma się oprzeć dowód własności stop algorytmu?
Okaże się, że wystarczą trzy następujące:
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}\ m:=m+1\ \mathbf{od}](m=n) } [/math]
Możemy zdefiniować relacje mniejszości
Definicja
[math]\color{blue} {x \lt y\ \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]
Lemat
- (N3') [math] \quad \color{blue}{ (\forall n \neq 0)[ \mathbf{while}\ n \neq 0\ \mathbf{do}\ n:=n \stackrel{_\centerdot}{-}1\ \mathbf{od}](n=0)}[/math]
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 (zasada Archimedesa)
Jeśli [math] \color{blue}{ 0 \lt n \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\gt m) } [/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} \mathbf{if}\ n\neq m\\ \mathbf{then} \\ \quad r:=0;\\\quad \mathbf{while} \ r \neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ \quad \mathbf{then}\\ \qquad n\_mniejsze:=true;\ maks:=m\\\quad \mathbf{else}\\ \qquad n\_mniejsze:=false;\ maks:=n\\\quad \mathbf{fi};\\ \mathbf{fi} \end{array} \right \} \ ((r=n \land n\lt m)\lor (r=m \land m\gt n )\land maks=\mathrm{max}(n,m))[/math]
Jeszcze raz korzystamy z aksjomatu (N3)
- [math]\{ r:=0; \mathbf{while} \ r\neq maks \ \mathbf{do}\ r:=r+1\ \mathbf{od}\} \ r=maks [/math]
- [math]\left \{\begin{array}{l} \mathbf{if}\ n\neq m\\ \mathbf{then} \\ \quad r:=0;\\ \quad \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ \quad \mathbf{then}\\ \qquad n\_mniejsze:=true;\ maks:=m\\ \quad \mathbf{else}\\ \qquad n\_mniejsze:=false;\ maks:=n\\ \quad \mathbf{fi};\\ \quad r:=0;\\ \quad \mathbf{while} \ r\neq maks \ \mathbf{do}\ r:=r+1\ \mathbf{od} \\ \mathbf{fi} \end{array} \right \} \ ( r=maks \land maks=\mathrm{max}(n,m))[/math]
Skorzystam z prawa przerwania i wznowienia podróży
- [math]\left \{\begin{array}{l} r:=0;\\ \mathbf{while} \ r\neq \mathrm{max}(n,m) \\ \mathbf{do}\\ \quad r:=r+1 \\ \mathbf{od}; \\ \end{array} \right \} \ ( r=\mathrm{max}(n,m)) \equiv \left \{\begin{array}{l} r:=0;\\ \mathbf{while} \ r\neq min(n,m) \\ \mathbf{do}\\ \quad r:=r+1\\ \mathbf{od}; \\ \mathbf{if}\ r= n\\ \mathbf{then}\\ \quad n\_mniejsze:=true;\\ \quad maks:=m\\ \mathbf{else}\\ \quad n\_mniejsze:=false;\\ \quad maks:=n\\ \mathbf{fi};\\ \mathbf{while} \ r\neq maks \\ \mathbf{do}\\ \quad r:=r+1\\ \mathbf{od} \\ \end{array} \right \} \ ( r=\mathrm{max}(n,m))[/math]
by uzyskać
- [math]\left \{\begin{array}{l} \mathbf{if}\ n\neq m\\ \mathbf{then} \\ \quad r:=0;\\ \quad \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ \quad \mathbf{then}\\ \qquad n\_mniejsze:=true;\ maks:=m\\ \quad \mathbf{else}\\ \qquad n\_mniejsze:=false;\ maks:=n\\ \quad \mathbf{fi};\\ \quad q:=0 \\ \quad \mathbf{while} \ r\neq maks \\ \quad \mathbf{do}\\ \qquad r:=r+1;\ q:=q+1\\ \quad \mathbf{od} \\ \mathbf{fi} \end{array} \right \} \left( \begin{array}{l} ( r=maks \land maks=\mathrm{max}(n,m)) \land \\ ((n\_mniejsze \land q=m-n)\lor(\neg n\_mniejsze \land q=n-m))\end{array} \right) [/math]
w tym programie wstawiam instrukcję
if n_mniejsze then m:=q else n := q fi
co pozwala mi udowodnić następującą implikację
- [math](\color{red} { \mathrm{max}(n,m) = l } \color{black}) {\Rightarrow \left \{\begin{array}{l} \mathbf{if}\ n\neq m\\ \mathbf{then} \\ \quad r:=0;\\ \quad \mathbf{while} \ r\neq n \land r\neq m\ \mathbf{do}\ r:=r+1\ \mathbf{od}; \\ \quad \mathbf{if}\ r=n\\ \quad \mathbf{then}\\ \qquad n\_mniejsze:=true;\ maks:=m\\ \quad \mathbf{else}\\ \qquad n\_mniejsze:=false;\ maks:=n\\ \quad \mathbf{fi};\\ \quad q:=0 \\ \quad \mathbf{while} \ r\neq maks \\ \quad \mathbf{do}\\ \qquad r:=r+1;\ q:=q+1\\ \quad \mathbf{od}; \\ \quad \mathbf{if}\ n\_mniejsze\ \mathbf{then}\ m:=q\ \mathbf{else}\ n := q \ \mathbf{fi}; \\ \mathbf{fi} \end{array} \right \} } \ ( \color{red} { \mathrm{max}(n,m))\lt l })[/math]
Zastosujemy lemat (N3'). Powiada on, dla każdego n, powtarzając odejmowanie 1 otrzymamy w końcu 0. Z tego powodu pętla zewnętrzna musi zakończyć swe obliczenia: nie można zmniejszać bez końca wartości [math]max(n,m)[/math]. Przy okazji uzyskaliśmy, bardzo niedoskonałe, oszacowanie górne kosztu algorytmu [math]O(max(n,m)^2)[/math].
Dowód poprawności algorytmu Euklidesa
Należy wykazać, że wynik algorytmu Euklidesa dla danych x i y to największy wspólny dzielnik.
Z postaci programu widać, że wynik jest największą liczbą [math]n[/math], mniejszą od [math]max(x,y)[/math] taką, że ... [math]n | x[/math] i [math]n | y[/math]. Algorytm wyznacza ciąg par [math]\{\langle n_i, m_i \rangle\} [/math] taki, że
- [math]\langle n_1,m_1 \rangle = \langle x,y \rangle [/math]
- [math]\langle n_{i+1},m_{i+1} \rangle = \begin{cases} \langle n_{i}-m_{i},m_{i} \rangle & \text{gdy}\ n_i\gt m_i \\ \langle n_{i},m_{i}-n_i \rangle & \text{gdy}\ n_i\lt m_i \\ \mbox{niezdefiniowany} & \text{gdy}\ n_i=m_i \end{cases}[/math]
zachodzi przy tym
- [math]\mathrm{NWD}( n_{i+1},m_{i+1})= \mathrm{NWD}( n_{i},m_{i}) [/math]
Ciąg wartości [math]\mathrm{max}( n_{i},m_{i}) [/math] jest ciągiem ściśle malejącym, ograniczonym od dołu przez 1.
- przejdź do algorytmu Euklidesa
-
- powrót do wybrane przykłady