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

http://reinventingtesla.com/キムさんに誘ってもらって、うちの近所の小劇場まで芝居を観に行った。芝居なんか観るのはマツケンサンバ以来だ。ずっと芝居には興味があったのだが、知らないしきたりとかあったら怖いので(靴を脱ぐとか)一人で行けなかったの…

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

git が使いにくいのはコマンド設計の悪さの他、レポジトリの状態と自分の位置を確認するのが難しいからだと思います。例えば Subversion ならある瞬間のファイルはパス名とリビジョン番号で一意に定まるので、時間的、空間的位置を把握するのは簡単です。し…

本でもマニュアルでも大変分かりずらく解説されてある 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でゆきます。この本は重くて固くて取っ付きにくいですが、基本的な事から順番に…

ふと、COBOL の事が気になったので遊んでみた。 インストール Mac OSX で OpenCOBOL というのを使ってみました。gmp と db というライブラリを先にインストールしておく必要があります。特に、db は新しすぎるやつじゃ駄目だったので、db45 を入れました。ど…

http://www.irisa.fr/asap/intranet/the-many-faces-of-publish-subscribe.pdfpublish / subscribe とは、通信方法の一つで、生産者と消費者間が以下の三つの点で依存しない方法。 Space (空間:お互いのポインタ) Time (時刻) Synchronization (同期: 処理中…

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 でインスト…

こないだ Will Rogers state park http://d.hatena.ne.jp/propella/20081116/p1 という所に行って、途中で迷子になって引き返す羽目になってしまったので再挑戦する事にしました。今日ものどかだ。ここ、ここ、ここで前回、右に曲がるのが分からなかったので…

こないだ C5 の後でちょっと話題になったので、CafeOBJ について調べてみました。http://www.ldl.jaist.ac.jp/cafeobj/system.html からダウンロードして展開、Mac の場合 lisp/CafeOBJ にバイナリがあるので、それを /usr/local/bin/cafeobj にシンボリック…