On the Transformation between Direct and Continuation Semantics
On the Transformation between Direct and Continuation Semantics
复制标题
论直接语义与延续语义的转换
DOI：
10.1007/3-540-58027-1_31
复制
发表时间：
1993
期刊：
影响因子：
--
通讯作者：
J. Hatcliff
中科院分区：
文献类型：
--
作者：
O. Danvy;J. Hatcliff
考虑到直接样式的λ术语可以自动转换为连续样式，证明直接语义和延续语义之间的一致性通常令人惊讶地复杂。然而，将直接样式语义的表示转换为延续样式通常不会产生预期的延续样式语义表示(即手工编写的语义)，我们的工作的目标是自动化直接语义的文本表示和延续语义的文本表示之间的转换。本质上，我们确定直接样式表示的属性(例如，总体)，并相应地将转换概括为延续样式。因此，我们可以自动生成预期的延续语义表示形式。理解直接语义和延续语义的表示之间的转换很重要，因为正是这些表示在任何类型的基于语义的程序操作(例如，编译、编译器生成和部分求值)中得到处理。在编程语言工作台中，生成各种延续样式表示的工具是一个有价值的新工具。
Proving the congruence between a direct semantics and a continuation semantics is often surprisingly complicated considering that direct-style λ-terms can be transformed into continuation style automatically. However, transforming the representation of a direct-style semantics into continuation style usually doesnotyield the expected representation of a continuation-style semantics (i.e., one written by hand).The goal of our work is to automate the transformation between textual representations of direct semantics and of continuation semantics. Essentially, we identify properties of a direct-style representation (e.g., totality), and we generalize the transformation into continuation style accordingly. As a result, we can produce the expected representation of a continuation semantics, automatically. It is important to understand the transformation between representations of direct and of continuation semantics because it is these representations that get processed in any kind of semantics-based program manipulation (e.g., compiling, compiler generation, and partial evaluation). A tool producing a variety of continuation-style representations is a valuable new one in a programming-language workbench.