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

点击翻译按钮获取中文摘要

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