2005 Fiscal Year Annual Research Report
| Project/Area Number |
16016202
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 東北大学, 電気通信研究所, 助教授 (00293390)
菊池 健太郎 東北大学, 電気通信研究所, 助手 (40396528)
|
|---|
| Keywords | 情報基礎 / ソフトウェア検証 / プログラム変換 / 定理自動証明 / 項書き換えシステム |
|---|
| Research Abstract |
プログラム変換の手法である融合変換と、定理自動証明の手法である完備化を組み合わせた新しいプログラム変換手法を提案することを目的として、プログラム変換の実験と解析を行った。とくに、帰納的定理の強力な自動証明手法である書き換え帰納法と組み合わせることによって、プログラム変換に必要な性質を自動証明しながら、その結果を利用してプログラム変換を進めていくので、従来よりも強力な変換が可能となる。また、変換に必要な性質を自動的に発見することを可能とする補題発見機構を組み入れることにより、高度なプログラム自動変換を実現することができることを実証することができた。
さらに、パターンをもちいたプログラム変換システムRAPTを開発した。これまでの研究から、プログラムの効率化にはいくつかの定石があることが明らかになっている。そこで、これらの定石を高階の変換パターンで表現し、パターンマッチングによるプログラム変換で効率を改良する方法を提案した。変換の正当性を検証するためには、プログラムのさまざまな帰納的性質を証明する必要がある。そこで、プログラムを書き換えシステムでモデル化し、定理自動証明の手法である潜在帰納法を適用することにより、プログラム変換とその正当性の検証を完全に自動化することに成功した。RAPTは入力プログラムを自動変換して出力プログラムを得るまでの手続きを6段階に分けて実現している。実装は関数型言語SMLをもちいて行い、ソースコードのサイズは約5000行である。
また、プログラムの変換や検証に不可欠な基礎技術である高階プログラムの帰納的性質や停止条件に関する理論的な解析を進めるとともに、プログラムの実行メカニズムの設計に不可欠なリダクションの戦略に関する基礎理論の確立を行った。
|
