二分決定グラフを用いたプログラム検証の自動化に関する研究

今年度は、前年度に得られた結果を項書換え系完備化手続きに応用する研究を行なった。その概要は以下のようにまとめられる。1. KnuthとBendixによって提案された完備化手続きは与えられた等式集合と等価で完備な項書換え系の生成を試みる(半)アルゴリズムである。等式集合を代数的仕様とすれば、完備化手続きは仕様から実行可能なプログラムを生成するコンパイラとみなすことができる。また、定理自動証明など種々の応用において非常に有用な手法でもある。しかし、完備化手続きの結果は与えられた簡約順序に大きく依存する。少なくとも以下の問題点が挙げられる。(a) 生成される項書換え系の停止性を保証するための簡約順序を利用者に要求する。(b) 簡約順序が不適当な場合、手続きが無限に継続する場合がある。(c) 簡約順序が適当な場合にも(完備な項書換え系が存在するにもかかわらず)失敗する場合がある。研究代表者は(b)の問題点を解決するために、平成6、7年度の研究において複数の簡約順序を同時に扱う完備化手続きを提案、実現し、その成果を学術論文誌等に発表している。しかし、提案した手法では(a)の問題点が解決できていなかった。2. 1(a)で述べた問題を解決するため、前年度提案した停止性検証のための二分決定グラフの利用法を平成6、7年度に研究した複数の簡約順序を同時に扱う完備化手続き対して適用し、新たな完備化推論規則を得た。3. 2.で得た完備化推論規則を多くの項書換え系に適用し、その効果を確認した。4. 現在も継続して、計算機上での実現及び改良を行っている。これまでの研究業績を国内全国大会、国際会議にて発表し、論文誌に投稿(採録決定)した。

今年度は、前年度に得られた結果を項書換え系完備化手続きに応用する研究を行なった。その概要は以下のようにまとめられる。1. KnuthとBendixによって提案された完備化手続きは与えられた等式集合と等価で完備な項書換え系の生成を試みる(半)アルゴリズムである。等式集合を代数的仕様とすれば、完備化手続きは仕様から実行可能なプログラムを生成するコンパイラとみなすことができる。また、定理自動証明など種々の応用において非常に有用な手法でもある。しかし、完備化手続きの結果は与えられた簡約順序に大きく依存する。少なくとも以下の問題点が挙げられる。(a) 生成される項書換え系の停止性を保証するための簡約順序を利用者に要求する。(b) 簡約順序が不適当な場合、手続きが無限に継続する場合がある。(c) 簡約順序が適当な場合にも(完備な項書換え系が存在するにもかかわらず)失敗する場合がある。研究代表者は(b)の問題点を解決するために、平成6、7年度の研究において複数の簡約順序を同時に扱う完備化手続きを提案、実現し、その成果を学術論文誌等に発表している。しかし、提案した手法では(a)の問題点が解決できていなかった。2. 1(a)で述べた問題を解決するため、前年度提案した停止性検証のための二分決定グラフの利用法を平成6、7年度に研究した複数の簡約順序を同時に扱う完備化手続き対して適用し、新たな完備化推論規則を得た。3. 2.で得た完備化推論規則を多くの項書換え系に適用し、その効果を確認した。4. 現在も継続して、計算機上での実現及び改良を行っている。これまでの研究業績を国内全国大会、国際会議にて発表し、論文誌に投稿(採録決定)した。