The Last Proof Obligation

今天回彰化。在火車上一口氣飆了快 100 頁的《Denotational Semantics》，到 continuous functions 才停下來 ─ 太累了 XD。這本書長得一副經典樣，融 CS, Mathematics, and Philosophy 於一爐，鋪陳非常成熟流暢，讀起來有如咀嚼鮮脆多汁的萵苣，極富快感！（「嚼萵苣」的形容方式借自 Gerald Durrell 的《鳥、野獸與親戚》。此書是「希臘三部曲」的第二部，這三部曲長久以來一直常駐在我的最愛書單上 XD。）唯一的怪異之處是我目前看到的定理都沒有證明（太簡單？）。

看到彰中學生戴著胸花出現在火車站附近，所以今天是畢業典禮嘍？

剛剛把 refinement of algebra to a function 證完了，所以現在終於只剩下最後一個 proof obligation，同時也是最關鍵的一個 ─ (partial) monotonicity condition！看來 scm 老師回國的時候幾乎篤定看得到整個 derivation 了。不過 refinement of algebra 我又用一片亂碼來證，看起來實在不賞心悅目，scm 老師看到大概會無奈地苦笑 XD。不過先確定證得出來再說嘍。

--
「關鍵」的意思就是說：如果證不出來，整個 derivation 大概就完蛋了 XD。