| 研究課題/領域番号 |
21K11750
|
|---|
| 研究機関 | 新潟大学 |
|---|
研究代表者 |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| キーワード | 正規形 / 項書換えシステム / UNC性 / NFP性 / UNR性 / 合流性 |
|---|
| 研究実績の概要 |
合流性(CR性)以外の解の一意性を保証する性質として，これまで研究されている性質には，正規形性(NFP性)，可換に関する一意正規形性(UNC性)，そして，簡約に関する一意正規形性(UNR性)の3つがある.これらの性質は，CR性⇒NFP性⇒UNC性⇒UNR性という論理関係がある.したがって，これらの3つの性質は合流性よりも弱い性質となっており，しかも，CR性，NFP性，UNC性，UNR性の順に階層を成している.本研究では，NFP性，UNC性，UNR性を始めとする，解の一意性を保証する，合流性より弱いさまざまな性質の検証理論や自動検証技術を開発する.
右線形フラット項書き換えシステムにおけるUNR性の決定不能性の証明が文献(GodoyとJacquemardら(2009)によって与えられてる．しかし，その証明にはギャップがある．そこで，その証明の修正を試み，正しい証明を与えることに成功した．また，弱左線形項書き換えシステムにおいて，永続性を利用して，合流性を保証する理論が知られている．これはRnfが合流性を持つならばRが合流性を持つことを利用して，合流性条件を拡張している．類似の技法が，UNC性についても適用できないか検討した．このため，以下の性質を満たす項書き換えシステムを構築した：UNCの十分条件であるω-重なり性をもつが，重なり性をもたず，合流性ももたない．このような項書き換えシステムについて，そのUNCを検証する条件を発見できれば，実際にUNC性についても永続性を利用した検証手法が考案するのに役立つと考えられる．また，指向式条件付き項書き換えシステムのレベル可換性を保証する条件や局所十分完全性を保証する条件についても新しい条件を与えた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
文献(GodoyとJacquemard,2009)では，右線形フラット項書き換えシステムのUNR性の決定不能性の証明は，ある右線形フラット項書き換えシステムのUNR性を，ポストの対応問題(PCP)に帰着することによって証明している．当該の右線形フラット項書き換えシステムのUNR性はたしかにPCPに帰着できるように思われるものの，証明で用いられているclean関数に関する性質の補題は間違っており，反例がある．また，さらにそれを用いた補題にも反例を見つかっている．これについて，著者に一人に問い合わせたものの，返事が得られなかった．当該結果は，UNR性の重要な理論的な性質であるため，やはり正しい証明を得ることが重要だと考え，この問題に取り組んだ．その結果，当該論文で用いられているclean関数に関する性質を，はるかに精密に明らかにすることで，証明の修復に成功することが出来た．
また，関連する技術についての研究という点では,指向式条件付き項書き換えシステムの可換性は，従来まったく知られていなかったが，指向式条件付き項書き換えシステムのレベル可換性という概念に着目して，その十分条件を示すことで，(条件なしの)項書き換えシステムの可換性と指向式条件付き項書き換えシステムのレベル合流性に関する条件を拡張する危険対条件を示すことができた．また，十分完全性より弱い性質である局所十分完全性という性質を考案して，その性質保証する条件を示した．
以上の成果により，概ね順調に進捗しているものと判断した．
|
| 今後の研究の推進方策 |
永続性を利用した弱左線形項書き換えシステムに関する証明手法について，UNC性やその他の性質の証明法が得られないか，引き続き検討を行う．また，右線形フラット項書き換えシステムの決定性についてはまだ肯定的にも否定的にも知られていない．これまでに得られたUNC性の決定不能性に関する知見を利用して，NFP性の決定不能性が示せないか検討する．また，NFPの決定可能性については，従来それほど研究がされていないため，木オートマトンの各種の判定手続きを利用した決定可能性証明手法についても検討し，NFPが決定可能なクラスを見い出せないか検討を行う．また，正則書き換えシステムについては，これらの性質は従来ほとんど知られていない．そこで，従来得られている交換律を用いた正則書き換えシステムについて，UNC性などの性質が示せないか検討を行いたい．
|
| 次年度使用額が生じた理由 |
2,3月開催の学会発表の多くが，新型コロナの影響により，オンライン開催またはハイブリット開催となり，また大学の方針により，ハイブリット開催となった研究会についても現地参加を見送ることとした．このため，予定していた学生の学会参加もすべてオンライン参加をさせることとなったため，予定していた交通費の支出がなくなることとなった．さらに，学生の参加費についてはオンライン開催となることで，大幅に値引きがあり，これらについても支出がなくなることとなった．残額は不足している専門書や論文の購入や計算機実験および成果発表に用いる各種ツール等の購入にあてる予定である．
|
