Skip to main content
SpringerLink
Log in

Higher-order equational unification via explicit substitutions

  • Higher-Order Methods
  • Conference paper
  • First Online:
Book cover Algebraic and Logic Programming (ALP 1997, HOA 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1298))

Abstract

We show how to reduce the unification problem modulo βη-conversion and a first-order equational theory E, into a first-order unification problem in a union of two non-disjoint equational theories including E and a calculus of explicit substitutions. A rule-based unification procedure in this combined theory is described and may be viewed as an extension of the one initially designed by G. Dowek, T. Hardin and C. Kirchner for performing unification of simply typed λ-terms in a first-order setting via the λσ-calculus of explicit substitutions. Additional rules are used to deal with the interaction between E and λσ.

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. Journal of Functional Programming, 1(4):375–416, 1991.

    Google Scholar 

  2. F. Baader and K. U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. Journal of Symbolic Computation, 21(2):211–243, February 1996.

    Google Scholar 

  3. V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 82–90, Edinburgh, Scotland, 5–8 July 1988. IEEE Computer Society.

    Google Scholar 

  4. G. Dowek, T. Hardin, and C. Kirchner.Higher-order unification via explicit substitutions, extended abstract. In D. Kozen, editor, Proceedings of LICS'95, pages 366–374, San Diego, June 1995.

    Google Scholar 

  5. E. Domenjoud, F. Klay, and C. Ringeissen. Combination techniques for non-disjoint equational theories. In A. Bundy, editor, Proceedings 12th International Conference on Automated Deduction, Nancy (France), volume 814 of Lecture Notes in Artificial Intelligence, pages 267–281. Springer-Verlag, June/July 1994.

    Google Scholar 

  6. G. Huet. A unification algorithm for typed lambda calculus. Theoretical Computer Science, 1(1):27–57, 1975.

    Google Scholar 

  7. J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebas: a rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257–321. The MIT press, Cambridge (MA, USA), 1991.

    Google Scholar 

  8. C. Kirchner and C. Ringeissen.Higher-Order Equational Unification via Explicit Substitutions. Research report, CRIN, 1997.

    Google Scholar 

  9. C. Mufioz. A left linear variant of λσ Manuscript.

    Google Scholar 

  10. G. Nadathur and D. Miller. An overview of λ PROLOG. In R. A. Kowalski and K. A. Bowen, editors, Proceedings of the Fifth International Conference and Symposium on Logic Programming, pages 810–827, Seatle, 1988. ALP, IEEE, The MIT Press.

    Google Scholar 

  11. T. Nipkow and Z. Qian. Modular higher-order E-unification. In R. V. Book, editor, Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), volume 488 of Lecture Notes in Computer Science, pages 200–214. Springer-Verlag, 1991.

    Google Scholar 

  12. B. Pagano. Extensions of lambda-calculi with explicit substitutions preserving the church-rosser's property. Manuscript.

    Google Scholar 

  13. Z. Qian and K. Wang. Modular higher-order equational preunification. Journal of Symbolic Computation, 22(4):401–424, October 1996.

    Google Scholar 

  14. A. Ríos.Contributions à l'étude des λ-calculs avec des substitutions explicites. Thèse de Doctorat d'Université, U. Paris VII, 1993.

    Google Scholar 

  15. W. Snyder. Higher-order E-unification. In M. E. Stickel, editor, Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture Notes in Computer Science, pages 573–587, July 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA-Lorraine & CRIN-CNRS, 615, rue du Jardin Botanique, BP 101, F-54602, Villers-lés-Nancy Cedex, France

    Claude Kirchner & Christophe Ringeissen

Authors
  1. Claude Kirchner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christophe Ringeissen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michael Hanus Jan Heering Karl Meinke

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kirchner, C., Ringeissen, C. (1997). Higher-order equational unification via explicit substitutions. In: Hanus, M., Heering, J., Meinke, K. (eds) Algebraic and Logic Programming. ALP HOA 1997 1997. Lecture Notes in Computer Science, vol 1298. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027003

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63459-1

  • Online ISBN: 978-3-540-69555-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation