Skip to Main content Skip to Navigation
Conference papers

Matching modulo superdeveloppements. Application to second-order matching.

Germain Faure 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Germain Faure <>
Submitted on : Monday, September 18, 2006 - 8:45:12 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Thursday, September 20, 2012 - 10:40:48 AM


  • HAL Id : inria-00095608, version 1



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⟩



Record views


Files downloads