Explicit Substitutions in the Reduction of Lambda Terms

Gopalan Nadathur, Xiaochu Qi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationProceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03)
PublisherAssociation for Computing Machinery
Number of pages12
ISBN (Print)1581137052, 9781581137057
StatePublished - 2003
EventFifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming - Uppsala, Sweden
Duration: Aug 27 2003Aug 29 2003

Publication series

NameProceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming


OtherFifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming


  • Beta reduction
  • Explicit substitution
  • Graph and environment based reduction procedures
  • Higher-order abstract syntax
  • Lambda calculus
  • Metalanguages
  • Suspension notation


Dive into the research topics of 'Explicit Substitutions in the Reduction of Lambda Terms'. Together they form a unique fingerprint.

Cite this