TY - GEN

T1 - Explicit Substitutions in the Reduction of Lambda Terms

AU - Nadathur, Gopalan

AU - Qi, Xiaochu

PY - 2003

Y1 - 2003

N2 - Substitution in the lambda calculus is a complex operation that traditional presentations of beta contraction naively treat as a unitary operation. Actual implementations are more careful. Within them, substitutions are realized incrementally through the use of environments. However, environments are usually not accorded a first-class status within such systems in that they are not reflected into term structure. This approach does not allow the smaller substitution steps to be intermingled with other operations of interest on lambda terms. Various new notations for lambda terms remedy this situation by proposing an explicit treatment of substitutions. Unfortunately, a naive implementation of beta reduction based on such notations has the potential of being costly: each use of the substitution propagation rules causes the creation of a new structure on the heap that is often discarded in the immediately following step. There is, thus, a tradeoff between these two approaches. This paper discusses these tradeoffs and offers an amalgamated approach that utilizes recursion in rewrite rule application but also suspends substitution operations where profitable.

AB - Substitution in the lambda calculus is a complex operation that traditional presentations of beta contraction naively treat as a unitary operation. Actual implementations are more careful. Within them, substitutions are realized incrementally through the use of environments. However, environments are usually not accorded a first-class status within such systems in that they are not reflected into term structure. This approach does not allow the smaller substitution steps to be intermingled with other operations of interest on lambda terms. Various new notations for lambda terms remedy this situation by proposing an explicit treatment of substitutions. Unfortunately, a naive implementation of beta reduction based on such notations has the potential of being costly: each use of the substitution propagation rules causes the creation of a new structure on the heap that is often discarded in the immediately following step. There is, thus, a tradeoff between these two approaches. This paper discusses these tradeoffs and offers an amalgamated approach that utilizes recursion in rewrite rule application but also suspends substitution operations where profitable.

KW - Beta reduction

KW - Explicit substitution

KW - Graph and environment based reduction procedures

KW - Higher-order abstract syntax

KW - Lambda calculus

KW - Metalanguages

KW - Suspension notation

UR - http://www.scopus.com/inward/record.url?scp=1242332694&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=1242332694&partnerID=8YFLogxK

U2 - 10.1145/888251.888270

DO - 10.1145/888251.888270

M3 - Conference contribution

AN - SCOPUS:1242332694

SN - 1581137052

SN - 9781581137057

T3 - Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming

SP - 195

EP - 206

BT - Proceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03)

PB - Association for Computing Machinery

T2 - Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming

Y2 - 27 August 2003 through 29 August 2003

ER -