Skip to main content
SpringerLink
Log in

Modular higher-order E-unification

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1991)

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

Included in the following conference series:

Abstract

The combination of higher-order and first-order unification algorithms is studied. We present algorithms to compute a complete set of unifiers of two simply typed λ-terms w.r.t. the union of α, β and η conversion and a first-order equational theory E. The algorithms are extensions of Huet's work and assume that a complete unification algorithm for E is given. Our completeness proofs require E to be at least regular.

Research supported by ESPRIT BRA 3245, Logical Frameworks.

Research partially supported by ESPRIT project 390, PROSPECTRA, and by ESPRIT Basic Research WG COMPASS3264.

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. Boudet, A.: Unification in a combination of equational theories: an efficient algorithm. Proc. 10th Int. Conf. Automated Deduction, LNCS 449 (1990), 292–307.

    Google Scholar 

  2. Breazu-Tannen, V.: Combing algebra and higher-order types. Proc. 3rd IEEE Symp. Logic in Computer Science (1988), 82–90.

    Google Scholar 

  3. Breazu-Tannen, V. and Gallier, J.: Polymorphic rewriting conserves algebraic strong normalization and confluence. Proc. ICALP, LNCS 372 (1989), 137–150.

    Google Scholar 

  4. Bürchert, H.-J.: Matching — a special case of unification? J. Symbolic Computation 8 (1989), 523–536.

    Google Scholar 

  5. Futatsugi, K., Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. Proc. 12th ACM Symp. Principles of Programming Languages (1985), 52–66.

    Google Scholar 

  6. Gallier, J. and Snyder, W.: Complete sets of transformations for general E-unification. Theoretical Computer Science 67 (1988), 203–260.

    Google Scholar 

  7. Garland, S.J., Guttag, J.V.: An Overview of LP, The Larch Prover. Proc. 3rd Int. Conf. Rewriting Techniques and Applications, LNCS 355 (1989), 137–151.

    Google Scholar 

  8. Goldfarb, W.: The undecidability of the second-order unification problem. Theoretical Computer Science 13 (1981), 225–230.

    Google Scholar 

  9. Herold, A.: Combination of Unification Algorithms. Proc. 8th Int. Conf. Automated Deduction, LNCS 230 (1986), 450–469.

    Google Scholar 

  10. Huet, G.: A Unification Algorithm for Typed λ-Calculus. Theoretical Computer Science 1 (1975), 27–57.

    Google Scholar 

  11. Huet, G.: Résolution d'equations dans les languages d'ordre 1, 2,...,ω. Thése d'Etat, Université de Paris VII (1976).

    Google Scholar 

  12. Kirchner, C.: Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories équationnelles, Thèse d'état de l'Université de Nancy I (1985).

    Google Scholar 

  13. Nadathur, G. and Miller, D.: An overview of λProlog. Proc. 5th Int. Conf. Logic Programming, eds. R.A.Kowalski and K.A. Bowen, MIT Press (1988), 810–827.

    Google Scholar 

  14. Nelson, G. and Oppen, D.: Simplification by cooperating decision procedures. ACM TOPLAS 1 (1979), 245–257.

    Google Scholar 

  15. Nipkow, T.: Combining matching algorithms: the regular case. Proc. 3rd Int. Conf. Rewriting Techniques and Applications, LNCS 355 (1989), 343–358.

    Google Scholar 

  16. Paulson, L.C.: Isabelle: The Next 700 Theorem Provers. In P. Odifreddi (editor), Logic and Computer Science, Academic Press (1990), 361–385.

    Google Scholar 

  17. Schmidt-Schauß, M.: Unification in a combination of arbitrary disjoint equational theories. J. Symbolic Computation 8 (1989), 51–99.

    Google Scholar 

  18. Snyder, W.: Higher-order E-unification. Proc. 10th Int. Conf. Automated Deduction, LNCS 449 (1990), 573–587.

    Google Scholar 

  19. Snyder, W and Gallier, J.: Higher-order unification revisited: complete sets of transformations. J. Symbolic Computation 8 (1989), 101–140.

    Google Scholar 

  20. Tidén, E.: Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols. Proc. 8th Int. Conf. Automated Deduction, LNCS 230 (1986), 431–449.

    Google Scholar 

  21. Yelick, K.A.: Unification in combinations of collapse-free regular theories. J. Symbolic Computation 3 (1987), 153–182.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory, University of Cambridge, Pembroke Street, CB2 3QG, Cambridge, England

    Tobias Nipkow

  2. FB Informatik, Universität Bremen, Postfach 330440, D-2800, Bremen 33, Germany

    Zhenyu Qian

Authors
  1. Tobias Nipkow
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhenyu Qian
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ronald V. Book

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nipkow, T., Qian, Z. (1991). Modular higher-order E-unification. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_97

Download citation

  • DOI: https://doi.org/10.1007/3-540-53904-2_97

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-53904-9

  • Online ISBN: 978-3-540-46383-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation