Abstract
We consider the problem of higher-order matching restricted to the set of linear λ-terms (i.e., λ-terms where each abstraction λx. M is such that there is exactly one free occurrence of x in M). We prove that this problem is decidable by showing that it belongs to NP. Then we prove that this problem is in fact NP-complete. Finally, we discuss some heuristics for a practical algorithm.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Angluin, D.: Finding patterns common to a set of strings. Journal of Computer and System Sciences 21, 46–62 (1980)
Cervesato, I., Pfenning, F.: Linear higher-order pre-unification. In: Proceedings of the 12th annual IEEE symposium on logic in computer science, pp. 422–433 (1997)
Comon, H.: Completion of rewrite systems with membership constraints. Part I: Deduction rules. Journal of Symbolic Computation 25(4), 397–419 (1998)
Comon, H.: Completion of rewrite systems with membership constraints. Part II: Constraint solving. Journal of Symbolic Computation 25(4), 421–453 (1998)
Dowek, G.: Third order matching is decidable. Annals of Pure and Applied Logic 69(2-3), 135–155 (1994)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science 13(2), 225–230 (1981)
Huet, G.: The undecidability of unification in third order logic. Information and Control 22(3), 257–267 (1973)
Huet, G.: A unification algorithm for typed λ-calculus. Theoretical Computer Science 1, 27–57 (1975)
Huet, G.: Résolution d’équations dans les langages d’ordre 1, 2,..., w. Thèse de Doctorat d’Etat, Université Paris 7 (1976)
Levy, J.: Linear second-order unification. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 332–346. Springer, Heidelberg (1996)
Levy, J.: Decidable and undecidable second-order unification problems. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 47–60. Springer, Heidelberg (1998)
Merenciano, J.M., Morrill, G.: Generation as deduction on labelled proof nets. In: Retoré, C. (ed.) LACL 1996. LNCS (LNAI), vol. 1328, pp. 310–328. Springer, Heidelberg (1997)
Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation 1(4), 497–536 (1991)
Moortgat, M.: Categorial type logic. In: van Benthem, J., ter Meulen, A. (eds.) Handbook of Logic and Language. ch. 2, Elsevier, Amsterdam (1997)
Morrill, G.: Type Logical Grammar: Categorial Logic of Signs. Kluwer Academic Publishers, Dordrecht (1994)
Padovani, V.: Filtrage d’ordre supérieure. Thèse de Doctorat, Université de Paris 7 (1996)
Paulson, L.C.: Isabelle, a generic theorem prover. LNCS, vol. 828. Springer, Heidelberg (1994)
Schmidt-Schauss, M., Schulz, K.U.: Solvability of context equations with two context variables is decidable. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 67–81. Springer, Heidelberg (1999)
Snyder, W., Gallier, J.: Higher order unification revisited: Complete sets of transformations. Journal of Symbolic Computation 8(1-2), 101–140 (1989)
Wierzbicki, T.: Complexity of the higher order matching. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 82–96. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Groote, P. (2000). Linear Higher-Order Matching Is NP-Complete. In: Bachmair, L. (eds) Rewriting Techniques and Applications. RTA 2000. Lecture Notes in Computer Science, vol 1833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721975_9
Download citation
DOI: https://doi.org/10.1007/10721975_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67778-9
Online ISBN: 978-3-540-44980-5
eBook Packages: Springer Book Archive