Analiza algorytmu Euklidesa: Różnice pomiędzy wersjami
(Utworzył nową stronę „ Należy udowodnić że algorytm zawsze kończy obliczenia. Algorytmiczne aksjomaty liczb naturalnych: :(n1) <math>(\forall n) (n+1 \neq 0 ) </math> :(n2) <math>(\...”) |
|||
| Linia 12: | Linia 12: | ||
'''Definicja''' | '''Definicja''' | ||
| − | <math>x<y \ | + | <math>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 19: | Linia 19: | ||
\mathbf{od} | \mathbf{od} | ||
\end{array} \right](r=x)</math> | \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 < 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> | ||
| + | |||
| + | '''Lemat''' (aksjomat Archimedesa) | ||
| + | |||
| + | Jeśli <math> 0<n < m </math> to | ||
| + | <math> \left[\begin{array}{l} | ||
| + | r:=n; \\ | ||
| + | \mathbf{while}\ r < m \ | ||
| + | \mathbf{do} | ||
| + | \quad r:=r+n; \ | ||
| + | \mathbf{od}; \\ | ||
| + | \end{array} \right] | ||
| + | (r>m) | ||
| + | </math> | ||
Wersja z 11:47, 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ć relację 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]
Lemat (aksjomat Archimedesa)
Jeśli [math] 0\ltn \lt m [/math] to [math] \left[\begin{array}{l} r:=n; \\ \mathbf{while}\ r \lt m \ \mathbf{do} \quad r:=r+n; \ \mathbf{od}; \\ \end{array} \right] (r\gtm) [/math]
