惰性求值和分隔控制
Lazy Evaluation and Delimited Control
摘要：
按需调用λ演算提供了一个等式框架，用于从语法上推理惰性求值。本文探讨了其业务特点。通过一系列的推理步骤，我们系统地解开了微积分的标准阶约简关系，发现了一个新的抽象机器定义，它和微积分一样，也是"在逻辑之下"的。“我们证明了机器评估等价于标准阶评估。与传统的抽象机器不同，定界控制在机器的行为中起着重要的作用。特别地，机器用使用基于控件的效果的评估堆栈的有纪律的管理来代替使用基于存储的效果的堆的操纵。简而言之，国家被控制所取代。为了进一步阐明这一观察结果，我们提出了一个模拟的调用需要在调用的值的语言使用分隔的控制操作。
英文摘要：
The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics. By a series of reasoning steps, we systematically unpack the standard-order reduction relation of the calculus and discover a novel abstract machine definition which, like the calculus, goes "under lambdas." We prove that machine evaluation is equivalent to standard-order evaluation. Unlike traditional abstract machines, delimited control plays a significant role in the machine's behavior. In particular, the machine replaces the manipulation of a heap using store-based effects with disciplined management of the evaluation stack using control-based effects. In short, state is replaced with control. To further articulate this observation, we present a simulation of call-by-need in a call-by-value language using delimited control operations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
