Trivializer

Fusion

考虑计算List最大值的 max 函数. 利用 sort，我们可以给出一个简单的规约：

max = head . sort
    where sort = foldr insert []
          insert x [] = [x]
          insert x (y:ys) | x >= y    = x : y : ys
                          | otherwise = y : insert x ys

但是大家都知道这样太慢了，因为 sort 会对整个List进行排序，而我们只需要最大值. 这个问题归结到直接利用sort会带来太多不需要的中间结果. 为了解决这个问题，我们考虑把head整合进sort中. 这样我们引入一个新的概念：Fusion.

Fusion Law for foldr

在处理List上的问题时经常会用到foldr. 在这里，我们考虑把一个外围的函数f整合入foldr中，给出如下的Lemma:

f (a ⊕ r) = a ⊗ f r
------------------------------------
f · foldr (⊕) e = foldr (⊗) (f e)

在这里和以后的一些表示中，\(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\)，因此我们可以得到：

head (insert a r) = a ⊗ (head r)

因此按照Fusion Law，我们可以得到：

max = head . foldr insert [] = foldr ⊗ (head []) = foldr ⊗ (-∞)

现在通过Fusion,我们的max已经是一个线性时间的算法了.

More Examples

以上关于max的推演还是比较显然的，但是仍然能展示出Fusion在消除中间结果、将两个函数合并成一个函数上的作用. 现在我们考虑一个更复杂的例子：在List上的reverse.

reverse = foldr snoc []
    where snoc x xs = xs ++ [x]

现在我们引入一个数组作为辅助，定义一个我们希望变得更快的函数fastrev.

helper xs ys = reverse xs ++ ys
-- 等价于
helper xs = (++) (reverse xs)
          = (++) (foldr snoc [] xs)

fastrev = helper xs []

考虑提升helper的效率，这可以通过将++ 和 snoc 合并成一个函数来实现.

  (++) (snoc a r)
= { η expansion }
  λ y -> ((r ++ [a]) ++ y)
= { associativity of ++ }
  λ y -> (r ++ ([a] ++ y))
= { }
  r ++ (λ y -> [a] ++ y)

在Fusion Law中取 f= λ x -> (++) x我们可以得到：

(++) (r ++ [a]) = a ⊗ ((++) r)
    where a ⊗ r' = λ y r' -> r' ([a] ++ y)

因此，helper可以被重写为：

helper xs = λ ys -> (++ ys) (foldr snoc [] xs)
          = foldr (⊗) (++ []) xs
          = foldr (⊗) id xs
    where a ⊗ r' = λ y r' -> r' ([a] ++ y)

我们通过Fusion的推理得到了一个线性时间的算法！

展开foldr,则fastrev可以被重写为：

fastrev xs = helper xs []
    where helper [] y = y
          helper (x:xs) y = helper xs (x:y)

这是我们常见的fastrev的样子. 通过以上的例子，我们可以看到Fusion Law的作用.

Exercises

利用Fusion Law证明以下等式：

1. foldr (⊕) e . map f = foldr (⊗) e
      where a ⊗ r = f a ⊕ r
2. map f . map g = map (f . g)
3. foldr (⊕) e . filter p = foldr (⊗) e
      where a ⊗ r = if p a then a ⊕ r else r

Solution

考虑map也可以利用foldr来实现：

map f = foldr ((:) . f) []

因此，我们便可以利用Fusion Law，将外围原有的foldr整合进map中. 记u = foldr (⊕) e，则：

u (((:) . f) a r) = u (f a : r)
                  = f a ⊕ u r
                  = a ⊗ u r
    where a ⊗ r = f a ⊕ r

由Fusion Law, 1是显然的.

考虑 2 中map f也可以写成foldr,这就回到了第一个问题，也是显然的.

类似地，3 中filter也可以利用foldr来实现：

filter p = foldr (λ a r -> if p a then a : r else r) []

至此，我们利用Fusion Law证明了以上三个等式.

To Be Continued...