2005 Fiscal Year Annual Research Report
リダクションの近似に基づくプログラム検証手法の研究
| Project/Area Number |
14580357
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 東北大学, 電気通信研究所, 助教授 (00293390)
菊池 健太郎 東北大学, 電気通信研究所, 助手 (40396528)
|
|---|
| Keywords | リダクションシステム / 必須リダクション / 正規保存近似 / 正規化戦略 |
|---|
| Research Abstract |
リダクションの近似による関数型プログラムの正規化戦略の解析は、プログラムの評価メカニズムの設計に不可欠な技術である。とくに、HeutとLevy(1979)によって直交項書き換えシステムの必須リダクションが正規化戦略であることが示されて以来、リダクションの近似による計算可能な正規化戦略の研究は直交項書き換えシステムに対して活発に進められてきた。例えば、強シーケンシャル近似、NV近似、右線形増加近似、増加近似などは、代表的な計算可能なリダクション近似である。しかし、これらの近似に基づく計算可能な正規化戦略は、項書き換えシステムが直交している場合にしか有効には働かない。
本研究では、項書き換えシステムの直交条件を取り除いても、計算可能な正規化戦略が実現可能な十分条件を明らかにしている。これは、従来の結果を拡張しており、プログラムのより強力な評価メカニズムの実現を可能としている。鍵となるアイディアは、バランス弱合流性という概念である。バランス弱合流性をもつリダクションシステムは、システム全体が合流性を持たない場合でも、正規性が保証されている。したがって、リダクション戦略がバランス弱合流性をみたすことを示せば、リダクション戦略は正規化戦略となることが保証される。
直交条件をみたさない項書き換えシステムの危険対がバランス弱合流であるなら、外的リダクションは正規化戦略となることが示された。また、外的リダクションが計算可能なリダクション戦略となるためには、正規保存近似によってリダクションの近似を求めればよいことも明らかにできた。
|
