今日はロビン・ミルナーの誕生日(1934)
さっき調べるまで、僕はこの人のことを全然知りませんでした。すみません。
というか、この人の業績分野に全然詳しくない。ただ、重要であることはわかります。
そこで、今回は資料首っ引きで、理解できた範囲で解説する形でお伝えします（笑）
彼は 1972年に、LCF (Logic for Computable Functions)という名前の、「自動定理証明」プログラムを作っています。
…まず、定理、って言葉を解説する必要があるでしょうね。
数学では、最初にその数学が成り立つ条件を「仮定」します。
あくまでも仮定ね。違う仮定だってあるかもしれない。
この仮定のことを「公理」と呼びます。
たとえば、「２つの点を結ぶ直線は、１つだけ存在する」というのは一般的な幾何学（ユークリッド幾何学）の公理です。
普通、図形を扱う場合にはユークリッド幾何学が使われますので、この仮定の上にすべてが成り立っています。
言い換えれば、「２つの点を結ぶ直線は１つ」というのは、必ず正しいです。
ただし、世の中には別の幾何学系と言うものもあり、その系では正しいとは言えないかもしれません。
必ず正しいというのは、あくまでも「仮定」に基づいた話ですから。
なんだか冒頭からややこしそうな話になっていますが、こうした「公理」から導かれ、「公理が正しいとするなら」という前提付で「必ず正しい」とされるものを、定理と言います。
「２つの直線が交差した時、向き合う角の角度は同じである」
というのは、ユークリッド幾何学における定理です。
先に書いたように、公理は「ユークリッド幾何学において」という条件付きで、必ず正しいです。
ですから、その公理から導かれる定理もまた、同じ条件では必ず正しいです。
あー、ややこしい数学の話になってきてしまっていますが、後の話は簡単。
公理から導かれる定理、というのは、あくまでも「絶対正しい」もののはずです。
じゃぁ、いくつかの公理を元に必ず推論できるはず。
どの公理をどのように組み合わせればよいのか、ひたすら組み合わせればいつかは正しい組み合わせに辿りつくはずなので、コンピューターにもできるはずです。
これを「やらせてみる」ためのシステムが、「自動定理証明」。
人工知能研究の一環として、今でも、よりシンプルで美しい証明を導けるシステムを目指した開発が行われています。
ロビン・ミルナーの作った LCF は、こうしたシステムのごく初期のものです。
さて、ミルナーは、LCF を作るにあたって、この「ややこしいシステム」を簡素に書けるためのプログラム言語から設計しました。
当時はプログラム言語も黎明期。科学計算向けの FORTRAN 、ビジネス計算向けの COBOL …など、目的別に違う設計の言語があるのが普通でした。
そして、彼は自動定理証明を行うシステムを書くために、「非常に複雑なシステムをすっきりと書ける」言語を設計したのです。
ここで注意すべきは、LCF 自体が「プログラム言語」である、ということです。
コンピューターに何かを行わせるような、いわゆるプログラムを書くわけではありません。
しかし、いくつかの公理と、証明すべき定理を「記述」する必要がある、という点で、LCF はプログラム言語なのです。
プログラム言語のプログラムを書くためのプログラム言語。
なんとも奇妙な関係ですが、ルミナーはこの言語に「メタ言語」という名前を付けました。
メタ、とは、何かの概念の元となる概念を意味する接頭語です。
言語の元となる言語なので、「メタ言語」…英語では Meta-Language です。
この「メタ言語」は、頭文字をとって ML と呼ばれました。
この ML がプログラム言語としてはなかなか使い勝手の良い言語で、多くの人が亜種を作りました。
しかし、あまり亜種が増えるのも困りもの。ML の「標準」を作ろう、という流れが出来上がります。
そして生み出されたのが Standard ML 。SML として知られる言語です。
この SML は「標準仕様」であり、これをもとに多くの実装が作られています。
ただ、ML の亜種がすべて SML に吸収されていったわけではない。
もう一つ、大きな亜種が育ちました。
Caml という ML の亜種があり、それに Object の機能をもたせた OCaml。
結構人気のある言語だそうです。（僕は使ったことないので伝聞調 (^^; ）
SML、OCaml 共に、いわゆる「関数型言語」と呼ばれるものです。
関数型と手続型（いわゆる、普通の「プログラム言語」）の何が違うのか、というのは宗教論争になりがちなのであまり踏み込みません (^^;;
晩年には並列プログラミングの研究も行っていたそうで、こちらにも重要な功績をいくつも持っているようです。
LCF の開発、ML の開発、並列プログラミングの研究…が、彼の３大功績のようです。
こんな多くの功績がある人ですから、チューリング賞も受賞していますし、多くの大学を渡り歩き、研究所の所長や、計算機科学科の学科長なども務めています。
…にもかかわらず、博士号を持っていません！
今回、彼のことを調べていて一番驚いたのがこのこと。
研究者として大学などに雇ってもらおうと思えば、博士号を持っていることは最低条件…のはずです。一般的には。いや、日本では。
でも、彼は博士号を持っていないのに多くの大学を渡り歩きましたし、所長や学科長も務めたのです。
博士号を持つということは、指導教官が付いたということでもあり、その指導教官の紹介でより「偉い人」に紹介してもらえることを意味します。
彼は、そんな重要な「パイプ」を持っていないにも関わらず、自分で道を切り拓き続けたのです。
…つまり、それは「優秀な人間がいるのであれば、肩書などにこだわらずに地位を与える」という、本当の意味での実力主義、本当の意味での「人を見る目」を持った社会の存在を意味しています。
これ、日本の社会に一番欠けているものではないかな、と思います。
同じテーマの日記(最近の一覧)
関連ページ
ロビン・ミルナー 命日 (2010)【日記 16/03/20】
別年同日の日記
申し訳ありませんが、現在意見投稿をできない状態にしています。 |