自己做 MSS Derivation

從來沒有自己做過一遍 maximum segment sum 的 derivation，對這個經典問題太失禮了。於是今天計算機網路課堂上就自己導一次。（啊，我真的聽不太下去 XD。）有進步的地方是一開始整理用到的其中兩條規則，我現在知道是 "naturality of concat : F ← FF" 和 "functor (map) respects composition"。可是到中間果然卡住了：在湊其中一個 fusion condition 時為了把 max 擠到 recursive term 旁邊，我直接和後面的 map (x+) 做 type functor fusion，然後就再也沒辦法把 max 析取出來。偷看 scm 老師的 slides，才知道這裡要一步到位，直接證明 max . map (x+) = (x+) . max。這個式子就很單純，左邊做 type functor (fold-map) fusion 右邊做 fold fusion 就得到同一個 fold，而右邊的 fold fusion 就會用到 scm 老師說的關鍵 "+ distributes into ↑"，即 x + (y ↑ z) = (x + y) ↑ (x + z)。

scm 老師最後停在一個 linear-time, linear-space algorithm，並說可藉著 tupling transformation 轉成一般看到的 linear-time, constant-space algorithm。既然如此就來導吧！We reason:

其中「天啟」（revelation）那一步其實也沒那麼神奇。如果我們想直接把 max 融進 scanr，試著證明 fusion condition：

這時就發現我們會用到 head xs，但我們只能用 max xs。於是為了兩個都能用，就很自然地引進 fst . <max, head> 啦。最後是 fusion condition 的證明：

可以看到最終演算法裡面的 0 ↑ (x + z) 算的就是 maximum prefix sum（"prefix" 是因為 foldr 是從尾端累積回來的），y 就是 maximum segment sum。

--
但我仍然還沒透徹了解為什麼四次 fold fusion 之後就能得到這個演算法…

---

想要一個也順便傳回那個 maximum segment 的演算法，但是改 specification 重導很麻煩。有好方法嗎？

--
該不會要用 monad 吧 XD。