λ計算の動機

English version

λ計算は Churchさんと Kleene さんが 1930 年代にこれを考えたと Wikipedia (日本語 ) にはある．彼らは最初これを数学の基礎を築こうとして考えたとある．

ところで私は素人なのであまりここに書いていることを鵜呑みにしないようにお願いする．これは私が理解する限りにおいての話である．この blog の元ネタはWikipedia である．かっこ良く言えば，Wikipedia に inspire されて書いているのである．もし，あなたがこの Wikipedia の Page の内容をわかってしまったのであればこの blog よりももっと面白いものは沢山あるのでそちらをおすすめする．たとえば，「数学の基礎を築こうとしてλ計算は考えられた」で「なるほど，そうかそうか」，と思う人はこの blog を読む必要はない．しかし，「1930 年というと数学の歴史からするとかなり最近のことだ．どうしてこの時に数学の基礎なんてものを考えようとしたのだろう．いったい数学の基礎というのはなんなのだろう．ピタゴラスやアポロニウス，ユークリッドとかが数学の基礎を作ったりしたのではないのだろうか」とか思うのであればもう少し読んでもいいかもしれない．

数学の基礎というのは数学はどこから出発できるかということと，どういう出発ならば問題がないかという疑問に端を発っする．数学はある定義から出発する．これは人が決めるものである．まず，数学で最も基本的なものは何かと言うと数であろう．他にはある「命題」が真とか偽とかいう論理や，計算とは何かとかいうものも基本的である．こういうものはあまりにあたりまえすぎてかなり後の時代になるまで注目されなかった．

しかし，あたりまえのことに注目してどうするというのだろうか．数学者達はこの時，形式化ということについて考えるようになっていた．あたりまえに思える数であるが，たとえば，それは言語によって違うのかもしれない．日本語での 1と英語の 1 は本当に同じものだろうか? そこで数というものから定義しなおすことを考えた．ところで数を定義する時には数は使えない．もし使えると，「数とは数である」と書けば良くなってしまうからである．「愛とは愛である」「自意識とは自意識を自意識できるものである．」は真かもしれないが，こういう定義では数学の基礎としては使えないのである．数というものを数を使わないで定義できるのか? ここまでくると数学者は偏執狂かという感まである．

私がこの考えを面白いと思うのは，これが十分に形式化されているので，機械でそれを作って実行できるという点である．計算する機械を作ろうとすると，それをなんとかして物質(鉄とか水とか石とか)で作らなくてはいけない．Zaphod ならば 2つの頭で「わかるだろう，1 とか 2 とか 3 だよ，そういうのをとりあえず計算してみせる機械をちゃちゃっと作ってみてくれよ」と言うかもしれないが，どうやって 1 とか2を示せば良いのだろうか．数というのは驚くほど抽象化された概念である．抽象化されているというのは，非常に応用範囲が広いということである．「地球と人間とパンと信号機とZaphodの頭と教会の共通点は?」という問いに，「どれも数えられるものだ」という答えは正しい．繰り返しになるが，私には数をどうやって子供に教えたら良いのか見当がつかないのである．これは高度に抽象化された考えである．

λ計算の動機は数学の基礎を築くためにあった．というのは，それまであたりまえと考えられていた数や計算を形式化して1から考え直すということであったのだ．当時の数学者には数学のシステムの正しさを単純なルールだけで示すことが目的であったようだが，このルールは十分単純化されており，機械でも作れる．私がλ計算に興味を持ったのはこの「機械としても作れる」という所である．λ計算が現代の計算機言語の基礎理論の一つであるのはそういうわけである．

次回は数(自然数)を 1, 2, 3 などを使わずに定義してみよう．

λへの導入

English version

標準的な数学の本ではある数学的ことがらを説明するのに，定義，定理，証明，定義，定理，証明，，，のように話が進んでいく．そのようにすると話は(ある意味)すっきりするし，数学の抽象化というものが上手く働く．だからλ計算に関してもそのように話をすすめるのが標準なのだが，マービンに言わせればそれほど気が滅入ることはないだろう．抽象化されたものは応用が利くし，余計なことを言わないので単純さと美しさがある．つまり，的を射ているのである．

日本の刀 はその美しさを刃に求め，余計な宝石で飾ったりしない．美しさはそのもの本質を追及することにあると考えるからである．美術館には刀や杖を宝石で飾りたてたものが多くある．そこに豪華な美を見ることも私にはできるが，本質と美しさを単純さの中に求めたものにも私は美を感じる．ある飛行機乗りが「全ての不要なものを取り去った時，完全性が達成される」と言ったという話を聞くと共感できるものである．そしてかつてスウェーデンの海に沈んだ Vasa の話は私のお気に入りの一つでもある．(これはプロジェクトマネージャーの王様が機能拡張を要求しすぎた例である．シリウスサイバネティクスのソフトウェアは顧客が欲しいとマネージャが思った機能を追加しすぎて使いものにならなくなったソフトが多い．顧客は単に機能縮小しても，安定したソフトが欲しかったりする．(Kode Vicious Pride and Prejudice (The Vasa) CASM Vol.51, No.9 ))

数学の美しさはその抽象性と単純さにある．だから余計な背景や説明を除いてそのものだけを論じたくなるのはよくわかる．しかし，それはわかる人にはわかるということである．私はここにちょっとした排他性を見る．

あるものの側面に，ああ，美しいなということを発見することはとても嬉しいことである．そして時にそれを独り占めしたくなるのも人情かもしれない．広く知られることによって大衆化して，皆が知っていると寂しく感じるということもあるのかもしれない．ある数学を愛する人は数学をますます純化し，抽象化してその美しさを求めてしまうかもしれない．しかしそうなったものは本当にその的だけになってしまい，その背景にあったものや歴史を捨ててしまう．それは本質なのだから，それでいいのかもしれないが，親しみがなくなってしまう．わかった気にならないのである．

そうやって捨てられてしまったものも，私は気になってしまう性質である．なんでλなんてものを考えるのか，ということはこの体系ができてしまった後ではそんなに重要ではないかもしれない．λに何ができるかというのが結局より本質的なことである．数学ではそれそのものよりも，それが何ができるかの方が重要である．

ガイドのボゴン人のビジネスはまったくドライである．相手が何ができるかということこそが重要であって，それが誰かということはまったくどうでも良い．いや，彼らには親戚関係だって単なる関係でしかない．おばあちゃんが助けを求めても，孫たちは契約書がなければ指一本動かさないのである．ドライな会社のようなものである．新しい機能を実装できるかどうかが従業員に求められているものの全てである．もちろんそれこそがビジネスには重要なことではあるのだが，それを行う人間はある意味本質ではなく，どうでも良いのである．その会社の誰かがそれをできれば，誰がやってもかまわない．するとそれは誰がやったかという意味がなくなる．通常は会社の機能としか見られない．ただし，人間の場合には，あんまりそうなるとそこでの働きがいがなくなってしまい，そういう会社は人材を失い，最後には機能も失うことが多い．

ラムダに何ができるかが重要であって本質であることは確かだが，ここでは余計なことを述べてみよう．まず，どうしてλなんてものを考えようと思ったかである．λだって人間の考えたものであるから，何か動機があるはずである．マービンもあれほど気が滅入っている存在は宇宙にはないほどであるが，そういうものを作りたくて作ったのではなかった．単に天才を何百人集めたら大天才になるだろうという考えで設計されたのだ．しかし，何百人分もの天才が集った脳が正気であるという保証はなかったこととか，天才はえてして紙一重であるという古くからの知恵を無視してしまった結果であった．λもある目的のために考えられた，それが後から見ていかに変であっても，目的自身はそんなに難しいものではなかった．次回はλの動機について書いてみよう．

realtime raytracing als 4k demo

私は CG の仕事をしているので，その話も時々しましょう．

これは最近同僚に教えてもらったリアルタイムレイトレーシング，フォトンマップでのコースティック付きデモです．私のマシンでは非力でデモを実行できませんが， 4K バイトのプログラムが，リアルタイムで caustics を見せてくれると驚きです．残念ながらコードは非公開のようです．

映画なんかでリアルに見える画像は1フレーム8時間とかかったりします．ですから1秒の映像を作るのには 8 日とかかかります．(でも私の会社のお客さんはrender farm と言う 1000 台位の計算機を並べているので，8 時間待てば1000 枚画像ができます．) そういうのに比べてこれはそのままビデオにとれるのがすごいですね．YouTube に行けばもっと高画質な画像もあります．

http://www.youtube.com/watch?v=LWx2HjvFzHw
http://www.pouet.net/prod.php?which=51443