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

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

http://ideone.com/3CQOn

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

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