Representation of lambda terms suitable for operations on their intensions

Gopalan Nadathur, Debra Sue Wilson

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

15 Scopus citations

Abstract

A representation for lambda terms is described based on the scheme of de Bruijn for eliminating variable names. The new notation provides for a class of terms that can encode other terms together with substitutions to be performed on them. The notion of an environment is used to realize this 'delaying' of substitutions. The precise mechanism that is used is, however, more complex than the usual so as to support the ability to examine subterms embedded under abstractions. A virtue of our representation is that it permits substitution to be realized as an atomic operation and thereby provides for efficient implementations of β-reduction. Operations on λ-terms are described based on our representation and the relationship of these to the conventional definitions are exhibited.

Original languageEnglish (US)
Title of host publicationProc 1990 ACM Conf LISP Funct Program
Editors Anon
PublisherPubl by ACM
Pages341-348
Number of pages8
ISBN (Print)089791368X
StatePublished - 1990
EventProceedings of the 1990 ACM Conference on LISP and Functional Programming - Nice, Fr
Duration: Jun 27 1990Jun 29 1990

Publication series

NameProc 1990 ACM Conf LISP Funct Program

Other

OtherProceedings of the 1990 ACM Conference on LISP and Functional Programming
CityNice, Fr
Period6/27/906/29/90

Fingerprint

Dive into the research topics of 'Representation of lambda terms suitable for operations on their intensions'. Together they form a unique fingerprint.

Cite this