読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

CPS変換されたフィボナッチ関数の証明をしてみた

Coq CPS変換 フィボナッチ

普通のフィボナッチ関数とCPS変換したフィボナッチ関数をそれぞれ定義して、それらが等価であるということを証明してみた。CPS変換についてちょっと理解できた気がする。

http://ideone.com/3CQOn

しかしfib_cps関数をもっと美しく定義できないものだろうか。

[追記 2010 09/07]
asパターンを使えばパターンマッチを入れ子にしなくても良いことがわかったので、少し実装をシンプルにして書いてみた。証明部分は ほぼ同じ。
http://ideone.com/ZFPeQ