|
関数型プログラミング言語のコンパイラなどで用いられるプログラム変換の正当性について研究を行った。特に、本研究では、プログラム変換がプログラムの性能に及ぼす影響について考慮し、性能に関して正当であることを示す研究を行った。
まず、値呼び出しの関数型プログラミング言語のコンパイラで用いられるCPS変換が、プログラムの実行に必要な記憶領域の大きさを定数倍の範囲で保存することを示した。これまで、プログラムの実行に必要な記憶領域に関して理論的に扱った研究はほとんどなく、このような性質の証明は、困難であると考えられていた。しかし、この研究では、reference(書き換え可能な値)を考慮したMLの型システムの健全性の証明の手法を応用することで、見通しの良い証明を与えることができた。
コンパイラなどで利用されるプログラム変換は、上のCPS変換のように良い性質(性能を定数倍の範囲で保存する)ものだけではない。多くの場合にプログラムを効率を良くするために、特殊な場合にはプログラムの効率を悪くする変換も用いられる。このような変換に関しては、最悪の場合の効率を保証することが重要だと思われる。本研究では、性能に関する正当性の条件として、プログラム変換による最悪の場合の性能の悪化の割合が、プログラムの大きさの多項式で抑えられるという条件を提案した。さらに、この条件に関して幾つかの基本的な性質を示し、A-normal変換の呼ばれるプログラム変換が、スタック空間の大きさについて、この条件を満たすことを示した。
|
