To perform higher-order matching, we need to decide the
-terms. The first way to do it is to use simply typed
-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
-terms for which we propose a terminating, sound and complete matching algorithm.
This is in particular of interest since all second-order
-matches are matches modulo superdevelopments. We further propose a restriction to second-order matching that gives exactly all second-order matches.