Abstract

It has long been argued that the notion of substitution in the λ-calculus needs to be made explicit. This resulted in many calculi have been developed in which the computational steps of the substitution operation involved in β-contractions have been atomised. In contrast to the great variety of developments for making explicit formalisations of the Beta rule, less work has been done for giving explicit definitions of the conditional Eta rule. In this paper constructive Eta rules are proposed for both the λσ- and the λse-calculi of explicit substitutions. Our results can be summarised as follows: 1) we introduce constructive and explicit definitions of the Eta rule in the λσ- and the λse-calculi, 2) we prove that these definitions are correct and preserve basic properties such as subject reduction. In particular, we show that the explicit definitions of the eta rules coincide with the Eta rule for pure λ-terms and that moreover, their application is decidable in the sense that Eta redices are effectively detected . The formalisation of these Eta rules involves the development of specific calculi for explicitly checking the condition of the proposed Eta rules while constructing the Eta contractum