| 研究概要 |
今年度は完備化手続きの自動化に向けた二分決定グラフを利用した完備化推論規則に関する研究を行なった。その概要は以下のようにまとめられる。
KnuthとBendixによって提案された完備化手続きは与えられた等式集合と等価で完備な項書換え系の生成を試みる(半)アルゴリズムである。等式集合を代数的仕様とすれば、完備化手続きは仕様から実行可能なプログラムを生成するコンパイラとみなすことができる。また、定理自動証明など種々の応用において非常に有用な手法でもある。しかし、完備化手続きの結果は与えられた簡約順序に大きく依存する。少なくとも以下の問題点が挙げられる。
1.生成される項書換え系の停止性を保証するための簡約順序を利用者に要求する。
2.簡約順序が不適当な場合、手続きが無限に継続する場合がある。
3.簡約順序が適当な場合にも(完備な項書換え系が存在するにもかかわらず)失敗する場合がある。
研究代表者は平成6、7年度の研究において、問題点2.を解決するため一般的な推論規則をもとに複数の簡約順序を同時に扱う推論規則を提案している。本年度は、1.の問題点を解決するため、この推論規則に基づき、如何にして二分決定グラフを利用するのかを検討した。その検討をもとに、簡約順序として関数記号の集合上の(厳格)半順序(優先順位)に基づく経路順序を用いて、ある条件を満たす優先順位を自動的に(複数)生成する完備化推論規則を考案した。この際、優先順位は平成9、10年度に提案した手法により、二分決定グラフ(Binary Decision Diagram:BDD)で表される。同時に、二分決定グラフの停止性検証の応用に関する研究を行ない,その成果を国際会議、学術論文誌等で発表した。
|
