ホワット・ア・ワンダフル・ワールド 1+1=2を証明するためには1万ステップ以上かかるよ，という話
なんかすごいサイトを見つけてしまいました． Metamath Proof Explorer Home Page 数学の基礎付けに関する 20 世紀の記念碑的偉業と称えられながらも，歴史上何人がこれまで読破したのか，と常にネタにされる Principia Mathematica （12 万円，2000 ページ！） に，1+1=2 の証明が載ってるっていうのはわりと有名な話だと思いますけど． 追記 : Radium Software Development 2006-06-30 : Proof that 1 + 1 = 2 # ちなみに，三巻組の大著の全文をオンラインで見ることができます．"From this proposition it will follow, when arithmetical addition has been defined, that 1+ 1= 2."． このサイ
ホワット・ア・ワンダフル・ワールド 数学屋さんの悪い癖だ
偉大になりすぎるとシェアを失いますよ，閣下 (笑) イネムリネズミ日記 2007-06-22 梅雨でも洗濯 _ Arrowのこと Open Source Conference 2007 Hokkaido の資料作り終えた。セミナーのほうはかなり初心者向きな講演になると思う。けど… あろはさんみたいな人ばかり来たらどうしようと思ったので Arrow の復習もしておいた。小さな部屋らしいから、「Arrowというものが世の中にはございまして、Kleisli 圏やら Premonoidal 圏がどうのこうの…」とか言っておけばよかろうと考えた。これでも甘いと言われたら Functional Reactive Programming とかですか（だんだん偉大なる Shelarcy さんに近づく例）。 いやー，僕はそっち方面は全然わかりませんよ．どんだけ買い被られているのだろう (苦笑) たぶん実際に
ホワット・ア・ワンダフル・ワールド OCaml で文字列からの read-eval-print
Author:あろは (alohakun) デバッガ開発者見習い（予定） 連絡先 : alohakun ___at___ gmail.com mixi : http://mixi.jp/show_friend.pl?id=182927 twitter : http://twitter.com/alohakun このページはインラインフレームを使用しています yoriyuki さんからコメントをいただきました． > 文字列を eval したり，型情報を取得したりするやりかた Toplevelというモジュールが標準でインストールされています。秘密のAPIなのでドキュメントはtoplevel.mliのコメントしかありませんが。 うほっ… そんな魅惑的なモジュールが． しっかし，toplevel.mli なんてファイルはどこにも見当たらない… orz というわけで，ソースを落としてきて，topl
ホワット・ア・ワンダフル・ワールド gcc フロントエンドの minimal
ずいぶん昔に GCC の ひらメソッド wiki (諸事情により wikia に移転しました) の方で教えていただいたネタなので，いまさらですが． チャレンジしたことが無いとなかなか実感がわかないと思うのですが，tree.h や tree.def を理解した上で LANGHOOKS や GGC など独特のフレームワークを攻略しないといけないので，GCC のフロントエンドを作るのは死ぬほど学習曲線が高いです． 一応，treelang というフロントエンドのサンプルが含まれていたりするのですが，これもまたけっこう独特なデータ構造を使っていたりするので，何が treelang に特有の部分で，どこが gcc 固有のお約束なのかが見えにくかったり．(何よりも，僕が yacc/lex 怖い現代っ子というのが大きい) そんなこんなで，こういう，本当に minimal なフロントエンドはいろいろ参考にな
ホワット・ア・ワンダフル・ワールド 全てのプログラミング言語は C コード生成器と割り切るべき
これは至言だと思う． イネムリネズミ日記 2007-06-17 梅雨が中休みするなら俺だって 業務系のシステムを作りたい人には申し訳有りませんが、世界の進歩のスピードは言語の成長のスピードを超えています。バグのない、安定したプログラムを作りたければ、熟練したプログラマに C で書かせるのが最も良い選択肢でしょう。バグがあるかもしれないけど、とりあえずできればいいや、ナンチャッテ、次のリリースで直すから許してチョという代物は軽量言語で書くのを僕はお勧めします。 僕にとって、軽量言語とはそういうものです。 しかし，いくらなんでも C コードを最初から人間が手書きするような時代では無い．C/C++ では，マシン間の互換性を取るだけでも，ifdef の塊になるし． となると，Haskell とかで型システムなどによる検証済みの C コードを吐くとか，そういう方向になってくる．つまり，Ruby とか
ホワット・ア・ワンダフル・ワールド 大手 SIer で働くメリット･デメリット
お断り : 今回の記事は，隣の芝が青くて青くてしょうがない負け組大学院生(ドクタ進学希望)が相対化のために書いているエントリーなので，非常に醜悪な内容です．すいません．そこはまぁ可哀想な人なんだということでお一つ． 大手 SIer で働くメリット･デメリット 大手SIerは技術志向のSEには向いていない？ 「何であんな良い会社を辞めたんですか？」――新卒後、大手シンクタンク系SIerでのSE経験を持つ山崎氏は、転職活動時に面接官からよくこう質問される。その会社でビジネスマンとしての基礎を作ってもらったこと自体には感謝しているが、会社を辞めたのにはそれなりの理由がある。 「まず、仕事がある時期から物足りなくなってしまう。結局大手SIerはある入社年次から外注さんをかき集めて、外注管理するのがメインの仕事になりがちです。若いうちから外注管理をメインにやっているから、自分でプログラムを書く機会が
ホワット・ア・ワンダフル・ワールド 閉塞社会を超えていかなくちゃ
今の優秀な若い人たち (といっても，ほとんどが身近な同期の連中で，サンプル数はとても少ないのだけど) の話を聞いていると，みんな驚くほど似通ったライププラン･キャリアパスを考えていることに驚く． # ちなみに，僕は今の所，両親祖母 (祖父は既に他界) も元気で，結婚を考えているような恋人もいない．ドクタ進学を考えており，まだまだ就職する気も無い．というわけで，23 歳にして未だぷらぷらモラトリアムの中で．少々普通の人 (?) とは異端のルートを生きている人間といえる． # 以下は，そんな人間から見たとりとめのない感想である． そんなこんなで就職活動の経験が無いので詳細はよくわからないのだけど，現在の学生は，非常に情報に恵まれているらしい．たくさんの企業の給料の上昇率や福利厚生待遇のまとめサイトや2 ch の専用スレッドは枚挙にいとまない．みな非常によく勉強していて，驚くほど知識が豊富だ．
ホワット・ア・ワンダフル・ワールド 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 (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 (4) 自然演繹法
前回までは，何の説明も無く，いきなり intro や apply を使って，非常に初歩的な命題論理の証明を行ってみました． # ちなみに，本職の Logician の方々が見たら噴飯モノの，訳語とか概念に関する間違いや誤解，曖昧さがゴロゴロしていると思いますが，あんまり修正とか見直しとかはしないで，とりあえずどんどん進んでいこうかと思います．その過程で段々理解が進んできて，誤解も訂正されていくと思うので．必要以上に過去は振り返らないで，未来だけを見つめて行きましょう ! (耳障りが良い常套句 ｗ) # とはいえもちろん，ツッコミやコメントは大歓迎です (⌒▽⌒) けっこういろいろやったので，復習としてコマンドをメモしておきます． Quit. Coq の終了． Check 識別子. 識別子の型を調べる． Section Declaration. 宣言セクションに入る． Variable va
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (3) Minimal Logic
今回は，最も基本的な組み込みの最小論理 (Minimal Logic) 推論エンジンの，ほんのさわりだけを見ていきます． 使用するのは，いわゆる三段論法ってやつです (厳密にいうと，この用語はけっこう曖昧なので，あんまり使わないほうが良いのですが…)．A と A → B が成り立つならば，B が成り立つという，アレです．うむ，常識ですな (笑) # でも，型理論の論文とかで， A A → B -------- B とか書いていると，べつにどおってことないことなのに，何だかびびってしまいませんか ? (笑) まぁ，あたりまえのことを，あたりまえにやっていくのが，論理学ですからね．そして気がつくと，当たり前のことをずっとやってきたはずなのに，とんでもない結論が出てくると w これが論理学の醍醐味です．基本は大事なんですよ． というわけで，まずは Coq を立ち上げ，セクションを切り替えておきま
ホワット・ア・ワンダフル・ワールド Ｔｈｅ Ｃｏｑ Ｐｒｏｏｆ Ａｓｓｉｓｔａｎｔ Ａ Ｔｕｔｏｒｉａｌ (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
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (6) トートロジーの自動証明
前回までは，命題論理における自明なトートロジーをいくつか，手動で証明してみました． しばらく定理証明系を触っていると，構成的数学における証明 ※ とプログラミングは，本質的に区別がつかない (極論すれば，同じモノ) ということがよくわかってくると思います． ※ 何かが成り立つということを，弁証ではなく，実際に作って見せることによって証明を行う数学の流派． 定理は，同じことを何度も書かないですませ，証明を短くし，見通しを良くするための「サブルーチン」，あるいは，いくつかの公理を組み合わせ，より高級な命令を作るための 「マクロ」 ですし，公理や規則はまんま「機械語」です． 流派によって公理系 (公理の集合) が違うのは，CPU の命令セットの違いに例えることができますし，どの高級言語が優れているかという論争は，まんま論理体系の優劣論争 ※1 です w ※1 ほとんど全ての論理体系が扱える範囲自
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
