2022 Fiscal Year Research-status Report

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

Research Project

Project/Area Number	21K11750
Research Institution	Niigata University
Principal Investigator	青戸等人新潟大学, 自然科学系, 教授 (00293390)
Project Period (FY)	2021-04-01 – 2024-03-31
Keywords	項書換えシステム / UNC性 / UNR性 / NFP性 / 合流性
Outline of Annual Research Achievements	合流性(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プロパティが利用可能ではないかとのアイデアに至り，その可能性について検討を進めるとともに，可換システムの決定可能性についても検討を行った．
Current Status of Research Progress	Current Status of Research Progress 2: Research has progressed on the whole more than it was originally planned. Reason 文献(GodoyとJacquemard,2009)では，右線形フラット項書き換えシステムのUNR性の決定不能性の証明は，ある右線形フラット項書き換えシステムのUNR性を，ポストの対応問題(PCP)に帰着することによって証明している．当該の右線形フラット項書き換えシステムのUNR性はたしかにPCPに帰着できるように思われるものの，証明で用いられているclean関数に関する性質の補題は間違っており，反例がある．また，さらにそれを用いた補題にも反例を見つかっている．これについて，著者に一人に問い合わせたものの，返事が得られなかった．本年度は正しい証明を論文として完成させるとともに国内会議へ投稿し，採択となり，論文発表を行った．また，以前に問い合わせた著者の一人にも連絡をするとともに完成した証明を含む論文を送付し，修正に関しての肯定的な返事が得られた．現状の証明はまだあまり完成度が高くはなく，さまざまな粗さが目立つ証明ではあるが，正しさという観点からは一定の完成度に到達したと考えられる．また，弱左線形項書き換えシステムに対する永続性を利用したUNC検証法についても制約が大きいながらもひとまず定理として形式化できた．さらに,指向式条件付き項書き換えシステムの可換性についても，別角度からの新しい結果を追加することが出来た．以上の成果により，概ね順調に進捗しているものと判断した．
Strategy for Future Research Activity	UNR性の決定可能性の証明についてさらに証明の完成度を上げられるよう，証明の単純化や一般化について検討する．また，右線形フラット項書き換えシステムの決定性についてはまだ肯定的にも否定的にも知られていない．これまでに得られたUNC性の決定不能性に関する知見を利用して，NFP性の決定不能性が示せないか検討する．また，可換性の危険対条件検証の実装について，現状では全くメドが立っていない．第一階述語論理の証明器や反証システムを利用することで，自動化できないか検討を行う．正則書き換えシステムのUNC性等については，直交システムの合流性以外，従来ほとんど知られていない．これまでの検討結果として，他の書き換えシステムの枠組みとはだいぶ異なるアプローチが必要になるように思われる．この問題についての何らかの解を与えられないか検討を進めたい．
Causes of Carryover	本年度も学会発表の多くが，新型コロナの影響により，オンライン開催またはハイブリット開催となり，現地参加を見送った会議も多くあった．特に国際会議についてはリスクと現職場における実務との兼ね合いから参加を見送ることとした。このため，予定していた学会参加や学生による発表も半数以上はオンラインとなったため，予定していた交通費の支出がなくなることとなった．さらに，学生の参加費についてはオンライン開催となることで，大幅に値引きがあり，これらについても支出がなくなることとなった．残額は不足している専門書や論文の購入や計算機実験および成果発表に用いる各種ツール等の購入にあてる予定である．