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

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 8: Linia 8:
 
Algorytmiczne aksjomaty liczb naturalnych:
 
Algorytmiczne aksjomaty liczb naturalnych:
  
:(N1) <math>(\forall n) (n+1 \neq 0 ) </math>
+
:(N1) <math>\color{blue} (\forall n) (n+1 \neq 0 ) </math>
:(N2) <math>(\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>(\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}\ n:=n+1\ \mathbf{od}](m=n)</math>
  
 
Możemy zdefiniować relacje mniejszości
 
Możemy zdefiniować relacje mniejszości
Linia 17: Linia 17:
 
| '''Definicja'''
 
| '''Definicja'''
  
<math>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 27: Linia 27:
 
|'''Definicja'''
 
|'''Definicja'''
  
<math>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 39: Linia 39:
 
'''Definicja'''
 
'''Definicja'''
  
Jeśli <math>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>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 56: Linia 56:
 
Operacja dodawania jest określona tak
 
Operacja dodawania jest określona tak
  
<math>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 \   

Wersja z 10:54, 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 sie.

Dowód poprawności algorytmu Euklidesa

Należy wykazać, że ...



przejdź do algorytmu Euklidesa
powrót do wybrane przykłady