日々の流転

λ. CoInduction in Coq. Yves Bertot

<URL:http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/Extra/bertot.pdf>

CoInductiveな場合でもInductiveな場合とほぼ同様の表記で書けるというのが少し面白かった。私は、Inductionと双対的な表記を漠然と想像していたのだけど、そんな必要は全然ないわけか。考えてみれば、こっちの方がHaskellなどの言語で無限リストなどを扱う方法に近いもんな。

bisimulationを明示的に扱わなくてはいけないのはやはり面倒みたい。Tacticsを使うこともできるけど、それでもすべての問題が解決するわけではない。もっと、根本的な解決はできないものだろうか?

例として実数を存在区間の縮小列で表現して色々やっている。 Coqについてよく知らないので、ここはあまり真面目に読んでいない。 この実数の表現方法は <URL:http://www.i.h.kyoto-u.ac.jp/~tsuiki/research/CompReal.html> でいう「個々の実数に複数の名前を許すことにより、名前を通した実数の計算を可能にするという方法」にあたるのだろう。