An inverse of the evaluation functional for typed lambda -calculus
An inverse of the evaluation functional for typed lambda -calculus
复制标题
类型化 lambda 演算的求值函数的反函数
DOI：
10.1109/lics.1991.151645
复制
发表时间：
1991
期刊：
影响因子：
--
通讯作者：
H. Schwichtenberg
中科院分区：
文献类型：
--
作者：
Ulrich Berger;H. Schwichtenberg
定义了一个函数p到e（过程到表达式），它将包含一些基本算术的任何类型lambda演算模型中的类型lambda项的求值函数反转。结合评价函数，p到e产生一个有效的归一化算法。该方法被扩展到lambda -演算常数，并用于规范（lambda表示）自然演绎证明（高阶）算术。理论上的一个有趣的结果是一个关于β-约化的强完备性定理.如果两个lambda项在包含原始递归函数（级别1）的表示的某些模型中具有相同的值，那么它们在beta eta演算中可能相等。<<ETX>>
A functional p to e (procedure to expression) that inverts the evaluation functional for typed lambda -terms in any model of typed lambda -calculus containing some basic arithmetic is defined. Combined with the evaluation functional, p to e yields an efficient normalization algorithm. The method is extended to lambda -calculi with constants and is used to normalize (the lambda -representations of) natural deduction proofs of (higher order) arithmetic. A consequence of theoretical interest is a strong completeness theorem for beta eta -reduction. If two lambda -terms have the same value in some model containing representations of the primitive recursive functions (of level 1) then they are probably equal in the beta eta -calculus.<<ETX>>