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.
|Number of pages||19|
|Journal||Annals of Pure and Applied Logic|
|Publication status||Published - 21 Mar 1999|