Patterns in second-order unification

Abstract

The second-order unification problem is undecidable. While unification procedures, like Huet’s pre-unification, terminate with success on unifiable problems, they might not terminate on non-unifiable ones. There are several decidability results for infinitary unification, such as for monadic second-order problems. These results are based on the regular structure of the solutions of these problems and by computing minimal unifiers. In this paper we describe a refinement to Huet’s pre-unification procedure for arbitrary second-order signatures which, in some cases, terminates on problems on which the original pre-unification procedure fails to terminate. We show that the refinement has, asymptotically, the same complexity as the original procedure. Another contribution of the paper is the identification of a new decidable class of second-order unification problems.