一句话:提出可扩展存储的演算,为带全局环境的 call-by-need 抽象机及其 CPS 翻译提供形式化基础。
call-by-need 是 λ-演算的一种惰性求值策略:只在需要时求值参数,并在所有使用处共享计算结果。实现该策略的抽象机通常需要某种全局环境。抽象机有助于理解执行过程中的控制流,尤其便于定义 continuation-passing style(CPS)翻译;然而,带有全局环境的抽象机在形式上更为微妙。本文提出一种可扩展存储(expandable stores)的演算,旨在为这类 call-by-need 抽象机提供合适的演算刻画,从而更清晰地分析其控制流与 CPS 翻译。
The call-by-need evaluation strategy for the λ-calculus is an evaluation strategy that lazily evaluates arguments only if needed, and if so, shares computations across all places where it is needed. To implement this evaluation strategy, abstract machines require some form of global environment. While abstract machines usually lead to a better understanding of the flow of control during the execution, facilitating in particular the definition of continuation-passing style translations, the case of machines with global environments turns out to be much more subtle.