Proving Associativity of List Concatenation by Fold Fusion

概念上 fold 是 structural induction，所以任何 inductive proof 應該都可以用 fold 重寫吧？關鍵可能就在於從 pointwise style 轉移到 point-free style。以下證明 list concatenation 的結合律，第一步先把欲證明的式子轉成 point-free style：

等號左邊和右邊都是一個 function 跟在一個 foldr 後面（「(++ys) 和 (++) 如何表示為 foldr」留給讀者作練習 ─ Richard Bird 最愛講這句了 XD），所以很自然地我們對兩邊做 fold fusion。（TRICK: 整理成 point-free style 的時候我其實已經知道要對 xs 做 induction 了！）左邊的 base case 是 (++zs) ys = ys ++ zs，inductive case 則是

右邊的 base case 是 rapp (ys ++ zs) id = ys ++ zs，inductive case 則是

因此兩邊的函式都等於 foldr (:) (ys ++ zs)，即得證 list concatenation 的結合律。不過這樣做下來，我寧願直接做 pointwise induction XD。

--
To hcsoso: if you're interested, we can perhaps meet some day and I'll talk about the derivation lectures in FLOLAC '07. I think it would be a faster way to get familiar with functional programming and reasoning. :P

---

再多看一眼，其實 foldr (:) (ys ++ zs) xs 就是 (++(ys ++ zs)) xs，所以可以只做左邊的 fold-fusion。另外，這樣的結果某種角度而言暗示了 list concatenation 應該定義為 right-associative。