コントロール・オペレータの計算系とプログラム合成

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

(1)前年度までの本研究で得た多重タグを持つ部分継続に対応する型理論的体系を洗練し,CPS変換を与えた.Aarhus大学(Denmark)のOlivier Danvy,Andrzej Filinski氏ら継続/部分継続の研究者と研究討論を行い、彼らの定式化と本研究の定式化について比較検討した.この結果、簡潔なCPS変換を得る事が適切な定式化の鍵である、との共通認識を得た。(2)新しい計算系の定式化としての部分継続の理解ではなく、論理的基礎の固まっている体系から部分継続の理解を得る事が可能ではないか、との着想を得て、体系を再度検討した。この結果、catch/throw体系やλμ計算など既存の古典論理的体系を基礎として、ある種の部分継続を説明できる事を発見した。この手法により説明がつくコントロール・オペレータは、既存のDanvy-Filinskiのshift/resetオペレータと完全には一致するものではないが、shiftオペレータが1回しかあらわれない場合には、完全に一致する意味論を持つ事を示した。多くの部分継続の使用例では、shiftオペレータはただ1回しか使われないか、あるいは、ただ1回しか使われない形に書き換え可能であるので、本研究は、かなり広い範囲の部分継続の使用例を確固とした論理の立場から説明しているものといえる。(3)上記の論理的説明から合流性、強正規化可能性などの性質を得る事ができた。また、簡潔なCPS変換も(論理体系に対するものとして、自動的に)得られる。さらに、これら全ての性質が2階論理に対しても(自動的に)得られている、という点は特筆すべきものである。(4)上記成果を、IFIP TCS2000とACM CW'01という2回の国際会議で発表した。