2009/02/07

動手

看起來不太可能復用那套 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。

Labels: