ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (12) 述語論理
いくらなんでも命題論理に時間をかけ過ぎでした． というわけで，まだまだ謎だらけですが，とりあえずガンガン進みます．進んでいくうちに見えてくるものもあるでしょう． そもそも Coq の真骨頂は (余) 帰納構成的論理 (the calculus of (co)inductive constructions) にあるので，いつまでもここらへんをやっていてもしょうがないのですが… そっち方面は全然わからないので，なるべく述語論理で時間を稼ぎたいところですね (笑) このペースで行くと，たぶん Coq のチュートリアルを紹介し終わるまでには，あと 10 年ぐらいかかりそう ｗ １人 「素人くさい Coq ドキュメント読書会」です．まぁのんびりのんびり行こうと思っています． さて，述語論理です．そもそも，命題論理と述語論理は，何が違うのでしょうか ? 一言で言うと，述語論理には，「内部構造」が加わり
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (11) 排中律の証明 (完結編)
いまだに Coq をよくわかってませんが，いちおう証明はできたみたいです． でも，いろいろ謎だらけです… 全然見当違いのことをしているのかもしれませんが… $ ledit coqtop Welcome to Coq 8.0pl3 (Jan 2006) Coq P. DN is assumed (* 排中律 EM を証明 *) Coq P ============================ P \/ ~ P EM P ============================ ~ ~ (P \/ ~ P) EM P H : ~ (P \/ ~ P) ============================ False EM P H : ~ (P \/ ~ P) ============================ P \/ ~ P EM P H : ~ (P \/ ~ P) ====
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (9) 排中律の証明
さかい さんからトラックバックをいただきました． ヒビルテ 2006-04-29 [Haskell] [quiz] (forall x. ((x->r)->r)->x) -> Either a (a->r) 問題の関数はこんな感じで定義できる。 notNotEM :: ((Either a (a->r)) -> r) -> r notNotEM k = k (Right (\a -> k (Left a))) dn2EM :: (forall x. ((x->r)->r)->x) -> Either a (a->r) dn2EM dn = dn notNotEM で、これが表しているのは何かだが……二重否定除去規則から排中律(The Law of excluded middle)を導く証明の計算的な表現だったりする。型はちょっと一般化してあるので、以下のようにより具体的な型にすると分かり易
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (10) 二重否定に関する小ネタ
直観主義というのは，「数学的対象は完結した存在 (神，イデア) ではなく，人間の心によって構成されていくものだ」 という思想です． π は π として最初から存在しているわけではなく，1 ステップずつ計算されて，徐々に形作られているものだよー，だから排中律なんてナンセンスだよーと． ブラウワ : 「本当，排中律とか無限 (極限) ってキモい．こんな，実際に作ることができないものを認めているから，数学は不確実になってしまうんだよー」 ヒルベルト : 「あんた馬鹿ぁ ? 数学者から排中律を奪うのは，天文学者から望遠鏡を，ボクサーから拳を奪うようなものだよー．よし，こうなったら，有限の立場でちゃんと数学の正しさを証明したる !」 という，数学の基礎をめぐる論争が，やがては不完全性定理へとつながり，チューリングマシンへとつながり，現在のコンピュータへとつながるわけですね．ドラマティック． 前回触れ
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (8) 一休み
現在，管理人は多忙と体調不良のため，あまり頭が回りません… もともとそんなに回りませんが． # 多忙と言っても，単に本人が無能で無駄に時間がかかっているというだけのことです．世間にはもっともっと大変な人達がたくさんいます．本当にもうしわけないです． 今回は，Coq に関係があるエッセイなどをいくつか紹介します． 萩谷先生のエッセイは，非常に面白くてオススメです．いつか私も，このような軽妙で優れた文章を書けるようになりたいものです． 機械による数学の型式化には，ドメインを限定して完全な自動証明を目指す定理証明系 (後述する B-M prover はこっち) と，体系は汎用的にしておいて，人間の手を借りる定理証明支援系 (Coq や Agda や HOL はこっち) があるそうです． ここらへんは， 形式化願望 論理と推論 --- 数学の形式化 ただ，人間の手を借りる以上は，やはりインタフェー
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (7) 古典論理
突然ですけど，古典論理 (排中律) ってうさんくさく感じませんか ? 一見 P ∨ ¬ P は，どう考えても自明に思えますが，本当にそう言い切ってしまって大丈夫なのでしょうか ? 一般的に，「古典」と名がつくものは，ある程度成熟して一般的になり，共通のコンセンサスが取れているもの，というような意味合いで使われます． # 「時代遅れ」とか「古くて適切ではない」，というニュアンスとは全く異なります． それらは非常に美しく理想化されており，普遍的なものであるからこそ，「古典」と呼ばれ，いつの時代も重要であり続けるのです． 例えば，バッハの音楽や中国の漢詩，宮本武蔵の五輪の書などは，立派な古典ですね． もちろん，これらは，そのまま現代の状況に応用できるわけではありませんが，その「コア」の部分は，時代に合わせて形を変え，脈脈と語り継がれて行くわけです． # 人間はそう変わるものではないので，5000
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (6) トートロジーの自動証明
前回までは，命題論理における自明なトートロジーをいくつか，手動で証明してみました． しばらく定理証明系を触っていると，構成的数学における証明 ※ とプログラミングは，本質的に区別がつかない (極論すれば，同じモノ) ということがよくわかってくると思います． ※ 何かが成り立つということを，弁証ではなく，実際に作って見せることによって証明を行う数学の流派． 定理は，同じことを何度も書かないですませ，証明を短くし，見通しを良くするための「サブルーチン」，あるいは，いくつかの公理を組み合わせ，より高級な命令を作るための 「マクロ」 ですし，公理や規則はまんま「機械語」です． 流派によって公理系 (公理の集合) が違うのは，CPU の命令セットの違いに例えることができますし，どの高級言語が優れているかという論争は，まんま論理体系の優劣論争 ※1 です w ※1 ほとんど全ての論理体系が扱える範囲自
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (5) 自然演繹法 II
前回は自然演繹法についてちょっと書いただけで終ってしまったのですが，今回はちゃんと Coq を使います (笑) とりあえず，Coq のコマンドと，自然演繹法の推論規則の対応を押さえておきましょう． → 導入 intro H. → 除去 generalize (H1 H2); intro H3. ∧ 導入 split ∧ 除去 elim H; intros H1 H2. ∨ 導入の左側 left. ∨ 導入の右側 right. ∨ 除去 elim H; [intro H1 | intro H2]. ¬ 導入 intro H. ¬ 除去 absurd A; try assumption. とか contradiction. らしい．まだよくわかりません． 後ろ向き推論 apply とりあえず，対応表にそって，テキトーに証明を行ってみましょう． 例題は，チュートリアルの通りに，A ∧ B → B
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (3) Minimal Logic
今回は，最も基本的な組み込みの最小論理 (Minimal Logic) 推論エンジンの，ほんのさわりだけを見ていきます． 使用するのは，いわゆる三段論法ってやつです (厳密にいうと，この用語はけっこう曖昧なので，あんまり使わないほうが良いのですが…)．A と A → B が成り立つならば，B が成り立つという，アレです．うむ，常識ですな (笑) # でも，型理論の論文とかで， A A → B -------- B とか書いていると，べつにどおってことないことなのに，何だかびびってしまいませんか ? (笑) まぁ，あたりまえのことを，あたりまえにやっていくのが，論理学ですからね．そして気がつくと，当たり前のことをずっとやってきたはずなのに，とんでもない結論が出てくると w これが論理学の醍醐味です．基本は大事なんですよ． というわけで，まずは Coq を立ち上げ，セクションを切り替えておきま
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (4) 自然演繹法
前回までは，何の説明も無く，いきなり intro や apply を使って，非常に初歩的な命題論理の証明を行ってみました． # ちなみに，本職の Logician の方々が見たら噴飯モノの，訳語とか概念に関する間違いや誤解，曖昧さがゴロゴロしていると思いますが，あんまり修正とか見直しとかはしないで，とりあえずどんどん進んでいこうかと思います．その過程で段々理解が進んできて，誤解も訂正されていくと思うので．必要以上に過去は振り返らないで，未来だけを見つめて行きましょう ! (耳障りが良い常套句 ｗ) # とはいえもちろん，ツッコミやコメントは大歓迎です (⌒▽⌒) けっこういろいろやったので，復習としてコマンドをメモしておきます． Quit. Coq の終了． Check 識別子. 識別子の型を調べる． Section Declaration. 宣言セクションに入る． Variable va
ホワット・ア・ワンダフル・ワールド Ｔｈｅ Ｃｏｑ Ｐｒｏｏｆ Ａｓｓｉｓｔａｎｔ Ａ Ｔｕｔｏｒｉａｌ (2) 定義
前回の続きです． 今回は，定義についてです． coq-interface の初期化の際に読みこまれるプレリュードは，いくつか数学的定義を含んでいます． 例えば，前回扱った nat は，数学的概念 (mathematical collection) (Set 型) として定義されています．また，定数 O (オー) や S，plus なども，それぞれ nat，nat -> nat，nat -> nat -> nat という型のオブジェクトとして定義が用意されています． では，O と S を用いて，自然数を定義してみましょう．ここでは，一番最初の自然数 O と，次の自然数を求める関数 S の存在を前堤とします． 1 は，どのように定義すれば良いでしょう ? そうです，1 は O の次の数ですね． $ coq-interface Welcome to Coq 8.0pl3 (Jan 2006) C
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (1) 宣言
The Coq Proof Assistant A Tutorial を参考にしつつ，Coq について勉強していこうと思っています． まずは，Windows を使っている人は，ここから， coq-8.0pl3-win.exeをダウンロードして，ダブルクリックして Coq (IDE 付き) をインストールしておいてください． Coq は Calculuc of Inductive Constructions という論理体系に基づいた，定理証明支援系なのだそうです． 対話的に形式的な証明を構成していくことができて，さらにそれを，そのまま関数型プログラムの仕様として扱うことができるとのこと． このチュートリアルでは Gallina と呼ばれる基本的な言語仕様だけを扱うそうで，発展的な情報は Coq Reference Manual とか Coq'Art を参照せよ，とのこと． とりあえず，C:\
ホワット・ア・ワンダフル・ワールド 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 Inducti
えぷりくす
http://portal.acm.org/citation.cfm?id=1040305.1040313 今年のPOPLにこんなのがあったそうで、まさしく今 quantitative な analysis をテーマにしてる身としてはちょっと読んでみようかなと思ったり。 それはそうとすみいさんもほそやさんも POPL 通ってて自分はさっぱりうだつがあがらんなあとちょっとがっくり http://www.excite.co.jp/News/odd/00081108087433.html ジョーンズさんの友人の手元に渡るまでの経緯が激しく気になる http://www.nikkansports.com/ns/general/f-so-tp0-050111-0019.html 「鈴木亜美で妻子３人殺害」に見えた。 処方されたリタリンを試してみた。さすが「合法覚醒剤」の別名を持つだけあって、他の薬が
にわとり小屋でのプログラミング
この記事はTppMark11の問題をCoqでやってみたという内容である。 問題はこちら: docs.google.com 命題論理式と同値であることの定義 命題論理式の定義 Inductive Term := | Var(v : Var.T) | Neg(t : Term) | And(t1: Term)(t2: Term) | Or(t1: Term)(t2: Term) | Impl(t1: Term)(t2: Term) | TRUE | FALSE . 同値であることの定義 変数環境を表すctxを Var.T -> bool の関数で表現し、命題論理式のevalを次で定義した。 Fixpoint eval ctx t : bool := match t with | Var v => ctx v | Neg t => negb (eval ctx t) | And t1 t2 =>
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
ソフトウェアの基礎