Landin的SECD机的J算子理性解构
A Rational Deconstruction of Landin's SECD Machine with the J Operator
摘要：
Landin的SECD机器是第一个应用表达式的抽象机器，即，功能程序。Landin的J运算符是函数式语言的第一个控制运算符，由SECD机的扩展指定。我们提出了一个家庭的评价功能，对应于此扩展的SECD机，使用一系列的基本变换（转换成连续传递风格（CPS）和defunctionalization，主要）和他们的左逆（转换成直接风格和refunctionalization）。为此，我们将SECD机器现代化为与原始机器同步操作的双相似机器，但（1）不使用数据堆栈，（2）使用调用者保存而不是环境中的被调用者保存约定。我们还发现，SECD机器的转储组件是以被调用方保存的方式管理的。现代化的SECD机器的呼叫者保存对应物精确地对应于Thielecke的双管延续和Felleisen在call/cc方面对J的编码。然后，我们不同的特点J运营商的CPS和CPS层次中的定界控制运营商。作为一个副产品，我们还提出了几个约简语义与J运算符的应用表达式，基于Curien的显式替换的原始演算。这些减少语义机械对应的现代化版本的SECD机，并尽我们所知，他们提供了第一个句法理论的应用表达式与J运营商。
英文摘要：
Landin's SECD machine was the first abstract machine for applicative expressions, i.e., functional programs. Landin's J operator was the first control operator for functional languages, and was specified by an extension of the SECD machine. We present a family of evaluation functions corresponding to this extension of the SECD machine, using a series of elementary transformations (transformation into continu-ation-passing style (CPS) and defunctionalization, chiefly) and their left inverses (transformation into direct style and refunctionalization). To this end, we modernize the SECD machine into a bisimilar one that operates in lockstep with the original one but that (1) does not use a data stack and (2) uses the caller-save rather than the callee-save convention for environments. We also identify that the dump component of the SECD machine is managed in a callee-save way. The caller-save counterpart of the modernized SECD machine precisely corresponds to Thielecke's double-barrelled continuations and to Felleisen's encoding of J in terms of call/cc. We then variously characterize the J operator in terms of CPS and in terms of delimited-control operators in the CPS hierarchy. As a byproduct, we also present several reduction semantics for applicative expressions with the J operator, based on Curien's original calculus of explicit substitutions. These reduction semantics mechanically correspond to the modernized versions of the SECD machine and to the best of our knowledge, they provide the first syntactic theories of applicative expressions with the J operator.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
