2018 Fiscal Year Research-status Report
条件付き項書き換えシステムにおける帰納的定理と基底合流性に関する研究
| Project/Area Number |
18K11158
|
|---|
| Research Institution | Niigata University |
|---|
Principal Investigator |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | 条件付き項書き換えシステム / ホーン節帰納的定理 / 基底合流性 / 補題生成法 / アンラベリング変換 |
|---|
| Outline of Annual Research Achievements |
項書き換えシステムは,形式手法に基づくソフトウェア構成・検証技術の基礎を与える重要な計算モデルである. 帰納的定理は,項書き換えシステムをプログラムとして見做したときに成立する性質に対応し,基底合流性は,項書き換えシステムの解析において重要な解の一意性を保証する性質である. 条件付き項書き換えシステムは,ホーン節論理の書き換えシステムによるモデル化であり,関数型プログラムのモデルとして,応用上重要な拡張である. 本研究は,条件付き項書き換えシステムにおける帰納的定理および基底合流性の自動証明・検証理論の基盤構築および証明・検証ツールの実現を目標としている．
本年度は，まず3型指向式条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明法について取り組んだ．与えられた指向式条件付き項書き換えシステムをアンラベリング変換を用いて項書き換えシステムへ変換し，帰納的定理を項書き換えシステムで証明したときに，どのような条件のもとで，その証明手続きの正しさが成立するのかという問題についての理論的な検討を行った．さらに，書き換え帰納法のおいて，与えられた式がホーン節の場合に適用できるような推論規則を検討した．実装についても取り組み，等式定理の場合と異なり，どのようなヒューリスティクスを適用すればよいかはあまり自明ではないことが判明した．
また，ホーン節帰納的定理の反駁証明や，書き換え帰納法の対話的定理証明器を用いた形式化，また，従来の発散鑑定法では補題の生成が困難な場合の補題生成法，さらに，帰納的定理の決定手続きを書き換え帰納法において利用する手法などについても検討を行なった．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
さまざまな条件付き項書き換えシステムの体系が知られているが，なかでも，3型指向式条件付き項書き換えシステムは，関数型プログラム言語のモデルとして最も自然なものである．3型指向式条件付き項書き換えシステムのアンラベリング変換において変換前の条件付き項書き換えシステムと変換後の項付き項書き換えシステムとの等価性を保証する条件がいくつか知られている．また，ホーン節等式論理で定理であることと，3型指向式条件付き項書き換えシステムによる書き換えで変換可能であることは，ギャップがあり，このギャップがないときに論理性が成立するというが，論理性を保証する条件がいくつか知られている．また，書き換え帰納法を適用するためにも，項書き換えシステムはいくつかの条件を満たす必要がある．これらの複数の条件を比較検討し，うまくすべての条件を満たし，実用性もそれほど損われないような条件を見いだすことが出来た．
次に，書き換え帰納法において，ホーン節帰納的定理を扱うための拡張について検討を行なった．まず，検討を行なうためにいくつかの自然な例を構築し，これらを用いて，どのように証明ができるか検討を行なった．そして，書き換え帰納法の3つの推論規則をそれぞれホーン節の条件部へ適用する場合に，どのような変更が必要になるかを検討することで3つの推論規則を考案した．これらの推論規則を適用することでいくつかの例において証明ができることを確認した．次に，これらの規則を実装した帰納的定理自動証明システムを実装した．しかし，等式定理の場合と異なり，推論規則の適用の仕方にどのようなヒューリスティクスを用いればよいかはあまり自明ではないことが判明した．
これらのことから，理論基盤の構築には一定の成果が得られたと考えている．しかし，実際の証明システムの構築技術には，さらなる検討が必要と考えられる．
|
| Strategy for Future Research Activity |
現在用いている書き換え帰納法は，基本的な書き換え帰納法であるが，より強力な書き換え帰納法も筆者らにより考案されている．より強力な自動証明システムを実現するためには，それを利用することが必要である．より詳細なヒューリスティクスを検討にあたっては，まずこの実装を進めてより強力な基本システムを確立する必要があると考えられる．また，新しい補題生成法を考案する過程で，補題の生成法においては規則的な発散系列の観測がまず必要であることがわかった．したがって，ホーン節帰納的定理の書き換え帰納法においても，うまく規則的な発散系列が生成できるような推論規則の適用も重要であると考えられる．ホーン節帰納的定理の反駁証明，書き換え帰納法の対話的定理証明器を用いた形式化，新しい補題生成法，帰納的定理の決定手続きを書き換え帰納法において利用する手法などについては，今後より検討を進めて，強力なホーン節帰納的定理証明法の実現に繋げていく必要がある．また，条件付き書き換えシステムの基底合流性に必要となる条件付き書き換えシステムの危険対解析についても調査を進める必要がある．これには条件項書き換えシステムの合流性解析や階層合流性の解析が参考になると考えており，より詳細な調査を進める必要がある．また，条件項書き換えシステムの合流性解析については，従来，項書き換えシステムの一意正規化可能性と非常に関連があることが知られており，項書き換えシステムの一意正規化可能性についても調査，研究を進める必要がある．また，書き換え帰納法を適用するための前提条件の1つである十分完全性についても，項書き換えシステムではその理論が従来得られているが，条件付き項書き換えシステムでは基本的な理論があまりない．アンラベリング変換を利用して，条件付き項書き換えシステムの十分完全性を解析する手法を検討することも課題である．
|
| Causes of Carryover |
国際会議の出張費の支払いを予定していたものの，予定外に利用可能となった他予算から支払いを行ったため，残額が生じたものである．現在使用しているノートPCの性能が悪く，出張中のデモンストレーションや研究打ち合わせの遂行に支障がでているため，この残額を利用してノートPCの購入を行う予定である．
|
-
-
-
-
[Journal Article] Confluence Competition 20182018
Author(s)
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani and Harald Zankl
-
Journal Title
Leibniz International Proceedings in Informatics
Volume: 108
Pages: 32:1-32:5
DOI
Open Access / Int'l Joint Research
-
-
