日々の流転

λ. Proof Methods for Corecursive Programs. Jeremy Gibbons, Graham Huttton.

recursiveなプログラムは定義域がinductiveなデータ型であるようなプログラム、corecursiveなプログラムは値域がcoinductiveなデータ型であるようなプログラム。そして、corecursiveなプログラムについての証明の基本は、二つのプログラムが等しいことの証明。この論文では The map-iterate property (map f . iterate f = iterate f . f) の証明を例として、以下の4つの方法を説明し比較している。

• fixpoint induction
• the approximation (or take) lemma
• coinduction
• fusion

ほとんど知ってることしか書いてなかったので、個人的にはあまり面白くなかった。 guarded coinduction (と guarded corecursion) について知りたかったんだけどなぁ。