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 Abstract Freely available
Right arrow Full Text (PDF)
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

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.

References

    [1]  Abadi M, Cardelli L, Curien P-L, Lévy J-J. Explicit Substitutions. Journal of Functional Programming (1991) 1(4):375–416.[CrossRef]

    [2]  Ayala-Rincón M, de Moura F, Kamareddine F. Comparing and Implementing Calculi of Explicit Substitutions with Eta-Reduction. Annals of Pure and Applied Logic (2005) 134:5–41.[CrossRef][Web of Science]

    [3]  Ayala-Rincón M, Kamareddine F. Unification via the {lambda}se-Style of Explicit Substitution. The Journal of the Interest Group in Pure and Applied Logics (2001) 9(4):489–523.

    [4]  Baader F, Nipkow T. Term Rewriting and All That (1998) Cambridge University Press.

    [5]  Borovansky P. Implementation of Higher-Order Unification Based on Calculus of Explicit Substitutions (1995) 363–368. Volume 1012 of Lecture Notes in Computer Science.

    [6]  Briaud D. An explicit Eta rewrite rule. In: Typed lambda calculi and applications (1995) 94–108. volume 902 of Lecture Notes in Computer Science.

    [7]  Dowek G, Hardin T, Kirchner C. Higher-order Unification via Explicit Substitutions. Information and Computation (2000) 157(1/2):183–235.[CrossRef][Web of Science]

    [8]  Hardin T. Eta-conversion for the languages of explicit substitutions. In: Algebraic and logic programming (1992) 306–321. volume 632 of Lecture Notes in Computer Science.

    [9]  Hindley J. Basic Simple Type Theory (1997) Cambridge University Press. Number 42 in Cambridge Tracts in Theoretical Computer Science.

    [10]  Kesner D. Confluence of extensional and non-extensional {lambda}-calculi with explicit substitutions. Theoretical Computer Science (2000) 238(1-2):183–220.[CrossRef][Web of Science]

    [11]  Kamareddine F, Ríos A. Extending a lambda-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms. Journal of Functional Programming (1997) 7(4):395–420.[CrossRef]

    [12]  Kamareddine F, Ríos A. Relating the Lambda-sigma and Lambda-s styles of Explicit Substitutions. Logic and Computation (2000) 10(3):349–380.[CrossRef]

    [13]  Melliès P-A. Typed {lambda}-calculi with explicit substitutions may not terminate in Proceedings of TLCA’95. Lecture Notes in Computer Science (1995) 902.

    [14]  Ríos A. Contribution à l’étude des {lambda}-calculs avec substitutions explicites (1993) 7. Université de Paris. PhD thesis.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
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?