Explicit substitutions calculi with one step Eta-reduction decided explicitly

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 ?s- and the ?s_e-calculi of explicit substitutions. Our results can be summarised as follows: 1) we introduce constructive and explicit definitions of the Eta rule in the ?s- and the ?s_e-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 (and contracted). 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. © The Author 2009. Published by Oxford University Press.