2008/09/19

死刑

不需要太多辯論,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。

Labels:

Blogger XOO9/19/2008 7:20 pm 說:

pi-calculus 第一印象就覺得定義很 massive,其實更之前有喵過,看到用的符號跟操作,心裡就浮上 "what a damn ..." _A_

 
Blogger Josh Ko9/20/2008 5:21 am 說:

對啊,實在是沒有很漂亮 XD。

 

<< 回到主頁