书接上文，在熟悉了基本的函数式编程的思想后，我们就来一起推导出最大子段和的线性算法。

推导最大子段和线性算法

回顾一下最大子段和的 Specification：

mss = maximum . map sum . concat . map tails . inits

以及上文中提到的基本函数：foldl，foldr，scanl，scanr 等等，忘了的自己回去看看。

在此我们约定一个新的高阶函数：reduce，满足 reduce f === foldl f e === foldr f e。我们要求传递给它的二元函数具有结合律，并且 e 是这个运算的单位元。这主要是方便大家阅读。所有用到了 reduce 的地方默认如此（注意，传给 reduce 一个空序列的返回值是单位元，也就是说 reduce f [] = e）。

我们要做的第一个变换是 map promotion：map sum . concat === concat . map (map sum)。通过简单的类型推导可以发现左右两边接受的参数都是三维列表。

mss = maximum . concat . map (map sum) . map tails . inits

下一步操作是 reduce promotion：maximum . concat === maximum . map maximum。也就是说你把一个二维数组先拼起来再求最大值，等价于把内层的数组分别求出最大值，再在这些求出来的结果中求出最大的那个。

mss = maximum . map maximum . map (map sum) . map tails . inits

接下来是 map 关于复合的分配律：map f . map g === map (f . g)。这个很好理解，你把一个数组里的数先全体加 2 再全体平方，等价于数组里的数分别做一次加 2 平方的操作。这里我们要求 g 的返回值类型与 f 接受的参数类型相同。带入这个定理可以得到

mss = maximum . map (maximum . (map sum) . tails) . inits

接下来我们先拆解 maximum 函数：maximum === reduce max，（max 具有结合律，单位元是负无穷，这也是上文 reduce promotion 可以用在 maximum 上的原因）。

另一方面，sum === reduce (+)。对于集合上的两个幺半群，，若对有右分配律（）那么

-- Horner's Rule
reduce f . map (reduce g) . tails === foldl h e-g

其中。这里可能大家看得有点懵，不妨带入加法，带入乘法感受一下。它表达的意思其实是

把带入 max，带入加法，你会发现这个本质上是对最大后缀和这一问题的优化，于是我们得到

h a b = max (a + b) 0
mss = maximum . map (foldl h 0) . inits

最后是 scanl 的定义。我们说 scanl 其实相当于把 foldl 的中间计算结果保留下来，也就是说它求出了每个前缀的计算结果：

--- 别忘了 inits 会求出所有前缀
scanl f z === map (foldl f z) . inits

因此我们就得到了

h a b = max (a + b) 0
mss = maximum . scanl h 0

仔细看看它，你会发现它和我们所写的最大子段和算法基本一致。

整个推导过程如下：

h a b = max (a + b) 0

mss = maximum . map sum . concat . map tails . inits
    = maximum . concat . map (map sum) . map tails . inits
    = maximum . map maximum . map (map sum) . map tails . inits
    = maximum . map (maximum . (map sum) . tails) . inits
    = maximum . map (foldl h 0) . inits
    = maximum . scanl h 0

后续

为了方便大家理解，有关 Agda 的部分我删掉了，不然有的地方会很繁琐。程序演算的应用还有很多，比如推理 FFT 的算法等，希望大家看完后都能有所收获～