圏論の言葉でナゾ解きし、理論研究に生かす
計算機システムの「安心・安全」研究のために

　「プログラミング言語で書かれたプログラムの意味をきちんと調べたら、そのプログラムが抱えている問題点が見えてくるかもしれない。そんなところにメスを入れたいのです」。角谷助教が攻めているのは、既存のプログラミング言語などが内包している問題のナゾ解きをし、パズルが解けて答えがわかったら、それを新しい理論研究などに活用しようというのが狙いなのだ。具体的には、圏論（Category Theory）という数学的な言葉で記述することによって、別々に行われていたものを共通の枠組みで扱い、解決の道を探ろうというのだ。

圏論への翻訳の壁、乗り越える策を探る

　角谷助教は、萩谷研究室のメンバー。研究室のキャッチフレーズの1つは『安心と安全』である。この安心と安全研究のもとで、論理学をベースに新しい計算モデルの提案、各種計算モデルの解析や検証、そのためのツールの設計と実装などを行っている。その中で、主として計算機システム、ソフトウエア、プログラミング言語などの安全性を保証する「安心と安全」の研究が角谷助教の中心と言ってよい。「私の研究は、クリエイティブな感じに見えないかもしれませんが」と謙遜するが、そうではなく、過去に生まれたものに光を当てることによって、あまりわかっていなかったこと、見過ごされていたことを発見する重要な研究なのだ。

　といっても、単に光を当てるだけではない。たとえば、誰かが開発したプログラミング言語を圏論で見直し、その一部にとてもユニークな視点に基づくアイデアが盛り込まれていたり、ちょっとした矛盾が含まれていたことがわかったとしよう。新しいアイデアの場合は、もっと掘り下げ、自らの新たな感性を投じて独自のものに仕上げる道につなぐ。一方、矛盾の内容が悪影響をもたらしそうな可能性があると判断すれば、改善を提案し、よりよいものしていく。つまり、プログラミング言語の安心・安全を裏付けるものになる、重要な意味を持つ研究である。

※画面をクリックして拡大画像をご覧下さい

　圏論は数学的構造と、その間の関係を扱う数学理論の1つ。数学の多くの分野だけでなく、計算機科学、数理物理学などの領域でも使われている。そこで、計算というものを圏論のフレームワークで説明し直すとか、書き下ろすことができれば、別々に書かれている理論を1つの言語で書くことが可能になる。わかりやすく言い換えれば「英語を使って話している人と、フランス語でしゃべっている人とかが、共通の言葉で話し合えば、すぐにコミュニケーションが取れるようになるでしょう」。角谷助教は、共通の世界語として圏論を取り上げ、その枠組みの中で統一的に扱う方法を模索している。その1つの対象としてプログラミング言語を取り上げているのだ。

圏論の分野で使われる 標準的な教科書

　ところが問題がある。プログラミング言語などを圏論の言葉で翻訳するのがむずかしいことだ。圏論の言葉で書き直せば、その中身を評価できるのはわかっているのだが、圏論の言葉でどのように書くか、その約束事がまだ固まっていない。「それを見つけられれば、そのあとは何とかなる」という。したがって、角谷助教の当面の研究は、圏論という言葉でいかに切り込んでいくか、その切り口を見いだすことにありそうだ。

　また、圏論研究に関連して行っているのは、双対性の研究である。2つのものを重ね合わせると、両方が鏡のように重なる状態のことを指す。2つのプログラミング言語が一見して違って見えても、それらを圏論に翻訳してみると、ピッタリ重なることがある。このため、まったく違ったアプローチで研究、開発されたプログラミング言語が実は同じだったということが双対性を見ることで明らかにできる。中身を検証することによって、プログラミング言語の優劣や、技術の有効性の判断などが可能になるのだ。

量子計算研究にも白羽の矢

　京都大学理学部数学科出身ながら、卒業研究は計算機科学を選択した。数学の中の計算機の位置づけは何かという点に興味を覚え、数理解析研究所に進んだときも、やはり計算機科学をメーンに研究した。「数学と計算機の両方をまたぐ研究」を推進し、5年前に現在の東大情報理工のコンピュータ科学専攻へ転身した。そしていま、圏論研究とともに、量子計算プログラミング研究に着手している。目的は「計算の本質を知りたくて」

　量子コンピュータをつくるにはどうしたらいいか、量子コンピュータを安定して動かすにはどのようなアプローチがあるのかといった、量子コンピュータが次世代研究として展開されている。こうしたなか、角谷助教は、量子計算が目指している抽象的な計算とはどういうものか、普通の計算とどのように違うのかを知りたいという。そのために温めているアイデアは、圏論研究の手法といっていいかもしれない。量子計算で行う計算方法と、普通に行われている計算をつなぎ合わせて1つの手法として確立すること、あるいは、複数の分野にまたがっていることを1つの枠組みで同じように使い合うことである。理論研究を通して新しい発見をしたい―角谷助教のフレッシュな可能性が大きく胎動し始めている。

角谷助教
萩谷研究室