妄想とか迷走
さて、Sparkleでsortの正しさを証明しようと思った。めんどいので、isSortedという関数を用意して、"isSorted (sort ls)=True"を証明しようとしたのだけど、オーバーローディングが解決できません！とか怒られる(なお自前の関数を利用するには、.iclファイルに関数書いてProject>Add Moduleでいいのだけど、こんときStart関数がないと何故か怒られる)。型クラス使えないのかよ、Sparkleつかえねー、ということで終わろうと思ったけど、そこらへんは大人なのでぐっとこらえて、Int限定でいいやと思い直した。適当に調べると、型を指定するときには、"[ls::[Int]] isSorted (sort ls)=True"のようにやればいいらしい。が、"Prove topmost theorem"して出てきたGoalを見ると、"forall ls::[a].isSorted(sort ls)"だった。Int指定はどこへ行ってしまったのか。Sparkleは謎が多い。というか、<とかオーバーロードする時、型さえ合ってれば何でも良くて、それが(数学的な意味での)順序関係である必要は全然ないから、x
当初は、Buchbergerアルゴリズムの正しさを証明してやるぜとか思ってたけど、sort程度で挫折してるようじゃ、先は遠い。というか、CoqでBuchbergerアルゴリズムを生成した人たちは、グレブナ基底の存在証明をやったわけだけど、それに一年かかったという話で、一方こっちは最初から関数持ってるから、もっと楽だろうという算段だったんだけど、冷静に考えると正しいかどうか確証が持てない関数を相手取って、正しさを証明しようと試みるのは精神衛生上大変よろしくないよな〜。ていうか、Haskellで適当に書いたBuchbergerアルゴリズム、十中八九まだバグが残ってるはず･･･デバッガの時代は当分続きそうだ
というのはいいんだけど、fixed point promotionによる変換length (map f ls)->length lsと、こないだのSparkleによるlength (map f ls)= length lsの証明とを見比べると、各ステップがよく対応しているように見える。このへんの事情は、shortut fusionでも同じで、まあ融合変換はある種の定理の自動証明になってるというような。ということは、融合変換M->Nがあったら、そのプロセスから、自動的にM=Nの証明@Sparkleを抽出できる(ほんとかよ。hylo-fusionは、本質的にfoldだけでなく、unfoldも含んでるのでSparkleの証明に翻訳できないかも)。そうすると、もし例えばshortcut fusionが間違ってたら、正しくない命題M=Nの証明が得られることになる。というわけで、Sparkleでshortcut fusionを証明するというのは、Sparkleで証明できた命題がCleanで正しいことを部分的に証明するのと同程度の難しさがある。というような、胡散臭いことを考えたのだった。
まあ、Sparkleでshortcut fusionを直接証明するのは無理そうだな〜。CleanでCleanの処理系を書くことはできるので、そういうの経由すれば、証明できなくもないのかもしれず、それが上で「直接証明するのは」って書いた理由。しかし、そもそもCoqではなく、Sparkleを使う理由っていうのは、そういう間接的な証明を避けるというのが、大元にあった気がするので、間接的な証明しかできないのだとすると、Sparkleを使う意義も大分薄れるよな〜とか
こういうクネクネしたことを考えるのは苦手というか、多分基本的な知識が足りてないというか、どうでもええがな、という気分になる
結論:どうでもいい
