| Project/Area Number |
22K11904
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Shimane University |
|---|
Principal Investigator |
岩見 宗弘 島根大学, 学術研究院理工学系, 准教授 (70314614)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2024: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2023: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2022: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| Keywords | 項書き換えシステム / 無限項書き換えシステム / 正則項 / 木変換器 / 組合せ子 / 非ω-強頭部正規化可能性 / 非基礎ループ性 / 非循環性・非停止性 / 非循環性 / 無限項書換えシステム / 定理自動証明 / 項書換えシステム |
|---|
| Outline of Research at the Start |
無限長のデータ構造を用いるプログラムの検証を行うために，無限項書換えシステムと呼ばれる体系が考えられている．そのようなプログラムに特徴的な性質として，生成性と余帰納的定理がある．前者は計算結果としてストリームが存在することを保証する概念であり，後者はストリームの等価性等を保証する性質である．先行研究において，無限項書換えシステムに対する一般生成性の反証法や，その反証法において重要な技術として正則項上の単一化に対する拡張について研究成果を得ている．本研究では，先行研究を発展させることで，（等式付）無限項書換えシステムに対する生成性自動反証法と余帰納的定理自動証明法の基礎理論を構築する．
|
| Outline of Annual Research Achievements |
(等式付)無限項書換えシステムに対する生成性自動反証法および余帰納的定理自動証明法の基礎理論を構築することを目的として，正則項の木変換器による書き換えに関する研究を行った．また，組合せ子がもつ書き換え規則からなる項書き換えシステムの非ω-強頭部正規化可能性，非循環性，非基礎ループ性に関する研究を行った．さらに，組合せ子がもつ書き換え規則からなる項書き換えシステムの停止性の反証に関する研究を行った．
本年度の具体的な成果は以下の通りである．
1. 有限項の繰り返しから生じる無限項は正則項として知られており，基本的な性質に関する研究が進んでいる．正則項は，有限表現ができるため，計算機で扱える無限項として重要な役割を果たす．決定性トップダウン木変換器を用いて，正則項を無限に書き換えてその極限として無限項が得られるならば，その無限項は正則項であることの証明の修正に取り組んだ．
2. 先行研究で提案した無限項書き換えシステムに対するω-強頭部正規化可能性の反証手続きを，Smullyan(1994)により新しく紹介された組合せ子の書き換え規則からなる項書き換えシステム37例に対して適用した．その結果，31例について反証手続きが成功した．すなわち，31例がω-強頭部正規化可能性をもたないことを示した．また，組合せ子の書き換え規則からなる項書き換えシステム37例のうち32例が非循環性をもち，12例が停止性，非基礎ループ性と非ループ性をもつことを示した．さらに，2種類のラベル付け手法を提案し，8例が非基礎ループ性をもつことを示した．最後に，10例は停止性をもつかどうかが不明であった．そこで，木オートマトンを用いて，7例の組合せ子が停止性をもたないことを示した．次に，書き換え規則が類似した組合せ子M, O, Pを一般化した組合せ子が停止性をもたないことを示した．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
研究の進捗状況がやや遅れている最大の理由は，所属大学の雑用と教育のノルマが非常に多く，十分な研究時間が確保できなかったことである．教員の人数が減っていることが原因であり，未だに十分な数の教員が補充されていない．所属大学には研究環境の早急な改善を強く望む．
昨年度，正則項の木変換器による書き換えに関する研究で，決定性トップダウン木変換器を用いて，正則項を無限に書き換えてその極限として無限項が得られるならば，その無限項は正則項であることを証明した．しかしながら，その証明は間違っていることが判明した．その後，この証明の修正に取り組んでいるいるが，まだ正しい証明は完成していない．
|
| Strategy for Future Research Activity |
正則項の木変換器による書き換えに関する研究で，決定性トップダウン木変換器を用いて，正則項を無限に書き換えてその極限として無限項が得られるならば，その無限項は正則項であることを証明した．しかしながら，その証明は間違っていることが判明した．今後もこの研究課題に継続して取り組み，正しい証明を与えることが課題である．
また，組合せ子がもつ書き換え規則からなる項書き換えシステムの非ω-強頭部正規化可能性，非循環性，非基礎ループ性に関する研究において，先行研究で提案した無限項書き換えシステムに対するω-強頭部正規化可能性の反証手続きを，Smullyan(1994)により新しく紹介された組合せ子の書き換え規則からなる項書き換えシステム37例に対して適用した．しかしながら，先行研究で作成したプログラムは最新の処理系だけではなく，当時のバージョンの処理系でも動作しなかった．今後はこのプログラムを改良して新しい処理系に対応させ，組合せ子のω-強頭部正規化可能性の反証実験を行うことが課題である．さらに，木オートマトンを用いて停止性の反証ができなかった3例に対して，停止性の証明または反証を行うことも今後の課題である．
|
