Skip to main content
SpringerLink
Log in

Efficient second-order matching

  • Regular Papers
  • Conference paper
  • First Online:
Book cover Rewriting Techniques and Applications (RTA 1996)

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

Included in the following conference series:

Abstract

The standard second-order matching algorithm by Huet may be expansive in matching a flexible-rigid pair. On one hand, many fresh free variables may need to be introduced; on the other hand, attempts are made to match the heading free variable on the flexible side with every “top layer” on the rigid side and every argument of the heading free variable with every subterm covered by the “top layer”. We propose a new second-order matching algorithm, which introduces no fresh free variables and just considers some selected “top layers”, arguments of the heading free variable and subterms covered by the corresponding “top layers”. A first implementation shows that the new algorithm is more efficient both in time and space than the standard one for a great number of matching problems.

Research partially supported by ESPRIT Basic Research WG COMPASS 6112 and BMBF Project UniForM.

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. T. Boy de la Tour and R. Caferra. Proof analogy in interactive theorem proving: A method to express and use it via second order pattern matching. In proceedings of AAAI'87, 1987.

    Google Scholar 

  2. T. Boy de la Tour and R. Caferra. A formale approach to some usually informal techniques used in mathematical reasoning. In ISSAC'88, pages 402–406. Lecture Notes in Computer Science, 1988.

    Google Scholar 

  3. R. S. Boyer and J. S. Moore. A Theorem Prover for a Computational Logic. In Proc. of the 10th International Conference on Automated Deduction, 1990.

    Google Scholar 

  4. R. Curien. Outils pour la preuve par analogie. PhD thesis, Université Henri Poincaré — Nancy 1, January 1995.

    Google Scholar 

  5. R. Curien. Second Order E-matching as a Tool for Automated Theorem Proving. In Proceedings of EPIA '93 (Portugese Conference on Artificial Intelligence) Porto, Portugal., volume 727 of Lecture Notes in Artificial Intelligence, 93.

    Google Scholar 

  6. R. Curien and Z. Qian. Efficiency for second-order matching: the syntactic and AC-cases. Technical report, 1995. Draft paper.

    Google Scholar 

  7. G. Dowek. A Second-order Pattern Matching Algorithm in the Cube of Typed λ-calculi. In Mathematical Fundation of Computer Science, LNCS 520, 1991.

    Google Scholar 

  8. R. Harper, D. MacQueen, and R. Milner. Standard ML. Technical report, Dept. of Cmputer Science, University of Edinburg, 1986.

    Google Scholar 

  9. G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

    Article  Google Scholar 

  10. G. Huet. Résolution d'Equations dans les langages d'Ordre 1,2, ...,ω. Thèse de Doctorat d'Etat, Université de Paris 7 (France), 1976.

    Google Scholar 

  11. G. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31–55, 1978.

    Article  Google Scholar 

  12. T. Kolbe and C. Walther. Reusing proofs. In A. Cohn, editor, ECAI'94, 11th European Conference on Artificial Intelligence, pages 80–84, 1994.

    Google Scholar 

  13. B. Krieg-Brüchner, J. Liu, H. Shi, and B. Wolff. Towards correct, effficient and reusable transformational developments. In ”KORSO: Methods, Languages, and Tools for the Construction of Correct Software”, ages 270–284. LNCS 1009, 1995.

    Google Scholar 

  14. T. Nipkow and Z. Qian. Modular higher-order E-unification. In R. Book, editor, Proc. 4th Int. Conf. Rewriting Techniques and Applications, pages 200–214. LNCS 488, 1991.

    Google Scholar 

  15. L. Paulson. Isabelle — A Generic Theorem prover. LNCS 828, 1994.

    Google Scholar 

  16. Z. Qian and K. Wang. Higher-order E-unification for arbitrary theories. In K. Apt, ed., Proc. 1992 Joint Int. Conf. and Symp. on Logic Programming. MIT Press, 1992.

    Google Scholar 

  17. H. Shi. Extended Matching with Applications to Program Transformation. PhD thesis, Universität Bremen, 1994.

    Google Scholar 

  18. W. Snyder. Higher-order E-unification. In M. Stickel, editor, Proc. 10th Int. Conf. Automated Deduction, pages 573–587. Springer-Verlag LNCS 449, 1990.

    Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIN-CNRS & INRIA-Lorraine, 615, rue du jardin botanique, BP 101, 54602, Vandoeuvre-les-Nancy Cedex, France

    Régis Curien

  2. FB3 Informatik, Universität Bremen, Bibliothekstr. 4, 28359, Bremen, Germany

    Zhenyu Qian & Hui Shi

Authors
  1. Régis Curien
    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

  3. Hui Shi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Harald Ganzinger

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Curien, R., Qian, Z., Shi, H. (1996). Efficient second-order matching. In: Ganzinger, H. (eds) Rewriting Techniques and Applications. RTA 1996. Lecture Notes in Computer Science, vol 1103. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61464-8_62

Download citation

  • DOI: https://doi.org/10.1007/3-540-61464-8_62

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61464-7

  • Online ISBN: 978-3-540-68596-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation