-
Notifications
You must be signed in to change notification settings - Fork 21
/
Copy pathchapter04.tex
385 lines (348 loc) · 25.6 KB
/
chapter04.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
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
\chapter{Ленивое вычисление}
\label{ch:4}
Ленивое вычисление является основной стратегий вычисления во многих
функциональных языках программирования (но не в Стандартном ML). У
этой стратегии есть два существенных свойства. Во-первых, вычисление
всякого выражения задерживается, или \term{подвешивается}{suspend},
пока не потребуется его результат. Во-вторых, когда задержанное
выражение вычисляется в первый раз, результат вычисления запоминается
(\term{мемоизируется}{memoize}), так что, если он потребуется снова,
можно его просто извлечь из памяти, а не вычислять заново. Оба этих свойства
ленивого вычисления оказываются алгоритмически полезными.
В этой главе мы вводим удобные обозначения для ленивых вычислений и, в
качестве иллюстрации, строим при помощи этой нотации простую
библиотеку потоков. В последующих главах мы будем активно пользоваться
как ленивыми вычислениями вообще, так и потоками в частности.
\section{$\$$-запись}
\label{sc:4.1}
К сожалению, определение Стандартного ML \cite{Milner-etal1997} не
включает поддержки ленивого вычисления, так что каждая реализация
может предоставлять свой собственный набор элементарных операций.
Мы представляем здесь один такой набор,
называемый $\$$-записью. Перевод программ, использующих
$\$$-запись, в другие варианты примитивов ленивого вычисления не
должен представлять трудности.
В $\$$-записи мы вводим новый тип \lstinline!$\alpha$ susp!,
представляющий задержки (задержанные вычисления). У этого типа имеется один
одноместный конструктор $\$$. В первом приближении
\lstinline!$\alpha$ susp! и $\$$ ведут себя так, как будто они введены при помощи
обыкновенного объявления типа
\begin{lstlisting}
datatype $\alpha$ susp = $\$$ of $\alpha$
\end{lstlisting}
Новая задержка типа \lstinline!$\tau$ susp! создается
при помощи конструкции \lstinline!$\$e$!, где $e$~---
выражение типа $\tau$. Подобным же образом, содержимое задержки можно
извлечь через сопоставление с образцом
$\$p$. Если образец $p$ сопоставляется со значениями типа $\tau$, то
$\$p$ сопоставляется с задержками типа
\lstinline!$\tau$ susp!.
Основное различие между $\$$ и обыкновенными конструкторами состоит в
том, что $\$$ не вычисляет свой аргумент немедленно. Вместо этого он
запоминает информацию, необходимую для того, чтобы вычислить
выражение-аргумент позже. (Как правило, эта информация состоит из
указателя на код, а также значений свободных переменных выражения.)
Выражение-аргумент не вычисляется до тех пор, когда (и если) оно не
сопоставится с образцом вида $\$p$. В этот момент выражение
вычисляется, а его результат запоминается. Затем результат
сопоставляется с образцом $p$. Если задержанное выражение потом
сопоставляется с другим образцом вида $\$p'$, запомненное значение
извлекается и сопоставляется с образцом $p'$.
Кроме того, конструктор $\$$ отличается от прочих конструкторов
синтаксически. Во-первых, его область действия распространяется
направо как можно дальше. Таким образом, например, выражение
\lstinline!$\$$f x! равнозначно \lstinline!$\$$(f x)!, а не
\lstinline!($\$$f) x!; образец \lstinline!$\$$Cons (x, xs)! обозначает
то же, что \lstinline!$\$$(Cons (x, xs))!, а не
\lstinline!($\$$ Cons) (x, xs)!. Во-вторых, $\$$ не является правильно
построенным выражением сам по себе~--- он всегда должен сочетаться с
аргументом.
В качестве примера $\$$--записи рассмотрим следующий фрагмент
программы:
\begin{lstlisting}
val s = $\$$primes 1000000 (* $\mbox{быстро}$ *)
...
val $\$$x = s (* $\mbox{медленно}$ *)
...
val $\$$y = s (* $\mbox{быстро}$ *)
...
\end{lstlisting}
Программа вычисляет миллионное простое число. Первая строка, которая
просто создает новую задержку, выполняется очень
быстро. Вторая строка выполняет задержанное вычисление и
находит простое число. В зависимости от алгоритма
поиска простых чисел, она может потребовать значительного
времени. Третья строка обращается к мемоизированному значению и также
выполняется очень быстро.
В качестве второго примера рассмотрим фрагмент
\begin{lstlisting}
let val s = $\$$primes 1000000
in 15 end
\end{lstlisting}
В этой программе содержимое задержки никогда не
требуется, и, значит, выражение \lstinline!primes 1000000! не
выполняется.
Хотя все примеры ленивого вычисления в этой книге можно было бы
выразить только через выражения и образцы со знаком $\$$, удобно
оказывается ввести два элемента синтаксического сахара. Первый из них~---
оператор \lstinline!force! (<<вынудить>>), определяемый как
\begin{lstlisting}
fun force ($\$$x) = x
\end{lstlisting}
Он полезен, чтобы извлечь содержимое задержки посредине
выражения, где было бы неудобно вставлять конструкцию сопоставления с
образцом.
Второй элемент синтаксического сахара полезен при написании некоторых
разновидностей ленивых функций. Рассмотрим, например, следующую
функцию для сложения задержанных целых:
\begin{lstlisting}
fun plus ($\$$m, $\$$n) = $\$$m+n
\end{lstlisting}
Несмотря на то, что определение функции выглядит совершенно разумно,
скорее всего, это не та функция, которую мы хотели написать. Проблема
состоит в том, что оба ее задержанных аргумента выполняются слишком
рано. Они вынуждаются в момент применения функции
\lstinline!plus!, а не тогда, когда требуется выполнить задержку,
создаваемую ей. Один из способов получить нужное
поведение~--- явным образом задержать сопоставление с образцом
\begin{lstlisting}
fun plus (x, y) = $\$$case (x, y) of ($\$$m, $\$$n) $\Rightarrow$ m+n
\end{lstlisting}
Подобные конструкции встречаются достаточно часто, поэтому мы введём
для них синтаксический сахар
\begin{lstlisting}
fun lazy f p = e
\end{lstlisting}
что равносильно
\begin{lstlisting}
fun f x = $\$$case x of p $\Rightarrow$ force e
\end{lstlisting}
При помощи дополнительного \lstinline!force! мы добиваемся того, что
ключевое слово \lstinline!lazy! никак не влияет на тип функции (если
предположить, что он уже был \lstinline!$\alpha$ susp!), так что эту
аннотацию можно добавлять и убирать, никак не меняя остальной
текст. Теперь требуемую нам функцию для сложения задержанных целых
можно написать просто как
\begin{lstlisting}
fun lazy plus ($\$$m, $\$$n) = $\$$m+n
\end{lstlisting}
Раскрытие синтаксического сахара дает
\begin{lstlisting}
fun plus (x, y) = $\$$case (x, y) of ($\$$m, $\$$n) $\Rightarrow$ force ($\$$m+n)
\end{lstlisting}
что совпадает с ранее вручную написанной версией с
точностью до дополнительных \lstinline!force! и $\$$ вокруг
\lstinline!m+n!. Хороший компилятор уберет эти \lstinline!force! и
$\$$ при оптимизации, поскольку для любого $e$ выражения $e$ и
\lstinline!force ($\$e$)! эквивалентны.
В функции \lstinline!plus! аннотация \lstinline!lazy! используется для
задержки сопоставления с образцом, чтобы $\$$-образцы не были
сопоставлены раньше времени. Однако аннотация \lstinline!lazy! полезна
также, когда правая сторона определения функции возвращает задержку
в результате вычисления, которое может оказаться долгим и
сложным. В такой ситуации использование \lstinline!lazy! сдвигает
выполнение дорогого вычисления от того момента, когда функция
применяется к аргументу, на тот, когда вынуждается возвращаемая ею
задержка. В следующем разделе мы увидим несколько
примеров такого использования \lstinline!lazy!.
Синтаксис и семантика $\$$-записи формально определены в
\cite{Okasaki1996a}.
\section{Потоки}
\label{sc:4.2}
В качестве расширенного примера ленивых вычислений и $\$$-записи в
Стандартном ML мы представляем простой пакет для работы с
потоками. Потоки будут использоваться в нескольких структурах данных
из последующих глав.
Потоки (известные также как ленивые списки) подобны обыкновенным
спискам, за исключением того, что вычисление каждой их ячейки задерживается. Тип
потоков выглядит так:
\begin{lstlisting}
datatype $\alpha$ StreamCell = Nil | Cons of $\alpha$ $\times$ $\alpha$ Stream
withtype $\alpha$ Stream = $\alpha$ StreamCell susp
\end{lstlisting}
Простой поток, содержащий элементы 1, 2 и 3, можно записать как
\begin{lstlisting}
$\$$Cons (1, $\$$Cons (2, $\$$Cons (3, $\$$Nil)))
\end{lstlisting}
Полезно сравнить потоки с задержанными списками типа
\lstinline!$\alpha$ list susp!. Вычисления, представленные последними,
по существу {\em монолитны}~--- единожды начав вычислять задержанный
список, мы вычисляем его до конца. Напротив, вычисления,
представленные потоками, часто {\em пошаговы}~--- при обращении к
потоку проводится только та часть вычисления, которая порождает его
первый элемент, а остальное задерживается. Такое поведение часто
встречается в типах, которые, подобно потокам, содержат вложенные
задержки.
Чтобы яснее прочувствовать эту разницу в поведении, рассмотрим функцию
конкатенации, записываемую \lstinline!s $\concat$ t!. Для задержанных
списков ее можно записать как
\begin{lstlisting}
fun s $\concat$ t = $\$$(force s @ force t)
\end{lstlisting}
что равносильно
\begin{lstlisting}
fun lazy ($\$$xs) $\concat$ ($\$$ys) = $\$$(xs @ ys)
\end{lstlisting}
Задержка, порождаемая этой функцией, вынуждает оба аргумента, а затем
конкатенирует полученные списки и возвращает результат целиком. Таким
образом, задержка монолитна. Можно также сказать, что монолитна вся
функция. Для потоков функция записывается как
\begin{lstlisting}
fun lazy ($\$$Nil) $\concat$ t = t
| ($\$$Cons (x, s)) $\concat$ t = $\$$Cons (x, s $\concat$ t)
\end{lstlisting}
Эта функция немедленно возвращает задержку, которая, будучи запущена,
требует первую ячейку первого потока, сопоставляя ее с
$\$$-образцом. Если эта ячейка представляет собой \lstinline!Cons!, мы
строим результат из \lstinline!x! и \lstinline!s $\concat$ t!.
Вследствие аннотации \lstinline!lazy! рекурсивный вызов просто
порождает ещё одну задержку, не производя никакой дополнительной
работы. Следовательно, эта функция описывает пошаговое вычисление:
порождается первая ячейка результата, а остальное задерживается. Мы
также говорим, что пошаговой является сама функция.
Ещё одна пошаговая функция~--- \lstinline!take!, извлекающая первые
$n$ элементов потока.
\begin{lstlisting}
fun lazy take (0, s) = $\$$Nil
| take (n, $\$$Nil) = $\$$Nil
| take (n, $\$$Cons (x, s)) = $\$$Cons (x, take (n-1, s))
\end{lstlisting}
Как и в случае с $\concat$, рекурсивный вызов \lstinline!take!
немедленно возвращает задержку, а не выполняет оставшуюся часть кода
функции.
Рассмотрим, однако, функцию, уничтожающую первые $n$ элементов потока,
которую можно записать как
\begin{lstlisting}
fun lazy drop (0, s) = s
| drop (n, $\$$Nil) = $\$$Nil
| drop (n, $\$$Cons (x, s)) = drop (n-1, s)
\end{lstlisting}
или, более эффективно, как
\begin{lstlisting}
fun lazy drop (n, s) = let fun drop' (0, s) = s
| drop' (n, $\$$Nil) = $\$$Nil
| drop' (n-1, $\$$Cons (x, s)) = drop' (n-1, s)
in drop' (n, s) end
\end{lstlisting}
Эта функция монолитна, поскольку рекурсивные вызовы \lstinline!drop'!
никогда не задерживаются~--- вычисление первой же ячейки результата
требует выполнения всей функции целиком. Здесь аннотация
\lstinline!lazy! используется, чтобы задержать исходный вызов
\lstinline!drop'!, а не сопоставление с образцом.
\begin{exercise}\label{ex:4.1}
Покажите, используя эквивалентность \lstinline!force ($\$e$)! и $e$,
что два определения \lstinline!drop! эквивалентны.
\end{exercise}
Ещё одна часто используемая монолитная функция над потоками~---
\lstinline!reverse!.
\begin{lstlisting}
fun lazy reverse s =
let fun reverse' ($\$$Nil, r) = r
| reverse' ($\$$Cons (x, s), r) = reverse' (s, $\$$Cons (x, r))
in reverse' (s, $\$$Nil) end
\end{lstlisting}
Здесь рекурсивные вызовы \lstinline!reverse'! никогда не
задерживаются. Обратите внимание, однако, что каждый такой вызов
создает задержку вида \lstinline!$\$$Cons (x, r)!. Может показаться,
что \lstinline!reverse! на самом деле не производит всю работу за один
раз. Однако задержки такого вида, где тело содержит лишь
несколько конструкторов и переменных, называются
\term{тривиальными}{trivial}. Тривиальные задержки создаются не из
каких-то алгоритмических соображений, а для того, чтобы удовлетворить
систему типов. Можно считать, что тело тривиальной задержки
выполняется в момент ее создания. На самом деле, при минимальной
оптимизации компилятором подобные задержки создаются уже в
мемоизированном виде. В любом случае, вынуждение тривиальной
задержки никогда не занимает больше, чем $O(1)$ времени.
Несмотря на распространенность монолитных функций над потоками вроде
\lstinline!drop! и \lstinline!reverse!, смыслом существования потоков
являются пошаговые функции вроде $\concat$ и \lstinline!take!. Каждая
задержка несет с собой небольшие, но существенные расходы, поэтому для
максимальной эффективности ленивость следует использовать только тогда,
когда для этого есть серьезные основания. Если все операции над
ленивыми списками в каком-то приложении монолитны, то в этом
приложении лучше пользоваться обыкновенными ленивыми списками, а не
потоками.
На Рис.~\ref{fig:4.1} потоковые функции собраны в единый модуль на
Стандартном ML. Заметим, что в модуле не экспортируются, как можно
было бы ожидать, функции вроде \lstinline!isEmpty! и
\lstinline!cons!. Вместо этого мы намеренно выставляем для обозрения
внутреннее представление, чтобы поддержать для потоков сопоставление с
образцом.
\begin{figure}
\centering
\begin{lstlisting}
signature STREAM = sig
datatype $\alpha$ StreamCell $=$ Nil | Cons of $\alpha \times \alpha$ Stream
withtype $\alpha$ Stream $=$ $\alpha$ StreamCell susp
val $\concat$ : $\alpha$ Stream $\times \alpha$ Stream $\rightarrow \alpha$ Stream /*$\mbox{ Конкатенация потоков }$*/
val take : int $\times \alpha$ Stream $\rightarrow \alpha$ Stream
val drop : int $\times \alpha$ Stream $\rightarrow \alpha$ Stream
val reverse : $\alpha$ Stream $\rightarrow \alpha$ Stream
end
structure Stream: STREAM = struct
datatype $\alpha$ StreamCell $=$ Nil | Cons of $\alpha \times \alpha$ Stream
withtype $\alpha$ Stream $=$ $\alpha$ StreamCell susp
fun lazy ($\$$Nil) ++ t = t
| ($\$$Cons(x,s)) ++ t $= \$$Cons(x,s++t)
fun lazy take (0,s) $= \$$Nil
| take (n, $\$$Nil) $= \$$Nil
| take (n, $\$$Cons(x,s)) $= \$$Cons(x,take(n-1,s))
fun lazy drop (n, s) =
let fun drop' (0, s) = s
| drop' (n, $\$$Nil) $= \$$Nil
| drop' (n-1, $\$$Cons (x, s)) $=$ drop' (n-1, s)
in drop' (n, s) en
fun lazy reverse s =
let fun reverse' ($\$$Nil, r) $=$ r
| reverse' ($\$$Cons(x, s), r) $=$ reverse' (s, $\$$Cons(x, r))
in reverse' (s, $\$$Nil) end
end
\end{lstlisting}
\centering
\caption{Небольшой пакет потоков.}
\label{fig:4.1}
\end{figure}
\begin{exercise}\label{ex:4.2}
Реализуйте сортировку вставками для потоков. Покажите, что
извлечение первых $k$ элементов \lstinline!sort xs! требует лишь
$O (n \cdot k)$ времени, где $n$~--- длина \lstinline!xs!, а не
$O(n^2)$, как можно было бы ожидать от сортировки вставками.
\end{exercise}
\section{Примечания}
\label{sc:4.3}
\textbf{Ленивое вычисление.} Ленивое вычисление было изобретено
Уодсвортом \cite{Wadsworth1971} как оптимизация нормального порядка
редукции в лямбда-исчислении. Позже Виллемин \cite{Vuillemin1974}
показал, что при некоторым образом ограниченных условиях ленивое
вычисление является оптимальной стратегией вычисления. Формальная
семантика ленивого вычисления подробно исследовалась в
\cite{Josephs1989, Launchbury1993, OkasakiLeeTarditi1994, Ariola-etal1995}.
\noindent
\textbf{Потоки.} Потоки изобрел Ландин \cite{Landin1965}, но без
мемоизации. Фридман и Уайз \cite{FriedmanWise1976} и Хендерсон и
Моррис \cite{HendersonMorris1976} расширили потоки Ландина
мемоизацией.
\noindent
\textbf{Мемоизация.} Термин <<мемоизация>> придумал Мичи
\cite{Michie1968}, чтобы называть так кэширование пар
аргумент-результат у функции. Поле аргумента можно отбросить при мемоизации
задержек, если рассматривать задержки как нульместные функции, то
есть функции с нулем аргументов. Позднее Хьюз \cite{Hughes1985}
применил мемоизацию в исходном смысле Мичи к функциональным
программам.
\noindent
\textbf{Алгоритмика.} Обе компоненты ленивых вычислений~--- задержка
вычисления и мемоизация результатов,~--- имеют долгую историю в науке
построения алгоритмов, хотя и не всегда в сочетании друг с
другом. Идея задержки вычислений, которые могут оказаться дорогими
(часто это уничтожение элементов) с пользой используется в
хэш-таблицах \cite{vanWykVitter1986}, очередях с приоритетами
\cite{SleatorTarjan1986b, FredmanTarjan1987} и деревьях поиска
\cite{Driscoll-etal1989}. В свою очередь, мемоизация является основой
таких методик, как динамическое программирование \cite{Bellman1957} и
сжатие путей \cite{HopcroftUllman1973, TarjanvanLeeuwen1984}.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "pfds"
%%% End: