Proof Assistant Coq
The Coq proof assistant
を，とりあえず apt-get でインストール (coq，coq-libs，coqide) してみようと思ったら，debian パッケージが壊れているっぽくて，インストールできませんでした (stable/testing/unstable いずれも)．残念．そのうち直ると思うので，しばらく様子を見てみます(軟弱者)．
ちなみに Coq ってのは，Agda や Isabelle/HOL と同じような，定理証明支援系のこと．Calculus of Inductive Construction とかいう，あまり聞きなじみが無い論理体系をベースにしているそうな．
# これについては，Interactive Theorem Proving And Program Development: Coq'art: The Calculus Of Inductive Constructions (Texts in Theoretical Computer Science. An Eatcs Series)，という本が，けっこう高いけど，良いらしいです．
# Isabella/HOL のリンク先は，日本語の，とても貴重な定理証明系の説明スライドです．HOL ってのは，高階論理 (Higher Order Logic) のことらしいです．Coq はほとんど日本語の資料は無いみたいですが… Isabella や agda はけっこうあるみたい．例えば 型理論での形式的証明記述の技法について．
さかいさんが使っている Agda は，関数型言語と同じような感じで証明を記述できるのがうりらしいのですが，私はもともと関数型言語全然わかりませんから… (^^;
というわけで，研究室の Windows にとりあえず Coq をインストールしてみました．一番歴史が古いらしく，完成度がとても高い気がします．
# そういえば，Agda はけっこうバギーだという噂を聞きますが，自分自身のソースコードは検証できないのでしょうか ? (笑)
普通に IDE 付きで，exe をダブルクリックすればインストール完了．Windows はよくわからないので，適当にパスを追加してみたりしましたが，何もしなくても動くかもしれません．とても簡単．やるな，Coq ！
しっかし，チュートリアルを見ても，何がなんだか全然わかりません．IDE の使い方から，文法，コンパイル方法まで，謎だらけです．
今日はちょっと忙しかったので，インストールしただけですが，これから少しづつ使って見ようかと．とてつもなくディープな世界なので，絶対使いこなせる日はこないと思いますが ｗ
# 「なるほど ITT の体系では選択公理が証明できるのか」とか，言ってみたい (笑)
最近ようやく Scheme とか Haskell などの関数型プログラミングが流行ってきたみたいなので，次のブームは定理証明系っしょ ! とか ｗ
企業の面接で，
「大学では，どんなプログラミング言語をやってきましたか ?」
「はい，Coq を少々たしなみます」
なんて会話が普通になるんですよ ｗ 今から備えておかないと (違
# しっかし，論理プログラミングとか，制約プログラミングは，なぜ流行らないのだろう… 型推論なんて，制約充足プログラミングパラダイムの一部です ! とか言って見るテスト ｗ
# 関数型のブームにこっそり乗って，関数論理型プログラミングとして復活すれば，また流行るかも !?
どうでも良いですけど，IDE のスクリーンショットが斬新です ｗ
Proof Fermat とかって，普通にあの超難問のフェルマー･ワイルズの定理を機械に証明させようとしています．アグレッシブだなぁ ｗ
無邪気にもほどがあります ｗ もちろん，絶対無理でしょう．100 頁以上にもわたって数式で埋め尽くされた，世界で 10 人も理解できないとかいう，そういうアレらしいですから ｗ
# 100 年後ぐらいには，計算機で検証できるレベルまで精密化されるのかなぁ ?
ふと思ったのですが，現在の数学者でも，やっぱり紙とペンだけでがんばっているのでしょうか ? 定理証明支援系とかを使うのは邪道なんですかね ? それとも，数学の種類 (構成的) が違うから，あんまり使われて無いとか ?
TAPL と同時進行で，少しづつ進めていこう．型理論と聞くと，なじみが薄いので戸惑いますが，定理証明とか論理学と言い換えると，不思議に抵抗感が薄らぐのが不思議です．両者は等価なんですけどね．
# 私はもともと AI 屋 (今は複雑系工学講座とかにいます) なので．知識表現系とか，一階述語論理とか，そっち方面は，ほんのちょっとだけかじってます．ほんとうにちょっとですが．
ていうか，本業の研究の方がさっぱり進んでないのに，何やってんだ俺は… orz
を，とりあえず apt-get でインストール (coq，coq-libs，coqide) してみようと思ったら，debian パッケージが壊れているっぽくて，インストールできませんでした (stable/testing/unstable いずれも)．残念．そのうち直ると思うので，しばらく様子を見てみます(軟弱者)．
ちなみに Coq ってのは，Agda や Isabelle/HOL と同じような，定理証明支援系のこと．Calculus of Inductive Construction とかいう，あまり聞きなじみが無い論理体系をベースにしているそうな．
# これについては，Interactive Theorem Proving And Program Development: Coq'art: The Calculus Of Inductive Constructions (Texts in Theoretical Computer Science. An Eatcs Series)，という本が，けっこう高いけど，良いらしいです．
# Isabella/HOL のリンク先は，日本語の，とても貴重な定理証明系の説明スライドです．HOL ってのは，高階論理 (Higher Order Logic) のことらしいです．Coq はほとんど日本語の資料は無いみたいですが… Isabella や agda はけっこうあるみたい．例えば 型理論での形式的証明記述の技法について．
さかいさんが使っている Agda は，関数型言語と同じような感じで証明を記述できるのがうりらしいのですが，私はもともと関数型言語全然わかりませんから… (^^;
というわけで，研究室の Windows にとりあえず Coq をインストールしてみました．一番歴史が古いらしく，完成度がとても高い気がします．
# そういえば，Agda はけっこうバギーだという噂を聞きますが，自分自身のソースコードは検証できないのでしょうか ? (笑)
普通に IDE 付きで，exe をダブルクリックすればインストール完了．Windows はよくわからないので，適当にパスを追加してみたりしましたが，何もしなくても動くかもしれません．とても簡単．やるな，Coq ！
しっかし，チュートリアルを見ても，何がなんだか全然わかりません．IDE の使い方から，文法，コンパイル方法まで，謎だらけです．
今日はちょっと忙しかったので，インストールしただけですが，これから少しづつ使って見ようかと．とてつもなくディープな世界なので，絶対使いこなせる日はこないと思いますが ｗ
# 「なるほど ITT の体系では選択公理が証明できるのか」とか，言ってみたい (笑)
最近ようやく Scheme とか Haskell などの関数型プログラミングが流行ってきたみたいなので，次のブームは定理証明系っしょ ! とか ｗ
企業の面接で，
「大学では，どんなプログラミング言語をやってきましたか ?」
「はい，Coq を少々たしなみます」
なんて会話が普通になるんですよ ｗ 今から備えておかないと (違
# しっかし，論理プログラミングとか，制約プログラミングは，なぜ流行らないのだろう… 型推論なんて，制約充足プログラミングパラダイムの一部です ! とか言って見るテスト ｗ
# 関数型のブームにこっそり乗って，関数論理型プログラミングとして復活すれば，また流行るかも !?
どうでも良いですけど，IDE のスクリーンショットが斬新です ｗ
Proof Fermat とかって，普通にあの超難問のフェルマー･ワイルズの定理を機械に証明させようとしています．アグレッシブだなぁ ｗ
Theorem Fermat :
(forall x y z n:nat, x^n+y^n = z^n -> n <= 2)
Proof.
無邪気にもほどがあります ｗ もちろん，絶対無理でしょう．100 頁以上にもわたって数式で埋め尽くされた，世界で 10 人も理解できないとかいう，そういうアレらしいですから ｗ
# 100 年後ぐらいには，計算機で検証できるレベルまで精密化されるのかなぁ ?
ふと思ったのですが，現在の数学者でも，やっぱり紙とペンだけでがんばっているのでしょうか ? 定理証明支援系とかを使うのは邪道なんですかね ? それとも，数学の種類 (構成的) が違うから，あんまり使われて無いとか ?
TAPL と同時進行で，少しづつ進めていこう．型理論と聞くと，なじみが薄いので戸惑いますが，定理証明とか論理学と言い換えると，不思議に抵抗感が薄らぐのが不思議です．両者は等価なんですけどね．
# 私はもともと AI 屋 (今は複雑系工学講座とかにいます) なので．知識表現系とか，一階述語論理とか，そっち方面は，ほんのちょっとだけかじってます．ほんとうにちょっとですが．
ていうか，本業の研究の方がさっぱり進んでないのに，何やってんだ俺は… orz
