2008/02/23

突破

這次到英國(或者說在英國)的一個實質成果就是終於看懂《Algebra of Programming》第二章了!裡面最重要的部份當然是用 initial algebras 表示 inductive datatypes 以及用 catamorphisms 表示 inductive datatypes 上的 induction。像下面這個 banana-split fusion 的證明是在機場無聊的時候順手寫下來的 XD。

Banana-split fusion 的意義是把兩個 parallel loops 合成一個。因為這裡用 category theory 的方法證明,所以對任意的 inductive datatypes(e.g., lists, trees, ...)都成立。既然提到 Leibniz,Oxford University Museum of Natural History 的柱子上有 Leibniz 的雕像:

其他還有 Newton、Galileo、Darwin 等大科學家,不過我只照了 Newton & Leibniz,理由應該很明顯 XD。

--
慢慢再放 Oxford 大冒險當天的照片上來。然後 scm 老師的照片會上網嗎?XD

Labels: ,

<< 回到主頁