[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

X.R.S: Explicit reduction systems — A first-order calculus for higher-order calculi

  • Conference paper
  • First Online:
Automated Deduction — CADE-15 (CADE 1998)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1421))

Included in the following conference series:

Abstract

The λ⇑-calculus is a confluent first-order term rewriting system which contains the λ-calculus written in de Bruijn's notation. The substitution is defined explicitly in λ⇑ by a subsystem, called the σ⇑-calculus. In this paper, we use the σ⇑-calculus as the substitution mechanism of general higher-order systems which we will name Explicit Reduction Systems. We give general conditions to define a confluent XRS. Particularly, we restrict the general condition of orthogonality of the classical higher-order rewriting systems to the orthogonality of the rules initiating substitutions.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. In Principles of Programming Languages, pages 31–46, 1990.

    Google Scholar 

  2. A. Asperti and C. Laneve. Interaction systems 1: The theory of optimal reductions. Mathematical Structures in Computer Science, 4:457–504, 1994.

    Article  MathSciNet  MATH  Google Scholar 

  3. R. Bloo and K.H. Rose. Combinatory reduction systems with explicit substitution that preserve strong normalisation. In Rewriting Techniques and Applications, pages 169–183, 1996.

    Google Scholar 

  4. P.-L. Curien, T. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362–397, March 1996.

    Article  MathSciNet  MATH  Google Scholar 

  5. P.-L. Curien. An abstract framework for environment machines. Theoretical Computer Science, 82, 1991.

    Google Scholar 

  6. G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions. In Logic in Computer Science, 1995.

    Google Scholar 

  7. G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning. Unification via explicit substitutions: the case of higher-order patterns. In Logic Programming, pages 259–273, 1996.

    Google Scholar 

  8. J. Goubault. Weak normalization of λσ-calculus. GDR-AMI, 1997.

    Google Scholar 

  9. T. Hardin and J.-J. Lévy. A confluent calculus of substitutions. In France-Japan Artificial Intelligence and Computer Science Symposium, 1989.

    Google Scholar 

  10. T. Hardin, L. Maranget, and B. Pagano. Functional back-ends within the lambda-sigma calculus. In International Conference on Functional Programming, pages 25–33, 1996.

    Google Scholar 

  11. D. Kesner. Confluence properties of extensional and non-extensional lambda-calculi with explicit substitutions. Lecture Notes in Computer Science, 1103:184–--, 1996.

    Google Scholar 

  12. Z.O. Khasidashvili. Expression reduction systems. In Proceedings of I. Vekua Institute of Applied Mathematics, volume 36, pages 200–220, 1990.

    MATH  MathSciNet  Google Scholar 

  13. J.W. Klop. Combinatory Reduction Systems. PhD thesis, University of Amsterdam, 1980.

    Google Scholar 

  14. J.W. Klop. Term rewriting systems. Technical report, Centrum voor Wiskunde en Informatica, 1990.

    Google Scholar 

  15. F. Kamareddine and A. Rios. Generalized-reduction and explicit substitution. Lecture Notes in Computer Science, 1140:378–--, 1996.

    Google Scholar 

  16. P. Lescanne. From λσ to λυ: A journey through calculi of explicit substitutions. In Principles of Programming Languages, pages 60–69, 1994.

    Google Scholar 

  17. P.-A. Mellies. Typed lambda-calculi with explicit substitutions may not terminate. In Typed Lambda Calculi and Applications, 1995.

    Google Scholar 

  18. D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, pages 497–536, 1991.

    Google Scholar 

  19. F. Müller. Confluence of the lambda calculus with left-linear algebraic rewriting. Information Processing Letters, 41:293–299, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  20. C. Muñoz. Meta-theoretical properties of λ φ : A left-linear variant of λ σ . Technical Report RR-3107, Unité de recherche INRIA-Rocquencourt, Février 1997.

    Google Scholar 

  21. T. Nipkow. Higher-order critical pairs. In Proceedings of Logic in Computer Science, pages 342–349, 1993.

    Google Scholar 

  22. V. Oostrom and F. Raamsdonk. Weak orthogonality implies confluence: The higher-order case. Lecture Notes in Computer Science, 813:379–--, 1994.

    Google Scholar 

  23. A. Rios. Contributions à l'étude des Lambda-calculs avec Substitutions Explicites. PhD thesis, Université PARIS 7, 1993.

    Google Scholar 

  24. K. H. Rose and R. R. Moore. Xy-pic Reference Manual, 1995.

    Google Scholar 

  25. F. van Raamsdonk. Confluence and Normalization for Higher-Order Rewriting. PhD thesis, University of Amsterdam, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIP6 - Université Pierre et Marie Curie, Paris, France

    Bruno Pagano

Authors
  1. Bruno Pagano
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Claude Kirchner Hélène Kirchner

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pagano, B. (1998). X.R.S: Explicit reduction systems — A first-order calculus for higher-order calculi. In: Kirchner, C., Kirchner, H. (eds) Automated Deduction — CADE-15. CADE 1998. Lecture Notes in Computer Science, vol 1421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054249

Download citation

  • DOI: https://doi.org/10.1007/BFb0054249

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64675-4

  • Online ISBN: 978-3-540-69110-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation