Ответ 1
Это довольно сложно объяснить. Я начну с более простого примера.
Нужно иметь в виду разницу между
\x -> let fz = f 0 in if x==0 then fz else f x
let fz = f 0 in \x -> if x==0 then fz else f x
Оба вычисляют одну и ту же функцию. Тем не менее, первый всегда (re) вычисляет f 0 при вызове с аргументом 0. Вместо этого последний будет вычислять f 0 только в первый раз, когда он вызывается с аргументом 0 - когда это произойдет, fz оценивается и результат сохраняется там навсегда, так что его можно снова использовать повторно в следующий раз fz.
Это не слишком отличается от
f 0 + f 0
let fz = f 0 in fz + fz
где последний вызовет f 0 только один раз, так как второй раз fz будет уже оценен.
Таким образом, мы могли бы получить свежую memoization f, сохраняя только f 0 следующим образом:
g = let fz = f 0 in \x -> if x==0 then fz else f x
Эквивалентное:
g = \x -> if x==0 then fz else f x
where
fz = f 0
Обратите внимание, что здесь мы не можем принести \x -> слева от =, или мы теряем memoization!
Эквивалентное:
g = g'
where
fz = f 0
g' = \x -> if x==0 then fz else f x
Теперь мы можем без проблем принести \x -> слева.
Эквивалентное:
g = g'
where
fz = f 0
g' x = if x==0 then fz else f x
Эквивалентное:
g = g'
where
fz = f 0
g' 0 = fz
g' x = f x
Теперь это только memoizes f 0 вместо каждого f n. Действительно, вычисление g 4 дважды приведет к вычитанию f 4.
Чтобы этого избежать, мы можем начать делать g для работы с любой функцией f вместо фиксированной:
g f = g' -- f is now a parameter
where
fz = f 0
g' 0 = fz
g' x = f x
Теперь мы используем следующее:
-- for any f, x
g f x = f x
-- hence, in particular
g (f . succ) (pred x) = (f . succ) (pred x) = f (succ (pred x)) = f x
Итак, g (f . succ) (pred x) - сложный способ записи f x. Как обычно, g запоминает функцию в нуле. Однако это (f . succ) 0 = f 1. Таким образом, мы получили memoization вместо 1!
Следовательно, мы можем рекурсировать
g f = g' -- f is now a parameter
where
fz = f 0
g' 0 = fz
g' x = g (f . succ) (pred x)
Если вызывается с помощью 0, то используется fz для хранения f 0, сохраняя его memoizing.
Если вызвано с 1, это вызовет g (f . succ), который выделит другой fz для случая 1.
Это выглядит хорошо, но fz длится недолго, поскольку он будет перераспределяться каждый раз, когда вызывается g' x, отрицая memoization.
Чтобы исправить эту проблему, мы используем другую переменную, так что g (f . succ) будет вычисляться только один раз, самое большее.
g f = g' -- f is now a parameter
where
fz = f 0
fs = g (f . succ)
g' 0 = fz
g' x = fs (pred x)
Здесь fs оценивается не более одного раза и приведет к выделению другого fz для случая 1. Этот fz теперь не исчезнет.
Рекурсивно можно убедиться, что теперь все значения f n запоминаются.