2007/12/07

新琴

好久沒到琴房了,今天進去發現換了新琴,可惜我的技巧愈來愈差了 XD。

晚上都在寫 DCL final project proposal(pdf 所在網址應該很好猜 XD),昨天就沒寫到 blog XD。

Relational derivation 一些簡單的性質都可以很簡單地組合出證明,看來還是要涉及比較具體的 functions 才用得上 chain reasoning。可是想做 chain reasoning 的話,proof terms 都是 functions,而且還要做 pattern matching,這樣整個 derivation 的長相會變得有點怪,大概上一半都是 by f1by f2、…,然後下一半以 where 開頭,把所有 functions 定義出來。找不到什麼好方法哩 XD。

--
我會用「哩」了 XD。

Labels:

Blogger yen312/08/2007 3:14 am 說:

那麼順便學會用"捏"吧XD

 
Anonymous scm12/08/2007 7:17 am 說:

有沒有用很多 chain reasoning 倒是沒關係啦,有證出來比較優先。

如果有很多 by f1, by f2, 這些 f1 f2 都可以當作要另外證明的 lemma 來看待吧。

 

<< 回到主頁