再換？

重寫 structural congruence 的目的是排除那些我們不想要的證明，例如各式各樣的 cycles（P1 = P2 = ... = P1 = P3 = P4 = ...），可是這似乎相當困難。剛才又想到一種可能的解法：幫 pi-calculus expressions 找一個 denotational semantics，然後在那個 semantics 上證明 structural congruence 的各項規則成立。不過這個 semantics 要單純一點才行，我現在找到的都是用遠超過我能力範圍的 category theory…

--
基礎實在不穩 XD。

---

來試試看這篇：〈Final semantics for the pi-calculus〉。

--
看起來似乎比較有機會看懂的一篇 XD。

---

說不定最後是自己造一個類似 trace semantics 的東西 XD。

---

然後才發現如果真的找到一個好用的 semantics，那也不需要 bisimulation 了，全部問題都回歸到 semantics 上面的 equality。

--
這樣大概沒太容易 XD。