2022 Fiscal Year Research-status Report
Automated Theorem Proving for Infinite Term Rewriting Systems
| Project/Area Number |
22K11904
|
|---|
| Research Institution | Shimane University |
|---|
Principal Investigator |
岩見 宗弘 島根大学, 学術研究院理工学系, 准教授 (70314614)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Keywords | 項書き換えシステム / 無限項書き換えシステム / 正則項 / 木変換器 / 組合せ子 / 非ω-強頭部正規化可能性 / 非基礎ループ性 / 非循環性 |
|---|
| Outline of Annual Research Achievements |
(等式付)無限項書換えシステムに対する生成性自動反証法および余帰納的定理自動証明法の基礎理論を構築することを目的として，正則項の木変換器による書き換えに関する研究を行った．さらに，組合せ子がもつ書き換え規則からなる項書き換えシステムの非ω-強頭部正規化可能性，非循環性，非基礎ループ性に関する研究を行った．本年度の具体的な成果は以下の通りである．
1. 有限項の繰り返しから生じる無限項は正則項として知られており，基本的な性質に関する研究が進んでいる．正則項は，有限表現ができるため，計算機で扱える無限項として重要な役割を果たす．まず，決定性トップダウン木変換器を用いて，正則項を無限に書き換えてその極限として無限項が得られるならば，その無限項は正則項であることを証明した．また，この結果は，決定性マクロ木変換器に対しては成立しないことを反例をあげて示した．本研究は，日本ソフトウェア科学第39回大会において報告した．
2. 先行研究で提案した無限項書き換えシステムに対するω-強頭部正規化可能性の反証手続きを，Smullyan(1994)により新しく紹介された組合せ子の書き換え規則からなる項書き換えシステム37例に対して適用した．その結果，31例について反証手続きが成功した．すなわち，31例がω-強頭部正規化可能性をもたないことを示した．また，組合せ子の書き換え規則からなる項書き換えシステム37例のうち32例が非循環性をもち，12例が停止性，非基礎ループ性と非ループ性をもつことを示した．さらに，2種類のラベル付け手法を提案し，8例が非基礎ループ性をもつことを示した．本研究は，第143回情報処理学会プログラミング研究発表会において報告した．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
研究の進捗状況がやや遅れている最大の理由は，所属大学の雑用と教育のノルマが非常に多く，十分な研究時間が確保できなかったことである．特に，4～7月はほとんど研究ができなかった．教員の人数が減っていることが原因であり，未だに十分な数の教員が補充されていない．所属大学には研究環境の早急な改善を強く望む．
また，正則項の木変換器による書き換えに関する研究で，決定性トップダウン木変換器を用いて，正則項を無限に書き換えてその極限として無限項が得られるならば，その無限項は正則項であることを証明した．しかしながら，その証明は間違っていることが判明した．
|
| Strategy for Future Research Activity |
正則項の木変換器による書き換えに関する研究で，決定性トップダウン木変換器を用いて，正則項を無限に書き換えてその極限として無限項が得られるならば，その無限項は正則項であることを証明した．しかしながら，その証明は間違っていることが判明した．今後はこの研究課題に再度取り組み，正しい証明を与えることが課題である．
また，組合せ子がもつ書き換え規則からなる項書き換えシステムの非ω-強頭部正規化可能性，非循環性，非基礎ループ性に関する研究において，先行研究で提案した無限項書き換えシステムに対するω-強頭部正規化可能性の反証手続きを，Smullyan(1994)により新しく紹介された組合せ子の書き換え規則からなる項書き換えシステム37例に対して適用した．しかしながら，先行研究で作成したプログラムは最新の処理系だけではなく，当時のバージョンの処理系でも動作しなかった．今後はこのプログラムを改良して新しい処理系に対応させ，組合せ子のω-強頭部正規化可能性の反証実験を行うことが課題である．さらに，AProVEで停止性が証明できなかった(かもしれない)と判定された10例に対して，停止性の証明または反証を行うことも今後の課題である．
|
