2006 Fiscal Year Annual Research Report
高階関数を用いたプログラム検証および変換技術の高度化に関する研究
| Project/Area Number |
17700002
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
青戸 等人 東北大学, 電気通信研究所, 助教授 (00293390)
|
|---|
| Keywords | 項群き換えシステム / 帰納的定理証明 / プログラム変換 / 高階書き換えシステム / 単純型付き書き換えシステム / 変換パターン / 補題自動発見 |
|---|
| Research Abstract |
自然数やリストなど,データ構造に基づくプログラムの性質の自動証明法として,項書き換えシステムの書き換え帰納法が知られている.この書き換え帰納法による証明手続きの正しさは,抽象原理に基づいて証明することが出来る.従来知られていた原理を拡張し,より強力な書き換え帰納法の証明手続きを提案した.この新しい証明手続きでは従来知られていたよりも一般的な単純化のための推論規則を備えている.また,順序付け不能な等式を扱うための新たな証明手続きの提案を行った.これらの改良により,より簡略な証明による自動証明の効率化や補題発見法と組み合わせによる新たな自動証明の成功などが期待される.順序付け不能な等式を扱うための証明手続きについては,項書き換えの国際会議にて報告を行った.
プログラム効率化のためのプログラム変換手法の1つとして,パターンによるプログラム変換が知られている.項書き換えに基づくパターンによるプログラム変換では、変換前後の操作的意味の不変性を項書き換えシステムの自動証明法を用いて保障することが出来る.この枠組みを実現した実験システムRAPTの実装を行い,RAPTを用いたプログラム自動変換実験を行った.基本的なプログラム変換およびその正当性について動作確認を行い,本手法の有効性を確認した.プログラム変換パターンの蓄積やプログラム変換例の一般化による変換パターンの抽出などが今後の課題として確認された.以上の,実験システムRAPTおよびにRAPTを用いたプログラム変換実験関する報告を書き換えシステムの国際会議において行った.項書き換えシステムの基づくプログラム変換の理論とその実験をとりまとめ,学術雑誌にて発表を行った.
|
