Skip to main content
SpringerLink
Log in

Complexity of the Higher Order Matching

  • Conference paper
  • First Online:
Automated Deduction — CADE-16 (CADE 1999)

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

Included in the following conference series:

Abstract

We use the standard encoding of Boolean values in simply typed lambda calculus to develop a method of translating SAT problems for various logics into higher order matching. We obtain this way already known NP-hardness bounds for the order two and three and a new result that the fourth order matching is NEXPTIME-hard

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Henk Barendregt, Lambda Calculi with Types, Handbook of Logic in Comput. Sci., vol. 2, S. Abramsky, D.M. Gabbay, T.S.E. Maibaum, eds., Clarendon Press, Oxford, 1992, 118–310.

    Google Scholar 

  2. Lewis D. Baxter, The Complexity of Unification, Ph.D. Thesis, University of Waterloo, 1976.

    Google Scholar 

  3. Paul Bernays, Moses Schönfinkel, Zum Entscheidungsproblem der mathematischen Logik, Math. Annalen, 99 (1928) 342–372.

    Article  MATH  Google Scholar 

  4. Egon Börger, Erich Grädel, Yuri Gurevich, The Classical Decision Problem, Springer-Verlag, 1997.

    Google Scholar 

  5. Hubert Comon, Yan Jurski, Higher order pattern matching and tree automata, Proc. 11th Int’l Workshop on Comput. Sci. Logic, CSL’97, Aarhus, Denmark, August 23-29, 1997, M. Nielsen, W. Thomas, eds., LNCS 1414, Springer-Verlag, 1998.

    Google Scholar 

  6. Gilles Dowek, Third order matching is decidable, Proc. 7th IEEE Symp. Logic in Comput. Sci., LICS’92, Santa Cruz, California, June 22-25, 1992, 2–10, also in Annals of Pure and Applied Logic, 69 (1994), 135-155.

    Google Scholar 

  7. Gilles Dowek, The undecidability of pattern matching in calculi where primitive recursive functionals are representable, Theoret. Comput. Sci., 107(1993) 349–56.

    Article  MATH  MathSciNet  Google Scholar 

  8. Cynthia Dwork, Paris C. Kanellakis, John C. Mitchell, On the sequential nature of unification, J. Logic Programming, 1(1) (1984) 35–50.

    Article  MathSciNet  MATH  Google Scholar 

  9. Warren D. Goldfarb, Note on the undecidability of the second order unification problem, Theoret. Comput. Sci. 13(1981) 225–230.

    Article  MATH  MathSciNet  Google Scholar 

  10. Gerard P. Huet, A unification algorithm for typed λ-calculus, Theoret. Comput. Sci., 1 (1) (1975) 27–57.

    Article  MathSciNet  Google Scholar 

  11. Gerard P. Huet, Résolution d’équations dans des langages d’ordre 1, 2,..., w. Thèse de Doctorat d’État, University of Paris, 1976.

    Google Scholar 

  12. Gerard P. Huet, Bernard Lang, Proving and applying program transformations expressed with second order patterns, Acta Informatica, 11 (1978) 31–55.

    Article  MATH  MathSciNet  Google Scholar 

  13. Ralph Loader, The undecidability of λ-definability, Church Memorial Volume, A. Anderson, M. Zeleny eds., Kluwer Acad. Press, to appear.

    Google Scholar 

  14. Harry G. Mairson, A simple proof of a theorem of Statman, Theoret. Comput. Sci., 103 (1992) 387–394.

    Article  MATH  MathSciNet  Google Scholar 

  15. Dale Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, J. Logic and Comput., 1(4) (1991) 497–536.

    Article  MATH  MathSciNet  Google Scholar 

  16. Vincent Padovani, Filtrage d’ordre supérieur, PhD Thesis, Université Paris VII, 1996.

    Google Scholar 

  17. Christos H. Papadimitriou, Computational Complexity, Addison-Wesley, 1994.

    Google Scholar 

  18. John Alan Robinson, A machine-oriented logic based on the resolution principle, J. ACM, 12(1) (1965) 23–41.

    Article  MATH  Google Scholar 

  19. Aleksy Schubert, Linear interpolation for the higher order matching problem, Technical Report of the Institute of Informatics, Warsaw University, TR 96-16 (237), also in Proc. 7th Int’l Joint Conf. Theory and Practice of Software Development, TAPSOFT’97, Lille, France, April 14-18, 1997, M. Bidoit, M. Dauchet, eds., LNCS 1214, Springer-Verlag, 1997.

    Google Scholar 

  20. Richard Statman, Intuitionistic propositional logic is polynomial-space complete, Theoret. Comput. Sci., 9 (1979) 67–72.

    Article  MATH  MathSciNet  Google Scholar 

  21. Richard Statman, The typed λ-calculus is not elementary recursive, Theoret. Comput. Sci., 9 (1979) 73–81.

    Article  MATH  MathSciNet  Google Scholar 

  22. Richard Statman, Completeness, invariance and λ-definability, J. Symbolic Logic, 47(1) (1982) 17–26.

    Article  MATH  MathSciNet  Google Scholar 

  23. Richard Statman, On the existence of closed terms in the typed λ-calculus II: transformations of unification problems, Theoret. Comput. Sci., 15 (1981) 329–338.

    Article  MATH  MathSciNet  Google Scholar 

  24. Sergei Vorobyov, The “Hardest” Natural Decidable Theory, Proc. 12th Annual IEEE Symp. Logic in Comput. Sci., LICS’97, Warsaw, Poland, June 29-July 2, 1997, 294–305.

    Google Scholar 

  25. David A. Wolfram, The decidability of higher-order matching, Proc. 6th Int’lWorkshop on Unification, Schloß Dagstuhl, Germany, July 29-31, 1992.

    Google Scholar 

  26. David A. Wolfram, The Clausal Theory of Types, Cambridge Tracts in Theor. Comput. Sci. vol. 36, Cambridge University Press, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Wroclaw, Germany

    ToMasz Wierzbicki

Authors
  1. ToMasz Wierzbicki
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wierzbicki, T. (1999). Complexity of the Higher Order Matching. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-48660-7_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66222-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation