Skip to Main content Skip to Navigation
Reports

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

Germain Faure 1, 2
2 TYPICAL - Types, Logic and computing
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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
Complete list of metadata

Cited literature [39 references]  Display  Hide  Download

https://hal.inria.fr/inria-00429978
Contributor : Germain Faure <>
Submitted on : Thursday, November 5, 2009 - 2:12:47 PM
Last modification on : Thursday, March 5, 2020 - 6:21:47 PM
Long-term archiving on: : Tuesday, October 16, 2012 - 1:20:22 PM

File

matching.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

268

Files downloads

217