第19回 日本IBM科学賞 コンピューター・サイエンス部門

計算の意味論とプログラミング言語の理論の研究

長谷川氏の計算の意味論における業績は、優れた独創性と数学的な深みをもち、計算とプログラミングの理論における大きな進歩であると同時に、ソフトウェア科学における新しい展開をもたらすブレークスルーであり、大きなインパクトを学会にもたらした。

ソフトウェアの安全性は、情報社会では最重要の要素である。ウィルスワクチンソフトの更新時に多くのコンピュータが作動しなくなるなど、ソフトウェアの設計や変更の不具合により生じた予期せぬトラブルは数多く報道されており、そこから派生する深刻な社会破綻を防ぐための技術の重要性が広く認知されている。

ソフトウェア設計における予期せぬトラブルを防ぐためにはプログラムや計算の意味の解析が重要であり、そのための基礎理論である意味論はコンピュータ科学の根本にあると同時に情報社会の安全性のための必須事項である。数学的に堅固な意味論のモデル構築においては、現代数学の先端理論であるカテゴリ理論を用いた多くの成果が得られている。しかしながら近年、ソフトウェアの進歩につれ、プロセスや計算結果の柔軟な共有、さらに非決定性を持つプロセスの利用が広く行われるようになった。このため、従来の理論ではモデル構築が困難となっており、先進的なソフトウェア設計においては堅固な意味論を欠いた状態で研究が行われ、大きな問題となっていた。

長谷川氏は共有構造と循環構造を包含するプログラムにおける厳密な意味論を世界に先駆けて与え(1999年)、上記の状況を打ち破った。これにより、意味論が扱える計算の対象は格段に広げられた。具体的には、共有グラフに関する深い洞察にもとづき、従来理論の舞台であるカルテジアンカテゴリ(直積を持つカテゴリ)よりも自由な数学世界であるモノイダルカテゴリ(テンソル積を持つカテゴリ)の上で意味論のモデルを構築し、グラフ書換え理論を厳密に定式化する事により共有計算の意味を記述する事を可能にしている。

この成果は計算の意味論や変換論における分野開拓と活性化を誘導し、国際的に多くの新たな研究成果を呼んでいる。長谷川氏はその中心となり、より複雑な副作用を扱うモデルの分析やλμ計算におけるパラメトリシティー理論など重要な貢献を続けている。

以上のように、長谷川氏の業績は安全なソフトウェアの設計理論体系に多大な貢献をもたらすものであり、日本IBM科学賞にふさわしいものである。

上に戻る