Analiza algorytmu Euklidesa: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(Dowód własności stop algorytmu Euklidesa)
 
(Nie pokazano 14 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 10: Linia 10:
 
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}\ n:=n+1\ \mathbf{od}](m=n)</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
 
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>
 
| &nbsp; &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
 
| &nbsp; &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
 
|'''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'''
 
'''Lemat'''
  
:(N3')&nbsp;&nbsp;&nbsp;&nbsp; <math> \quad \color{blue}   \color{blue} (\forall n \neq 0)[ \mathbf{while}\ n \neq 0\ \mathbf{do}\ n:=n  \stackrel{_\centerdot}{-}1\ \mathbf{od}](n=0)</math>
+
:(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>
 
   
 
   
  
Linia 61: Linia 61:
 
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 68: Linia 68:
 
\mathbf{od}; \\  
 
\mathbf{od}; \\  
 
\end{array} \right]  
 
\end{array} \right]  
(wynik = r)
+
(wynik = r) }
 
</math>
 
</math>
  
Linia 74: Linia 74:
 
'''Lemat''' (zasada Archimedesa)
 
'''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 82: Linia 82:
 
\mathbf{od}; \\  
 
\mathbf{od}; \\  
 
\end{array} \right]  
 
\end{array} \right]  
(r>m)
+
(r> m) }
 
</math>
 
</math>
  
Linia 96: 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>  
  
Linia 105: Linia 105:
 
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>  
  
Linia 117: Linia 117:
 
:<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;\ max:=m\\\quad \mathbf{else}\\
+
\qquad  n\_mniejsze:=true;\ maks:=m\\\quad \mathbf{else}\\
\qquad  n\_mniejsze:=false;\ max:=n\\\quad \mathbf{fi};\\
+
\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 max=\mathrm{max}(n,m))</math>
+
\ ((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 max \ \mathbf{do}\ r:=r+1\ \mathbf{od}\}  
+
:<math>\{ r:=0; \mathbf{while} \ r\neq maks \ \mathbf{do}\ r:=r+1\ \mathbf{od}\}  
\ r=max </math>
+
\ r=maks </math>
  
 
:<math>\left \{\begin{array}{l} \mathbf{if}\ n\neq m\\
 
:<math>\left \{\begin{array}{l} \mathbf{if}\ n\neq m\\
Linia 133: Linia 133:
 
\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;\ max:=m\\ \quad \mathbf{else}\\
+
\qquad  n\_mniejsze:=true;\ maks:=m\\ \quad \mathbf{else}\\
\qquad  n\_mniejsze:=false;\ max:=n\\ \quad \mathbf{fi};\\
+
\qquad  n\_mniejsze:=false;\ maks:=n\\ \quad \mathbf{fi};\\
 
\quad r:=0;\\
 
\quad r:=0;\\
\quad \mathbf{while} \ r\neq max \ \mathbf{do}\ r:=r+1\ \mathbf{od} \\
+
\quad \mathbf{while} \ r\neq maks \ \mathbf{do}\ r:=r+1\ \mathbf{od} \\
 
\mathbf{fi}  \end{array} \right \}
 
\mathbf{fi}  \end{array} \right \}
\ ( r=max \land max=\mathrm{max}(n,m))</math>
+
\ ( 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
Linia 153: 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 max:=m\\  
+
\quad maks:=m\\  
 
\mathbf{else}\\
 
\mathbf{else}\\
 
\quad  n\_mniejsze:=false;\\
 
\quad  n\_mniejsze:=false;\\
\quad max:=n\\  \mathbf{fi};\\
+
\quad maks:=n\\  \mathbf{fi};\\
  \mathbf{while} \ r\neq max \\ \mathbf{do}\\
+
  \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 171: Linia 171:
 
\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;\ max:=m\\ \quad \mathbf{else}\\
+
\qquad  n\_mniejsze:=true;\ maks:=m\\ \quad \mathbf{else}\\
\qquad  n\_mniejsze:=false;\ max:=n\\ \quad \mathbf{fi};\\
+
\qquad  n\_mniejsze:=false;\ maks:=n\\ \quad \mathbf{fi};\\
 
\quad q:=0 \\
 
\quad q:=0 \\
\quad  \mathbf{while} \ r\neq max \\ \quad \mathbf{do}\\
+
\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=max \land max=\mathrm{max}(n,m)) \land \\
+
\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 186: Linia 186:
 
co pozwala mi udowodnić następującą implikację
 
co pozwala mi udowodnić następującą implikację
  
:<math>\color{red}   max(n,m) =l   \color{black} \Rightarrow \left \{\begin{array}{l} \mathbf{if}\ n\neq m\\
+
:<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;\ max:=m\\ \quad \mathbf{else}\\
+
\qquad  n\_mniejsze:=true;\ maks:=m\\ \quad \mathbf{else}\\
\qquad  n\_mniejsze:=false;\ max:=n\\ \quad \mathbf{fi};\\
+
\qquad  n\_mniejsze:=false;\ maks:=n\\ \quad \mathbf{fi};\\
 
\quad q:=0 \\
 
\quad q:=0 \\
\quad  \mathbf{while} \ r\neq max \\ \quad \mathbf{do}\\
+
\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{black})</math>
+
\ ( \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 O(max(n,m)^2).
+
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 218: 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