Higher-order matching modulo (super)developements. Applications to second-order matching - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Reports (Research Report) Year : 2009

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

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.
Fichier principal
Vignette du fichier
matching.pdf (314.68 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00429978 , version 1 (05-11-2009)

Identifiers

  • HAL Id : inria-00429978 , version 1

Cite

Germain Faure. Higher-order matching modulo (super)developements. Applications to second-order matching. [Research Report] 2009. ⟨inria-00429978⟩
71 View
159 Download

Share

Gmail Facebook X LinkedIn More