The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed $\lambda$-calculus, i.e. to solve the equation a = b where a and b are simply typed $\lambda$-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 occurring in the problem are at most third order.

翻译：高阶匹配问题是指在简单类型λ演算中判断一个项是否为另一个项的实例的问题，即求解方程a = b，其中a和b是简单类型λ项，且b是基项。该问题的可判定性仍未解决。我们证明了问题中出现的变量至多为三阶这一特殊情形的可判定性。