型付き項書換え系の変換に基づく関数型プログラムの自動検証

点击翻译按钮获取中文摘要

書き換え理論における自動証明向き停止性判定法として,依存対法という手法が近年注目されている.この停止性証明法は,十分広いクラスの書き換え系に対して効率的で強力な自動判定のできる手法であるが,高階関数のあるプログラムに対して直接使えないなど,適用範囲が限られていた.高階関数とは,データとして関数を受け渡しできる関数であり,プログラムの汎用性を高めるための,関数型言語の本質的な機能の1つである.そこで,より広範囲のプログラムに対して,書き換えによる停止性自動証明法が使えるよう,高階性を考慮して依存対法の理論を拡張した.具体的には,高階関数がない場合の停止性判定に有効な,簡約順序対や引き数選択の概念を,高階関数を許す単純型付き書き換えの体系に拡張で使えるようにした.関数変数を具体化する際に,同じ型の項に対する引き数選択の同期をとる必要があることなどを明らかにした.得られた理論的成果に基づいて,関数型プログラムの停止性を自動証明するための検証システムを試作し,その性能を評価した.比較的小規模なプログラムから構成される122個の例題のうち,117個(96%)の停止性の自動証明に成功した.