Abstract

The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed [lgr]-calculus, i.e. to solve the equation a = b where a and b are simply typed [lgr]-terms and b is ground. The decidability of this problem is still open. We prove the decidability of the particular case in which the variables occuring in the problem are at most third order