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

术语重写理论、证明理论及其在复杂性理论中未解决问题的应用

• 批准号: 13J00726
• 负责人: 江口 直日
• 金额: $ 2.53万
• 依托单位: Chiba University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2013
• 资助国家: 日本
• 起止时间: 2013-04-01 至 2016-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13J00726/
• 关键词: 項書き換えシステム; 計算量解析; 多項式時間計算量; 無限グラフ書き換えシステム; 停止性証明; 形式体系; 多項式領域計算量; 項書き換え理論; 証明論; 計算量理論; グラフ書き換え; 限定算術; 計算量クラス; 多項式時間; 停止性順序

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

Definition of the relationship between the calculation time and the close relationship between the number of items, the number of items, the items, the number of itemsボローニャ大学 M. Dr. Avanzini, G. Professor Moser's joint research project on polynomial order analysis and polynomial time calculation of possible relations between new characteristics is developed. The minimum upper bound of the calculation time of the correlation number is defined by the minimum upper bound of the calculation time of the correlation number. The correct relationship is obtained. Dal Lago's research project "Unfolding the book and changing the rules" was abstracted, and last year's development began with the infinite book and changing the rules. The term transformation is not determined by the calculation of the upper bound of the long polynomial of the transformation column. When the input term root is complete, the possible transformation column is derived from the index of the transformation column. The reason for this is that the book itself is complex, and the stopping proof is that the index exists, and the solution is not clear. The concept of fixed point solution is used to derive the substitution of wood and the approximate composition of fixed point in weak formal system under the condition of constraint. For example, if the term is changed, the formal system and the polynomial field are calculated.

项目成果

Complexity Analysis of Precedence Terminating Infinite Graph Rewrite Systems

终止无限图重写系统的优先级复杂性分析

• DOI: 10.4204/eptcs.183.3
• 发表时间: 2015
• 期刊: Electronic Proceedings in Theoretical Computer Science
• 作者: T. Umakoshi;Y. Saito;and P. Verma;Naohi Eguchi
• 通讯作者: Naohi Eguchi

Formalizing Termination Proofs under Quasi-interpretations Optimally

准解释下最优形式化终止证明

• 发表时间: 2015
• 作者: 長崎祐介;宮田将司;高原淳一;Naohi Eguchi
• 通讯作者: Naohi Eguchi

Predicative Lexicographic Path Orders - An Application of Term Rewriting to the Region of Primitive Recursive Functions

谓词词典路径顺序 - 术语重写在原始递归函数区域中的应用

• DOI: 10.1007/978-3-319-12466-7_5
• 发表时间: 2014
• 期刊: Lecture Notes in Computer Science
• 作者: 浅見拓哉;和久 剛;全 孝静;松本 健;高橋 智;依馬 正次;Naohi Eguchi
• 通讯作者: Naohi Eguchi

Characterising Complexity Classes by Inductive Definitions in Bounded Arithmetic

通过有界算术中的归纳定义来表征复杂性类

• 发表时间: 2013
• 作者: LI Cheng;INAGAKI Yoshihiko;SAKAKIBARA Yutaka;Naohi Eguchi
• 通讯作者: Naohi Eguchi

Formalizing Termination Proofs under Polynomial Quasi-interpretations

多项式拟解释下的形式化终止证明

• DOI: 10.4204/eptcs.191.5
• 发表时间: 2015
• 期刊: Electronic Proceedings in Theoretical Computer Science
• 作者: Iwamoto H;Matsuhisa K;Saito A;Kanemoto S;Asada R;Hino K;Takai T;Cui M;Cui X;Kaneko M;Arihiro K;Sugiyama K;Kurisu K;Matsubara A;Imaizumi K.;Naohi Eguchi
• 通讯作者: Naohi Eguchi