Tekst źródłowy strony Analiza algorytmu Euklidesa


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 [[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 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 < 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>
| &nbsp; &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|'''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 < 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')&nbsp;&nbsp;&nbsp;&nbsp; <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 < n < 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> 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< m)\lor (r=m \land m> 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))< 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> m_i \\  
\langle n_{i},m_{i}-n_i \rangle & \text{gdy}\ n_i< 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 [[algorytm Euklidesa|algorytmu Euklidesa]]
:
:::::::::::::::::powrót do [[wybrane przykłady]]