## 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 language | English |
---|---|

Pages (from-to) | 27-45 |

Number of pages | 19 |

Journal | Annals of Pure and Applied Logic |

Volume | 97 |

Issue number | 1-3 |

Publication status | Published - 21 Mar 1999 |

## Keywords

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