| 研究課題/領域番号 |
13J00726
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
江口 直日 千葉大学, 理学研究科, 特別研究員(PD)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
3,960千円 (直接経費: 3,300千円、間接経費: 660千円)
2015年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2014年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2013年度: 1,100千円 (直接経費: 1,100千円)
|
|---|
| キーワード | 項書き換えシステム / 計算量解析 / 多項式時間計算量 / 無限グラフ書き換えシステム / 停止性証明 / 形式体系 / 多項式領域計算量 / 項書き換え理論 / 証明論 / 計算量理論 / グラフ書き換え / 限定算術 / 計算量クラス / 多項式時間 / 停止性順序 |
|---|
| 研究実績の概要 |
定義される関数の計算時間量との密接な対応関係から，項書き換えシステムの複雑さは典型的には書き換え列の長さにより測られる．ボローニャ大学 M. Avanzini 博士，インスブルック大学 G. Moser 准教授との共同研究で項書き換えシステムに対する多項式級の解析法及び多項式時間計算可能関数に対する新しい特徴付けを開発した．関数の計算時間量と項書き換えシステムの複雑さの間に密接な対応関係がある一方で木構造上のような一般化された再帰原理を表現する項書き換えシステムについては，書き換え列の長さの最小上界が定義される関数の計算時間量の最小上界とは必ずしもならない．正確な対応関係を得るために U. Dal Lago らによって考案された「展開グラフ書き換え規則」という無限グラフ書き換えシステムの概念を抽象化し，昨年度に開発を開始した無限グラフ書き換えシステムに対する多項式級の解析法を論文にまとめ上げた．項書き換えシステムは非決定的な計算モデルなので書き換え列の長さに多項式的上界が存在する場合でも，入力項を根として全ての可能な書き換え列からなる導出木のサイズは指数的になりうる．この理由により項書き換えシステム自身の複雑さと停止性証明の間には指数的なギャップが存在し，そのギャップが解消しうるのか否かは明らかでなかった．プログラム意味論で知られている不動点解釈の概念を援用し，導出木の代替物として適当な不動点を弱い形式体系内で近似的に構成することにより制限的な条件下では指数的なギャップが解消できることを証明した．その例として項書き換えシステム，形式体系，及び多項式領域計算量を関連づけることに成功した．
|
| 現在までの達成度 (段落) |
27年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
27年度が最終年度であるため、記入しない。
|
