2008/09/21

再換?

重寫 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。

Labels: