紹介文(2008年)

■龍田真 情報学プリンシプル研究系 教授

【タイトル】
型理論の真理を極めてプログラムに反映させる

【本文】
  多くのプログラミング言語では、データや関数がさまざまな「型」を持っています。このよう
な型の理論を抽象化して、数理論理学の「型理論」を用いて分析すると、自動的に型を推論でき
るようになります。推論が失敗すればエラーになるので、誤った型を用いることによるバグが回
避できるようにもなります。私は「型理論」を研究しており、プログラミング言語と計算の中に
ある数学的真実についての理解を深めることを、第一の目的としています。一方で型理論を究め
れば、それを基盤とするプログラミング言語の設計や、誤りのないプログラミングを実現すると
いう実用的な貢献ができるようになります。

プログラミングの誤りを検出し質を向上
  今日、社会のあらゆる場面にプログラムが用いられています。金融やロケットなど大規模で複
雑化したシステムもコンピューターで制御されていますが、その最大の問題はプログラムを人手
で書かざるをえないという点です。自動車のような工業製品の製造は機械化されていますから、
大量に均一で質の高いものをつくり出すことができますが、人手によるプログラムの場合には量
産ができず、質も一律に向上させることはできません。そこで型理論を用いて、誤りのないもの
に仕上げていくことが有用になるのです。
  最近のプログラミング言語の多くには、型理論が弱い形で組み込まれており、ある程度まで自
動的に誤りを見つけ出す機構が入っています。計算する対象や計算する機械が複雑になるのにし
たがって、プログラミング言語自身を発展させていくという方向があります。もう1 つ、自動的
にはチェックしきれない部分には、人手で数学的に誤りがないことを証明しようという方向が模
索されています。

22 問の未解決問題のうちの1つの解決に成功
  いずれの方向でもコンピューターサイエンスにおける型理論の重要性が高まっており、世界中
で広く研究が進められています。型理論自体には70 年余りの歴史があり、プログラミング言語に
応用されるようになってからも50 年近く経ちますが、なお多くの未解決の問題があります。数年
前に重要かつ困難な未解決問題として22 題リストアップされたうち、私は2007 年に20 番目の
問題を解くことに成功しました。他の問題はまだ解かれていないので、現時点では“世界一”と
言えるかもしれません。
  実用面の成果ではこれまでに、高レベルの仕様を基に正しいプログラムだけを自動的に生成す
る「プログラム合成」という技術の基盤の1つとなる理論を構築しました。仕様を論理式に見立
ててそれに対して証明を書くことで、仕様に合ったプログラムができるという仕組みになってい
ます。
  型理論は切りがないほど奥が深く、理論的に深みのある分野なので、数学的な真実を探ること
にはおもしろさがあります。同時に、研究成果をプログラム言語やバグの除去といった実用面に
すぐに反映させられることも楽しみです。大規模、高品質のプログラムの実現に生かしていける
よう、計算理論の美しさを究めていきたいと思っています。(取材・構成 塚崎朝子)