A generic account of continuation-passing styles
A generic account of continuation-passing styles
复制标题
延续传递风格的通用说明
DOI：
--
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
O. Danvy
中科院分区：
文献类型：
--
作者：
J. Hatcliff;O. Danvy
我们在基于Moggi的计算元语言的通用框架中统一了之前关于延续传递样式（CPS）转换的工作。该框架用于获得各种评估策略的CPS转换，并描述相应的管理缩减和逆转换。我们建立了运算语义与方程理论之间的一般形式联系。特定求值顺序的转换的形式属性作为推论遵循。
We unify previous work on the continuation-passing style (CPS) transformations in a generic framework based on Moggi's computational meta-language. This framework is used to obtain CPS transformations for a variety of evaluation strategies and to characterize the corresponding administrative reductions and inverse transformations. We establish generic formal connections between operational semantics and equational theories. Formal properties of transformations for specific evaluation orders follow as corollaries.
Essentially, we factor transformations through Moggi's computational meta-language. Mapping λ-terms into the meta-language captures computation properties (e.g., partiality, strictness) and evaluation order explicitly in both the term and the type structure of the meta-language. The CPS transformation is then obtained by applying a generic transformation from terms and types in the meta-language to CPS terms and types, based on a typed term representation of the continuation monad. We prove an adequacy property for the generic transformation and establish an equational correspondence between the meta-language and CPS terms.
These generic results generalize Plotkin's seminal theorems, subsume more recent results, and enable new uses of CPS transformations and their inverses. We discuss how to aply these results to compilation.