On the Value of Variables
On the Value of Variables
复制标题
论变量的值
DOI：
10.1007/978-3-662-44145-9_3
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
C. Coen
中科院分区：
文献类型：
--
作者：
Beniamino Accattoli;C. Coen
按值调用和按需要调用 l 演算是使用不同的值语法类别来定义的。在理论研究中，值是变量和抽象。在更实际的工作中，值通常被简单地定义为抽象。本文表明，一旦实现的通常假设保持条件成立，实用值就会导致更有效的替换过程（对于按值调用和按需求调用），减少不会进行抽象，并且替换会以微步骤完成，替换当时出现的一个变量。即，替换步骤的数量与β-氧化还原的数量成线性关系，而理论值仅提供二次界。
Call-by-value and call-by-need l-calculi are defined using the distinguished syntactic category of values. In theoretical studies, values are variables and abstractions. In more practical works, values are usually defined simply as abstractions. This paper shows that practical values lead to a more efficient process of substitution--for both call-by-value and call-by-need--once the usual hypothesis for implementations hold terms are closed, reduction does not go under abstraction, and substitution is done in micro steps, replacing one variable occurrence at the time. Namely, the number of substitution steps becomes linear in the number of β-redexes, while theoretical values only provide a quadratic bound.