2008/11/21

Fold 刻劃定理

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

從這個定理的 list 版可以推得 zipzip 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 1fact 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。

Labels:

Blogger XOO11/21/2008 8:03 pm 說:

小小聲的說,有些東西我不是那麼喜歡直覺詮釋... 囧

 
Blogger 單中杰11/23/2008 2:59 am 說:

zip' xs = foldr f [] where f y zip_xs_ys = zip xs (y : map snd zip_xs_ys)

其中 zip' 是新定義的, zip 則是用 Prelude 的。就好像正整數的 fact 那樣,會被不明事理的人罵在耍嘴皮子的定義。

 
Blogger nobunari11/24/2008 7:54 am 說:

嗯嗯,定理只說 zip 是一個 fold, 但並不要求要用有效率的方式做出來。 :)

 

<< 回到主頁