| 研究概要 |
本研究は等式論理における検証法の確立し,さらに,一般のソフトウェアを代数的手法を用いて等式論理に自動的に変換することにより,これらの検証への応用を図るものである.
今年度は,停止順序を満たす等式を通常の項書換え規則とみなし,これを満たさない等式は集合としての書換え規則とみなす項集合書換え系の形式的定義を与えた.さらに,(1)停止条件,(2)線形規則における合流条件が明らかになた.
(1)項集合書換え系においては,通常の項書換え系におけるE合同上の書換えよりも緩い条件で停止性を持つことが分かった.
(2)この条件は,停止性を満たし非線形規則を持たない項集合書換え系に対して,その危険対が合流するならば合流性を持つというものである.これは,等式付の項書換え規則に対応させて考えると,Huet(1980)の条件とほぼ同じ結果であるが,本結果の方が(1)の停止条件が緩い分だけ拡張になっている.
また,優先順位つき項書換え系の定義を行ない,その等式論理に基づく意味論を与えた.これにより,関数型プログラムを等式論理に変換して検証するための基礎が与えられた.
|
