項書き換えシステムの解の一意性を保証する性質に関する研究

保证术语重写系统解唯一性的性质研究

基本信息

批准号：
21K11750
负责人：
青戸等人
金额：
$ 2.66万
依托单位：
Niigata University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2021
资助国家：
日本
起止时间：
2021-04-01 至 2024-03-31
项目状态：
已结题

项目摘要

合流性(CR性)以外の解の一意性を保証する性質として，これまで研究されている性質には，正規形性(NFP性)，可換に関する一意正規形性(UNC性)，そして，簡約に関する一意正規形性(UNR性)の3つがある.これらの性質は，CR性⇒NFP性⇒UNC性⇒UNR性という論理関係がある.したがって，これらの3つの性質は合流性よりも弱い性質となっており，しかも，CR性，NFP性，UNC性，UNR性の順に階層を成している.本研究では，NFP性，UNC性，UNR性を始めとする，解の一意性を保証する，合流性より弱いさまざまな性質の検証理論や自動検証技術を開発する.右線形フラット項書き換えシステムにおけるUNR性の決定不能性の証明が文献(GodoyとJacquemardら(2009)によって与えられてる．しかし，その証明にはギャップがある．そこで，その証明の修正を試み，正しい証明を与えることに成功した．本年度は，証明全体を細部まできちんと検討して正しい証明を完成させた．また，その成果を論文としてまとめた．また，永続性を利用したUNC検証法についても検討し，ω-重なり性をもつが，重なり性をもたず，合流性ももたないようなTRSに対するUNC検証法を考案した．十分条件のもとでの検証法の正しさを証明した．ただし，現状で得られた十分条件は制約が強く，適用範囲を広げるためには今後の検討が必要である．UNC性の検証手法として，条件線形化により得られた条件付き項書き換えの合流性を用いる手法がある．条件付き項書き換えシステムの可換性検証法についていくつかの観点から検討を行うとともに，可換性の危険対条件検証の実装について検討を進めた．また，正則書き換えシステムの検証についてZプロパティが利用可能ではないかとのアイデアに至り，その可能性について検討を進めるとともに，可換システムの決定可能性についても検討を行った．

保证汇合（CR）以外的解决方案唯一性的属性包括已经研究的三个属性：正常形式（NFP），唯一的正常形式（UNC）和独特的正常形式（UNR）有关简化。这些属性具有CR→NFP→UNC→UNR的逻辑关系。因此，这三个属性比汇合弱，并且在层次上按CR，NFP，UNC和UNR的顺序层次。这项研究开发了验证理论和自动验证技术，以比汇合的各种属性（例如NFP，UNC和UNR），这些技术保证了解决方案的独特性。文献给出了UNR在右键纯正重写系统中不确定性的证明（Godoy和Jacquemard等人（2009年）。但是，证据中存在差距。 ω-不重叠，但在足够的条件下证明了验证方法的正确性。观点，还检查了可交流风险与条件验证的实施。我们还想到了Z属性可用于验证常规重写系统，并且我们还检查了确定的可能性，并研究了交换系统的可能性。

项目成果

期刊论文数量（13）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

正則項書き換えにおける書き換えステップの決定可能性について

论正则项重写中重写步骤的可判定性

DOI：
发表时间：
2023
期刊：
影响因子：
0
作者：
望月美希;青戸等人
通讯作者：
青戸等人

A Proof Method for Local Sufficient Completeness of Term Rewriting Systems

术语重写系统局部充分完备性的证明方法

DOI：
10.1007/978-3-030-85315-0_22
发表时间：
2021
期刊：
Proceedings of the 18th International Colloquium on Theoretical Aspects of Computing (ICTAC 2021)
影响因子：
0
作者：
Tomoki Shiraishi;Kentaro Kikuchi;Takahito Aoto
通讯作者：
Takahito Aoto

書き換え帰納法による帰納的定理証明と循環余帰納法による余帰納的定理証明の融合

重写归纳法的归纳定理证明与循环共归纳法的共归纳定理证明的融合