Closed reduction: explicit substitutions without $\alpha$-conversion
Closed reduction: explicit substitutions without $\alpha$-conversion
复制标题
封闭归约：无需 $alpha$ 转换的显式替换
DOI：
10.1017/s0960129504004633
复制
发表时间：
2005
影响因子：
0.5
通讯作者：
François
中科院分区：
文献类型：
--
作者：
M. Fernández;I. Mackie;François
从$\lambda$-演算的名称，我们开发了一个家庭的演算明确的替代，克服了通常的语法问题的替代。关键的思想是只有封闭的替换可以在某些构造中移动。这给出了一种弱形式的归约，称为闭合归约，它足够丰富，可以捕获$\lambda$-演算中的按值调用和按名称调用求值策略。此外，由于替换可以通过抽象移动，并且在抽象下允许约简（如果某些条件成立），因此封闭约简自然提供了一种具有高度共享和低开销的有效约简概念。我们提出了一个家庭的抽象机关闭减少。我们的基准测试表明，封闭约简比所有标准的弱策略表现得更好，其低开销使其在许多情况下比最优约简更有效。
Starting from the $\lambda$-calculus with names, we develop a family of calculi with explicit substitutions that overcome the usual syntactical problems of substitution. The key idea is that only closed substitutions can be moved through certain constructs. This gives a weak form of reduction, called closed reduction, which is rich enough to capture both the call-by-value and call-by-name evaluation strategies in the $\lambda$-calculus. Moreover, since substitutions can move through abstractions and reductions are allowed under abstractions (if certain conditions hold), closed reduction naturally provides an efficient notion of reduction with a high degree of sharing and low overheads. We present a family of abstract machines for closed reduction. Our benchmarks show that closed reduction performs better than all standard weak strategies, and its low overheads make it more efficient than optimal reduction in many cases.