Linear-Time Self-Interpretation of the Pure Lambda Calculus
Linear-Time Self-Interpretation of the Pure Lambda Calculus
复制标题
纯 Lambda 演算的线性时间自我解释
DOI：
10.1023/a:1010058213619
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Torben Æ. Mogensen
中科院分区：
文献类型：
--
作者：
Torben Æ. Mogensen
我们证明了纯无类型 lambda 演算的线性时间自解释是可能的，因为与各种执行模型下的直接执行相比，解释具有恒定的开销。本文展示了在按名称调用、按值调用和按需要调用的情况下还原为弱头范式的结果。我们使用基于先前对纯无类型 lambda 演算的自解释和部分评估工作的自解释器。我们使用操作语义来定义每个还原策略。对于每一个，我们都展示了一个模拟引理，该引理指出，通过操作语义评估术语的每个推理步骤都是通过应用于该术语的自解释器评估的一系列步骤来模拟的（使用相同的操作语义）。通过将成本分配给操作语义中的推理规则，我们可以比较正常评估和自我解释的成本。使用三种不同的成本度量：β-缩减的数量、基于替换的实现的成本（类似于图缩减）和基于环境的实现的成本。对于按需调用，我们使用非确定性语义，这大大简化了证明。
We show that linear-time self-interpretation of the pure untyped lambda calculus is possible, in the sense that interpretation has a constant overhead compared to direct execution under various execution models. The present paper shows this result for reduction to weak head normal form under call-by-name, call-by-value and call-by-need.We use a self-interpreter based on previous work on self-interpretation and partial evaluation of the pure untyped lambda calculus.We use operational semantics to define each reduction strategy. For each of these we show a simulation lemma that states that each inference step in the evaluation of a term by the operational semantics is simulated by a sequence of steps in evaluation of the self-interpreter applied to the term (using the same operational semantics).By assigning costs to the inference rules in the operational semantics, we can compare the cost of normal evaluation and self-interpretation. Three different cost-measures are used: number of beta-reductions, cost of a substitution-based implementation (similar to graph reduction) and cost of an environment-based implementation.For call-by-need we use a non-deterministic semantics, which simplifies the proof considerably.