| 研究概要 |
本研究の目的は、制御演算子(コントロール・オペレータ)を持つ計算系を型理論および論理の視点から観察することにより,その妥当な定式化や意味についての理論を展開すること、および、その理論に基づき,仕様を表す論理式が与えられた時,その仕様を満たす,制御演算子を持つ関数型プログラムを作成するという手法へ応用することである。前年度の本研究では、『限定継続』と呼ばれる制御演算子の健全かつ完全な公理化を行ったが(発表は本年度)、本年度はこれをさらに拡張して、『多レベルの限定継続』の計算体系について検討を行った。その結果、(1)限定継続演算子を持つプログラムを組み合わせて大きなソフトウェアを構成する場合において、前年度に扱った単純な限定継続では問題があること、(2)この問題は、多レベルの限定継続を使うと解消されること、(3)多レベルの限定継続に対する健全かつ完全な公理体系が前年度の公理体系の拡張として得られること、の3点の成果を得た。特に、健全かつ完全な公理については、レベル2やレベル3という個別の場合だけでなく、任意のレベルに対する公理化を完成したという意味で、本研究が当初目的としていた目標を完全に達成することができた。このほか、メタ変数の取り扱いについても従来の体系にはない代入(textual substitution)を持つ体系の定式化に成功し、この2つの成果を合わせることにより、部分計算やCPS変換など、プログラムをデータとして扱うプログラムの検証を行うことが可能になった。
|
