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

  • Bruno Pagano
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


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.


Free Algebra Computation Rule Binding Operator Left Member Unary Symbol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [ACCL90]
    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. [AL94]
    A. Asperti and C. Laneve. Interaction systems 1: The theory of optimal reductions. Mathematical Structures in Computer Science, 4:457–504, 1994.MathSciNetCrossRefzbMATHGoogle Scholar
  3. [BR96]
    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. [CHL96]
    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.CrossRefMathSciNetzbMATHGoogle Scholar
  5. [Cur91]
    P.-L. Curien. An abstract framework for environment machines. Theoretical Computer Science, 82, 1991.Google Scholar
  6. [DHK95]
    G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions. In Logic in Computer Science, 1995.Google Scholar
  7. [DHKP96]
    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. [Gou97]
    J. Goubault. Weak normalization of λσ-calculus. GDR-AMI, 1997.Google Scholar
  9. [HL89]
    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. [HMP96]
    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. [Kes96]
    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. [Kha90]
    Z.O. Khasidashvili. Expression reduction systems. In Proceedings of I. Vekua Institute of Applied Mathematics, volume 36, pages 200–220, 1990.zbMATHMathSciNetGoogle Scholar
  13. [Klo80]
    J.W. Klop. Combinatory Reduction Systems. PhD thesis, University of Amsterdam, 1980.Google Scholar
  14. [Klo90]
    J.W. Klop. Term rewriting systems. Technical report, Centrum voor Wiskunde en Informatica, 1990.Google Scholar
  15. [KR96]
    F. Kamareddine and A. Rios. Generalized-reduction and explicit substitution. Lecture Notes in Computer Science, 1140:378–--, 1996.Google Scholar
  16. [Les94]
    P. Lescanne. From λσ to λυ: A journey through calculi of explicit substitutions. In Principles of Programming Languages, pages 60–69, 1994.Google Scholar
  17. [Mel95]
    P.-A. Mellies. Typed lambda-calculi with explicit substitutions may not terminate. In Typed Lambda Calculi and Applications, 1995.Google Scholar
  18. [Mil91]
    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. [Mül92]
    F. Müller. Confluence of the lambda calculus with left-linear algebraic rewriting. Information Processing Letters, 41:293–299, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  20. [Muñ97]
    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. [Nip93]
    T. Nipkow. Higher-order critical pairs. In Proceedings of Logic in Computer Science, pages 342–349, 1993.Google Scholar
  22. [OR94]
    V. Oostrom and F. Raamsdonk. Weak orthogonality implies confluence: The higher-order case. Lecture Notes in Computer Science, 813:379–--, 1994.Google Scholar
  23. [Rio93]
    A. Rios. Contributions à l'étude des Lambda-calculs avec Substitutions Explicites. PhD thesis, Université PARIS 7, 1993.Google Scholar
  24. [RM95]
    K. H. Rose and R. R. Moore. Xy-pic Reference Manual, 1995.Google Scholar
  25. [vR96]
    F. van Raamsdonk. Confluence and Normalization for Higher-Order Rewriting. PhD thesis, University of Amsterdam, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Bruno Pagano
    • 1
  1. 1.LIP6 - Université Pierre et Marie CurieParisFrance

Personalised recommendations