Почему моя интуиция о самореферентных ленивых последовательностях неверна?
В Haskell я могу написать самоссылочную последовательность в GHCI, например, так:
λ> let x = 1:map (+1) x
λ> take 5 x
который производит:
[1,2,3,4,5]
Однако моя интуиция о ленивой оценке говорит, что это должно произойти во время расширения
let x = 1:map (+1) x
1:2:map (+1) x
1:2:map (+1) [1, 2] <-- substitution
1:2:2:3:map (+1) x
1:2:2:3:map (+1) [1, 2, 2, 3] <-- substitution
1:2:2:3:2:3:3:4:map (+1) x
...
Это явно не то, что происходит. Я могу видеть образец в правильном ответе. Мы просто перемещаем один элемент в списке за один раз вниз по бесконечному потоку. Шаблон, который я узнаю, и я могу применить его в коде. Однако это не соответствует моей ментальной модели ленивой оценки. Это чувствует себя немного "волшебным". Где моя интуиция не так?
5 ответов
Не забудьте только заменить что-то своим определением. Поэтому всякий раз, когда вы расширяете x, вы должны заменить 1 : map (+1) x, а не его "текущее значение" (что бы это ни значило).
Я воспроизведу идею Джеффри, но с должным уважением к лени.
x = 1 : map (+1) x
take 5 x
= take 5 (1 : map (+1) x) -- x
= 1 : take 4 (map (+1) x) -- take
= 1 : take 4 (map (+1) (1 : map (+1) x) -- x
= 1 : take 4 (2 : map (+1) (map (+1) x)) -- map and (+)
= 1 : 2 : take 3 (map (+1) (map (+1) x)) -- take
= 1 : 2 : take 3 (map (+1) (map (+1) (1 : map (+1) x))) -- x
= 1 : 2 : take 3 (map (+1) (2 : map (+1) (map (+1) x))) -- map and (+)
= 1 : 2 : take 3 (3 : map (+1) (map (+1) (map (+1) x))) -- map and (+)
= 1 : 2 : 3 : take 2 (map (+1) (map (+1) (map (+1) x))) -- take
и так далее.
Упражнение закончите оценку в этом стиле самостоятельно (это довольно информативно).
Обратите внимание, как мы начинаем создавать цепочку map с ростом списка. Если вы просто print x через некоторое время вы начнете замедляться; вот почему. Существует более эффективный способ, оставленный в качестве упражнения (и [1..] обманывает:-).
NB это все еще немного менее ленив, чем то, что на самом деле произойдет. map (+1) (1 : ...) оценивает (1+1) : map (+1) ..., и сложение произойдет только тогда, когда число действительно наблюдается, либо распечатав его, либо, например, сравнив его.
Уилл Несс обнаружил ошибку в этом посте; смотрите комментарии и его ответ.
Вот что происходит. Лень - это не строгость + запоминание (громов). Мы можем показать это, назвав все промежуточные данные, которые появляются как принудительное выражение:
λ> let x = 1 : map (+1) x
>>> x = a1 : x1 -- naming the subexpressions
a1 = 1
x1 = map (+1) x
λ> take 5 x
==> take 5 (a1:x1) -- definition of x
==> a1:take 4 x1 -- definition of take
>>> x1 = map (1+) (1:x1) -- definition of x
= (1+) 1 : map (1+) x1 -- definition of map
= a2 : x2 -- naming the subexpressions
a2 = (1+) 1
x2 = map (1+) x1
==> a1:take 4 (a2:x2) -- definition of x1
==> a1:a2:take 3 x2 -- definition of take
>>> x2 = map (1+) (a2:x2) -- definition of x1
= (1+) a2 : map (1+) x2 -- definition of map
= a3 : x3 -- naming the subexpressions
a3 = (1+) a2
x3 = map (1+) x2
==> a1:a2:take 3 (a3:x3) -- definition of x2
==> a1:a2:a3:take 2 x3 -- definition of take
>>> x3 = map (1+) (a3:x3) -- definition of x2
.....
Элементы в результирующем потоке a1:a2:a3:a4:... каждый ссылается на своего предшественника: a1 = 1; a2 = (1+) a1; a3 = (1+) a2; a4 = (1+) a3; ...,
Таким образом, это эквивалентно x = iterate (1+) 1, Без совместного использования данных и их повторного использования через обратную ссылку (включается в памятку хранения), это будет эквивалентно x = [sum $ replicate n 1 | n <- [1..]] что является радикально менее эффективным вычислением (O (n2) вместо O (n)).
Мы можем объяснить обмен или отказ от обмена с
fix g = x where x = g x -- sharing fixpoint
x = fix ((1:) . map (1+)) -- corecursive definition
_Y g = g (_Y g) -- non-sharing fixpoint
y = _Y ((1:) . map (1+)) -- recursive definition
Попытка распечатать y по подсказке GHCi показывает заметное замедление по мере продвижения вперед. Там нет замедления при распечатке x поток.
(см. также /questions/33341173/chto-proishodit-v-etoj-funktsii-haskell/33341187#33341187 для аналогичного примера).
Вы картируете +1 по всему списку, так что начальный 1 становится n, где n это количество раз, которое вы лениво повторяли, если это имеет смысл. Таким образом, вместо деривации, о которой вы думаете, она выглядит примерно так:
1:... -- [1 ...]
1: map (+1) (1:...) -- [1, 2 ...]
1: map (+1) (1:map (+1) (1:...)) -- [1, 2, 3 ...]
1 добавляется в лениво вычисляемый список, все элементы которого увеличиваются на каждом шаге рекурсии.
Таким образом, вы можете думать о nшаг рекурсии как взятие списка [1, 2, 3, ..., n ...], превращая его в список [2, 3, 4, ..., n+1 ...]и предваряющий 1,
Давайте посмотрим на это немного более математически. Предположим, что
x = [1, 2, 3, 4, ...]
затем
map (+1) x = [2, 3, 4, 5, ...]
так
1 : map (+1) x = 1 : [2, 3, 4, 5, ...] = x
Это (обернулось) уравнение, с которого мы начали:
x = 1 : map (+1) x
Итак, мы показали, что
x = [1, 2, 3, 4, ...]
является решением уравнения
x = 1 : map (+1) x -- Eqn 1
Следующий вопрос, конечно, заключается в том, есть ли какие-либо другие решения уравнения 1. Ответ, как выясняется, - нет. Это важно, потому что модель оценки Хаскелла эффективно выбирает "наименее определенное" решение любого такого уравнения. Например, если мы вместо этого определили x = 1 : tail xзатем любой список, начинающийся с 1 было бы решением, но мы бы на самом деле получить 1 : _|_, где _|_ представляет ошибку или не прекращение. Уравнение 1 не приводит к такого рода беспорядку:
Позволять y быть любым решением уравнения 1, так
y = 1 : map (+1) y
Обратите внимание, что мы можем сказать из определения, что
take 1 y = [1] = take 1 x
Теперь предположим
take n y = take n x
затем
take (n+1) y = take (n+1) (1 : map (+1) y)
= 1 : take n (map (+1) y)
= 1 : map (+1) (take n y)
= 1 : map (+1) (take n x)
= 1 : take n (map (+1) x)
= take (n+1) (1 : map (+1) x)
= take (n+1) x
По индукции мы находим, что take n y = take n x для каждого n, То есть, y = x,
Что вы ошиблись
В вашем порядке оценки:
let x = 1:map (+1) x
1:2:map (+1) x
1:2:map (+1) [1, 2] <-- here
Вы делаете неправильное предположение. Вы предполагаете x является [1, 2] потому что это количество элементов, которые вы можете увидеть там. Это не. Вы забыли считать, что x в конце нужно вычислить рекурсивно.
Фактический поток
x в конце последовательности необходимо вычислить путем рекурсивного вычисления самого себя. Вот фактический поток:
take 5 $ 1:map (+1) ...
take 5 $ 1:map (+1) (1:map (+1) ...
take 5 $ 1:map (+1) (1:map (+1) (1:map (+1) ...
take 5 $ 1:map (+1) (1:map (+1) (1:map (+1) (1:map (+1) ...
take 5 $ 1:map (+1) (1:map (+1) (1:map (+1) (1:map (+1) (1:map (+1) ...
take 5 $ 1:map (+1) (1:map (+1) (1:map (+1) (1:map (+1) [1 ...
take 5 $ 1:map (+1) (1:map (+1) (1:map (+1) [1, 2 ...
take 5 $ 1:map (+1) (1:map (+1) [1, 2, 3 ...
take 5 $ 1:map (+1) [1, 2, 3, 4 ...
take 5 $ [1, 2, 3, 4, 5 ...
[1, 2, 3, 4, 5]