結城浩さんへ
お手紙ありがとうございます。プログラミングの話題がいくつか出ていましたので、今回はそれらに関連したお返事を差し上げたいと思います。
3インチの望遠鏡
『ベーシック圏論』の訳者あとがきでもふれましたが、『Accelerated C++』という教科書があります(K&Rと並んで好きなプログラミングの本です)。この本ではまず具体的で現実的な問題を提示して、それを解決するのに必要な事項を徐々に説明していくというスタイルがとられます。
たとえば「学生の成績をつける」(3.1節)ために、標準テンプレートライブラリ(STL)のvectorの使い方が説明され、後に簡単なvectorの実装を行う(11章)ことで、他のSTLについてもだいたいどのように書かれているか想像できるようになります(なお15章でデザインパターンの例が、そう明記されずに登場します)。この本の序文で、このアプローチについて
3インチ望遠鏡を作ってから6インチのものを作る方が、最初から6インチ望遠鏡を作るよりやさしい
と引用説明がなされますが、“toy model”としてなじみ深いという人もいることでしょう。
『ベーシック圏論』の原著を初めて読んだとき、何となくこのプログラミングの教科書を思い出し、訳してみたいと思ったのでした(もちろん他にも理由はありますが)。『ベーシック圏論』中の(たとえば6.3節中の)いくつかの思考実験は、証明したい定理(この場合、定理6.3.10や定理6.3.20)のtoy modelですが、そもそも『ベーシック圏論』自体が、圏論の教科書(たとえば、マクレーン)のtoy modelと言えるでしょう。
部品を組み合わせる
プログラミングの面白さはいろいろあると思いますが、その中でも『ソフトウェア開発の神話』にある
可動部品を組み合わせて複雑なメカニズムのようなものを作り、それが原理どおりに微妙な周期で動作するのを観察する魅力
というのは、個人的にしっくりきます(現在では、『人月の神話【新装版】』として異なる訳が入手可能)。
一つひとつの部品は他と独立に、約束されたインタフェース通りに振る舞うように実装された動作をしているだけなのに、全体としてはその部品も思いもつかないような機能を果たしている、というのにはロマンがあります。
少し前に線型代数の講義で「講義中に紹介した固有値などの諸概念は、今は何が嬉しいのかわからないかもしれないけれど、『明確な目的を持たないから、逆にいろいろなことに使える』“素材”の役割も果たせるんだよ」ということを、ページランクを例に説明しました。このうち『』の部分は、これまたプログラミングの本の『プログラミング道への招待』から借用したもので、著者の竹内郁雄さんは道(Tao)であると言っています。
ちなみに『ベーシック圏論』の索引に「あひる、125」の項目があるのですが(注:原著にあるからです)、ここが結城さんの言う「インターフェースとインプリメント」の比喩とも読めます。
計算機と同一視
『人類の歴史とAIの未来』に、計算機は物理をシミュレートできる「哲学的な機械」とありました。私は計算機には「有限の範囲で数学をシミュレートして、数学の知見を深めてくれる機械」の側面があると思っています。
たとえば、有限体をプログラムで実装しようとする中で、相等(同一)と同型と自然な同型の違いを明確に意識することもあるでしょう(注:標数pの有限体Fpdは、Fp[x]を既約d次多項式で割って実装できますが、この既約多項式の自然な選択はないと思います。他の人との計算結果を共有しようとするなら、同型(=同一視の方法)を明確にする必要があるでしょう)。
このようにある数学的概念を計算機に“のせる”場合、その概念を「数の塊」としてエンコードする必要があるので(これは『ベーシック圏論』の3.3節と関係があるかもしれません)、逆にその概念が何をどう“coordinate-freeに同一視しているのか”よく理解できることがあると思うのです。
こうしてみると、圏論がどのくらい計算機にのるのか、というのはわれわれの理解度に直結していると思います。たとえば、ストリング図で自然変換を計算するという話が『ベーシック圏論』にさらっと紹介されています(注意2.2.9)。そこで、2つのストリング図が同じ自然変換を表すかどうかを判定する、というのは手頃で需要がある問題だと思います(少なくとも、圏論化された代数の研究に役に立ちます。たとえば、最近ブランダン等が証明したハイゼンベルグ圏論化の論文の、48ページのような計算の補助になるかもしれません)。この問題がそもそもアルゴリズムで決定可能かどうかわかりませんが、研究して(部分的であっても)成果がiPadのアプリにでもなれば、圏の定義を知らない子供でも、ゲーム感覚で自然変換の’‘直観’’を身につけることがあるかもしれません。
計算機と数学
計算機と数学の相互作用に関する例をもう一つ挙げてみます。 最近、博士研究員の方と一緒にナンディの予想というものを解決したのですが、その際にキーとなったのが、私たちが発見した
という恒等式です。これは無限級数の恒等式ですが、q60くらいまでの有限の範囲の展開で打ち切ることで、計算機で発見することができます。q1000でもq100000まででも正しいことをチェックするのは計算機には容易なので、定理が成り立つことを確信することもできます。そして運が良ければ、伝統的な方法で証明することができます(カナデ・ラッセル予想と呼ばれる、もっと簡単な見かけの同じような恒等式があるとおり、いつでも証明できるわけではありません)。
このように無限和が2重和の場合、ありふれたラップトップのコンピュータでもさくさくと探索することができます(ロジャーズ・ラマヌジャン恒等式は、1重和=無限積の形の有名な公式です)。3重和の場合でも、参照の局所性などを考慮しながら注意深くコードすることで、少し高級なXeonマシンを用いればそこそこ満足のいく探索を行えます。ここまでは「原理どおりに微妙な周期で動作するのを観察する魅力」なのですが、4重和になるとなかなか大変です。いまのところこのような4重和の恒等式を二つ“見つけ”たのですが、たしかに「何インチかの望遠鏡」で覗いているような気分になります。
こういった恒等式は、アフィン・リー環という無限次元リー環の表現論と関係しているという期待があるものの(たとえば、『An Invitation to the Rogers-Ramanujan Identities』の5.2節)、まだまだわかっていません。先ほど、計算機は「数学の知見を深めてくれる機械」だと書きましたが、氷山の一角を教えてくれる機械でもあると思います。『A=B―等式証明とコンピュータ』(原著が著者の一人のウェブページで公開されています)にも書かれているとおり、その一角は氷山によって立ち位置が明確になりますが、そもそも一角がなければ氷山に気づくことすら難しいはずです。
チューリングが、実際に完成したチューリング・マシンである計算機でゼータ関数の零点を計算していたというのはよく知られた話です(たとえば『万能コンピュータ:ライプニッツからチューリングへの道すじ』が人物伝的計算機史として印象に残りました)。『Coherence in Three-Dimensional Category Theory』などにある長大な図式を眺めていると、計算機が教えてくれる圏論の氷山の一角もあるのではないかと思えてきます。
おわりに
プログラミングから始まって、今回はあまり圏論と関係ない話になってしまったかもしれません。それでは最後のお手紙をお待ちしています。
追伸
「見なす」ことに価値がある、というのは、見なせること自体が証明を要する非自明な数学的命題である場合がほとんどなのでそうだと思います。実際、教科書に「~であるとしてよい」と一行書いてあるところは、初学者が時間をかけて徹底的に補うべき内容の定番であることが多いです。ただ、一つひとつ「見なす」ことを重ねていくことで、実際に計算しないと示せなさそうな定理が示せるのは、確かに不思議だと思います。