2004 Fiscal Year Annual Research Report
型付き項書き換え系の停止性自動証明とそのプログラム検証への応用
| Project/Area Number |
16700030
|
|---|
| Research Institution | Mie University |
|---|
Principal Investigator |
山田 俊行 三重大学, 工学部, 助手 (60312831)
|
|---|
| Keywords | 関数型プログラム / プログラム検証 / 単純型付き項書き換え系 / 帰納的定理 / 停止性 / 自動証明 |
|---|
| Research Abstract |
関数型のプログラム言語を対象とし,等式により記述されたプログラムの性質の正当性を自動証明する方法を研究した.関数型プログラムを扱う自動証明に適した計算の理論としては,単純型付き項書換え系を採用した.プログラムを,型付き項上の等式で記述された関数定義の集合としてとらえ,その実行を,定義に基づく式の書き換えととらえる.この定式化のもとでは,プログラムの性質は,関数定義の等式集合を公理とした帰納的定理に相当する.
そこで,まず,単純型付き項書き換え系における,帰納的定理の自動証明について研究した.関数の同等性を扱う際の帰納的定理である「高階帰納的定理」の概念を新たに導入し,帰納的定理を導くための十分条件を明らかにした.これにより,一階項書き換えの自動証明法として知られる潜在帰納法を,単純型付きの体系へと拡張できた.
さらに,プログラム検証や定理自動証明で重要な役割を果たす,書き換え系の停止性の自動証明法についても研究した.一階項書き換え系の停止性自動証明法として有効であることが知られている依存対の手法を,単純型付き項書き換え系向けに拡張した.依存対や推定依存グラフなどの基本概念を拡張し,高速な判定が可能な構文的な判定条件である部分項規準が,型付きの書き換え系に適用可能であることを明らかにした.また,関数型プログラムのための停止性証明システムを試作し,その有効性を実験により確認した.
|
