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

Typed λ-calculus uses two abstraction symbols (λ and Π) which are usually treated in different ways: View the MathML source has as type the abstraction View the MathML source, yet View the MathML source 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.