On Π-conversion in the λ-cube and the combination with abbreviations

Fairouz Kamareddine, Roel Bloo, Rob Nederpelt

Research output: Contribution to journalArticlepeer-review

14 Citations (Scopus)

Abstract

Typed ?-calculus uses two abstraction symbols (? and ?) which are usually treated in different ways: ??:*.? has as type the abstraction ??:*. *, yet ??:*. * has type ? rather than an abstraction; moreover, (??:A.B)C is allowed and ß-reduction evaluates it, but (??:A.B)C is rarely allowed. Furthermore, there is a general consensus that ? and ? are different abstraction operators. While we agree with this general consensus, we find it nonetheless important to allow ? to act as an abstraction operator. Moreover, experience with AUTOMATH and the recent revivals of ?-reduction as in [11, 14], illustrate the elegance of giving ?-redexes a status similar to ?-redexes. However, ?-reduction in the ?-cube faces serious problems as shown in [11, 14]: it is not safe as regards subject reduction, it does not satisfy type correctness, it loses the property that the type of an expression is well-formed and it fails to make any expression that contains a ?-redex well-formed. In this paper, we propose a solution to all those problems. The solution is to use a concept that is heavily present in most implementations of programming languages and theorem provers: abbreviations (viz. by means of a definition) or let-expressions. We will show that the ?-cube extended with ?-conversion and abbreviations satisfies all the desirable properties of the cube and does not face any of the serious problems of ?-reduction. We believe that this extension of the ?-cube is very useful: it gives a full formal study of two concepts (?-reduction and abbreviations) that are useful for theorem proving and programming languages. © 1999 Published by Elsevier Science B.V. All rights reserved.

Original languageEnglish
Pages (from-to)27-45
Number of pages19
JournalAnnals of Pure and Applied Logic
Volume97
Issue number1-3
Publication statusPublished - 21 Mar 1999

Keywords

  • λ-Calculus
  • π-reduction
  • Normalisation
  • Subject-reduction

Fingerprint

Dive into the research topics of 'On Π-conversion in the λ-cube and the combination with abbreviations'. Together they form a unique fingerprint.

Cite this