Hopeless

這幾天照著 Robin Milner 的《Communicating and Mobile System: the π-Calculus》把 pi-calculus 從頭再模映一遍，一直到 weak bisimilarity。定義完 weak bisimilarity 之後，我覺得根本不可能有辦法證明任何有點規模的東西嘛…

--
光想到要對之前那個小例子做 case analysis 就頭皮發麻…

---

唔，如果很順利地一下全部寫完，大概就只能寫 blog 不能寫 paper 了 XD。不過我還是覺得這次和 AoPA 有個決定性的差異 ─ AoP 已經有很多乾淨的 formulation，克服 predicativity 搬進 AoPA 就能得到不錯的成效。（例如可以比較 foldR-fusion 的第一個證明和現在 AoPA 的眾多 algebraic proofs。）可是 pi-calculus 好像沒有這麼好的資源。

--
重做 pi-calculus？XD