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。