GHC测试套件中的这种简短的记忆功能如何工作？

Question

以下是memoization函数的完整可运行代码:

memo f = g
  where
    fz = f Z
    fs = memo (f . S) 
    g  Z    = fz
    g (S n) = fs n
    -- It is a BAD BUG to inline 'fs' inside g
    -- and that happened in 6.4.1, resulting in exponential behaviour

-- memo f = g (f Z) (memo (f . S))
--        = g (f Z) (g (f (S Z)) (memo (f . S . S)))
--        = g (f Z) (g (f (S Z)) (g (f (S (S Z))) (memo (f . S . S . S))))

fib' :: Nat -> Integer
fib'             =  memo fib
  where
  fib Z          =  0
  fib (S Z)      =  1
  fib (S (S n)) = fib' (S n) + fib' n

我试图通过手工扩展这些术语来解决这个问题,但是这种扩展看起来就像是缓慢的,未经修饰的功能.它是如何工作的？注释掉的代码是如何派生出来的？

Answer 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

两者都计算相同的功能.但是,前者将f 0在使用参数调用时始终(重新)计算0.相反,后者f 0只会在第一次使用参数调用时计算0- 当发生这种情况时,会fz对其进行评估,并将结果永久存储在那里,以便下次fz需要时可以再次使用它.

这并没有太大的不同

f 0 + f 0
let fz = f 0 in fz + fz

后者只会调用f 0一次,因为第二次fz将被评估.

所以,我们可以实现轻松的记忆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 ->左侧=,或者我们失去了记忆!

等价的:

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

现在,这只是记忆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.通过这种方式,我们获得了备忘录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,记忆它.

如果调用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都被记忆.