Matching modulo superdeveloppements. Application to second-order matching. - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2006

Matching modulo superdeveloppements. Application to second-order matching.

Résumé

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 based on finite superdevelopments. We consider higher-order matching modulo this equivalence over untyped lambda-terms for which we propose a terminating, sound and complete matching algorithm. 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.
Fichier principal
Vignette du fichier
lpar06.pdf (203.45 Ko) Télécharger le fichier

Dates et versions

inria-00095608 , version 1 (18-09-2006)

Identifiants

  • HAL Id : inria-00095608 , version 1

Citer

Germain Faure. Matching modulo superdeveloppements. Application to second-order matching.. 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning - LPAR 2006, Nov 2006, Phnom Penh/Cambodge. ⟨inria-00095608⟩
50 Consultations
90 Téléchargements

Partager

Gmail Facebook X LinkedIn More