Skip Navigation


Logic Journal of IGPL Advance Access originally published online on July 19, 2009
Logic Journal of IGPL 2009 17(6):697-718; doi:10.1093/jigpal/jzp027
This Article
Right arrow Full Text (PDF)
Right arrow All Versions of this Article:
17/6/697    most recent
jzp027v1
Right arrow References
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Ventura, D.
Right arrow Articles by Kamareddine, F.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Explicit substitutions calculi with one step Eta-reduction decided explicitly

Daniel Ventura

Grupo de Teoria da Computação, Departamento de Matemática, Universidade de Brasília, Brasília D.F., Brasil.
E-mail: ventura{at}mat.unb.br

Mauricio Ayala-Rincón

Grupo de Teoria da Computação, Departamento de Matemática, Universidade de Brasília, Brasília D.F., Brasil.
E-mail: ayala{at}mat.unb.br

Fairouz Kamareddine

School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, Scotland. E-mail: fairouz@macs.hw.ac.uk


  Abstract

It has long been argued that the notion of substitution in the {lambda}-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 {lambda}{sigma}- and the {lambda}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 {lambda}{sigma}- and the {lambda}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 {lambda}-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.

Key Words: Lambda Calculus • Eta reduction • Explicit Substitutions • Subject Reduction

Received for publication 7 September 2007.
Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.