2006-06-02
Peter E. Hart, Nils J. Nilsson, Bertram Raphael. A Formal Basis for the Heuristic Determination of Minimum Cost Paths. IEEE Transactions on Systems Science and Cybernetics, Vol.4, No.2, pp. 100-108, 1968.
A* アルゴリズム（"a-star" 「エースター」と読む）はグラフ探索アルゴリズムの一種として知られる。最短の経路を極力少ない反復によって見つけることができるという性質を持つ。その性質から，経路探索の問題においてはほぼ定番の解法となっている。
上の論文は 1968 年に発表された A* アルゴリズムの原典である。その内容のほとんどは， A* アルゴリズムの持つ諸性質の証明に費やされている。これらの証明は，本来ならば A* アルゴリズムを応用する上で必要とされる知識ではないが，非常に丁寧にまとめられているがゆえに，参考になる点も多い。参考書や雑誌記事などの解説では不足する情報もあるため，補足としてこちらの原典に目を通すことが望まれるのではないかと思う。
この論文では主に， A* アルゴリズムの持つ２つの性質の証明が行われている。ひとつは， A* アルゴリズムは許容的 (admissible) であるという性質であり，もうひとつは，許容的なアルゴリズムの中でも A* アルゴリズムは最適 (optimal) であるという性質である。
ここでの「許容的」とは，確実に最短の経路を見つけ出す性質のことを表す。この性質が成立するには，ゴールまでのコストを見積もるヒューリスティック関数 h^(n) が常に過小評価を行うことが必要とされる。「過小評価」とは即ち，ゴールまでの実際のコストよりも常に小さい値を見積もることを意味する。
また，ここでの「最適である」とは，評価するノードの数が最小であることを表す。この性質が成立するには，ヒューリスティック関数 h^(n) に一貫性 (consistency) が認められなければならない。この「一貫性」とは，隣接ノードとの間のコストを常に過小評価する性質のことを表す。例えば，ノード m とそれに続くノード n を考えるとき， h(m, n) + h^(n) ≧ h^(m) となる必要がある。
ただし，「最適である」のは，「A* よりも少ない情報から探索を行う許容的なアルゴリズム」と比較した場合に限られる。その効率は，ヒューリスティック関数から与えられる情報の多寡によって変化する。また，許容的ではない「不正確なアルゴリズム」が， A* よりも少ない反復から解を見つけ出す可能性も考えられる。
加えて，評価関数 f(n) が複数のノードにおいて全く同じ評価値を導き出した場合，それらのノードから候補を選択する際の順序如何によって，効率に優劣が付く可能性も指摘される。
A* アルゴリズムの持つ諸性質を有効に活かしたいならば，この辺りの前提を正確に守っておく必要がある。オーソドックスな経路探索を行う限りにおいては，テキスト通りの実装を行っておけば問題無いものの，例えばノード間のコスト評価に特殊な要素を盛り込む場合や，ヒューリスティック関数に特殊な条件を盛り込む場合などには，それらの変更が前提を崩してしまっていないかどうか気をつけなければならない。
名前の由来
論文中では，許容的 (Admissible) なアルゴリズムを "algorithm A" として総称し，その中でも最適なものを "algorithm A*" として表している（アスタリスクは上付き）。恐らく， "A*" という奇妙な名前の由来はここにあるものと思われる。
2006-06-06
secretGeek - "how reddit encourages mediocrity"
ソーシャルブックマーク "reddit" [reddit1] は，登録ユーザーからの投票を基にリンクの評価を行っている [reddit2] [Wikipedia] 。登録ユーザーが "hot" を押せばポイントが上がり， "cold" を押せばポイントが下がる。このような評価システムによって，多くの人が "hot" だと思うリンクがランキングの上位に浮上してくるようになっている。
……というのが，恐らくは設計上の意図であるが，この評価システムは必ずしも意図通りに働いているとは言えない。 "secretGeek" の Leon Bambrick 氏は，このシステムが凡庸さ (mediocrity) を助長するものであると指摘する。
芸能関連のニュースなどで，「好きな芸能人」「嫌いな芸能人」のランキングが公表されることがあるが，この両方に同じ人物がランクインしているのを目にすることがある*1。本当に優れた芸能人は，人々に好かれるのと同時に，別の人々には嫌われている。そのどちらでもない芸能人は，誰からも気にかけてもらえないような凡庸な存在であるに違いない。
人々にとって本当に意味のあるもの，価値のあるものは，人々に何らかの感情を喚起するものである ― そのような見地からすれば， reddit のような１次元的な評価システムは，話題の重要性を正しく捉えることができないと考えられる。人々が重要と思う話題に対して投じた "hot" と "cold" は相殺し，他の凡庸な話題の中に埋もれることを助けてしまう。
かくして，「誰からも嫌われないが，なんとなく好かれることはある」というような話題だけが上位に浮上してくることになる。それが必ずしも悪いわけではないが……凡庸さに支配される危険性からは逃れることができない。
"Creating Passionate Users" の Kathy Sierra 氏は次のように述べる [Passionate] 。
「もし，誰かが嫌うようなことをやっていないのであれば，それは恐らく凡庸である。」
リスクに対する恐怖，「誰かの意思に反するのではないか」という恐怖，それらに屈服することから，凡庸さへの下降は始まる。本当に人々にとって意味のあることを見つけ出すには，それらの恐怖に囚われてはいけない。人々から嫌われることの中にも一片の価値が隠されていることを，常に心に留めておく必要がある。
*1: ここで参考資料を示すべきだが，残念ながら適当な記事を見つけることができなかった。勘違いだろうか？
2006-06-07
"wizard" という語は，コンピュータに関して高等な知識を持った人のことを表すのによく用いられるが，特に UNIX の達人を指して用いられることもある [JargonFile] 。 The Open Group （UNIX 関連の標準化団体）が過去の USENIX カンファレンスにおいて配布したという "UNIX Magic" と題されたポスターには，白い髭をたくわえた魔法使いが妖しげな錬金術を駆使する様が描かれている [CodingHorror] [unix.org] 。
Image from Coding Horror
ところで，この絵をよく見てみると，魔法使いの周囲に UNIX にちなんだ物品がちりばめられていることに気付く。自分がその意図を汲み取ることができたものだけでも，以下のようなものがある。
自分が意図を汲み取ることのできなかったものも，まだかなり残されている。例えば "uucp" の瓶に半分隠されて "ke" しか見えない瓶が存在するが，これを何を意味するものなのかは，よく分からない。右下に居る黒猫にも何らかの意味があるに違いない。 "oregano" と記された瓶は，どうやら ALGOL 60 の処理系を意味しているらしい [DanielBerry] 。窓の外に見える鎌を持った農夫の姿も，なにやら意味深長ではある。
2006-06-08
Creating Passionate Users. "What a graphic can tell you".
情報可視化 (information visualization) とは，抽象的な情報（データ）を，人間が容易に理解することのできる表現に変換する手法のことを指す [Wikipedia] 。例えば Ben Shneiderman 氏の treemap [Shneiderman] は，各要素の持つ量と，それらの包含関係を同時に表現することのできる可視化手法である。単純な図表では把握の難しい情報も，このような可視化を経ることによって，直感的に理解することのできる表現になることがある。
ある日， "Creating Passionate Users" の執筆陣の一人である Dan Rusell 氏は，何気なく PowerPoint 上でドットを並べている最中に，あるひとつのアイデアを思いついた ― もし，このドットひとつが１日に相当するとしたら，自分の一生全体は，果たしてどのように見えることだろう？
Image from "What a graphics can tell you" (Creating Passionate Users)
朝起きて，昼活動して，夜眠りに就き，１日が終わる。その延々と繰り返されるサイクルはあまりにも当たり前すぎて，その中で過ぎ去っていく時間の流れを絶対的に認識することは難しい。しかし，その１日１日を点にして敷き詰め，全体として見渡してみると，ある感覚が沸き起こってくる ― たったこれだけしかないのか。この吹けば飛んでしまいそうな点々の中に，これまでに過ごしてきた日々と，これから過ごすべき日々の全てが含まれている。仕事の日も休みの日も，勤勉の日も怠惰の日も，嬉しい日も悲しい日も，焦りを感じた日も諦めを感じた日も，全てはたったこれだけの点でしかない。
この敷き詰められた点の中で，今日という日は何処に位置するだろう？ これまでに費やしてきた点はどれほどあるだろう？ そして，これから先にどれほどの点が残されているのだろう？ その小さな点の集まりを見つめながら，そこにある意味を考えてみるのも面白い。
（註： この図では，時間という１次元的な広がりを持つ概念を２次元的な表現に変換しているが，この変換が認識に誤った性質を与えてしまう可能性がある。表現の方法を工夫すれば，その認識を恣意的に操作することもできるかもしれない。例えば，平たく配置すれば人生は短く感じられるかもしれないし，極端に長細く配置すれば案外に長く感じられるようになるかもしれない。）
2006-06-09
David Harel, Bernhard Rumpe. Modeling Languages: Syntax, Semantics and all that Stuff. Technical paper number MCS00-16, The Weizmann Institute of Science, 2000.
著者の David Harel 氏は，状態遷移図の一種である Statechart の考案者として知られる。 Statechart のコンセプトは UML のステート図に受け継がれていると一般には考えられているが，ここで Harel 氏は UML に対する批判を展開する。
Harel 氏の主張するところでは， UML には厳密な意味論 ― いわゆる「セマンティクス」の定義が欠落している。論文の前半部分では，「セマンティクス」という概念自体の定義を明らかにするとともに，その定義に必要とされる要件を挙げている。 UML は，公式には OCL (Object Constraint Language) を用いたメタモデリングによってセマンティクスの定義がなされていることになっているが，氏の指摘によれば，これは文法 (syntax) の定義にしか及んでいないとされる。
Harel 氏の言説の根幹には，視覚言語 (visual language) もテキスト言語 (textual language) も本質的には差が無いとする考えがある。 UML の非形式性にしてみても，決して視覚言語という手法自体に限界があるわけではなく，本来はテキスト言語と同程度に形式的であることができると主張する。現に Statechart は厳密なセマンティクスの定義を行うことができている。他方で UML はその定義に失敗してしまっている。現場の技術者にとって UML が厳密なセマンティクスを持つことにどれほどの重要性があるのかは分からないが，言語設計者や方法論研究者などのようにセマンティクスを拠り所のひとつとしなくてはならない人々にとっては重大な問題となりうる。
UML は下書きのための言語であるべきではない。本来，「図」と「テキスト」は同程度に厳密であることができる。「図」を簡易表現の手段として捉えることを氏は否定する。その心情は次の一節にもよく表れている。
「図」とは，視覚補助の一種であり，技術者がナプキンの裏に殴り書きする類のものである ― そのような「落書き現象」 (doodling phenomenon) に遭遇することがしばしばある。そこでは，論理立てられた「本気の仕事」はテキスト言語で行われるべきであるとされる。悲しいことに，多くの言語設計者や方法論研究者もこのような観点を持ってしまっている。
[via Lambda the Ultimate]
2006-06-13
Stephen Rubin. "Which patents have you violated today?". Game Developers Conference 2006.
「ゲーム開発者は特許制度とどのように付き合っていくべきなのか」という問題に関して，法律の専門家の視点から助言を与えている。典型的な訴訟の分類に始まり，昨今の動向や，特許制度の仕組み，賠償額の決め方，防衛の方法，訴えられた場合の対処，等々，「浅く広く」の解説を行っている。基礎知識を集める分には参考になる点が多い。実例を交えつつ平易な説明がなされているという点も有難い。
ただし，読み進めるにあたって辞書を引かなくては分からない箇所が多くあったように感じられた。普段，技術文書にばかり目を通しているためか，たまにこういった「普通の話題」に目を通そうとすると，知らない単語や言い回しに出くわす確率が高くなる。語彙が妙な方向に偏ってしまっていることを痛感させられる。
2006-06-14
Image from EepyBird.com
ダイエット・コークにメントスを投入すると，不気味なほどに激しく泡を生じる [Google] 。ボトルの口から猛烈に泡を吹き出す様は，まるで噴水のようでもある。 EepyBird.com の Fritz Grobe 氏と Stephen Voltz 氏は，この反応を利用して芸術的なショーを作り上げた [EepyBird] 。
しかしなぜ，ダイエット・コークにメントスを投入すると，激しく泡を生じるのだろう？ これほどまでに分かりやすい反応を見せるとなると，何らかの化学反応が起きているのではないだろうかと思わされる。しかし， EepyBird および Steve Spangler Science の解説 [SteveSpangler] によれば，これは核生成 (nucleation) [Wikipedia1] と呼ばれる物理現象が要因であり，化学反応の類ではないとされている。
核生成は，液体から気体，あるいは液体から固体への相転移 [Wikipedia2] の際に生じる現象のひとつであり，何も下地の無い所に生じる均質核生成と，何らかの下地の上に生じる不均質核生成の２種類に分けられる [西谷] 。この二つのうち，均質核生成が生じることはほとんど無い（例えば水が均質核生成により沸騰するには１気圧下で約 300 度まで熱される必要がある [安部] ）。通常は，容器との接触面や不純物を「よりしろ」とした不均質核生成のみが生じることになる。
つまるところ，炭酸飲料が泡を生じるためには，何らかの「よりしろ」が無くてはならない。通常は容器との接触面がこの役割を果たしている。ここに，例えば塩や砂糖のように顆粒状のものを投入すると，この１粒１粒が不均質核生成を生じるための「よりしろ」となり，激しく泡を生じることになる [暮らしの科学] 。
メントスをダイエット・コークに投入した際に起こる反応も，これと同様のものであると考えられている。メントスの表面にはザラつきやヒビがあり，その分，核生成を生じるための面積が大きくなっている。また，メントスが十分な重量を持っており，ボトルの底まで素早く沈むことも，核生成を助ける要因のひとつとなっている。
2006-06-16
Outerthought 社の Marc Portier 氏は，ソフトウェアの信頼性には次のようなパラドックスが存在すると主張する [Outerthought] 。
間違っていることを示す手段が多いほど ― つまり，挙げることのできるバグが多いほど，人々はあなたの正しさに確信を持つだろう。
逆に言えば，物事が正しく動いているという証拠は，それが正しく動いていないことの証明（の手段）を提供することによってもたらされる。
例えば，ソフトウェアのテストなどは，この文脈における「正しく動いていないことを証明するための手段」を提供するものであると考えることができる。
Portier 氏はこれを「ソフトウェア信頼性のパラドックス」であると主張するが，反証主義の見地からすれば，これはパラドックスと言うよりもむしろ正当な言明であるとみることができる。
カール・ポパーを始めとする反証主義では，科学と非科学を区別するための基準として，反証可能性 [Wikipedia] の概念を導入する。科学的な言明には必ず反証の手立てが認められなければならない。ポパーの反証主義と算出可能性については [蔭山] が参考になる。
反証可能性の概念は経験科学の立証に必要とされるものであり，どちらかと言えば数学的な性質を持つソフトウェアの分野において，無条件に受け入れられるものではない。コンピュータの動作が完全に予測可能なもの ― 決定論的なものであるとするならば，その上にあるソフトウェアの動作は論理的な演繹によって確証を得ることが可能であると考えられる。そこに経験科学的な手法を用いることが常に適切であるとは言い難い。
しかし，ソフトウェアの動作がいかに決定論的であるとしても，その論理的確証が現実的なコストにおいて得られるとは限らない。昨今のソフトウェアは無数のシステムとコンポーネントの上に構築されており，そのうえネットワークや外部デバイスのようにある種の不確実性を持つ要素とのやりとりを行うこともある。そのようなソフトウェアに関して，とりうる動作を余す所無く論理的検証のふるいにかけることは，現実的にみて不可能であると言わざるを得ない。
また，人為的な誤謬の入る可能性も考慮に入れなければならない。ソフトウェアには必ず基となる仕様が存在するが，通常は自然言語によって記述されているこれらの仕様を，人の手によってプログラミング言語に置き換える（実装する）作業が必要とされる。いかに基となる仕様が完全なものであったとしても，それを実装する過程において誤りが生じれば，そのソフトウェアは元の仕様を反映していない「不完全なもの」へと変質してしまう。
これらのリスクを回避するための手段として，ブラックボックス・テストの手法がある。ブラックボックス・テストにおいては，ソフトウェアの中身に関する知識はすべて放棄し，ただ外部からの操作と観察のみによって，ソフトウェアと仕様の一致を検証する。もし仮に，ソフトウェアに対する唯一の要求が「仕様との一致」であるとするならば，このような手法によっても十分に確証を得ることができると考えられる。そして，ここに来て初めて，「自然法則に関する仮説を実験観察によって検証する」という経験科学的手法との間の類似性を見ることができる。
このような科学的手法との類似性と，前述の反証主義の見地を組み合わせるならば，次のような言明を新たに行うことができる。
ソフトウェアの仕様は，その実装を反証する可能性を持たなければならない。
仕様が十分に厳密かつ理論的なものであれば，それは自ずと反証可能性を持つと考えられる。それでは，反証不可能な仕様とは一体どのようなものだろうか？
例えば，次のような「仕様」が与えられたとする。
関数 p() は 1/10 の確率で true を返し，それ以外は false を返す。
このような「仕様」が与えられた場合，策定者に突き返すのが正当なやりとりだが，やる気が無いならば次のような実装を渡すだけで十分かもしれない。
bool p() { static int c = 0; return ((c++ % 10) == 0); }
あるいは，悪意があるならば次のようにしてもよい。
bool p() { static int c = 0; return ((c++ % 1000) < 100); }
もし，この関数の使用者が，この関数の動作を観察によってしか確認できない（つまり，実装を見ることができない）という特殊な状態にあるならば，その場合はもう，中身など何でもよいのかもしれない。文句を言われたら次のように返せばよい ― 「確かに私の実装は１万回連続で true を返したかもしれません。しかし，この場合の『確率』が純粋な偶然に従うものだとすれば，それが１万回連続で true を返す可能性を完全に棄却することはできないのではないですか？」
このような言い逃れを防ぐために単体テストを用意しようとしても，憐れな使用者はそれを行うことができない。この「仕様」は反証が不可能なほどに曖昧なものであり，実のところ，何も言っていないのに等しいものがある。これを反証可能にするには，何らかの前提条件を付加する必要があるが，そのような条件を付加した時点で仕様は別のものに変化してしまう。結局は，この「仕様」が実装に足るようなものではないことを指摘し，反証が可能になる程度まで修正することを要求しなければならない。
2006-06-20
Image from Incremental Operations
Incremental Operations. "Java call stack - from HTTP upto JDBC as a picture".
Peter Thomas 氏は，ある日， JBoss （Java EE ベースのアプリケーションサーバー）上で動いているウェブアプリのコールスタックを，１枚の画像に収めるという試みを行った。その結果は非常に印象的なものになっている ― ほんの一片のビジネスロジックを囲うために積み上げられた階層のなんと深いことか！
この画像に対する反応は，大きく分けて二通りある。ひとつは，オブジェクト指向における設計原則 [atmarkIT] を忠実に実践したことに対する感嘆。もうひとつは，途方も無く深いスタックフレームに対する直感的な嫌悪。そのいずれを表すかは，その人が持つ思想的背景によると考えられるが，概して後者の反応の方が強いように感じられる。
個人的には，深いスタックフレームに対して，どうしても「危険な匂い」を感じずにはいられない。過去の経験において，スタックフレームの深さはデバッグの難しさと結びつくことが多かった。また，スタックフレームの深さがパフォーマンスの低下と結びつくことも多かった。「危険な匂い」は，こうした過去の経験を漠然と反映している。
スタックフレームの深さは，設計が高度に階層化されている状態を表すとも考えられる。こうした階層化によって，各々のコンポーネントに十分な抽象性がもたらされる。しかし，その抽象性とは，アプリケーションを実現するために本当に必要とされるものなのだろうか？
実際にこのようなウェブアプリが市場において運用されているという事実は，その必要性を裏付ける証左であると言うこともできる。しかし，その裏舞台をこのような形で覗いてしまうと，どうしてもそこに危うさを感じてしまう。
度の過ぎた抽象化は，設計を実体から遠く離してしまう恐れがある [Joel1] 。また，完全な抽象性というものは実現が難しく，そこにはどうしても「漏れ」が生じてしまう [joel2] 。設計原則には「本音と建前」が存在する。ただひたすらに抽象化のドグマを守れば良いわけではない。「設計のための設計」ではなく，常に実用との結びつきを意識した設計を心掛けることが，その境界を正しく見極めるための視点を与えるのではないかと考える。
[via Ned Batchelder]
2006-06-23
Brian Hayes. The Semicolon Wars. American Scientist, 94(4), July-August 2006, pp.299-303.
地球上には様々な文化が存在し，それぞれに異なった言語が存在する。 Ethnologue.com の調査によれば，現在使用されている言語だけでも，地球上には約 6,900 種類もの言語が存在するとされている [Ethnologue] 。人類の歴史の長さと文化の多様性を考えれば，この種類の多さに不思議は無い。
コンピュータの世界に目を向けてみても，やはり様々な文化が存在し，それぞれに異なったプログラミング言語が存在する。 Diarmuid Pigott 氏の調査によれば，プログラミング言語という概念がこの世に現れて以来，約 8,500 種類もの言語が考案されたことになっている [HOPL] 。たかだか 50 年ほどの歴史の中で，これほどの多様性が生み出されたことには驚きを感じる。しかし一体何ゆえに，これほどまでの多様性を生み出さなければならなかったのだろうか？
Brian Hayes 氏は本稿において，プログラミング言語の持つ多様性について考察を展開する。例えば，ステートメントの終わりに付けられるセミコロンに注目してみても，言語によって微妙に異なった意味が与えられている。 C のセミコロンは「ステートメントの終わり」を意味するのに対して， Pascal のセミコロンは「ステートメントの区切り」を意味する。 Pascal の場合ならば，次のように最後のステートメントからセミコロンを省略することができる。
x:=0; y:=0; z:=0
C では，このように記述するわけにはいかない。しかし，それで困るということは無い。このような表層的な違いがいくら存在したところで，「その言語を使って表現できること」に違いが現れるわけではない。このような違いから，各々の言語に優劣を付けることは難しい。
Hayes 氏によれば，ほぼ全てのプログラミング言語は，その文法的骨格として文脈自由文法 [Wikipedia1] を用いており，なおかつ，意味論（セマンティクス）のレベルにおいては皆同じような能力を有している。これは， C や Pascal のような同族の言語はもちろん，オブジェクト指向型言語，関数型言語，宣言型言語，等々にも同様に見られる普遍的な属性であるとされる。
結局のところ，プログラミング言語によって表現される「プログラムの意味」に注目する限りでは，ある言語において表現可能なものが，他の言語において表現不可能であるということは，まず無い。ただ，それをどのような視点によって捉えるのか，どのような記述によって表現するのか，という部分において差異を生じる。その差異が，ある特定の問題領域における問題の扱いやすさを左右するということは有り得る。
しかし，あらゆる問題領域に適した究極の言語というものは存在し得ない。そのような言語が存在したらなば，ここまで多様性を生じることは無かったのではないだろうか。そのような言語が存在し得ないからこそ，次々と現れる新たな問題領域に対して新たな言語が考案され，そしていつかは廃れていくことになるのではないだろうか。
ところで，言語学者 Edward Sapir と Benjamin Lee Whorf の仮説（サピア・ウォーフの仮説）によれば，人間の思考や行動は，その人間の用いる言語に影響を受けるとされる [Wikipedia2] 。この仮説は，言語学においては懐疑的に扱われることが多いが，プログラミング言語の領域においては適切な言説なのではないかと Hayes 氏は主張する。この辺りの人間的要素については， Ruby の設計思想（あるいは "Ruby = Babel-17" 説）に興味深い示唆が含まれている [Matz1] [Matz2] 。
[via Lambda the Ultimate]
2006-06-24
循環小数 0.999... は 1 に等しい。これを説明する方法は幾通りもある [Wikipedia1] 。しかし何故か，この等式をどうしても受け入れることのできない人々が存在する。そういった人々に対して，この等式をどうしても受け入れさせようとする人々も存在する。 Polymathematics の記事 "No, I'm Sorry, It Does." は，この等式の捉え方を簡潔に表した記事だったが，結局，不毛な水掛け論がコメント欄において展開される始末となってしまった。
Polymathematics: "No, I'm Sorry, It Does", "The Saga Continues", "Refutations".
コメントの中には「とんでもないもの」も存在する。 Good Math, Bad Math の MarkCC 氏による指摘は皮肉と冷笑に満ちているが，そうしたくなる気持ちは理解できる。
Good Math, Bad Math: "Good Math, Repeating Decimals, and Bad Math", "The Stupidity of Numerology, illustrated by Infinite Sequences".
ゼノンのパラドクス [Wikipedia2] に似て，無限の概念の捉え難さをよく表している。自分には，これを全力で否定しようとする人を説き伏せる自信は無い。
2006-06-30
……私の娘たちは，もう何学期も化学を学んでいるし，微分法や積分法も習得済みなのだが，今日に至ってもなぜ x y = y x が真になるのかを知らずにいるのだ。 ― ランダウ (Edmund Landau) [metamath]
例えば実数の場合ならば，実数の乗算は交換法則を満たすから， x y = y x は常に真となる [Wikipedia] 。しかし，なぜそうなのだろう？ それは，誰か賢明な先人が，そうあるべきと決めたからに違いない。天下り的ではあるが，それを受け入れて困ることは無いのだから，拒む道理は無い。
しかし，もし「受け入れて困ることがある」としたら，話は違ってくる。例えば 19 世紀末にカントール (Georg Cantor) によって創唱された集合論（素朴集合論） [Wikipedia] は，様々な数学分野を包摂する強力な理論として認められるようになるが，その一方で，幾つかの矛盾やパラドックスが存在することも明らかになってくる。様々な数学の基礎となるべき理論の中に矛盾が存在するという事実は，当時の数学者にとっては，数学全体への信頼をも揺るがしかねない事件として受け止められることになる。
このような「数学の危機」を回避すべく，数学者たちは形式化への道を歩み始めることになる。すなわち，注意深く選ばれた公理系を出発点として，推論規則の適用を繰り返すことによって，様々な命題の正しさを形式的に確かめるという試みを推し進めていく。
このような試みは，フレーゲ (Gottlob Frege) [Wikipedia] による数理論理学の構築に始まり，ラッセル (Bertrand Russell) [Wikipedia] による数学基礎理論の探求，ツェルメロ (Ernst Zermelo) [Wikipedia] による集合論の公理化，等々のように推し進められていき，最終的にはヒルベルト (David Hilbert) [Wikipedia] によるヒルベルト・プログラム [Wikipedia] のような壮大な構想にまで至ることになる。
何人も，カントールの創り出した楽園から我々を追い出すことはできない。 ― ヒルベルト [Wikiquote]
形式的体系においては，あらゆる命題の証明が単純な公理の積み重ねによって成り立っている。これらの公理には，例えば「x = y かつ x ∈ z ならば y ∈ z である」（外延性の公理） [MathWorld] のようなものや，「F と F ⇒ G から G が導かれる」（分離規則） [MathWorld] のようなものが含まれる。このような非常に単純な公理であっても，延々と（しかし有限回の）推論を繰り返すことによって，あらゆる数学の理論を導き出すことができると考えられていた。
しかしその試みは，尋常ならざる困難さを伴うものであったらしい。例えば，ラッセルによる大書 Principia Mathematica （「数学原理」）をミシガン大学の数学史コレクションから覗いてみると，これが常軌を逸した内容であることが分かる。
Principia mathematica Volume1, Volume2, Volume3. (University of Michigan Historical Math Collection)
全 3 巻，計 1,900 ページ余りにも及ぶ大書でありながら，この書物でカバーすることができたのは，集合，基数，順序数，実数までの理論にしか過ぎない。実数から展開される諸理論（実解析）には触れることができていない。また，当初は第 4 巻において幾何学の基礎を扱うことが構想されていたが，第 3 巻が完成した時点で著者は知的枯渇を認めざるを得ない状況にまで追い込まれていたとされる [Wikipedia] 。
第 1 巻の 379 ページに，次のような記述を見つけることができる。
「この命題より，算術加算が定義されるとき， 1+1=2 が導かれる。」
379 ページを費やした末に，ようやく辿り着くことのできた証明が "1+1=2" とは！ もはや数学の深遠さなどを通り越して滑稽さすら覚えかねない。その 3 ページ後には，「つまり 0 でも 1 でも 2 でもないあらゆる基数は 3 以上であることが導かれる」との記述が見られる。この調子では，実数にまで辿り着くには相当な紙面が必要とされるに違いない。
ブルバキ (Bourbaki) は，数 "1" の定義が数万の記号に達することを示唆している。我々は，これが相当な過小評価であることと，本当の記号の数は 4,523,659,424,929 個に達することを示す。この数に 1,179,618,517,981 個の結合は含まれていない。 ― マティアス (A. R. D. Mathias) [Mathias]
結局，このように数学を形式的な体系として捉えなおすという試みは，原理的には可能であるとしても，実現性に乏しいということが明らかになってくる。また，形式化によって矛盾の無い体系を創り出すことができるであろうという確信も，ゲーデル (Kurt Gödel) [Wikipedia] によって打ち砕かれることになる。かくして 19 世紀後半から 20 世紀初頭にかけて華開いた純粋数学の探求は，より実用を意識した応用数学の探求へと推移していくことになる。
以来，厳密な意味での形式的体系の構築は流行らなくなってしまったが，現在はコンピューターを利用してこれをデータベース化しようという試みが行われている [Metamath] 。データベースの形であるがゆえに検索性に優れ，効率的な相互参照が可能であるという点と，ソフトウェアによる証明の確認が行われているという点は，形式的体系の有り様に新たな意味を与え得るように思われる。例えば，冒頭の交換法則の例であれば， [Metamath] へのリンクを示したうえで次のように言い逃れることができる： 「ZFC 公理系に拠る限り，実数の乗算は交換法則を満たす。証明はリンク先の通りである。」
参考文献
文中のリンクの他に以下の文献を参考にした。