2005 Fiscal Year Annual Research Report
高階関数を用いたプログラム検証および変換技術の高度化に関する研究
| Project/Area Number |
17700002
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
青戸 等人 東北大学, 電気通信研究所, 助教授 (00293390)
|
|---|
| Keywords | 項書き換えシステム / 単純型付き項書き換えシステム / 停止性 / 高階書き換えシステム / プログラム変換 / 帰納的定理証明 / 変換パターン |
|---|
| Research Abstract |
第一階項書き換えシステムの停止性に対する強力な自動証明法として依存対法が知られている.この手法を拡張し,単純型付き項書き換えシステムの停止性を自動証明するための方法を考案した.このために,まず,依存対や推定依存グラフなど,依存対法の基本的な概念を単純型付き項書き換えシステムにおいて定式化した.また,広川ら(RTA,2004)による部分項条件による停止性証明を適用するために,頭部具体化法を考案した.これにより高階関数がある単純型付き項書き換えシステムの停止性証明が取り扱い可能となる。この新手法により単純型付き項書き換えシステムの停止性を自動証明するプロトタイプシステムの開発・実装を行なった.最後に,単純型付き項書き換えシステムの停止性証明法を評価するために,サンプル集を作成し,新手法と従来の第一階項書き換えシステムへの変換を経由する停止性証明法との比較を行った。
一方,ラムダ計算に基づくプログラム変換の理論を項書き換えシステムに導入するため,Huet(1978)によるパターンに基づくプログラム変換を項書き換えシステムの枠組みを用いて定式化した.そして,項書き換えシステムをベースにした枠組みでは,項書き換えシステムの帰納的等価性を応用することにより,プログラム変換の正当性の検証が可能となることを明らかにした.次にプログラム変換パターンについて発展的という概念を導入し,発展的変換パターンに基づくプログラム変換について,その正当性の自動検証法を考案した.これには,項書き換えシステムの帰納的定理証明法および十分完全性や合流性等の性質の自動検証法を応用する.最後に,この手法に基づくプログラム変換およびその正当性の自動検証を行うプロトタイプシステムを開発・実装し,プログラム自動変換の実験を行なった.
以上の結果は査読付きの国際会議録において採録され、報告を行っている.
|
