歴代受賞者一覧

受賞者紹介

外山　芳人(とやま・よしひと）
昭和27年10月30日生まれ
北陸先端科学技術大学院大学情報科学研究科　教授

贈賞の理由

項書き換えシステムのモジュラ性の研究

項書き換えシステムは、方向付けられた等式（書き換え規則）の集合として定義される計算システムである。等式を、複雑な式から単純な式への非可逆な一方向の書き換え規則とみなすと、等式で記述された論理の世界を自然な形で計算の世界に結びつけることができる。このようなシステムは、定理自動証明、代数的仕様記述、関数型プログラミング言語の意味論など、さまざまな分野で広く利用され、1980年代以降は、計算機科学の重要な研究分野として認められている。

外山教授は1980年代初頭から項書き換えシステムの研究に取り組み、特に項書き換えシステムのモジュラ性に関して、優れた成果を上げてきた。すなわち、直和のもとでのモジュラ性という概念を初めて導入することにより、従来まったく知られていなかったモジュラ解析の可能性と有効性を明らかにした。

ある性質Pがモジュラであるとは、2つの項書き換えシステムがそれぞれPを満たすとき、その直和システムも性質Pを満たすということである。したがって、Pがモジュラならば、複雑な項書き換えシステムをより単純なシステムに分解し、それぞれのシステムが性質Pを持つことを示すことで、複雑なシステム全体の性質を示すことが可能となる。

同教授は、まず項書き換えシステムのもっとも重要な性質である、チャーチ・ロッサ性がモジュラであることを明らかにした。この結果は古典的定理として現在広く文献に引用されており、しばしば「Toyama's Theorem」と呼ばれている。この結果を用いることにより、チャーチ・ロッサ性の解析手法の限界を打ち破ることが可能となった。一方、直和にもとづくモジュラ性は、必ずしも自明なものではなく、もう一つの重要な性質である停止性がモジュラであるかが問題となった。ここでも同教授は、大方の予想に反して、停止性が直和によっては保存されないことを、非常に巧妙な反例を用いて示した。

以上の外山教授によるモジュラ性の研究は、着想のオリジナリティと数学的な美しさから、10年を経た現在でも多くの研究者を引き付け、関連する分野の研究を大きく発展させる基礎となっており、計算機科学の重要な成果として高く評価される。

上に戻る

※所属名および役職は、受賞時のものです。