Linear Higher-Order Matching Is NP-Complete

We consider the problem of higher-order matching restricted et 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.

• Type: Conference
• Year: 2000
• Where: RTA
• Authors: Philippe de Groote
• Keywords: Abstraction X, Free Occurrence, Linear -terms, RTA 2000, Theoretical Computer Science