日々の流転

λ. 型理論での形式的証明記述の技法について; 木下 佳樹, 高村博紀

メモ。Chainがちょっと面白かった。

(追記)「系統的な等号の与えかたで, すべての点で満足できるものはない」とあるが、Extensional Equality in Intensional Type Theory の型システムを直接実装したものはどうなんだろう。結構良い線をいっているのではないかと思うが。

(追記) 「Calculational Proof っぽい書き方」も参照。

(2008-02-04追記) どうでも良い点だけど、Leibniz equality との比較で「Id では, 等号の階層が上がってしまう, という問題は生じないが, 今度は, 外延性の問題が生じる.」とあるが、Leibniz equality でも外延性の問題は生じる。