forked from wesolyfoton/aisd-skrypt
-
Notifications
You must be signed in to change notification settings - Fork 1
/
wiesniakow.tex
168 lines (137 loc) · 5.48 KB
/
wiesniakow.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
\section{Algorytm rosyjskich wieśniaków}
Algorytm rosyjskich wieśniaków jest przypisywany sposobowi mnożenia liczb używanemu w XIX-wiecznej Rosji.
Aktualnie jest on stosowany w niektórych układach mnożących.
W celu obliczenia $a \cdot b$ tworzymy tabelkę i liczby $a$ i $b$ zapisujemy w pierwszym jej wierszu.
Kolumnę $a$ wypełniamy następująco: w $i+1$ wierszu wpisujemy wartość z wiersza $i$ podzieloną całkowicie przez 2.
W kolumnie $b$ kolejne wiersze tworzą ciąg geometryczny o ilorazie równym 2.
Wypełnianie tabelki kończymy wtedy, gdy w kolumnie $a$ otrzymamy wartość 1.
Na koniec sumujemy wartości w kolumine $b$ z tych wierszy dla których wartości w kolumine $a$ są nieparzyste.
Uzyskany wynik to $a \cdot b$.
W poniższym przykładzie obliczymy $42 \cdot 17$.
\begin{center}
\begin{tabular}{ c|c }
a & b \\
\hline
42 & 17 \\
\textbf{21} & $17 \cdot 2 = 34$ \\
10 & $17 \cdot 2^2 = 68$ \\
\textbf{5} & $17 \cdot 2^3 = 136$ \\
2 & $17 \cdot 2^4 = 272$ \\
\textbf{1} & $17 \cdot 2^5 = 544$ \\
\end{tabular}
\end{center}
\comment{Jak usuniecie enter po tabelce, to to zdanie nie dostanie w pdfie tabulatora.
Tabulator powinien się znajdować przed akapitami.
To zdanie jest częścią poprzedniego akapitu.}
Wartości $a$ są nieparzyste w wierszach 2, 4 oraz 6. Zatem będziemy sumować wartości $b$ z wierszy 2, 4 i 6.
\begin{equation*}
\begin{split}
a \cdot b &= 17\cdot2 + 17\cdot2^3 + 17\cdot2^5 \\
&= 34 + 136 + 544 \\
&= 714
\end{split}
\end{equation*}
Faktycznie, otrzymaliśmy wynik poprawny. Spójrzmy raz jeszcze na na tę sumę:
\begin{equation*}
\begin{split}
a \cdot b &= 17\cdot2 + 17\cdot2^3 + 17\cdot2^5 \\
&= 17 \cdot ( 2^5 + 2^3 + 2) \\
&= 17 \cdot ( 1 \cdot 2^5 + 0 \cdot 2^4 + 1 \cdot 2^3 + 0 \cdot 2^2 + 1 \cdot 2^1 + 0 \cdot 2^0 ) \\
&=17_{10} \cdot 101010_2 \\
&=17 \cdot 42 = 714
\end{split}
\end{equation*}
Przypomnij sobie algorytm zamiany liczby w systemie dziesiętnym na system binarny.
Okazuje się, że algorytm rosyjskich wieśniaków "po cichu" wylicza tę reprezentację $a$.
W kolejnych paragrafach podamy algorytm i w celu jego udowodnienia sformułujmy \textit{niezmiennik} oraz wykażemy jego prawdziwośc.
\begin{algorithm}[h]
\DontPrintSemicolon
\SetAlgorithmName{Algorytm}{}
\KwData{ $a$, $b$ - liczby naturalne }
\KwResult{ $wynik = a \cdot b$ }
$a' \leftarrow a$\;
$b' \leftarrow b$\;
$wynik \leftarrow 0$\;
\While{\upshape $a' > 0$}
{
\If{\upshape $a' \textsf{ mod } 2 = 1$}
{
$wynik \leftarrow wynik + b'$\;
}
$a' \leftarrow a' \textsf{ div } 2$\;
$b' \leftarrow b' \cdot 2$\;
}
\caption{Algorytm rosyjskich wieśniaków}
\label{alg-wiesniakow}
\end{algorithm}
\begin{theorem}
Niech $a'_i$ (kolejno: $b'_i$, $wynik_i$) będzie wartością zmiennej \texttt{a'} (\texttt{b'}, \texttt{wynik}) w $i-tej$ iteracji pętli \texttt{while}. Zachodzi następujący niezmiennik pętli:
\[
a'_i \cdot b'_i + wynik_i = a \cdot b \enspace.
\]
\end{theorem}
\begin{lemma}
Przed wejściem do pętli \texttt{while} niezmiennik jest prawdziwy.
\end{lemma}
\begin{proof}
Skoro przed przed wejściem do pętli mamy: $a'_0 = a$, $b'_0 = b$ oraz $wynik_0 = 0$, to oczywiście: $a'_0 \cdot b'_0 + wynik_0 = a \cdot b + 0 = a \cdot b$.
\end{proof}
\begin{lemma}
Po $i-tym$ obrocie pętli niezmiennik jest spełniony.
\end{lemma}
\begin{proof}
Załóżmy, że niezmiennik zachodzi w $i-tej$ iteracji i sprawdźmy co dzieje się w $i+1$ iteracji.
\comment{Nie możesz czegoś takiego założyć :)}
Rozważmy dwa przypadki.
\begin{itemize}
\item $a'_i$ parzyste. Instrukcja \texttt{if} się nie wykona, w $i+1$ iteracji $wynik_i$ pozostanie niezmieniony, $a'_i$ zmniejszy się o połowę, a $b'_i$ zwiększy dwukrotnie.
\[
wynik_{i+1} = wynik_i
\]
\[
a'_{i+1} = a'_i \textsf{ div } 2 = \frac{a'_i}{2}
\]
\[
b'_{i+1} = b'_i \cdot 2
\]
W tym przypadku otrzymujemy:
\[
a'_{i+1} \cdot b'_{i+1} + wynik_{i+1} = \frac{a'_i}{2} \cdot 2 b'_i + wynik_i = a'_i \cdot b'_i + wynik_i = a \cdot b
\]
\item $a'_i$ nieparzyste:
\[
wynik_{i+1} = wynik_i + b'_i
\]
\[
a'_{i+1} = a'_i \textsf{ div } 2 = \frac{a'_i-1}{2}
\]
\[
b'_{i+1} = b'_i \cdot 2
\]
Ostatecznie otrzymujemy:
\[
a'_{i+1} \cdot b'_{i+1} + wynik_{i+1} = \frac{a'_i-1}{2} \cdot 2 b'_i + wynik_i +b'_i = a'_i \cdot wynik_i + b'_i= a \cdot b
\]
\end{itemize}
\end{proof}
\begin{lemma}
Po zakończeniu algorytmu $wynik = a \cdot b$
\end{lemma}
\begin{proof}
Wystarczy zauważyć, że tuż po wyjściu z pętli \texttt{while} wartość zmiennej $a'$ wynosi $0$.
Podstawiając do niezmiennika okazuje się, że faktycznie algorytm rosyjskich wieśniaków liczy $a \cdot b$.
\end{proof}
\begin{lemma}
Algorytm sie kończy.
\end{lemma}
\begin{proof}
Skoro $a_i \in \mathbb{N} $ oraz $\mathbb{N}$ jest dobrze uporządkowany, to połowiąc $a_i$ po pewnej liczbie iteracji otrzymamy 0.
\end{proof}
Z powyższych lematów wynika, że niemiennik spełniony jest zarówno przed, w trakcie jak i po zakończeniu algorytmu.
Algorytm rosyjskich wieśniaków jest poprawny.
\paragraph{Złożoność}
Z każdą iteracją połowimy $a'$.
Biorąc pod uwagę kryterium jednorodne pozostałe instrukcje w pętli nic nie kosztują.
Stąd złożoność to $O(\log a)$.
W kryterium logarytmicznym musimy uwzględnić czas dominującej instrukcji: dodawania $wynik \leftarrow wynik + b'$.
W najgorszym przypadku zajmuje ono $O(\log ab)$. Zatem złożoność to $O(\log a \cdot \log ab)$.