| 研究課題/領域番号 |
14580357
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究分担者 |
青戸 等人 東北大学, 電気通信研究所, 助教授 (00293390)
菊池 健太郎 東北大学, 電気通信研究所, 助手 (40396528)
|
|---|
| 研究期間 (年度) |
2002 – 2005
|
| キーワード | リダクションシステム / 必須リダクション / 正規保存近似 / 正規化戦略 / 外延リダクション / バランス弱合流性 |
|---|
| 研究概要 |
リダクションの近似によるプログラム検証手法の基礎を確立する目的で、リダクションの正規化戦略、変換パターンに基づくプログラム等価変換、高階システムの停止性、高階帰納的定理の自動証明、到達可能性の決定可能性について研究し、理論解析と実験をとおして以下の成果を得た。
(1)バランス弱合流性という概念に基づくリダクション戦略を提案した。左線形の項書き換えシステムの危険対が弱合流性をみたせば、外延リダクションが正規化戦略となることを明らかにした。これは、従来知られていた必須リダクションの正規化戦略を拡張しており、重なりのある項書き換えシステムに対しても適用可能である。また、正規保存近似によってリダクションを近似することで、外延リダクションが計算可能なリダクション戦略となることを示した。
(2)変換パターンに基づく書き換えシステムの等価変換の理論を与え、それに基づくプログラム変換システムの提案を行った。ここで開発された手法は、潜在帰納法をもちいてデータ構造に基づくプログラムの帰納的性質を導いており、自動証明システムと組み合わせることで高度なプログラムの等価変換が可能となる。
(3)書き換えシステムの正規化戦略の近似を理論的に解析し、従来知られていた強シーケンシャル近似、NV近似、右線形増加近似よりも強力な増加近似を提案した。この近似によって、これまでは困難であった広いクラスの書き換えシステムに対して正規化戦略を与えることが可能となった。さらに、増加近似が正規保存近似であることを利用して、書き換えシステムの合流性や停止性が決定可能となるクラスを明らかにした。
|
