2011年04月25日

「形から入る」平井 洋一

[質問]
僕のいる萩谷研というところは、後輩が「『イデア』のようなものを、機械に組み込む」と言ったり、別の後輩が初対面で「数学的実在を信じますか?」と質問してきたり、たいへんおもしろいところです。このエッセーも彼らに書かせたほうが楽しいかもしれません。学部では情報科学科というところで、大学院ではコンピュータ科学専攻というところです。

[期待]
大学の学科を選ぶときに考えたことは、法律をやっても人間のことしか相手にできないし、生物をやっても地球の表面のことしかわからないし、化学や物理をやってもこの宇宙のことしかわからない、ということでした。では数学はというと、あるのかないのかよくわからないものの話をしていて、数学者にしか話が通じなくなると思いました。ここで情報科学という抜け道があって、記号列さえあれば、この宇宙に限らずどこでも成り立つことを研究できますし、あるのかないのか疑われたら計算機の中に作ってみせてやればいいのです。しかも、役に立つか立たないか聞かれたときの答え方も比較的かんたんで、裏では数学をやっていながら、表ではソフトウェアを作るためのソフトウェアを作るための道具ですよと言ってお澄まししていればいいのです。もちろん物理や化学で説明できる現象も数学に従っているのは同じかもしれないけれど、その数学を勝手に変えるのには熟練の技が必要です。その点計算機の中で動くものは、もともと数学に合わせて人手で作ったものだから、数学を変えても変えた数学に合わせてつくり直すのは、物理や化学に比べれば簡単です。

[幻滅]
そういう目論見で情報科学科に行ってみたのですが、数学の果たしている役割が思ったよりも小さくてがっかりしました。たぶん数学者が細かいところまで証明を書き込まないのがいけないと思うのですが、数学ができていても、それを計算機に載せるところで間違いが出ます。そこで数学とはかかわりなくソフトウェアを作ってみて動いたとか動かなかったとか言って、動かなかったら動くまで直して、不具合を見つけられなくなったらそれで満足してしまう人も多いのです。ソフトウェアの動きは数学的に定義できるはずなのに、調子が悪いとか不具合であるとか不思議なことを言っているのが気に入りません。

[作戦]
コンピュータ科学専攻なのに、新入生が数学的実在の有無について先輩を詰問するのはなぜかというと、萩谷研というところが論理学を標榜しているからです(さいきんでは分子計算もやっているそうです)。数学ではなく論理学まで身を低くすれば、人間が理解するための証明ではなくて、機械が読んで機械がチェックするための証明について研究することもできます。数学者にとっての理想の証明は人間が理解するためのものですから、機械が読むには適しません。数学者が避けたがるような、冗長で微に入り細を穿つ証明を機械に読ませてチェックさせ、その微に入り細を穿った証明からソフトウェアを取り出して動かせば、ソフトウェアの動きを数学的に定義できた旨みが生きてくるに違いないと考えて、そういうことをしています。

[答え]
イデアというのもあるのか無いのかわからないし、数学的実在もあるのかないのかわからないです。あるのかないのかわからないので、あってもなくても良いように、とりあえず、目の前にある記号列のことを考えて暮らしています。