Improvement in a lazy context: an operational theory for call-by-need
Improvement in a lazy context: an operational theory for call-by-need
复制标题
惰性上下文中的改进：按需调用的操作理论
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
David Sands
中科院分区：
文献类型：
--
作者：
Andrew Moran;David Sands
惰性函数语言的标准实现技术是按需调用，这确保任何给定调用中函数的参数最多被评估一次。按需调用的一个重要问题是，即使对于编译器编写者来说，也很难预测程序转换的效果。惰性函数语言的传统理论基于按名称调用模型，并且无法帮助确定哪些转换确实可以优化程序。在本文中，我们提出了一种基于程序改进排序的按需要调用的操作理论：如果在所有程序上下文 C 中，当 C[M] 终止，那么 C[N] 至少同样便宜地终止，则 M 改进 N。我们证明这种改进关系满足“上下文引理”，并支持丰富的不等式理论，包含 Ariola 等人的按需调用 lambda 演算。 [原子力显微镜+95]。基于归约的按需调用演算作为惰性程序转换的理论是不够的，因为它们只允许将程序加速至多一个常数因子的转换（我们证实了这一说法）；我们通过提供强大的递归证明规则，超越了各种基于约简的按需调用计算，包括句法连续性——定点归纳式推理的基础，以及适合论证基于递归的程序转换的正确性和安全性的改进定理。
The standard implementation technique for lazy functional languages is call-by-need, which ensures that an argument to a function in any given call is evaluated at most once. A significant problem with call-by-need is that it is difficult -- even for compiler writers -- to predict the effects of program transformations. The traditional theories for lazy functional languages are based on call-by-name models, and offer no help in determining which transformations do indeed optimize a program.In this article we present an operational theory for call-by-need, based upon an improvement ordering on programs: M is improved by N if in all program-contexts C, when C[M] terminates then C[N] terminates at least as cheaply.We show that this improvement relation satisfies a "context lemma", and supports a rich inequational theory, subsuming the call-by-need lambda calculi of Ariola et al. [AFM+95]. The reduction-based call-by-need calculi are inadequate as a theory of lazy-program transformation since they only permit transformations which speed up programs by at most a constant factor (a claim we substantiate); we go beyond the various reduction-based calculi for call-by-need by providing powerful proof rules for recursion, including syntactic continuity -- the basis of fixed-point-induction style reasoning, and an improvement theorem, suitable for arguing the correctness and safety of recursion-based program transformations.