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

Typed ¿-calculus uses two abstraction symbols (¿ and ¿) which are usually treated in different ways: ¿x:*.x has as type the abstraction ¿x:*.*, yet ¿x:*.* has type ¿ rather than an abstraction; moreover, (¿x:A.B)C is allowed and ß-reduction evaluates it, but (¿x: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.