動手

看起來不太可能復用那套 Coq 的 pi-Calculus library 了：

• Process terms 是用 inductive 的定義。理論上方便，實用上不好寫。
• 對於 (channel) names 的處理，scm 老師本來用的 polymorphic 版本雖然涉及 Set1，但實用上應該比較方便。（Universe construction 畢竟麻煩一些。）
• 只做了 strong bisimilarity，我們真正想要的是 weak congruence。

所以直接動手用 LTS semantics 寫一套新的 modelling of pi-Calculus 吧。還是用 Agda 試一試 ─ 內鎖效應很難掙脫 XD。雖然他們參考的 paper〈A Calculus of Mobile Processes, Part 2〉沒描述 weak bisimilarity（和 weak congruence），但反正就自己定義嘛，證不出來就知道錯了 XD。

另一方面，我們常看到類似「pi-Calculus 不適合用來做 practical programming languages」的說法。這樣的話，把 Haskell 的 concurrency library 和 pi-Calculus 拉在一起似乎引出兩個（或許是同一個）問題：

• 會不會這兩者的層級其實不一樣呢？我的意思是，直接使用 pi-Calculus 對於模映 Haskell's concurrent programs 會不會太低階了呢？
• pi-Calculus 能方便地寫出有意思的規格嗎？

如果有一個實際的好例子的話，這兩個問題就一併解決了，但我目前沒有很好的想法。

--
甩掉 structural congruence，路似乎就又鋪開了 XD。