Program Calculation: Fusion and Tupling
Fusion
考虑计算List最大值的 max
函数. 利用
sort
,我们可以给出一个简单的规约:
1 | max = head . sort |
但是大家都知道这样太慢了,因为 sort
会对整个List进行排序,而我们只需要最大值.
这个问题归结到直接利用sort
会带来太多不需要的中间结果.
为了解决这个问题,我们考虑把head
整合进sort
中.
这样我们引入一个新的概念:Fusion.
Fusion Law for foldr
在处理List上的问题时经常会用到foldr
.
在这里,我们考虑把一个外围的函数f
整合入foldr
中,给出如下的Lemma:
1 | f (a ⊕ r) = a ⊗ f r |
在这里和以后的一些表示中,\(r\)意味着“recursive”,即foldr
的递归部分.
因此我们需要的是通过程序演算找到合适的运算符⊗.
以max
为例,可以对head (insert a r)
做如下的演算:
- 对于 \(r = []\),
\[ \begin{align*} \text{head} \space ( \text{insert} \space a \space r) &= \text{head} \space ( \text{insert} \space a \space []) \\ &= \text{head} \space [a] \\ &= a \\ \end{align*} \]
- 对于 \(r = y:ys\),
\[ \begin{align*} & \text{head} \space (\text{insert} \space a \space (y : ys)) \\ =& \space \{ \space \text{def. of insert} \space \} \\ & \text{head} \space (\text{if} \space a \geqslant y \space \text{then} \space a : y : ys \space \text{else} \space y : \text{insert} \space a \space ys) \\ =& \space \{ \space \text{distribute head over if} \space \} \\ & \text{if} \space a \geqslant y \space \text{then} \space \text{head} \space (a : y : ys) \space \text{else} \space \text{head} \space (y : \text{insert} \space a \space ys) \\ =& \space \{ \space \text{def. of head} \space \} \\ & \text{if} \space a \geqslant y \space \text{then} \space a \space \text{else} \space y \\ =& \space \{ \space \text{assumption: } r=y:ys \space \} \\ & \text{if} \space a \geqslant \text{head} \space r \space \text{then} \space a \space \text{else} \space \text{head} \space r \\ \end{align*} \]
(以后的演算会适当省略一些推理依据,并按照Haskell的语法来书写)
最后我们得到了一个合适的运算符 \(\otimes = \text{if} \space a \geqslant \text{head} \space r \space \text{then} \space a \space \text{else} \space \text{head} \space r\),因此我们可以得到:
1 | head (insert a r) = a ⊗ (head r) |
因此按照Fusion Law,我们可以得到:
1 | max = head . foldr insert [] = foldr ⊗ (head []) = foldr ⊗ (-∞) |
现在通过Fusion,我们的max
已经是一个线性时间的算法了.
More Examples
以上关于max
的推演还是比较显然的,但是仍然能展示出Fusion在消除中间结果、将两个函数合并成一个函数上的作用.
现在我们考虑一个更复杂的例子:在List上的reverse
.
1 | reverse = foldr snoc [] |
现在我们引入一个数组作为辅助,定义一个我们希望变得更快的函数fastrev
.
1 | helper xs ys = reverse xs ++ ys |
考虑提升helper
的效率,这可以通过将++
和
snoc
合并成一个函数来实现.
1 | (++) (snoc a r) |
在Fusion Law中取 f= λ x -> (++) x
我们可以得到:
1 | (++) (r ++ [a]) = a ⊗ ((++) r) |
因此,helper
可以被重写为:
1 | helper xs = λ ys -> (++ ys) (foldr snoc [] xs) |
我们通过Fusion的推理得到了一个线性时间的算法!
展开foldr
,则fastrev
可以被重写为:
1 | fastrev xs = helper xs [] |
这是我们常见的fastrev
的样子.
通过以上的例子,我们可以看到Fusion Law的作用.
Exercises
利用Fusion Law证明以下等式:
1 | 1. foldr (⊕) e . map f = foldr (⊗) e |
Solution
考虑map
也可以利用foldr
来实现:
1 | map f = foldr ((:) . f) [] |
因此,我们便可以利用Fusion
Law,将外围原有的foldr
整合进map
中.
记u = foldr (⊕) e
,则:
1 | u (((:) . f) a r) = u (f a : r) |
由Fusion Law, 1是显然的.
考虑 2
中map f
也可以写成foldr
,这就回到了第一个问题,也是显然的.
类似地,3
中filter
也可以利用foldr
来实现:
1 | filter p = foldr (λ a r -> if p a then a : r else r) [] |
至此,我们利用Fusion Law证明了以上三个等式.
To Be Continued...