2014 Fiscal Year Annual Research Report
項書き換え理論，証明論，及びそれらの計算量理論における未解決問題への応用
| Project/Area Number |
13J00726
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
江口 直日 千葉大学, 理学研究科, 特別研究員(PD)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 項書き換え理論 / 証明論 / 計算量理論 / グラフ書き換え / 計算量解析 / 限定算術 |
|---|
| Outline of Annual Research Achievements |
項書き換えシステムの複雑さは，定義される関数の時間計算量との関係性より典型的には書き換え列の長さにより測られるが，木構造上のような一般化された再帰原理を表現する書き換えシステムについては書き換え列の最小上界が定義される関数の計算量の最小上界とは必ずしもならない．正確な対応関係を得るために考案された展開グラフ書き換え規則という無限グラフ書き換えの概念を抽象化し，ある制限的なリダクション順序で順序付け可能な無限グラフ書き換えシステムは多項式解釈が可能であり，したがって書き換え列の長さと標準形の(グラフ表現による)サイズは多項式上界をもつことを示した．
たとえ項書き換えシステムの複雑さの(最小)上界の存在が示されても，(多項式上界など)上界がべき乗に関して閉じていない多くの場合は証明中にその上界を超越した数学的概念が必要になる．「最小関数グラフ」 (minimal function graphs) のようにグラフ表現を明示的に使うことなくメモ化を実現する方法を形式化することにより，そうした指数的なギャップを解消できる可能性を発見した．
上記以外の研究成果として，多項式時間計算可能な関数に対して健全かつ完全なリダクション順序についての研究成果を発展・精密化し論文にまとめ上げた．また項書き換えによる計算量解析の応用として，原始再帰的関数が制限的な多重再帰法に関して閉じているという古典的な事実を導くリダクション順序を考案した．
特別研究員奨励費を使用して国内では唯一の項書き換え理論専門の研究集会を開催した(第42回 TRS ミーティング，2015年2月7日～9日，東京都中央区晴海グランドホテル)．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究計画にしたがって主に(i)「展開グラフ書き換え規則」(unfolding graph rewrite rules) に対する計算量解析法の開発，及びその実際計算可能な集合関数 (predicatively computable set functions) への応用可能性の調査，及び(ii)限定算術上での「帰納的定義の公理による計算量クラス P, PSPACE の特徴づけ」の研究の完成に取り組んだ．
展開グラフ書き換え規則に基づいた無限グラフ書き換えシステムの計算量解析法については発表論文，学会発表，及びプレプリント(N. Eguchi, Complexity Analysis of Precedence Terminating Infinite Graph Rewrite Systems, Post-proceedings of 8th International Workshop on Computing with Terms and Graphs に採録予定)を含む一定の成果が得られた．
集合の要素は「探索可能でない」(一つの要素を選ぶアルゴリズムがない)という理由で集合関数への素朴な応用は難しいことが分かった．
(ii)についてはプレプリント(N. Eguchi, Characterising Complexity Classes by Inductive Definitions in Bounded Arithmetic, arXiv: 1205.2879)の改正，完成を予定したが，数学的な難点を度外視しても成果の意義が残念ながら広く受け入れられなかった．そこで帰納的定義が形式化される限定算術上でどのような興味深い原理が成り立つか調査し，その過程で項書き換えシステムの複雑性証明における指数的ギャップの解消可能性について萌芽的な成果が得られた．
|
| Strategy for Future Research Activity |
展開グラフ書き換え規則に基づいた無限グラフ書き換えシステムに対する計算量解析法の深化可能性，項書き換えシステムの複雑性証明における指数的ギャップの解消可能性，及びそうした複雑性証明の限定算術上での形式化可能性を調査し，「11．現在までの達成度」で述べた研究テーマ(i), (ii)の完成を目指す．そのために例えば，論理と計算量についてのワークショップ 16th International Workshop on Logic and Computational Complexity (2015年7月京都市)にて，項書き換えシステムの複雑性証明の形式化についての萌芽的な成果を報告し，関連研究者と研究交流を行う．
実数上の複雑性についての国際会議 12th International Conference on Computability and Complexity in Analysis (2015年7月明治大学)に組織委員として参加するなど，項書き換えシステムやグラフ書き換えシステムに対する計算量解析法の実数上の計算や DNA 計算への展開可能性を調査する．
平成26年度は学内での旅費の精算が著しく滞り研究費の使用額が交付額を超過したので，平成27年度は担当事務局との連携を緊密化し過不足無く研究費を使用する．
|
Research Products
(11 results)
