高階関数を用いたプログラム検証および変換技術の高度化に関する研究
| Project/Area Number |
17700002
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
青戸 等人 Tohoku University, 電気通信研究所, 准教授 (00293390)
|
|---|
| Project Period (FY) |
2005 – 2007
|
| Project Status |
Completed (Fiscal Year 2007)
|
| Budget Amount *help |
¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 2007: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2006: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2005: ¥700,000 (Direct Cost: ¥700,000)
|
|---|
| Keywords | 項書き換えシステム / 高階関数 / 単純型付き項書き換えシステム / プログラム検証 / 書き換え帰納法 / プログラム変換 / パターン基づくプログラム変換 / 補題自動発見法 / 項群き換えシステム / 帰納的定理証明 / 高階書き換えシステム / 単純型付き書き換えシステム / 変換パターン / 補題自動発見 / 停止性 |
|---|
| Research Abstract |
単純型付き項書き換えシステムの停止性検証手法の高度化を以下の点について試みた。(1)依存対手法における引数フィルタリングおよび使用可能規則を高階の場合への拡張を行った。(2)実験システムについての検討を進めた。特に、効率的な実装を実現するためのSAT検証器を用いた実装法についての検討を行い、その基本となる経路順序の符号化法について改良を行った。また停止性にもとづく帰納的定理の自動証明法である書き換え帰納法についての検討を進めた。特に反証付き書き換え帰納法に適した補題自動導入法について検討を行った。発散鑑定法を改良し、健全性を持つ発散鑑定法を提案した。実験システムを実装するとともに証明システムのベンチマークとなる例題集を抽出し、他の書き換え帰納法に基づく定理証明器との比較実験を行った。また、反証付き書き換え帰納法を利用するために必要な合流性を保障する方法について検討を進めた。停止性の検証器は多数提案されているのに対して、合流性の検証器の提案はあまりなされていないため、合流性の自動検証法について実験システムを構築し検討を行った。合流性の十分条件を満たさない項書き換えシステムについて分解手法を用いる判定法を利用することの検討を行い、分解手法を利用した合流性検証器の提案を行った。変換パターンに基づくプログラム変換のための変換パターンの抽出法について検討をすすめた。2階の一般化アルゴリズムを提案し、それに基づいて具体的なプログラム変換から変換パターンを抽出する実験を行った。変換に利用可能なパターンの抽出を容易にするためのヒューリスティクスについて検討を行い、いくつかの変換パターンの抽出に成功した。
|
Report
(3 results)
Research Products
(6 results)
