| 研究概要 |
本研究の目的は, 項書き換え理論や証明論の基礎研究, 及びそうした手法によりP(多項式時間), NP(非決定性多項式時間), PSPACE(多項式領域), EXP(指数時間)等の「計算量クラス」に計算機モデルとは独立な数学的特徴付けを与えることである. またそれにより, 実際的計算可能性について新たな知見を得ることである. 当該年度は研究計画にしたがいUniversity of InnsbruckにてGeorg Moser准教授, Martin Avanzini博士らと共同研究を行い, PとEXUの中間的なクラスであるETIE関数にちょうど対応する停止性順序を考案し, P, ETIME, MXPの三クラスが項書き換え理論の手法により一様に特徴付けられることを示した. また「可述的辞書式経路順序」という停止性順序を考案し, 原始再帰的関数の閉方条件に関する古典的な事実について既知のものより簡明な証明を与えた. それにより項書き換え理論の手法が計算量クラスなどの関数クラスへ応用しうることが一層明らかになった. こうして得られた成果は国際研究会にて報告し, 論文を会議録に投稿した. 証明論的手法による計算量理論へのアプローチとして, 二階限定算術による計算量クラスの特徴付けに取り組んだ. 有限モデル理論によるP, PSPACE等の特徴付けを十分に形式化できる集合存在公理の発見を目指し「不動点公理」(帰納的定義の公理)を二階限定算術上で導入し, そうした特定の公理がPとPSPACEに対して必要であることを示した. 進行中の研究成果は国際研究会で報告した.
|
| 今後の研究の推進方策 |
項書き換え理論の手法によるETIME関数の特徴付けについての結果を深化, 発展させ論文にまとめあげる。証明論による計算量クラスの特徴付けについては, 導入した不動点公理を推敲, 改良し, P, PSPACE等の計算量クラスについて必要性だけでなく十分性も成り立つことを証明する. また項グラフ書き換えの多項式計算解析を構築し, 新井敏康, A. Beckmann, S. Bussらによる実際計算可能な集合開数への応用可能性を調査する. 研究計画にしたがい平成26年9月まではUniversity of lnnsbruckに滞在し, 必要に応じてGeorg Moser准教授らと共同で研究を遂行する.
|
