权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

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

基本信息

批准号：
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プロパティが利用可能ではないかとのアイデアに至り，その可能性について検討を進めるとともに，可換システムの決定可能性についても検討を行った．

The properties of a solution other than CR property are guaranteed. The properties of a solution are studied. The properties of a solution are normal form (NFP property). The properties of a solution are commutative. The properties of a solution are normal form (UNC property). CR property <$NFP property <$UNC property <$NR property <$logical relation. The nature of CR, NFP, UNC, NR and the order of hierarchy are formed. In this study, NFP, UNC and NR properties are first developed, and the theory and technology of automatic identification are developed. A proof of the indeterminacy of UNR properties in the literature (Godoy Jacquemard, 2009).しかし，その证明にはギャップがある.そこで，その证明の修正を试み，正しい证明を与えることに成功した. This year, the proof is complete. The results of the paper are as follows: For example, if you want to use the UNC method, you can use the TRS method to test it. The proof of the correctness of the method of proof under the very condition. The present condition is very strong, the applicable range is very strong, the future is very strong, the UNC is very strong, the condition is very strong. The condition of exchange is the condition of exchange. The condition of exchange is the condition of exchange. The condition is the condition of exchange. In this case, the possibility of using the system to determine the possibility of the system is discussed.

项目成果

期刊论文数量（13）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

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

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

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

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

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

DOI：
发表时间：
2021
期刊：
影响因子：
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

フラット右線形項書き換えシステムの簡約に関する一意正規形性の決定不能性の証明について

关于平右线性项重写系统简化唯一范式不可判定性的证明