Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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
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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [39 references]  Display  Hide  Download
Contributor : Germain Faure Connect in order to contact the contributor
Submitted on : Thursday, November 5, 2009 - 2:12:47 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:00 AM
Long-term archiving on: : Tuesday, October 16, 2012 - 1:20:22 PM


Files produced by the author(s)


  • HAL Id : inria-00429978, version 1



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



Record views


Files downloads