JFLP: Volume 1999, Article 2

The Journal of Functional and Logic Programming

Volume 1999

Article 2

Published by The MIT Press . Copyright 1999 Massachusetts Institute of Technology.

Your institution may already be a subscriber to JFLP. If not, please subscribe for legitimate access to all journal articles.

A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations

Gopalan Nadathur

15 March 1999

Abstract

We discuss issues relevant to the practical use of a previously proposed notation for lambda terms in contexts where the intensions of such terms have to be manipulated. This notation uses the ``nameless'' scheme of de Bruijn, includes expressions for encoding terms together with substitutions to be performed on them, and contains a mechanism for combining such substitutions so that they can be effected in a common structure traversal. The combination mechanism is a general one and consequently difficult to implement. We propose a simplification to it that retains its functionality in situations that occur commonly in beta-reduction. We then describe a system for annotating terms to determine if they can be affected by substitutions generated by external beta-contractions. These annotations can lead to a conservation of space and time in implementations of reduction by permitting substitutions to be performed trivially in certain situations and can also foster a greater sharing in reduction. The use of the resulting notation in the reduction and comparison of terms is examined. Notions of head normal forms and head reduction sequences are defined in context and shown to be useful in equality computations. Our head reduction sequences generalize the usual ones for lambda terms so that they subsume the sequences of terms produced by a variety of graph- and environment-based reduction procedures for the lambda calculus. They can therefore be used in correctness arguments for such procedures. This fact and the efficacy of our notation are illustrated in the context of a particular reduction procedure that we present. The relevance of the present discussions to the unification of lambda terms is also outlined.

The following versions of the article are available:

• Preformatted versions of the article (compressed with gzip )
  • DVI (gzip'ped 85 kb)
  • PostScript (gzip'ped 248 kb)
  • PDF (gzip'ped 444 kb; uncompressed 640 kb)
• Source materials for custom formatting
  • LaTeX ( JFLP-A99-02.tex , gzip'ped 48 kb)
  • BIBTeX ( JFLP-A99-02.bib , gzip'ped 3 kb)
  • Parameter settings for custom formatting ( cjropts.tex , 165 bytes)

You can find this article also on the ftp-server of The MIT Press (access may be faster from some sites).

Self citation

    @article{jflp98-09,
      author={Gopalan Nadathur},
      title={A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations},
      journal={Journal of Functional and Logic Programming},
      volume={1999},
      number={2},
      publisher={The MIT Press},
      month={March},
      year={1999}
    }

Main page