Linear higher-order matching is NP-complete

Philippe De Groote 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We consider the problem of higher-order matching restricted to the set of linear lambda-terms (i.e., lambda-terms where each abstraction (lambda 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.
Keywords : filtrage matching
Type de document :
Communication dans un congrès
Leo Bachmair. International Conference on Rewriting Techniques & Applications - RTA'2000, 2000, Norwich, UK, Springer-Verlag, 1833, pp.127-140, 2000, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00099220
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:51:57
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00099220, version 1

Collections

Citation

Philippe De Groote. Linear higher-order matching is NP-complete. Leo Bachmair. International Conference on Rewriting Techniques & Applications - RTA'2000, 2000, Norwich, UK, Springer-Verlag, 1833, pp.127-140, 2000, Lecture Notes in Computer Science. 〈inria-00099220〉

Partager

Métriques

Consultations de la notice

75