As usual when a problem is undecidable, besides building a semi-decision algorithm, we are also interested in identifying decidable subcases. In this section, we present a few decidable subcases of higher-order unification. These subcases are obtained by restricting the order, the arity or the number of occurrences of variables, or by taking terms of a special form. For some subcases, Huet's algorithm terminates, for others it does not and we must design another algorithm to prove decidability.
The main conjectures in this area are the decidability of pattern-matching, i.e. the subcase of unification where variables occur only in a single side of equations and the decidability of context unification.