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

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

• 批准号: 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 らによって考案された「展開グラフ書き換え規則」という無限グラフ書き換えシステムの概念を抽象化し，昨年度に開発を開始した無限グラフ書き換えシステムに対する多項式級の解析法を論文にまとめ上げた．項書き換えシステムは非決定的な計算モデルなので書き換え列の長さに多項式的上界が存在する場合でも，入力項を根として全ての可能な書き換え列からなる導出木のサイズは指数的になりうる．この理由により項書き換えシステム自身の複雑さと停止性証明の間には指数的なギャップが存在し，そのギャップが解消しうるのか否かは明らかでなかった．プログラム意味論で知られている不動点解釈の概念を援用し，導出木の代替物として適当な不動点を弱い形式体系内で近似的に構成することにより制限的な条件下では指数的なギャップが解消できることを証明した．その例として項書き換えシステム，形式体系，及び多項式領域計算量を関連づけることに成功した．

术语重写系统的复杂性通常通过重写序列的长度来衡量，因为它与定义函数的计算时间量密切相关。我们与博洛尼亚大学的 M. Avanzini 博士和因斯布鲁克大学的 G. Moser 副教授合作，开发了一种用于术语重写系统的多项式级分析方法以及多项式时间可计算函数的新表征。虽然函数的计算时间量与术语重写系统的复杂度之间存在密切的对应关系，但对于表达广义递归原理（例如树结构）的术语重写系统，重写序列的长度为最小上限不一定是为其定义的函数的计算时间量的最小上限。我们抽象了 U. Dal Lago 等人设计的称为“扩展图重写规则”的无限图重写系统的概念，以获得准确的对应关系，并开发了我们最后开始开发的无限图重写系统的多项式级分析方法。年的结果总结在一篇论文中。由于项重写系统是一个非确定性的计算模型，即使重写序列的长度存在多项式上界，以输入项为根的所有可能的重写序列组成的推导树的大小也可以为指数。因此，术语重写系统本身的复杂性与停机属性证明之间存在指数级差距，并且尚不清楚这种差距是否能够得到解决。通过使用程序语义中已知的不动点解释的概念，我们可以在弱形式系统中近似构造一个适当的不动点作为推导树的替代，从而在限制条件下创建指数间隙我们证明了这是可能的。解决问题。例如，我们成功地将术语重写系统、形式系统和多项式域复杂性联系起来。

项目成果

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