|
本年度は、昨年度に引き続いて基礎理論の確立を行うとともに、継続計算の直接実装に向けての研究を開始し、以下のような成果を得た。
・多相性の入った部分継続の型システムを定義し、それに対して各種の性質を証明した。具体的には、型システムの健全性、最も一般的な型と型推論アルゴリズムの存在、そして強正規化性などである。作成した型システムには、不動点演算子や条件分なども含んでおり、ほぼ、普通のプログラミング言語と考えることができる。これにより、継続計算においても他のプログラミング言語と同様の多相性が確立された。なお、ここで提案している多相性は、従来の値制約と同様の制約があるが、従来の制約よりはやや弱い制約ですむことも示した。また、多相性の入った継続計算に対しても、自然にCPS変換を定義することができることを示した。
・型システムの健全性については、Isabelle/HOLを使って証明する予定であったが、Isabelle/HOLのNominalパッケージでは、名前の付け替え問題に完全に対応するためには問題が残っていることがわかった。そこで、別の定理証明系であるCoqを用いて、最近発表されたlocally nameless手法を使って証明を完成させた。ここでの証明は、継続を含まない体系に対する証明を拡張した形になっており、継続が入ってもlocally namelessの手法が有効であることが示された。
・Danvyらの提案するfunctional derivationの手法を継続計算に適用した。その結果、まだいろいろな部分で研究が必要だが、この手法が継続計算の直接実装に関して有効そうである感触を得た。次年度も引き続きこの手法の研究を行う予定である。
|
