10月10日の集い

ranha 10月10日ぐらいに、簡単に定理証明系で殴り合うみたいなイベント無いかなぁ。メジャーな○○の使い方も、各々異なる所があるので、やってる人が個別にスタイルを教えてくれたりすると手っ取り早くて良いかなーとか。Proof Generalというかtacticalな証明系は分からんので link

という事(自分の発言ですけど...)だったので、ATNDに早速ページを作ってみました。

http://atnd.org/events/1507

詳しい話(?)はATNDの方を見てもらえば良くて、また例によってどこかで難しそうな話なんだろうなぁとか思われると嫌気なので書いておくと、やっぱり難しい話じゃないわけです。正確には私としてはそのつもりです。

で「定理証明」なんて言われてもピンと来ないかもしれないのですね。まず「定理」と「証明」がピンと来ない。

ここでいう「定理」っていうのは、何も数学数学したモノに限った話じゃないという事です。
あんまりエキサイティングな例では無いと思うのですけれども、

QuickSortが本当に停止するよね
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20090831#p01
http://d.hatena.ne.jp/yoshihiro503/20080308

みたいな話(この2つのエントリには、filter list <= length listになるよねなんていう事も含まれているんですけれども)もあります。

あとは、QuickSortが本当にソートしてくれるのか！という定理、を調べたり(証明したり)。

「証明」は何をもってそうするかっていうと、CoqとかAgdaでは型のレベルである定理が言えるかという事を補題を作るだとかで調べるのですが、
まぁこれは「型のレベル」で、「実行される前」に本当に言えるのかどうかっていうのが調べられます。
すると、「何が起こるかあんまり分からん実行レベル」の挙動に保証が付けられるわけです。

依存型を持つ言語って言うのは、値のレベルで定義した関数を型のレベルで使う事も出来て、そうでない言語からはちょっとそれはどうよみたいな部分があるんですけれども、そういう型レベルの何ソレが余り考慮されてない言語、C++は考慮されてると思うんですが、とか、そもそも型の無い言語で定理を証明するって、どうするの??という話もあります。

これも今回の響おめでとう！の会では、自分の言語でどうやってのければ、証明した雰囲気が出るかという事まで含めてやれれば良いんじゃないかなーと。

個人的には、Isabelle/HOLとかCoqで「証明を支援する使い方」をするのが良く分からなくて、それどころかIsabelle/HOLとCoqは全然知らないので、そういうのも知ってる人が知ってない人に教えられると良いんじゃないかなとは。

多分ある程度面白い「お題」を決めた方が良いと思うんですけれども、手頃な何かがあれば教えてください。

型が無くてもどうこう

としては、

もあったりですね。