Coqで証明中ですよと

えーと、TAPLの3.2.5をCoqを使って、証明しようと思ってたところです。

TAPLの3.2.5を証明するには、Coqで実装する方法を知らないと出来ないのでした。なので、実装方法を知らねばならず、4章の内容を知らないと出来ない事をやろうとしてますと。しかも、Coq良く知らないので、移植するだけでも大変そうですが、それよりも、ソフトウェアの基礎っていう素晴らしい教科書があるのでそちらを参考にします。

要するに http://proofcafe.org/sf/Imp_J.html をコピる簡単なお仕事をしてみます。

     Z ::= X;
     Y ::= 1;
     WHILE not (Z = 0) DO
       Y ::= Y * Z;
       Z ::= Z - 1
     END 

みたいな言語の話で面白いんですけど。
で、面白いので、ひたすら読んでました。
しかしこの方法じゃぁ、TAPL読み進めないよ。
おわんねーよ。
っていうことが分かってきました。

Coqは面白いツールですけど、使うと返ってTAPLの理解が遅くなります。
だから、Coqなしで、TAPLを素直に読もうと思いました。
あと、TAPLの2章は何故必要なのかが分からないので、覚え辛いのだと気がつきました。だから、必要になったら見る事にします。ただ、どんな概念があるのかは把握しておくのはよいので、一通り目を通したけど、よくわからないというところでよいのかなと思います。

こんな気持で、３章を、証明は飛ばすって読み方はやめることにして、覚えられなくても、目を通して、なんとなくでよいので、「どんなことをして証明をしているのか」と、「何を証明しているのか」を見て行く事にしました。

こうする事で、読むスピードは上がってくれると嬉しいです。

ということで、3.2,3.3を読み進める事が出来ましたよ。良くわかった気がします。そして、Coqで帰納法を勉強したのでよりよくわかりました。証明なんていらないし、そんなの昔やったとかいうプライドを捨てたので気が楽になったし。

述語と、帰納法が出て来たし。２章はゲームで言うとアイテムボックスみたいな物だと思うと良いようです。

こんなゲームあんまないけど、最初っから色んな道具を一気にバっと渡される。
これを使ってゲームを解くんだ。ってね。

こんなん、一体どうやって使うんだ？？？って思う訳ですよね。

そして、そのアイテムを徐々に使って行くのが、３章以降ってわけ。3.2,3.3で「述語」と「帰納法」を使った。使ったマークを付けるときっと楽しいです。

なんかもう、頭がソーシャルゲームになってます。
５個つかったら、プレゼントとか貰えると良いのにな。
まぁ、貰えんでも良いけど。

うーん。そんな電子ブックが欲しい。
それが、Eラーニングなのか。ってまた、別な話になりそうなのでいいや。ゲームブックだと思えば良いんだな。２章がキャラクターシートだと思って、キャラクターシートにチェックマークを付けるゲームだってことで見て行きましょう。

最初アイテムボックスっぽいと思ったんですけど、アイテムボックスはどっちかというと索引で、手に入れるアイテムは沢山あるので、多分面倒いんじゃないかなと。でも、覚えた事を索引にマーク付けることはやったことないので、楽しいかもしれません。

書き出して表にしてみたりすれば、理解が進むんだろうし。

で、3.2,3.3で言ってる事は、この本の証明でよく使う方法にはいろんなやり方がある中のうちで、分かりやすいやり方を使って行きますよ。って言う話です。

で、その分かりやすいやり方以外もいろいろ考えられるんですよ。そのために、サイズとか深さとかの計算が必要になったんですけど、基本的には難しくなるから使わないですよ。使うのは操作的な帰納法ですよ。ってことらしいです。

とくに3.3の帰納法の文章の構造の理解は重要です。

3.3では帰納法よく使う帰納法についての説明ですけど、これがボトムアップ的に書かれています。

最初に定義があって、定義の次に補題があり、最後に定理があります。

補題は定理を証明する為のものです。定義は定理を決める時に必要になる決めごとです。

で、定理を使って帰納法の章で言いたい事を言ってます。

いや、補題は定理を証明する為にあるっていうのは知ってた訳ですが、定理を証明する中で補題が複数出て来てっていう構造になってるのかと思ってたらそうではないこともあるってことを知っておくとよいんだろうなと言う事です。

mainと呼び出される関数の順番はどっちでもいいというかんじですね。

ま、そんなかんじです。
どーでも良い話が多いなと思いつつ。。。