Confluence properties of weak and strong calculi of explicit substitutions

被引:49
作者
Curien, PL
Hardin, T
Levy, JJ
机构
[1] INST NATL RECH INFORMAT & AUTOMAT, F-78153 LE CHESNAY, FRANCE
[2] CONSERVATOIRE NATL ARTS & METIERS, PARIS, FRANCE
关键词
confluency; explicit substitutions;
D O I
10.1145/226643.226675
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Categorical combinators [Curien 1986/1993; Hardin 1989; Yokouchi 1989] and more recently lambda sigma-calculus [Abadi 1991; Hardin and Levy 1989], have been introduced to provide an explicit treatment of substitutions in the lambda-calculus. We reintroduce here the ingredients of these calculi in a self-contained and stepwise way, with a special emphasis on confluence properties. The main new results of the paper with respect to Curien [1986/1993], Hardin [1989], Abadi [1991], and Hardin and Levy [1989] are the following: (1) We present a confluent weak calculus of substitutions, where no variable clashes can be feared; (2) We solve a conjecture raised in Abadi [1991]: lambda sigma-calculus is not confluent (it is confluent on ground terms only). This unfortunate result is ''repaired'' by presenting a confluent version of lambda sigma-calculus, named the lambda En upsilon-calculus in Hardin and Levy [1989], called here the confluent lambda sigma-calculus.
引用
收藏
页码:362 / 397
页数:36
相关论文
共 38 条
[1]  
Abadi M., 1991, Journal of Functional Programming, V1, P375, DOI 10.1017/S0956796800000186
[2]  
ABRAMSKY S, 1989, DECLARATIVE PROGRAMM, P65
[3]  
BARENDREGT H, 1984, LAMBDA CALCULUS, V103
[4]   MINIMAL AND OPTIMAL COMPUTATIONS OF RECURSIVE PROGRAMS [J].
BERRY, G ;
LEVY, JJ .
JOURNAL OF THE ACM, 1979, 26 (01) :148-175
[5]   LAMBDA-CALCULI FOR (STRICT) PARALLEL FUNCTIONS [J].
BOUDOL, G .
INFORMATION AND COMPUTATION, 1994, 108 (01) :51-127
[6]  
BREAZUTANNEN V, 1988, P LICS 88 ED
[7]   THE CATEGORICAL ABSTRACT MACHINE [J].
COUSINEAU, G ;
CURIEN, PL ;
MAUNY, M .
SCIENCE OF COMPUTER PROGRAMMING, 1987, 8 (02) :173-202
[8]  
Curien P.-L., 1994, Journal of Functional Programming, V4, P113, DOI 10.1017/S0956796800000976
[9]   AN ABSTRACT FRAMEWORK FOR ENVIRONMENT MACHINES [J].
CURIEN, PL .
THEORETICAL COMPUTER SCIENCE, 1991, 82 (02) :389-402
[10]  
CURIEN PL, 1986, RES NOTES THEORETICA