Higher-order matching modulo superdevelopements. Applications to second-order matchingReportar como inadecuado




Higher-order matching modulo superdevelopements. Applications to second-order matching - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LIX - Laboratoire d-informatique de l-École polytechnique Palaiseau 2 TYPICAL - Types, Logic and computing LIX - Laboratoire d-informatique de l-École polytechnique Palaiseau, Inria Saclay - Ile de France, Polytechnique - X, 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 superdevelopments 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.





Autor: Germain Faure -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados