如何使用等式推导化简Haskell中take 3 (fibs)表达式？

代码定义 #

fibs = 1 : scanl (+) 1 fibs

scanl :: (a -> b -> a) -> a -> [b] -> [a] 
scanl f q ls =
    q : (case ls of 
            [] -> []
            x:xs -> scanl f (f q x) xs
        )

take                   :: Int -> [a] -> [a]
take n _      | n <= 0 =  []
take _ []              =  []
take n (x:xs)          =  x : take (n-1) xs

问题描述 #

需要化简表达式 take 3 (fibs)，我的推导进行到一半卡住了：

take 3 (fibs)
= 
take 3 (1 : scanl (+) 1 fibs)
= 
1 : take 2 (scanl (+) 1 fibs)
= 
1 : take 2 (scanl (+) 1 (1 : (scanl (+) 1 fibs)))
=
...

请问该如何继续推导？

后来我继续推导，但结果不符合预期——我以为下一个斐波那契数应该是5，哪里出错了？我的推导过程：

take 3 (fibs)
= 
take 3 (1 : scanl (+) 1 fibs)
= 
1 : take 2 (scanl (+) 1 fibs)
= 
1 : take 2 (scanl (+) 1 (1 : (scanl (+) 1 fibs)))
= 
1 : take 2 (1 : scanl (+) 2 (scanl (+) 1 fibs))
= 
1 : 1 : take 1 (scanl (+) 2 (scanl (+) 1 fibs))
= 
1 : 1 : take 1 (scanl (+) 2 (1 : scanl (+) 1 fibs))
= 
1 : 1 : take 1 (2 : scanl (+) 3 (scanl (+) 1 fibs))
= 
1 : 1 : 2 : take 0 (scanl (+) 3 (1 : scanl (+) 1 fibs))
= 
1 : 1 : 2 : take 0 (3 : scanl (+) 4 (1 : scanl (+) 1 fibs))
= 
...

问题分析与正确推导 #

错误原因 #

你的核心误解有两个：

1. 推导时没必要无限展开后续的scanl，因为take 0 _直接等于[]，到1:1:2:take0 (...)就可以终止推导了；
2. 混淆了take的参数含义：take 3 fibs取的是序列的前3个元素，而这个定义下的fibs是[1,1,2,3,5,...]，前3个元素本来就是[1,1,2]，5是第5个元素，需要用take 5 fibs才能得到。

正确推导步骤 #

我们严格按照定义逐步展开，时刻利用fibs = 1 : s（其中s = scanl (+)1 fibs）来避免混淆：

1. 初始表达式：

take 3 fibs

2. 代入fibs的递归定义：

= take 3 (1 : scanl (+) 1 fibs)

3. 应用take的规则（take n (x:xs) = x : take (n-1) xs）：

= 1 : take 2 (scanl (+) 1 fibs)

4. 展开scanl (+)1 fibs：
   先代入fibs = 1 : s到scanl的参数，再应用scanl的规则：

scanl (+)1 fibs = scanl (+)1 (1 : s)
= 1 : scanl (+) (1+1) s
= 1 : scanl (+)2 s

把这个结果代入上一步：

= 1 : take 2 (1 : scanl (+)2 s)

5. 再次应用take规则：

= 1 : 1 : take 1 (scanl (+)2 s)

6. 展开scanl (+)2 s：
   因为s = scanl(+)1 fibs = 1 : scanl(+)2 s，代入后应用scanl规则：

scanl (+)2 s = scanl (+)2 (1 : scanl(+)2 s)
= 2 : scanl (+) (2+1) (scanl(+)2 s)
= 2 : scanl (+)3 (scanl(+)2 s)

代入上一步：

= 1 : 1 : take1 (2 : scanl(+)3 (...))

7. 应用take规则：

= 1 : 1 : 2 : take0 (scanl(+)3 (...))

8. 应用take0 _ = []：

= 1:1:2:[]
= [1,1,2]

推导包含5的结果（take5 fibs） #

如果想要得到包含5的序列，需要推导take5 fibs，继续上面的步骤：
从take1 (scanl(+)3 (...))开始：

scanl(+)3 (scanl(+)2 s) = scanl(+)3 (2 : scanl(+)3 (...))
=3 : scanl(+) (3+2) (...)
=3 : scanl(+)5 (...)

所以take1这个序列得到3，take2得到3:5，最终take5 fibs会是[1,1,2,3,5]。

内容的提问来源于stack exchange，提问作者F. Zer