項書き換え理論，証明論，及びそれらの計算量理論における未解決問題への応用

定義される関数の計算時間量との密接な対応関係から，項書き換えシステムの複雑さは典型的には書き換え列の長さにより測られる．ボローニャ大学 M. Avanzini 博士，インスブルック大学 G. Moser 准教授との共同研究で項書き換えシステムに対する多項式級の解析法及び多項式時間計算可能関数に対する新しい特徴付けを開発した．関数の計算時間量と項書き換えシステムの複雑さの間に密接な対応関係がある一方で木構造上のような一般化された再帰原理を表現する項書き換えシステムについては，書き換え列の長さの最小上界が定義される関数の計算時間量の最小上界とは必ずしもならない．正確な対応関係を得るために U. Dal Lago らによって考案された「展開グラフ書き換え規則」という無限グラフ書き換えシステムの概念を抽象化し，昨年度に開発を開始した無限グラフ書き換えシステムに対する多項式級の解析法を論文にまとめ上げた．項書き換えシステムは非決定的な計算モデルなので書き換え列の長さに多項式的上界が存在する場合でも，入力項を根として全ての可能な書き換え列からなる導出木のサイズは指数的になりうる．この理由により項書き換えシステム自身の複雑さと停止性証明の間には指数的なギャップが存在し，そのギャップが解消しうるのか否かは明らかでなかった．プログラム意味論で知られている不動点解釈の概念を援用し，導出木の代替物として適当な不動点を弱い形式体系内で近似的に構成することにより制限的な条件下では指数的なギャップが解消できることを証明した．その例として項書き換えシステム，形式体系，及び多項式領域計算量を関連づけることに成功した．

定義される関数の計算時間量との密接な対応関係から，項書き換えシステムの複雑さは典型的には書き換え列の長さにより測られる．ボローニャ大学 M. Avanzini 博士，インスブルック大学 G. Moser 准教授との共同研究で項書き換えシステムに対する多項式級の解析法及び多項式時間計算可能関数に対する新しい特徴付けを開発した．関数の計算時間量と項書き換えシステムの複雑さの間に密接な対応関係がある一方で木構造上のような一般化された再帰原理を表現する項書き換えシステムについては，書き換え列の長さの最小上界が定義される関数の計算時間量の最小上界とは必ずしもならない．正確な対応関係を得るために U. Dal Lago らによって考案された「展開グラフ書き換え規則」という無限グラフ書き換えシステムの概念を抽象化し，昨年度に開発を開始した無限グラフ書き換えシステムに対する多項式級の解析法を論文にまとめ上げた．項書き換えシステムは非決定的な計算モデルなので書き換え列の長さに多項式的上界が存在する場合でも，入力項を根として全ての可能な書き換え列からなる導出木のサイズは指数的になりうる．この理由により項書き換えシステム自身の複雑さと停止性証明の間には指数的なギャップが存在し，そのギャップが解消しうるのか否かは明らかでなかった．プログラム意味論で知られている不動点解釈の概念を援用し，導出木の代替物として適当な不動点を弱い形式体系内で近似的に構成することにより制限的な条件下では指数的なギャップが解消できることを証明した．その例として項書き換えシステム，形式体系，及び多項式領域計算量を関連づけることに成功した．