On the complexity of higher-order matching in the linear $\lambda$-calculus

Sylvain Salvati 1 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 prove that linear second-order matching in the linear $\lambda$-calculus with linear occurrences of the unknowns is NP-complete. This result shows that context matching and second-order matching in the linear $\lambda$-calculus are, in fact, two different problems.
Mots-clés : lambda-calcul matching lambda-calculus linear logic unification logique linéaire filtrage
Type de document :
Communication dans un congrès
Robert Nieuwenhuis. International Conference on Rewriting Techniques and Applications - RTA'2003, Jun 2003, Valencia, Spain, 2706, pp.234-245, 2003, Lecture notes in Computer Science
Liste complète des métadonnées
https://hal.inria.fr/inria-00099593
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:39:07
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00099593, version 1

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Sylvain Salvati, Philippe De Groote. On the complexity of higher-order matching in the linear $\lambda$-calculus. Robert Nieuwenhuis. International Conference on Rewriting Techniques and Applications - RTA'2003, Jun 2003, Valencia, Spain, 2706, pp.234-245, 2003, Lecture notes in Computer Science. 〈inria-00099593〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

160

Contact


archive-ouverte@inria.fr