和 nu 有關的性質總是證不出來。覺得可能是因為用 lambda 做 modelling 太強了,之前忽略的條件 name occurrences 似乎也對情勢沒什麼影響。又卡住了…

趁機跳回 graphical games 一陣子?XD

看起來是 "name" type 的問題。Coq paper 裡面直接預設一些關於 name type 的性質(as Axioms),而我們的 encoding 裡面 name type 是任意的 a : Set,直覺上的確性質比較少。

摘錄一句(from p.~22):These properties capture the idea that functions of type name->proc are actually "processes with a hole", which can be filled in by any name without changing the structure of the process itself.

可是隨便 postulate 好像有危險…


<< 回到主頁