Explicit Substitutions Calculi with Explicit Eta rules which Preserve Subject Reduction

**
Daniel Lima Ventura,
Mauricio Ayala-Rinco n,
Fairouz Kamareddine.
**

Subject reduction (for short SR) is an essential property of any type system. This property guarantees that all terms of the system preserve their types during any possible computation. It is well-known that the classic simply typed ?-calculus has this property, which means that any well-typed ?-term preserves its type under ?- and ?-contractions. It has been argued in the past decade that the notion of substitution in the ?-calculus needs to be made explicit. In this paper, we show that SR poses computational difficulties when the ?-calculus is extended with explicit substitutions. In particular, we show that two important calculi of explicit substitutions enlarged with Eta rules, when no explicit type and normalisation considerations are given, do not preserve subject reduction. However, we show also that if Eta reduction was made "explicit" then SR will hold for these calculi. More specifically, our results can be summarized as follows: * We show that one needs to define constructively the Eta rule in both the ??-calculus and the ?se-calculus in order to guarantee SR when Eta is applied to well-typed unrestricted terms (note that these calculi without Eta already preserve SR). * We introduce constructive and explicit Eta rules for ?? and ?se and prove that the enlarged calculi satisfy SR. The formalization of these rules involves the development of specific calculi for explicitly checking the condition of the proposed Eta rules while constructing the Eta contractum.

http://www.lbd.dcc.ufmg.br/colecoes/lsfa/2006/001.pdf

Biblioteca Digital Brasileira de Computação - Contato: bdbcomp@lbd.dcc.ufmg.br