Linearly-Used Continuations in the Enriched Effect Calculus
Linearly-Used Continuations in the Enriched Effect Calculus
复制标题
丰富效应微积分中线性使用的延拓
DOI：
10.1007/978-3-642-12032-9_3
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
A. Simpson
中科院分区：
文献类型：
--
作者：
J. Egger;R. E. Møgelberg;A. Simpson
丰富效应演算是 Moggi 计算元语言的扩展，其中包含从线性逻辑中选择的原语。在本文中，我们提出了丰富效应演算中的扩展案例研究：延拓的线性用法。我们表明，已建立的按值调用和按名称调用线性使用的 CPS 翻译均由丰富效果演算自身的单个通用翻译统一捕获。作为一个主要的句法定理，我们证明了泛型翻译在同构上是内合的。作为推论，我们获得了原始按值调用和按名称调用翻译的完整完整性结果。主要句法定理是使用范畴论语义来证明丰富效果演算的。我们证明模型在自然的双模型构造下是封闭的。然后，规范线性使用的 CPS 翻译作为从句法初始模型到其自身对偶的唯一（直到同构）映射而出现。该地图是模型的等价物。因此初始模型是自对偶的。
The enriched effect calculus is an extension of Moggi's computational metalanguage with a selection of primitives from linear logic. In this paper, we present an extended case study within the enriched effect calculus: the linear usage of continuations. We show that established call-by-value and call-by name linearly-used CPS translations are uniformly captured by a single generic translation of the enriched effect calculus into itself. As a main syntactic theorem, we prove that the generic translation is involutive up to isomorphism. As corollaries, we obtain full completeness results for the original call-by-value and call-by-name translations. The main syntactic theorem is proved using a category-theoretic semantics for the enriched effect calculus. We show that models are closed under a natural dual model construction. The canonical linearly-used CPS translation then arises as the unique (up to isomorphism) map from the syntactic initial model to its own dual. This map is an equivalence of models. Thus the initial model is self-dual.