Third order matching is decidable (Q1337691)

The matching problem in the simply typed \(\lambda\)-calculus has been shown decidably by Huet in the case of at most second order, but it is open in general. The author shows that it is decidable in the case of third order. The main idea is that if a problem \(a=b\), where \(b\) is ground, has a solution, then it also has a solution whose depth (of Böhm tree) is bounded by some integer depending only on the problem. This is first shown for an interpolation problem as an intermediate stage. The proof is very neatly described.