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

控制算子计算系统及程序综合

基本信息

批准号：
11780213
负责人：
亀山幸義
金额：
$ 1.54万
依托单位：
Kyoto University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1999
资助国家：
日本
起止时间：
1999 至 2000
项目状态：
已结题

项目摘要

(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回の国際会議で発表した。

（1）对对应于部分延续的类型理论系统，在本研究中获得了前一年的多个标签，并给出了CPS转换。我们与阿尔胡斯大学（丹麦）的奥利维尔·丹维（Olivier Danvy）和安德烈·菲林斯基（Andrzej Filinski）等研究人员进行了研究讨论，包括延续/部分延续的研究人员，并比较了他们的表述和这项研究的制定。结果，我们获得了共同的理解，即获得简洁的CPS转换是适当配方的关键。（2）我们重新审查了该系统，灵感来自于从具有坚实逻辑基础的系统中了解部分延续的想法，而不是理解部分延续作为新计算系统的表述。结果，我们发现可以根据现有的经典逻辑系统（例如捕获/投掷系统和λμ计算）来解释某些部分延续。通过此技术解释的控制操作员与现有的Danvy-Filinski Shift/Reset运算符不完全匹配，但表明，如果Shift Operator仅出现一次，则它们具有完全一致的语义。在大多数次要使用的用例中，可以将移位运算符重写为仅使用一次或仅一次使用的形式，因此可以从可靠的逻辑角度描述该研究。（3）上述逻辑解释已用于获得诸如汇合和强归一化之类的属性。此外，还获得了简单的CPS转换（自动与逻辑系统一样）。此外，值得注意的是，对于二阶逻辑，也（自动）获得了所有这些属性。（4）上述结果在两个国际会议上提出，IFIP TCS2000和ACM CW'01。