Decidable higher-order unification problems

Abstract

Second-order unification is undecidable in general. Miller showed that unification of so-called higher-order patterns is decidable and unitary. We show that the unification of a linear higher-order pattern s with an arbitrary second-order term that shares no variables with s is decidable and finitary. A few extensions of this unification problem are still decidable: unifying two second-order terms, where one term is linear, is undecidable if the terms contain bound variables but decidable if they don't.