こんな日記にもたまにブックマークを付けてくださる方がいらっしゃて有り難い事です。しかし自分が理解した順番に書いてるだけなので、話題が前に後ろに飛びまくって読みづらくて申し訳ない。いつかそのうちちゃんと分かりやすい順番にまとめたいと思ってい…

真の定義 真実とは何でしょうか?それは人類始まって以来の謎に満ちた疑問に思えますが、プログラムの世界では割と簡単です。真と偽を表す値と演算子を使って真偽表で判定します。例えば真理表はこんなのです。 真 ならば 真 => 真 真 ならば 偽 => 偽 偽 な…

なんか Coq の事ばかり書くとどんどん日記のアクセス数が落ちて行く。。。ま、いいか。とりあえず Coq の型システムの勉強したいんだけど、その前提知識が沢山あるので仕方なく細かい部分をやっています。ただ、今まで勉強した事はどれも最初すごく難しく感…

本でもマニュアルでも大変分かりずらく解説されてある unfold を使ってみます。関数を使うという意味で unfold は apply となんだか良く似ています。 unfold はゴールの中の関数名を定義で置き換えます。 apply は前提の関数型 A->B の B がゴールにマッチす…

日曜日も一日 Coq で遊んでいた。Coq'Art の冒頭に、Coq を使えばソートプログラムの証明が出来ると書いてあって、それが知りたくて頑張って読んでいるがいつまでたっても具体的な方法が出てこなくてがっかりしている。これだけの本をさっと読むのは大変だし…

Coq in a Hurry ではこの後 Inductive Types の話になりますが、難しすぎてついてゆけないのでInteractive Theorem Proving and Program Development (Coq'Art) isbn:3540208542でゆきます。この本は重くて固くて取っ付きにくいですが、基本的な事から順番に…

forall についての雑文 さて、ここで教科書の Coq in a Hurry に戻ると、私が作った「風が吹く」「桶屋が儲かる」なんかの命題を Variable で定義する代わりに、forall というキーワードを使っています。つまり、 Variable 風が吹く 桶屋が儲かる : Prop. Th…

前回の Coq はいきなり難しすぎました。forall とか、数学やってる人には常識なのかも知れないけど一介のプログラマには高度すぎます。ikegami さんに単純な例 http://www.youtube.com/watch?v=f9XOdpmeJ0o を教えてもらったんだけど同じじゃつまらないので…

CafeOBJ の雰囲気が分かった所で今度は Coq に挑戦。かなり難しいですが、あきらめずに Coq in a Hurry http://cel.archives-ouvertes.fr/inria-00001173 を元に勉強しています。 起動と終了 起動は coqtop で終了は Quit. です。また、macports でインスト…