Coqプログラマの集会、Coq庵でした
発表者の皆さん。お手伝いいただいた皆さん。ありがとうございました。たくさんのCoqerが集まって、大変濃密な時間を過ごす事ができました。
スライドは以下から参照できます。
Coq庵 - coqグループ
CPS変換されたフィボナッチ関数の証明をしてみた
普通のフィボナッチ関数とCPS変換したフィボナッチ関数をそれぞれ定義して、それらが等価であるということを証明してみた。CPS変換についてちょっと理解できた気がする。
しかしfib_cps関数をもっと美しく定義できないものだろうか。
[追記 2010 09/07]
asパターンを使えばパターンマッチを入れ子にしなくても良いことがわかったので、少し実装をシンプルにして書いてみた。証明部分は ほぼ同じ。
http://ideone.com/ZFPeQ