2007/07/04

Church Numeral

今日 functional programming 談到 untyped lambda calculus,舉了一些例子,其中一個是 Church numeral,即以一組特定的 higher-order functions 表示自然數。我於是趁午休試著用 OCaml 實作,算可以 work:

(* primary definitions *)
let zero = fun f ->fun x -> x
let succ x = fun f -> fun n -> f (x f n)
let plus x y = fun f -> fun n -> x f (y f n)
let mul x y = x (plus y) zero

(* translating functions *)
let cnum2int x = x (fun f -> fun x d -> f (0+x) (d+0) + 1) (fun x d -> 0) 0 0
(* let cnum2int x = x (fun n -> n + 1) 0 *)
let rec iter f n = fun x -> if n = 0 then x else f (iter f (n - 1) x)
let cnum n = iter succ n zero

如果單用 cnum2int (mul (plus (cnum 4) (cnum 5)) (plus (cnum 6) (cnum 7))) 這樣的算式可以 work,但如果先把某個數繫結到 identifier 上而後對它施行某個操作,就會發生(對我而言)複雜的型別錯誤。此類錯誤引我嘗試未註解掉的那個 cnum2int 畸形版本,但問題仍然存在。目前我沒辦法解決,先暫時放著 XD。

下午是 program derivation,穆老師的語速很快,和 cyy 與 Y 老師講課的速度差不多(cyy 平時講話又是另一個等級了 XD),不過整體速度適中。作業看起來很多的樣子 XD。

--
來做做看就知道實際上多不多了 ─ appearances can be deceiving XD。


我照 Wikipedia 的方式把乘法的定義改為 let mul x y = fun f -> x (y f) 就好像全部都 work 了,cnum2int 也可以用比較簡單的那個版本。目前尚未去理解為何這樣就 work XD。


時間 9:45,program derivation 的作業寫完了,最後一題還滿好玩的 XD。待會再接再厲把 functional programming 的作業也寫一寫 XD。


時間 11:17,functional programming 作業也寫完了。前兩題很簡單,第三題我花了很多時間才恍然大悟 type 'a t 的作用和 'a option 很像,之後才慢慢地把 fold/unfold 兜出來。Functional programming 真的很可愛 XD。


隨便寫一個 function possum 計算一個 int list 各元素(假設均非負)的和,測試 type nat 的 unfold:

let possum =
  let rec seed l =
    match l with
      [] -> Z
    | 0 :: tl -> seed tl
    | hd :: tl -> S ((hd - 1) :: tl)
  in
    unfold seed

Functional programming 真的很可愛 XD。

Labels: