Applications of infinitary lambda calculus

被引:13
作者
Barendregt, Henk [1 ]
Klop, Jan Willem [1 ,2 ]
机构
[1] Radboud Univ Nijmegen, Fac Sci, NL-6500 GL Nijmegen, Netherlands
[2] Vrije Univ Amsterdam, Dept Comp Sci, NL-1081 HV Amsterdam, Netherlands
关键词
REDUCTION; SYSTEMS; MODELS;
D O I
10.1016/j.ic.2008.09.003
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We present an introduction to infinitary lambda calculus, highlighting its main properties. Subsequently we give three applications of infinitary lambda calculus. The first addresses the non-definability of Surjective Pairing, which was shown by the first author not to be definable in lambda calculus. We show how this result follows easily as an application of Berry's Sequentiality Theorem, which itself can be proved in the setting of infinitary lambda calculus. The second pertains to the notion of relative recursiveness of number-theoretic functions. The third application concerns an explanation of counterexamples to confluence of lambda calculus extended with non-left-linear reduction rules: Adding non-left-linear reduction rules such as delta xx -> x or the reduction rules for Surjective Pairing to the lambda calculus yields non-confluence, as proved by the second author. We discuss how an extension to the infinitary lambda calculus, where Bohm trees can be directly manipulated as infinite terms, yields a more simple and intuitive explanation of the correctness of these Church-Rosser counterexamples. (C) 2009 Elsevier Inc. All rights reserved.
引用
收藏
页码:559 / 582
页数:24
相关论文
共 42 条
[1]   FULL ABSTRACTION IN THE LAZY LAMBDA-CALCULUS [J].
ABRAMSKY, S ;
ONG, CHL .
INFORMATION AND COMPUTATION, 1993, 105 (02) :159-267
[2]  
[Anonymous], 1963, T AM MATH SOC, V108, P106
[3]  
[Anonymous], HDB LOGIC COMPUTER S
[4]  
[Anonymous], 2005, WE WILL SHOW THEM ES
[5]  
Ariola Z. M., 1996, Fundamenta Informaticae, V26, P207
[6]   Lambda calculus with explicit recursion [J].
Ariola, ZM ;
Klop, JW .
INFORMATION AND COMPUTATION, 1997, 139 (02) :154-233
[7]  
ARIOLA ZM, 1994, IEEE S LOG, P416, DOI 10.1109/LICS.1994.316066
[8]  
BARENDREGT H, 1974, Z MATH LOGIK, V20, P289, DOI 10.1002/malq.19740201902
[9]  
Barendregt H. P., 1984, LAMBDA CALCULUS ITS
[10]  
BARENDREGT HP, 1999, J FUNCT PROGRAM, V9, P565