死刑

不需要太多辯論，scm 老師很輕易地就判先前那個 modelling of weak bisimilarity 死刑了 XD。Jeremy Gibbons 在他的 MPC '08 paper 提到 "[...] observational equivalence can be formalised in two ways, which turn out to be equivalent: via bisimulation and coinduction or via universal properties of final coalgebras." 所以看看他提到的 references 說不定會找到好方法。不過就算換一種證明 observational equivalence 的方法，最基礎的 structural congruence 的問題總要解決的…

--
在那之前先把代數作業寫完吧 XD。

---

我漸漸說服自己其實是 pi-calculus 的體質不好才導致這一切麻煩… 方法再怎麼變總是要處理 structural congruence，就算弄成很漂亮的 unfold 也一樣…

真要硬拚的話，有沒有辦法對 structural congruence 證明做點 normalisation，弄成一個比較好進行 induction 的型式？

--
不過就算成功也還是要做至少二十幾個 cases 的分析…

---

睡前總是靈感特別多… 剛才想對 structural congruence 的證明做 normalisation 而得到一些關於證明結構的性質保證，然後改而對那些性質的證明結構做 induction 而避免掉不想要的情況。既然如此，那直接讓 structural congruence 的證明造出來的時候有那些性質就好了呀！也就是說要改寫 structural congruence，比較精準地刻畫出我們心中想要的證明結構。

規則應該還是很多條啦，可是我覺得 "somehow" 比較有希望了 XD。反正如果 pi-calculus 要繼續做下去，一定得找到對付 structural congruence 的辦法。

--
先記下來，睡醒再試 XD。