Analiza algorytmu Euklidesa: Różnice pomiędzy wersjami
| Linia 8: | Linia 8: | ||
:(n3) <math>(\forall n)[m:=0; \mathbf{while}\ m \neq n\ \mathbf{do}\ n:=n+1\ \mathbf{od}](m=n)</math> | :(n3) <math>(\forall n)[m:=0; \mathbf{while}\ m \neq n\ \mathbf{do}\ n:=n+1\ \mathbf{od}](m=n)</math> | ||
| − | Możemy zdefiniować | + | Możemy zdefiniować relacje mniejszości |
| − | + | {| | |
| − | '''Definicja''' | + | |- |
| + | | '''Definicja''' | ||
<math>x<y\ \stackrel{df}{\equiv}\ \neg (x=y) \wedge \left[\begin{array}{l} | <math>x<y\ \stackrel{df}{\equiv}\ \neg (x=y) \wedge \left[\begin{array}{l} | ||
| Linia 19: | Linia 20: | ||
\mathbf{od} | \mathbf{od} | ||
\end{array} \right](r=x)</math> | \end{array} \right](r=x)</math> | ||
| − | + | | | |
| − | '''Definicja''' | + | |'''Definicja''' |
<math>x\leq y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} | <math>x\leq y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} | ||
| Linia 29: | Linia 30: | ||
\mathbf{od} | \mathbf{od} | ||
\end{array} \right](r=x)</math> | \end{array} \right](r=x)</math> | ||
| − | + | |} | |
oraz operację odejmowania | oraz operację odejmowania | ||
| Linia 45: | Linia 46: | ||
(wynik = q) | (wynik = q) | ||
</math> | </math> | ||
| + | |||
| + | i operację dodawania | ||
| + | |||
| + | '''Definicja''' | ||
| + | Operacja dodawania jest określona tak | ||
| + | |||
| + | <math>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) | '''Lemat''' (aksjomat Archimedesa) | ||
| Linia 51: | Linia 68: | ||
<math> \left[\begin{array}{l} | <math> \left[\begin{array}{l} | ||
r:=n; \\ | r:=n; \\ | ||
| − | \mathbf{while}\ r | + | \mathbf{while}\ r \leq m \ |
\mathbf{do} | \mathbf{do} | ||
\quad r:=r+n; \ | \quad r:=r+n; \ | ||
Wersja z 13:06, 15 lut 2013
Należy udowodnić że algorytm zawsze kończy obliczenia.
Algorytmiczne aksjomaty liczb naturalnych:
- (n1) [math](\forall n) (n+1 \neq 0 ) [/math]
- (n2) [math](\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]
Możemy zdefiniować relacje mniejszości
| Definicja
[math]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]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]y \lt x [/math] to operacja odejmowania jest określona tak
[math]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]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] 0\ltn \lt m [/math] to [math] \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]
