2006 Fiscal Year Annual Research Report
型付き項書換え系の変換に基づく関数型プログラムの自動検証
| Project/Area Number |
18700007
|
|---|
| Research Institution | Mie University |
|---|
Principal Investigator |
山田 俊行 三重大学, 大学院工学研究科, 講師 (60312831)
|
|---|
| Keywords | 型付き項書き換え / 関数プログラム / 自動検証 |
|---|
| Research Abstract |
書き換え理論において近年注目されている自動証明向き停止性判定法として,依存対法という手法が知られている.この停止性証明法は,十分広いクラスの書き換え系に対して,効率的で強力な自動判定のできる手法であるが,高階関数のあるプログラムに対して適用範囲が限られていた.高階関数とは,データとして関数を受け渡しできる関数であり,プログラムの汎用性を高めるための,関数型言語の本質的な機能の1つである.そこで,より広範囲のプログラムに対して,書き換えによる停止性自動証明法が使えるよう,高階性を考慮して依存対法の理論を拡張した.具体的には,高階関数がない場合の停止性判定に有効な,簡約順序対や引き数選択の概念を,高階関数を許す単純型付き書き換えの体系に拡張で使えるようにした.関数変数を具体化する際に,同じ型の項に対する引き数選択の同期をとる必要があることなどが明らかになった.
また,関数プログラムの等しさを,振る舞いの等価性に基づいて検証するための基礎理論について考察を深めた.関数プログラムの単純型付き等式の集合としてとらえると,これをソート付き1階等式系に変換することで,従来の等式論理に基づく定理証明の豊富な知見が活用できるようになる.今年度は,振る舞いの等価性や非等価性を保証するための十分条件を明らかにした.無予盾性や強完全性などの条件をどこまで自動証明できるかを考察することが残された課題である.
さらに,書き換えによる合流可能性や到達可能性の決定可能性と決定不能性についても,従来研究が十分でなかったmonadic項書換え系やsemi-constructor項書換え系のクラスに対する新たな結果を得た.この研究結果は,停止性や単一化問題など,プログラム検証のための基本性質の決定アルゴリズムとしての利用が期待できる.
|
