###
DOI:
Journal of Software:2008.19(10):2508-2516

传名调用演算的二值传递CPS变换
喻钢,柳欣欣
(中国科学院 软件研究所 计算机科学国家重点实验室,北京 100190; 中国科学院 研究生院,北京 100049)
Two Values Passing CPS Transformation for Call-by-Name Calculus with Constants
YU Gang,LIU Xin-Xin
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 3440   Download 2938
Received:January 29, 2007    Revised:August 03, 2007
> 中文摘要: 为Plotkin带常数传名调用(演算定义了一个新的CPS(continuation-passing-style)变换方法.方法基于求值上下文变换,新颖之处在于,每次传递二值给继续而不是常规的一值.先给出二值CPS变换编码,再在此基础上定义CPS语言,最后建立源语言和CPS语言的一一映射关系并证明Plotkin的模拟定理.与Plotkin的工作比较,工作特点在于,给出了一个CPS归约闭语言,该语言中所有继续都可以用函数形式表达,且模拟定理的可靠性和完备性方向证明更为简单.
Abstract:In this paper, a new CPS (continuation-passing-style) transformation for Plotkin's call-by-name ( calculus with constants is proposed. It is based on evaluation contexts transformation and the features that two values, instead of one, are passed to the continuation every time. With encodings, a CPS language is introduced. Then, Plotkin's simulation theorem is proved by establishing 1-to-1 correspondence between the source language and CPS language. Compared with Plotkin's work, a reduction closed CPS language is defined in which all continuations are explicitly expressed as functional encodings and it is simpler to prove both the soundness and completeness directions of simulation theorem.
文章编号:     中图分类号:    文献标志码:
基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60496321, 60673045 (国家自然科学基金) Supported by the National Natural Science Foundation of China under Grant Nos.60496321, 60673045 (国家自然科学基金)
Foundation items:
Reference text:

喻 钢,柳欣欣.传名调用演算的二值传递CPS变换.软件学报,2008,19(10):2508-2516

YU Gang,LIU Xin-Xin.Two Values Passing CPS Transformation for Call-by-Name Calculus with Constants.Journal of Software,2008,19(10):2508-2516