Analiza algorytmu Euklidesa - Historia wersji

AndrzejSalwicki o 19:05, 23 sie 2015

2015-08-23T19:05:53Z

AndrzejSalwicki: /* Dowód własności stop algorytmu Euklidesa */

2015-08-23T19:04:37Z

‎Dowód własności stop algorytmu Euklidesa

AndrzejSalwicki: /* Dowód poprawności algorytmu Euklidesa */

2015-08-23T19:03:29Z

‎Dowód poprawności algorytmu Euklidesa

AndrzejSalwicki o 19:01, 23 sie 2015

2015-08-23T19:01:33Z

AndrzejSalwicki: /* Dowód własności stop algorytmu Euklidesa */

2014-04-09T18:07:31Z

‎Dowód własności stop algorytmu Euklidesa

AndrzejSalwicki o 17:51, 9 kwi 2014

2014-04-09T17:51:39Z

AndrzejSalwicki o 17:48, 9 kwi 2014

2014-04-09T17:48:03Z

AndrzejSalwicki o 08:56, 6 mar 2013

2013-03-06T08:56:55Z

AndrzejSalwicki: /* Dowód poprawności algorytmu Euklidesa */

2013-03-05T20:17:55Z

‎Dowód poprawności algorytmu Euklidesa

AndrzejSalwicki: /* Dowód własności stop algorytmu Euklidesa */

2013-02-27T21:01:07Z

‎Dowód własności stop algorytmu Euklidesa

@@ Linia 82: / Linia 82: @@
 \mathbf{od}; \\
 \end{array} \right]
-(r>m) }
+(r> m) }
 </math>

@@ Linia 122: / Linia 122: @@
 \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>
+\ ((r=n  \land n< m)\lor (r=m \land m> n )\land maks=\mathrm{max}(n,m))</math>
 Jeszcze raz korzystamy z aksjomatu (N3)

@@ Linia 212: / Linia 212: @@
 :<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
 \end{cases}</math>

@@ Linia 19: / Linia 19: @@
 | '''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; \\
 \mathbf{while}\ r\neq x \land r \neq y \\
@@ Linia 35: / Linia 35: @@
 \quad r:=r+1 \\
 \mathbf{od}
-\end{array} \right](r=x) } </math>
+\end{array} \right](r = x) } </math>
 |}
 oraz operację odejmowania
@@ Linia 74: / Linia 74: @@
 '''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}
 r:=n;  \\
@@ Linia 96: / Linia 96: @@
 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>
@@ Linia 105: / Linia 105: @@
 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>
@@ Linia 117: / Linia 117: @@
 :<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 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}\\
@@ Linia 153: / Linia 153: @@
 \quad r:=r+1\\
   \mathbf{od}; \\
-   \mathbf{if}\ r=n\\
+   \mathbf{if}\ r= n\\
   \mathbf{then}\\
 \quad  n\_mniejsze:=true;\\
@@ Linia 186: / Linia 186: @@
 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\\
+:<math>(\color{red} {  \mathrm{max}(n,m) = l  }  \color{black}) {\Rightarrow \left \{\begin{array}{l} \mathbf{if}\ n\neq m\\
 \mathbf{then} \\
@@ Linia 198: / Linia 198: @@
 \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>
+\ ( \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>.
@@ Linia 207: / Linia 207: @@
 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
 :<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 \\
 \mbox{niezdefiniowany}  & \text{gdy}\ n_i=m_i

@@ Linia 186: / Linia 186: @@
 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\\
+:<math>(\color{red} {  \mathrm{max}(n,m) =l  }  \color{black}) {\Rightarrow \left \{\begin{array}{l} \mathbf{if}\ n\neq m\\
 \mathbf{then} \\
@@ Linia 197: / Linia 197: @@
 \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 \}
+\mathbf{fi}  \end{array} \right \} }
-\ ( \color{red}  \mathrm{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 <math>O(max(n,m)^2)</math>.

@@ Linia 11: / Linia 11: @@
 :(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}\ m:=m+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
@@ Linia 19: / Linia 19: @@
 | '''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; \\
 \mathbf{while}\ r\neq x \land r \neq y \\
@@ Linia 25: / Linia 25: @@
 \quad r:=r+1 \\
 \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;
 |'''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; \\
 \mathbf{while}\ r\neq x \land r \neq y \\
@@ Linia 35: / Linia 35: @@
 \quad r:=r+1 \\
 \mathbf{od}
-\end{array} \right](r=x)</math>
+\end{array} \right](r=x) } </math>
 |}
 oraz operację odejmowania
@@ Linia 41: / Linia 41: @@
 '''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; \\
 \mathbf{while}\ r \neq x \
@@ Linia 50: / Linia 50: @@
 \mathbf{od}; \\
 \end{array} \right]
-(wynik = q)
+(wynik = q)}
 </math>
 '''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
-:<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; \\
 \mathbf{while}\ q \neq y \
@@ Linia 68: / Linia 68: @@
 \mathbf{od}; \\
 \end{array} \right]
-(wynik = r)
+(wynik = r) }
 </math>
@@ Linia 74: / Linia 74: @@
 '''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;  \\
 \mathbf{while}\ r \leq m \
@@ Linia 82: / Linia 82: @@
 \mathbf{od}; \\
 \end{array} \right]
-(r>m)
+(r>m) }
 </math>

@@ Linia 204: / Linia 204: @@
 == 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 ...