Call-by-value Solvability
Call-by-value Solvability
复制标题
按值调用的可解性
DOI：
10.1051/ita:1999130
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
S. D. Rocca
中科院分区：
文献类型：
--
作者：
Luca Paolini;S. D. Rocca
从操作和逻辑的角度定义了按值调用λ -演算中的可解性概念，并对其进行了完整的刻画。通过一个归约机，根据最内层策略执行经典的β -归约，给出了操作特征。事实上，按值调用归约规则对于捕获项的可解性属性来说太弱了。逻辑特征是通过一个交集类型分配系统给出的，它将给定形状的类型分配给所有且仅分配给按值调用的可解项。
The notion of solvability in the call-by-value λ -calculus is defined and completely characterized, both from an operational and a logical point of view. The operational characterization is given through a reduction machine, performing the classical β -reduction, according to an innermost strategy. In fact, it turns out that the call-by-value reduction rule is too weak for capturing the solvability property of terms. The logical characterization is given through an intersection type assignment system, assigning types of a given shape to all and only the call-by-value solvable terms.