2023 Fiscal Year Annual Research Report
項書き換えシステムの解の一意性を保証する性質に関する研究
| Project/Area Number |
21K11750
|
|---|
| Research Institution | Niigata University |
|---|
Principal Investigator |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Keywords | 正規形 / 項書き換えシステム / UNC性 / NFP性 / UNR性 / 合流性 |
|---|
| Outline of Annual Research Achievements |
合流性(CR性)以外の解の一意性を保証する性質として，これまで研究されている性質には，正規形性(NFP性)，可換に関する一意正規形性(UNC性)，そして，簡約に関する一意正規形性(UNR性)の3つがある.これらの性質は，CR性⇒NFP性⇒UNC性⇒UNR性という論理関係がある.したがって，これらの3つの性質は合流性よりも弱い性質となっており，しかも，CR性，NFP性，UNC性，UNR性の順に階層を成している.本研究では，NFP性，UNC性，UNR性を始めとする，解の一意性を保証する，合流性より弱いさまざまな性質の検証理論や自動検証技術を開発する.
最終年度では，UNR性を検証する手法について以下の成果が得られた．CR性とUNC性については，書き換え規則を追加または削除したときに，どのような場合に，それらの性質を保存するかという条件が知られている．同様の問題が，UNR性については知られていないことがわかり考察研究を進めた結果，UNR性についてのそのような条件を与えることができた．また，これらの条件について，UNR性のみならずUNC性も保存するが，CR性は保存しないことも明らかにし，UNR性の検証システムに用いる場合の扱い方に知見を与えた．さらに，UNC性がない場合のUNR性の検証方法には利用できないことも導かれる．そのため，UNC性を持たない場合のUNR性の検証方法が重要であることが明らかになり，その手法の考察研究を進め，2種類の手法を考案し，その正しさの証明を与えた．さらに，これらの検証手法の実装も行い，計算機実験によりその有効性を明らかにした．
|
-
-
[Journal Article] A new format for rewrite systems2023
Author(s)
Takahito Aoto, Nao Hirokawa, Dohan Kim, Misaki Kojima, Aart Middeldorp, Fabian Mitterwallner, Naoki Nishida, Teppei Saito, Jonas Schoepf, Kiraku Shintani, Rene Thiemann and Akihisa Yamada
-
Journal Title
Proceedings of the 12th International Workshop on Confluence
Volume: NB
Pages: 32-37
Open Access / Int'l Joint Research
-
-
-
-
