最近入了本SICP，发现自己对Lisp没以前那么反感了……好像括号看起来还不错……

OwnWaterloo

回复 54# starwing83

似乎用归纳法更好说明……
归纳法准确步骤不记得了……  下面乱来……


需证明的是对任意有限链表bs：

1. 
   
2. foldr F id bs = \y -> foldl f y bs
   
3.   where F = \b g x -> g (f x b)
   

复制代码

成立。


1. 对空链表 bs = [] ：

1. 
   
2.   foldr F id []      ; foldr f a [] = a
   
3. = id
   
4. 
   
5.   \y -> foldl f y [] ; foldl f a [] = a
   
6. = \y -> y
   
7. = id
   

复制代码

成立。


2. 非空有限链表 [c0,c1,...cn] 由 c0:c1:...cn:[] 构成。
对任意 c:cs：

1. 
   
2. 
   
3.   foldr F id (c:cs)                        ; foldr f a (x:xs) = f x (foldr f a xs)
   
4. = F c (foldr F id cs)
   
5. = F                     c (foldr F id cs)
   
6. = (\b g x -> g (f x b)) c (foldr F id cs)
   
7. = (\  g x -> g (f x c))   (foldr F id cs)
   
8. = (\    x -> (foldr F id cs) (f x c))      ; foldr F id cs = \y -> foldl f y cs
   
9. = (\    x -> (\y -> foldl f y cs) (f x c))
   
10. =  \    x -> foldl f (f x c) cs
    
11. = \y -> foldl f (f y c) cs
    
12. 
    
13.   \y -> foldl f y (c:cs)                   ; foldl f a (x:xs) = foldl f (f a x) xs
    
14. = \y -> foldl f (f y c) cs
    

复制代码

成立。

starwing83

回复 61# OwnWaterloo


    你真的确定这个写法能过编译？？？？

1. foldr' F id bs = \y -> foldl f y bs
   
2.     where F = \b g x -> g $ f x b
   

复制代码

我这边不能上外网，麻烦给个正确的示例，我再想想～

OwnWaterloo

回复 62# starwing83

完整的正确的是这个：

1. 
   
2. foldl f a bs = foldr (\b g x -> g (f x b)) id bs a
   

复制代码

或者为了避免重名，将foldl改为foldl''或者lfold。


你引用的：

1. 
   
2. foldr' F id bs = \y -> foldl f y bs
   
3.     where F = \b g x -> g $ f x b
   

复制代码

其实是伪代码……   lambda演算化简与后面归纳法都是伪代码……
其实就是说： 需要证明的是对任意 bs ，foldr' F id bs = \y -> foldl f y bs 成立。 其中F = \b g x -> g $ f x b。
我不该写where的……


不能上外网？ 不能下载haskell的意思？ http://tryhaskell.org/ 能访问么？
一个例子：

1. 
   
2. foldl (-) 0 [1,2] -- > -3
   
3. foldr (\b g x -> g ((-) x b)) id [1,2] 0 -- > -3
   

复制代码

starwing83

回复 63# OwnWaterloo


    不能访问。SICP对面向对象（或者说ADT，或者说名字空间，或者说代码组织，或者说模块封装）有十分独特的看法，让人觉得耳目一新，我要不要发个贴讲解一下？

三月廿七

回复 64# starwing83


    希望你发个帖讲解一下，

starwing83

回复 63# OwnWaterloo


    擦……回错了……重回

    关于foldr转foldl的我搞清楚了。这里说明一下。首先，我们有：

1. 
   
2. foldr' f i [] = i
   
3. foldr' f i (x:xs) = f x (foldr' f i xs)
   

复制代码

当定义foldl‘’的时候，我们有：

1. 
   
2. foldl'' f i xs = foldr' (\b g x -> g (f x b)) id xs i

复制代码

首先我们知道，foldl的功能是对f和i，[x1, x2, ... , xn], 产生这样的计算过程：

1. 
   
2. ( ... ((i `f` x1) `f` x2) ... ) `f` xn)

复制代码

而foldr是产生这么一个计算过程：

1. 
   
2. (x1 `f` (x2 `f` ( ... ( xn `f` i)) ... )

复制代码

从foldr的定义中可以很清楚的看到这种转换。

现在我们看用foldr的那个定义是如何处理的。首先用`f`计算xn和i：

1. 
   
2.     (\b g x -> g(f x b)) xn id
   
3. --> (\     x -> id (x `f` xn))
   
4. --> (\x -> x `f` xn)

复制代码

由此可知，我们将xn放到了右边，并延缓了计算（直到给出x为止）
然后我们以这个函数、给出的函数和xn-1计算新的值：

1. 
   
2.   (\b g x -> g (f x b)) xn-1 (\x -> x `f` xn)
   
3. --> (\ x -> (\x -> x `f` xn) (x `f` xn-1))
   
4. --> (\x  -> ((x `f` xn-1) `f` xn))

复制代码

一样的过程，将xn-1插入到了xn之前，并延缓执行。

以此类推，最后的结果就是将计算按照foldl的方式安排好了，但是所有的计算都被延缓了。

最后，给出一个初始值i，启动整个计算，这个计算就是foldl的了。

问题是：
1. 展开的时候，有没有栈的问题？会不会有无穷展开导致编译错误的情况？
2. 这种延缓的执行启动的时候，是否是in-place执行的？就和foldl一样？
3. foldr本身是延缓执行的。它能不能通过参数调整的方式做到in-place执行？比如，先执行最后一个，然后逐次向前迭代，做到in-place？
4. 最后，Haskell有没有尾调用？Haskell的优化可以保证到什么程度？在逻辑上有迭代执行的可能性的时候，Haskell是不是一定可以迭代执行？

pandaiam

starwing83 发表于 2012-03-28 22:19
额……主要是灵活的表达方式和隐式return很吸引人。跟C/C++完全是不同的思想。在SICP的第一章看到了大量的设 ...

网上还有卖的啊..给个连接吧...

starwing83

回复 67# pandaiam


    亚马逊搜一下把，直接搜sicp

OwnWaterloo

回复 64# starwing83

好啊好啊
不过我对耳目一新没有太高期望

OwnWaterloo

回复 68# starwing83

亚马逊都好贵好贵的……  这书不是有online版本么……  直接看不就素了……