A sound and complete axiomatization of delimited continuations
A sound and complete axiomatization of delimited continuations
复制标题
定界延续的健全且完整的公理化
DOI：
10.1145/944705.944722
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Masahito Hasegawa
中科院分区：
文献类型：
--
作者：
Yukiyoshi Kameyama;Masahito Hasegawa
由Danvy和Filinski提出的移位和复位操作符是用于捕获定界连续的强大控制原语。定界延拓是一个类似于标准（无限）延拓的概念，但它代表了剩余计算的一部分，而不是整个剩余计算。在文献中，移位和复位的语义已经给出了一个CPS翻译。本文给出了带移位和复位的微积分的一个直接公理化，即引入一组方程，并证明了它关于CPS-平移是可靠的和完备的。我们还介绍了一个演算与控制运营商，这是表达的演算与移位和复位，有一个健全的和完整的公理化，是保守的Sabry和Felleisen的理论为第一类的延续。
The shift and reset operators, proposed by Danvy and Filinski, are powerful control primitives for capturing delimited continuations. Delimited continuation is a similar concept as the standard (unlimited) continuation, but it represents part of the rest of the computation, rather than the whole rest of computation. In the literature, the semantics of shift and reset has been given by a CPS-translation only. This paper gives a direct axiomatization of calculus with shift and reset, namely, we introduce a set of equations, and prove that it is sound and complete with respect to the CPS-translation. We also introduce a calculus with control operators which is as expressive as the calculus with shift and reset, has a sound and complete axiomatization, and is conservative over Sabry and Felleisen's theory for first-class continuations.