JFLP: Volume 1998, Article 5

The Journal of Functional and Logic Programming

Volume 1998

Article 5

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

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

Calculi of Generalized beta-Reduction and Explicit Substitutions:
The Type-Free and Simply Typed Versions

Fairouz Kamareddine , Alejandro Ríos , and Joe B. Wells

4 June 1998

Abstract

Extending the lambda-calculus with either explicit substitution or generalized reduction has been the subject of extensive research recently, and still has many open problems. This paper is the first investigation into the properties of a calculus combining both generalized reduction and explicit substitutions. We present a calculus, lambda-gs, that combines a calculus of explicit substitution, lambda-s, and a calculus with generalized reduction, lambda-g. We believe that lambda-gs is a useful extension of the lambda-calculus, because it allows postponement of work in two different but complementary ways. Moreover, lambda-gs) (and also lambda-s) satisfies properties desirable for calculi of explicit substitutions and generalized reductions. In particular, we show that lambda-gs preserves strong normalization, is a conservative extension of lambda-g, and simulates beta-reduction of lambda-g and the classical lambda-calculus. Furthermore, we study the simply typed versions of lambda-s and lambda-gs, and show that well-typed terms are strongly normalizing and that other properties, such as typing of subterms and subject reduction, hold. Our proof of the preservation of strong normalization (PSN) is based on the minimal derivation method. It is, however, much simpler, because we prove the commutation of arbitrary internal and external reductions. Moreover, we use one proof to show both the preservation of lambda-strong normalization in lambda-s and the preservation of lambda-g-strong normalization in lambda-gs. We remark that the technique of these proofs is not suitable for calculi without explicit substitutions (e.g., the preservation of lambda-strong normalization in lambda-g requires a different technique).

The following versions of the article are available:

• Preformatted versions of the article (compressed with gzip )
  • DVI (gzip'ped 61 kb)
  • PostScript (gzip'ped 205 kb)
  • PDF comming soon!
• Source materials for custom formatting
  • LaTeX ( JFLP-A98-05.tex , gzip'ped 32 kb)
  • BIBTeX ( JFLP-A98-05.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-05,
      author={Fairouz Kamareddine and Alejandro R\'{\i}os and J. B. Wells},
      title={Calculi of Generalized \protect\(\beta\protect\)-Reduction and
	     Explicit Substitutions: The Type-Free and Simply Typed Versions},
      journal={Journal of Functional and Logic Programming},
      volume={1998},
      number={5},
      publisher={The MIT Press},
      month={June},
      year={1998},
    }

Main page