BMF学习笔记

引言

学习了Haskell、学习了Agda，我们已经初步掌握了使用函数式编程进行编写程序、编写证明的方法。
但是目前我们使用Agda进行的证明还是十分规范的代数形式的证明。如果想要严格地证明两个算法的等价性（而不是像OI题解里一样各种画图、感性理解之类的），我们就需要一种方法把算法写成代数的形式，再使用Agda之类的工具进行证明。
于是，我们有了BMF(Bird Meeterns Formalism)。简要来说，这是一种用于将程序代数风格化，以方便程序设计和程序转换的方法。

List

BMF建立在函数式编程的基础上，把计算描述为函数的复合。计算的一大特征是，一般要对一系列数据进行操作，不妨把这些数据按某种顺序排成一列，于是发现，我们的计算主要是建立在列表List上的。对List，我们有基本的操作 ++(append) ，即将 (x ++ y) 就是将List x,y 首尾相连拼起来。很明显，++具有结合律和单位元 []， 故(List,++,[])是一个幺半群。

先介绍在List上基本的高阶函数：map，reduce。
map：用 \(*\) 来表示，\(f * [a_1,\cdots,a_n] = [f (a_1),\cdots,f (a_n)]\)
reduce：用 / 来表示 \(\oplus / [a_1,\cdots,a_n] = a_1 \oplus a_2 \oplus \cdots \oplus a_n\)
对应命令式编程里的循环，定义foldl,foldr：
\(\oplus \to _e [a_1,\cdots,a_n] = e \oplus a_1 \oplus \cdots \oplus a_n\)
\(\oplus \leftarrow _e [a_1,\cdots,a_n] = (a_1 \oplus \cdots \oplus (a_n \oplus e))\)
又定义scanl,scanr
\(⊕→// _e[a_1, a_2, . . . , a_n] = [e, e ⊕ a_1, . . . ,((e ⊕ a_1)⊕)· · · ⊕ a_n]\)
\(⊕ ←// _e[a_1, a_2, . . . , a_n] = [a_1 ⊕ (a_2 ⊕ · · · ⊕ (a_n ⊕ e)), . . . , a_n ⊕ e, e]\)

Homo

在幺半群上定义同态映射(homomorphism)，\(h\)，定义如下：
对函数 \(h : A \to B\) ，其中 \((A,\oplus,e_1),(B,\otimes,e_2)\)为两个幺半群，以下两条成立，则称 \(h\) 为同态映射：

1. \(h (e_1) = e_2\)
2. \(h(x \oplus y) = h(x) \otimes h(y), \forall x,y \in A\)

List是幺半群，于是我们可以定义在 List 上的homo \(h : [A] \to B\)，只要满足：

1. \(h ([]) = e\)
2. \(h ([x]) = f (x)\)
3. \(h (xs ++ ys) = h(xs) \otimes h(ys)\)
   把 \(h (a)\) 按定义展开，可以发现 \(h =\otimes / \cdot f *\)，其中 \(\cdot\) 表示函数复合。为什么要介绍homo？因为其计算过程是满足结合律的，适合并行计算！

一些等式

map&reduce promotion

有map和reduce的定义可以得：

1. \(f * \cdot ++ / = ++ / \cdot (f *)*\)
2. \(\oplus / \cdot ++ /= \oplus / \cdot (\oplus /) *\)
   这个等式可以让我们把 ++ 往左移或去掉，可以尽量减少++的次数，减少对数据结构的改动

Accumulation lemma

1. \(\oplus \to// _e =\oplus \to _e * \cdot inits\)
2. \(\oplus \leftarrow // _e =\oplus \leftarrow _e * \cdot tails\)
   这个等式十分强大，可以发现从复杂度的角度来看，左边的计算是线性的，而右边的是平方。我们可以通过这个等式变换降低计算的复杂度

Horner's rule

如果两个homo \(\oplus,\otimes\)，满足分配率： \((a\oplus b) \otimes c = (a\otimes c) \oplus (b\otimes c)\)则以下等式成立：
\(\oplus / \cdot \otimes / * \cdot tails = \odot \to _e,a \odot b = (a \otimes b) \oplus id_\otimes\)
这条性质同样可以降低复杂度。

Maxium Segment Sum

先在BMF的形式下写出从定义直接得到的算法：\(mss = \uparrow / \cdot +/* \cdot segs\)
其中segs表示虽有子段，\(segs = ++ / \cdot tails * \cdot inits\)
然后类似Agda等式推理的形式，我们进行推理：

\[\begin{aligned} mss =& \uparrow / \cdot +/* \cdot segs \\ =&\uparrow / \cdot +/* \cdot ++/ \cdot tails * \cdot inits \\ =&\{map \; promotion\}\\ &\uparrow / \cdot ++/ \cdot (+/*)* \cdot tails * \cdot inits \\ =& \{ (f*) \cdot (g*) = (f \cdot g) *\} \\ &\uparrow / \cdot ++/ \cdot ((+/*) \cdot tails) * \cdot inits \\ =& \{reduce promotion\} \\ &\uparrow / \cdot( \uparrow / \cdot +/* \cdot tails) * \cdot inits \\ =& \{Horn's \; rule \}\\ &\uparrow / \cdot (\odot \to _0 )* \cdot inits ,a \odot b= (a+b) \uparrow 0\\ =& \{accumulation \; lemma\} \\ &\uparrow \cdot (\odot \to // _0) \end{aligned} \]

（好麻烦，我手敲了半个小时)。

然后只需使用agda编写上面所说的所有性质即可。