前言：这应该是下半学期（甚至可以说整个学期，因为上半期haskell感觉在铺垫）计算概论课主要想讲的内容了
Bird Meertens Formalism (BMF)
应该是一种计算理论？
是建立在半群（幺半群）上的理论
沿袭FP的思想，把算法描述成函数组合的形式（在这里可以看出FP的高妙之处，就是用函数组合的方式，使得我们的算法可以利用等式进行推导）
而怎么推导呢，就需要利用一些理论
引入了同态概念之后，又多了很多推导的等式
同态（Homomorphism）：简单来说，就是在两个群之间映射，满足如果第一个群里有a\(\oplus\)b=c，那么第二个群里有f(a)\(\otimes\)f(b) = f(c)
而我们熟知的List，就是一个幺半群，对它可以衍生出很多同态函数
一些记号和约定：
f*表示map，对List里所有元素施加f
⊕/表示reduce，把List里的元素按顺序从左向右用⊕连起来计算
⊕→/e or ⊕←/e 表示foldl/foldr，把List里的元素从e开始复合从左向右/从右向左运算，e可以不给出直接算
⊕→//e or ⊕←//e表示accumulation，就是把foldl/foldr计算的每一个值都记下来，按原顺序顺塞到一个List里
inits，所有前缀的集合，inits = (++→//[]) · [·]∗
tails，所有后缀的集合，tails = (++←//[]) · [·]∗
一些Tips
无疑map和reduce是两个Homomorphism
而所有homo都可以表示成reduce和map的复合，证明很有意思
即：h = ⊕/ · f∗
显然
(⊕→/) · ([a]++) = ⊕→/a
(⊕←/) · (++[a]) = ⊕←/a
一些法则
map distributivity
(f · g)∗ = (f∗) · (g∗)
map && reduce promotion
f∗ · ++/ = ++/ · (f∗)∗
⊕/ · ++/ = ⊕/ · (⊕/)∗
Accumulation Lemma
(⊕→//e) = (⊕→/e) ∗ ·inits
(⊕→//) = (⊕→/) ∗ ·inits+
Horner's rule
如果两个同态 ⊗ 对 ⊕ 满足右结合律:
(a ⊕ b) ⊗ c = (a ⊗ c) ⊕ (b ⊗ c)
那么
⊕/ · ⊗/∗ ·tails = ⊙→/e
where
e = id⊗
a ⊙ b = (a ⊗ b) ⊕ e
一些经典推导
The Maximum Segment Sum (mss) Problem
segs = ++ / · tails ∗ ·inits
即所有非空子串
mss
= { definition of mss }
↑ / · +/ ∗ ·segs
= { definition of segs }
↑ / · +/ ∗ · ++ / · tails ∗ ·inits
= { map and reduce promotion }
↑ / · (↑ / · +/ ∗ ·tails) ∗ ·inits
= { Horner’s rule with a ⊙ b = (a + b) ↑ 0 }
↑ / · ⊙→/ 0 ∗ ·inits
= { accumulation lemma }
↑ / · ⊙→// 0