Higher-order matching modulo (super)developements. Applications to second-order matching

Germain Faure 1, 2
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : To perform higher-order matching, we need to decide the beta eta-equivalence on lambda-terms. The first way to do it is to use simply typed lambda-calculus and this is the usual framework where higher-order matching is performed. Another approach consists in deciding a restricted equivalence. This restricted equivalence can be based on finite developments or more interestingly on finite superdevelopments. We consider higher-order matching modulo (super)developments over untyped lambda-terms for which we propose terminating, sound and complete matching algorithms. This is in particular of interest since all second-order beta-matches are matches modulo superdevelopments. We further propose a restriction to second-order matching that gives exactly all second-order matches. We finally apply these results in the context of higher-order rewriting.
Type de document :
Rapport
[Research Report] 2009
Liste complète des métadonnées

Littérature citée [39 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00429978
Contributeur : Germain Faure <>
Soumis le : jeudi 5 novembre 2009 - 14:12:47
Dernière modification le : mercredi 25 avril 2018 - 10:45:26
Document(s) archivé(s) le : mardi 16 octobre 2012 - 13:20:22

Fichier

matching.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00429978, version 1

Collections

Citation

Germain Faure. Higher-order matching modulo (super)developements. Applications to second-order matching. [Research Report] 2009. 〈inria-00429978〉

Partager

Métriques

Consultations de la notice

217

Téléchargements de fichiers

116