带 J 算子的 Landin SECD 机器的理性解构
编程语言
2015-07-01 v2 计算机科学中的逻辑
摘要
Landin 的 SECD 机器是第一个用于应用表达式（即函数式程序）的抽象机器。Landin 的 J 算子是函数式语言的第一个控制算子，并通过 SECD 机器的扩展来定义。我们提出了一系列对应于 SECD 机器这种扩展的求值函数，使用了一系列基本转换（主要是转换为延续传递风格 (CPS) 和去函数化）及其左逆运算（转换为直接风格和重新函数化）。为此，我们将 SECD 机器现代化为与原机器同步运行但 (1) 不使用数据栈且 (2) 对环境使用调用者保存而非被调用者保存约定的互似机器。我们还发现 SECD 机器的转储组件是以被调用者保存方式管理的。现代化 SECD 机器的调用者保存对应物精确对应于 Thielecke 的双管延续和 Felleisen 用 call/cc 对 J 的编码。然后，我们用 CPS 和 CPS 层次结构中的定界控制算子来多方面刻画 J 算子。作为副产品，我们还基于 Curien 最初的显式替换演算，提出了几种带 J 算子的应用表达式的归约语义。这些归约语义在机制上对应于 SECD 机器的现代化版本，并且据我们所知，它们提供了带 J 算子的应用表达式的首个句法理论。
引用
@article{arxiv.0811.3231,
title = {A Rational Deconstruction of Landin's SECD Machine with the J Operator},
author = {Olivier Danvy and Kevin Millikin},
journal= {arXiv preprint arXiv:0811.3231},
year = {2015}
}