| Budget Amount *help |
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 2003: ¥2,100,000 (Direct Cost: ¥2,100,000)
|
|---|
| Research Abstract |
完備化に基づくプログラム融合変換のアイデアを,高階プログラムに適用するためには,高階書き換えシステムの完備化を実現する必要がある。しかし,高階書き換えシステムの完備化手続きの多くは机上の提案にとどまっており,実装にはいたっていない。これは,完備化手続きを実装するために不可欠な高階書き換えシステムの停止性が,簡単に判定できなかったからである。
本研究では,項の幅の上界を設定することで,固定次数の関数記号に対する単純化順序の定義が,可変次数の関数記号に対してもそのまま有効に働くことに注目し,S式書き換えシステムの停止性が辞書式経路順序で簡単に判定できることを示した。実際に利用される高階書き換えシステムの多くは,S式書き換えシステムで表現できるため,ここで提案された停止性判定法をもちいて完備化可能である。我々は,S式書き換えシステムの完備化手続きを計算機上に実装し,高階書き換えシステムの完備化と融合変換が容易に実現できることを実験によって明らかにした。
さらに,本研究で目指している完備化に基づくプログラム変換の適用範囲を広げることを目的として,高階関数を含む帰納的定理の自動証明法を検討し,高階書き換えシステムにおける潜在帰納法の枠組みを提案するとともに,潜在帰納法の適用に不可欠な十分完全性の判定が決定可能であることを明らかにした。
また,書き換え代入に基づく2階のパターンマッチングを提案し,パターマッチングをもちいたプログラム変換手続きを改良するとともに,書き換え帰納法に基づく高階プログラムの融合変換の実験を行った。
|
