2009/02/09

Late Semantics

剛寫完新一版的 pi-Calculus modelling,包括 syntax、LTS semantics、weak late bisimilarity 和它是 equivalence relation 的證明。受不了 PB 的速度,只好把 Agda 裝在系上工作站,透過 ssh 把 emacs 的 X Window 畫面傳回來,原本就不知所云的證明搭配預設字型,證得我眼花撩亂 XD(不休息一下眼睛會爆掉…)。用 HOAS 模映 late semantics 意味著要處理 higher-order terms,而這在 Agda 裡面特別不方便。不過用了一個 lemma "lambda distributes over Sigma" 之後,目前的複雜度還算可以接受。Transition rules 有些 side conditions 沒有檢查,所以有可能出錯。下一步是證明所有 congruence rules。

--
證得出來就有進度了 XD。

Labels:

<< 回到主頁