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。


<< 回到主頁