Normalization by Evaluation for the Computational Lambda-Calculus
Normalization by Evaluation for the Computational Lambda-Calculus
复制标题
通过计算 Lambda 演算的评估进行归一化
DOI：
10.1007/3-540-45413-6_15
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Andrzej Filinski
中科院分区：
文献类型：
--
作者：
Andrzej Filinski
我们展示了如何将λβη演算通过赋值对规范化的简单语义刻画扩展到计算λ演算中术语的规范化的类似构造。具体地说，我们证明了基类型、常量和计算效果的适当剩余解释允许我们从术语的表示中提取句法范式。所需的解释本身可以被构造为类似ML的语言中适当的函数式程序的含义，从而直接导致实际的规范化算法。结果很容易扩展到乘积和和类型，并且可以被视为按值调用类型导向的部分计算的正式基础。
We show how a simple semantic characterization of normalization by evaluation for the λβη-calculus can be extended to a similar construction for normalization of terms in the computational λ-calculus. Specifically, we show that a suitable residualizing interpretation of base types, constants, and computational effects allows us to extract a syntactic normal form from a term's denotation. The required interpretation can itself be constructed as the meaning of a suitable functional program in an ML-like language, leading directly to a practical normalization algorithm. The results extend easily to product and sum types, and can be seen as a formal basis for call-by-value type-directed partial evaluation.