構成的プログラミングの手法による制御機構を持つプログラムの合成

点击翻译按钮获取中文摘要

関数型プログラミング言語におけるコントロールオペレータとして昨年度の研究では主としてキャッチスロー機構について研究を行ってきたが,今年度の研究では,より強力なオペレータとして部分継続に着目し,その定式化を行った.部分継続は,継続をより洗練した機構であり,通常の継続が「残りの計算の全て」を表すオブジェクトを抽象するのに対して,部分継続は「残りの計算の一部」を表すオブジェクトを抽象する.一部を指定するために,control del1miter(制御限定子)をプログラム中の任意の場所に設定することができる.本年度の研究では,部分継続を型理論の枠組みの中で定式化した.特に,継続限定子と部分継続オペレータの対が従来の研究では1種類の限定していた制限を除去し,複数の種類の対を使うことができるよう拡張した.ここで定式化した体系の性質を調べ,合流性や型の安全性など望ましい性質が満たされることを証明した.また,この体系がCurry-Howardの同型対応のもとで古典論理に対応することを示し,この体系を古典論理の証明からのプログラム抽出に用いることができることを示した.一方,プログラミングの観点からの成果としては,まず,この計算系の処理系(イシタープリタ)を作成し,さらに,この枠組みでのプログラミングの実例を蓄積した.特に,部分継続を用いてcoroutineを自然に表現できることを示し,二分木の走査関数を用いたsaome-fringe問題の効率的なプログラミング例を示した.