突破

這次到英國（或者說在英國）的一個實質成果就是終於看懂《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