Fold 刻劃定理

今天很簡單用 Church encoding 開場，然後講下面這個 fold 的刻劃定理，描述「一個 total function 可以寫成 fold」的充要條件：

從這個定理的 list 版可以推得 zip 和 zip xs 都是 fold。zip 是 fold 還可以想像，zip xs 是 fold 就有點匪夷所思 ─ 怎麼從 zip xs ys 造出 zip xs (y :: ys) 啊？（這個問題我在 FLOLAC '07 的時候就問過了，一直擱到現在。）事實上我今天一開始說 zip xs 不是 fold，卻造不出反例 XD。

再從這個定理的自然數版（依 CS 慣例，自然數包括 0）可以推得 factorial function 不是 fold，因為 fact 0 = 1 = fact 1 但 fact 1 = 1 /= 2 = fact 2。不過這是唯一的反例。如果把 fact 定義在正整數上，就會發現 fact 是一個 fold 了。這是因為 fact 在正整數上是 injective，所以可以經過複雜計算從 fact n 推得 n，然後算出 (1+n) * fact n。當然計算上最有效率的解法還是用 primitive recursion (paramorphism)。

回到定理本身。臨時準備的東西果然強度不夠，蔡老師要求直覺詮釋的時候我就掛在台上了 XD。不過蔡老師也很快發揮功力，給 "ker f ⊆ ker g" 一個直覺詮釋：f 的 "discrimination power" 不弱於 g。證明定理的一個關鍵引理是 "∃h : B -> C s.t. g = h . f" iff "ker f ⊆ ker g and ∃h' : B -> C"。先不理會右側的 "∃h' : B -> C" 條件，蔡老師把 g 詮釋為我們想完成的動作，而 f 只做了一半。如果想宣稱有個 function h 能夠從 f 結束的地方出發，把 g 的動作完成，那麼 g 把 a 和 a' 映射到不同的值時，f 必定不能把 a 和 a' 映射到同一個值 b，因為 h 沒辦法把單一個值 b 分射到 g a 和 g a'。從另一個方向看，如果當 g 把 a 和 a' 映射到不同的值時，f 都會把 a 和 a' 映射到不同的值 b 和 b'，那就一定有辦法繼續把 b 和 b' 送到 g a 和 g a'。

如果把這個詮釋類推到定理的 "ker(Fh) ⊆ ker(h . α)" 呢？我目前認為這個條件捕捉的是「fold 的結果僅依賴於遞迴算得的結果（即 Fh 算出的 FA-structure）」。當 h 拿到一個 object of type T，我們可以把它拆成一個 FT-structure，改而考慮 h . α。假設我們有兩個 FT-structures，只有內藏的 T object(s) 不同，其餘成分皆相同。當我們遞迴地把那些 T object(s) 轉換成 A object(s) 而且這兩堆 A object(s) 完全相同時，h . α 套用在這兩個 FT-structures 的結果也會相同。因此即便 h 拿到的是兩個「內藏的 T object(s) 不同」的 FT-structures，只要遞迴地轉換後的 A object(s) 相同，h 就必須給相同的結果 ─「內藏的 T object(s) 不同」這樣的資訊是 h 無法利用（得知）的。

話說回來，「fold 的結果僅依賴於遞迴算得的結果」不就是 universal property 所說的一部份事情嗎？這樣有沒有重造輪子的嫌疑呢？這就回到我們打造這個定理的初衷：我們之所以搜尋一個不同於 universal property 的刻劃，是因為 universal property 要求我們找到 fold 用的 algebra，而這樣的要求對於「檢驗一個函式是不是 fold」太麻煩了。至於這個定理找到的刻劃只涉及函式的外延（extensional）行為，檢驗上比較方便。而剛剛的分析告訴我們這個刻劃講的事情和 universal property 相當吻合，這就更穩固我們對這個定理的信心嘍。

--
我還是覺得 zip xs 是 fold 很奇怪… 如果可以用 xs 就行，但是可以嗎？好像可以 XD。