| 研究概要 |
本研究の目的は、制御演算子(コントロール・オペレータ)を持つ計算系を型理論および論理の視点から観察することにより,その妥当な定式化や意味についての理論を展開すること、および、その理論に基づき,仕様を表す論理式が与えられた時,その仕様を満たす,制御演算子を持つ関数型プログラムを作成するという手法へ応用することである。この研究では、制御演算子の中で特に『限定継続』と呼ばれる制御演算子について検討を深め、等式論理に基づいて健全かつ完全な公理化を行った。この公理系は従来の無制限の(範囲を限定できない)継続演算子に対する公理化の保守的拡張となっており、また、拡張部分の公理は冗長でないことまで示した。これにより、限定継続演算子の基礎理論を確立することができ、限定継続演算子を持つプログラムの検証が可能であることを示した。さらに、この結果を『多レベルの限定継続』の計算体系に拡張することに成功し、驚くほど少ない数の公理によって多レベルの限定継続演算子が特徴つけられることを示した。
このほか、限定継続計算がメタレベルの制御フローをとらえるものであるのと同様に、メタレベルの変数束縛をとらえる計算機構についても研究を行い、従来の体系にはない代入(textual substitution)を持つ体系の定式化に成功し、この2つの成果を合わせることにより、部分計算やCPS変換など、プログラムをデータとして扱うプログラムの検証を行うことが可能になった。
|
