研究課題
基盤研究(C)
実数や無限リストなどをコンピュータ上で扱う際に必要になる技術の基礎研究を行った。そのようなデータを扱うプログラムは潜在的に停止しない関数を用いることが多く、遅延評価と呼ばれる特殊な計算方法が必要となる。本研究はプログラムを変形することで、多くの場合、最左最外書換えと呼ばれる単純な計算方法で遅延評価が可能になることを示した。またプログラムの実行の安全性を保証するためには遅延評価が停止性を持つこと(有限ステップで計算を終えること)を証明する必要があるが、それを自動的に行う手法を開発した。
計算モデル
本研究において遅延評価の実現方法とその停止性(正規化性)を解析する枠組み・手法を構築した。遅延評価は関数型プログラミング言語のみならず、数学的な定理を証明する定理証明支援システムにおいても採用されている。実数や無限列などの数学的構造を扱う上で必須の技術であり、本研究はそれらをより良く扱うための計算・演繹機構の理論基盤、より良い自動化の枠組みを与えるための技術基盤の確立に貢献する。