Incremental reduction in the lambda calculus
Incremental reduction in the lambda calculus
复制标题
lambda 演算的增量减少
DOI：
10.1145/91556.91679
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
T. Teitelbaum
中科院分区：
文献类型：
--
作者：
J. Field;T. Teitelbaum
<italic>增量</italic>算法是一种利用其计算的函数将在彼此仅略有不同的输入上重复计算的事实的算法，从而避免了不必要的共同计算的重复。
本文在无类型λ演算中定义了一个新的约简增量概念，并给出了一个增量约简算法Λ<supscrpt>inc</supscrpt>.我们表明，Λ<supscrpt>inc</supscrpt>具有理想的性能，执行<italic>非重叠</italic>减少相关条款，但足够简单，允许一个实际的实施。该算法基于一种新的λ-约简策略，该策略在非增量设置中也可能被证明是有用的。
增量λ-约简可以在任何以函数或应用方式指定算法的设置中使用。
An <italic>incremental</italic> algorithm is one that takes advantage of the fact that the function it computes is to be evaluated repeatedly on inputs that differ only slightly from one another, avoiding unnecessary duplication of common computations.
We define here a new notion of incrementality for reduction in the untyped λ-calculus and describe an incremental reduction algorithm, Λ<supscrpt>inc</supscrpt>. We show that Λ<supscrpt>inc</supscrpt> has the desirable property of performing <italic>non-overlapping</italic> reductions on related terms, yet is simple enough to allow a practical implementation. The algorithm is based on a novel λ-reduction strategy that may prove useful in a non-incremental setting as well.
Incremental λ-reduction can be used to advantage in any setting where an algorithm is specified in a functional or applicative manner.