Access Restriction

Author Curien, Pierre-Louis ♦ Hardin, Thrse ♦ Lvy, Jean-Jacques
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1996
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Confluency ♦ Explicit substitutions
Abstract Categorical combinators [Curien 1986/1993; Hardin 1989; Yokouchi 1989] and more recently λ&sgr;-calculus [Abadi 1991; Hardin and Le´vy 1989], have been introduced to provide an explicit treatment of substitutions in the λ-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 Le´vy [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]: λ&sgr;-calculus is not confluent (it is confluent on ground terms only).This unfortunate result is “repaired” by presenting a confluent version of λ&sgr;-calculus, named the $λ\textit{Env}-caldulus$ in Hardin and Le´vy [1989], called here the confluent λ&sgr;-calculus.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1996-03-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 43
Issue Number 2
Page Count 36
Starting Page 362
Ending Page 397

Open content in new tab

   Open content in new tab
Source: ACM Digital Library