研究 / Research

型理論の真理を極めてプログラムに反映させる

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

プログラミングの誤りを検出し質を向上

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

22 問の未解決問題のうちの１つの解決に成功

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

PDFをダウンロード