Higher-Order Matching in the Linear Lambda Calculus in the Absence of Constants Is NP-Complete

  • Ryo Yoshinaka
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


A lambda term is linear if every bound variable occurs exactly once. The same constant may occur more than once in a linear term. It is known that higher-order matching in the linear lambda calculus is NP-complete (de Groote 2000), even if each unknown occurs exactly once (Salvati and de Groote 2003). Salvati and de Groote (2003) also claim that the interpolation problem, a more restricted kind of matching problem which has just one occurrence of just one unknown, is NP-complete in the linear lambda calculus. In this paper, we correct a flaw in Salvati and de Groote’s (2003) proof of this claim, and prove that NP-hardness still holds if we exclude constants from problem instances. Thus, multiple occurrences of constants do not play an essential role for NP-hardness of higher-order matching in the linear lambda calculus.


Problem Instance Free Variable Interpolation Problem Atomic Type Categorial Grammar 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    de Groote, P.: Linear higher-order matching is NP-complete. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 127–140. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  2. 2.
    de Groote, P.: Towards abstract categorial grammars. In: Association for Computational Linguistics, 39th Annual Meeting and 10th Conference of the European Chapter, Proceedings of the Conference, pp. 148–155 (2001)Google Scholar
  3. 3.
    Dougherty, D., Wierzbicki, T.: A decidable variant of higher order matching. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 340–351. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Dowek, G.: Third order matching is decidable. Annals of Pure and Applied Logic 69, 135–155 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science 13, 225–230 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Huet, G., Lang, B.: Proving and applying program transformations expressed with second order patterns. Acta Informatica 11, 31–55 (1978)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Kilpeläinen, P., Mannila, H.: Ordered and unordered tree inclusion. SIAM Journal of Computing 24(2), 340–356 (1995)zbMATHCrossRefGoogle Scholar
  8. 8.
    Levy, J.: Linear second-order unification. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 332–346. Springer, Heidelberg (1996)Google Scholar
  9. 9.
    Loader, R.: Higher order β matching is undecidable. Logic Journal of the IGPL 11(1), 51–68 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Padovani, V.: Decidability of fourth-order matching. Mathematical Structures in Computer Science 10(3), 361–372 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Pogodalla, S.: Using and extending ACG technology: Endowing categorial grammars with an underspecified semantic representation. In: Proceedings of Categorial Grammars 2004, Montpellier, June 2004, pp. 197–209 (2004)Google Scholar
  12. 12.
    Salvati, S., de Groote, P.: On the complexity of higher-order matching in the linear λ-calculus. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 234–245. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Ryo Yoshinaka
    • 1
    • 2
  1. 1.Graduate School of Interdisciplinary Information StudiesUniversity of TokyoTokyoJapan
  2. 2.National Institute of InformaticsTokyoJapan

Personalised recommendations