| 研究概要 |
プログラムの時間効率がどれくらいなのかを解析することは、プログラムを解析する上での中心的なテーマである。仮に探索アルゴリズムやソートアルゴリズムを開発したとする。そのとき時間的計算量、すなわち「入力の大きさに対しどれくらいの速度(ステップ数)で動作するか」という自然な疑問が生じる。本研究の目的はこの計算量を自動解析する手法を確立することであり、本年度は重差原理の研究とUncurrying変換の研究が課題であった。
まず重差原理の研究から、1970年に導入されたKnuth-Bendix順序が要求する探索空間が実は有限であることが判明した。この順序は定理証明システムに広く採用されている停止性証明の手法であり、この順序を用いるには関数記号から自然数への適切な写像を見つける必要がある。本研究により入力の項書き換え系のサイズをnとした場合、{0,…,2^(2^n)}への写像で全ての場合が網羅されることが証明された。この成果は国際論文誌JARに掲載された。
Uncurryingは関数型プログラムの項構造の変換手法であり、変換後の計算量解析は容易である。本研究では変換後のプログラムが最内停止性を持つなら元のプログラムの最内停止性が結論できること(健全性)、しかし驚くべきことにその逆(完全性)は成立しないことを証明した(full strategyでは完全だった)。またfull strategyでは多項式計算量が変換前後で保存されることを明らかにした。この成果は計算量自動解析ツールTCTやCaTに採用されている。これらの成果をまとめた論文は国際ワークショップHORに受理された。
|
