Higher order disunification: Some decidable cases

Abstract

This paper deals with higher-order disunification, i.e solving constraints on simply typed lambda-terms involving the ηβ equality, negation, the logical connectives ∧ and ∨ and universal and existential quantification. Contrary to the first-order case, higher-order disunification is undecidable and even not semi-decidable since it contains higher-order unification and its negation. Therefore we merely give general rules to simplify the basic constraints called equational problems and we use these rules to get decision procedures in some useful cases. First we prove that the second-order top-linear complement problem and other special cases of complement problems are decidable. Then we consider the case when all the terms involved in the constraints are patterns i.e when the arguments of a free variable are distinct bound variables. In this case, we can devise new rules to extend the initial set of rules, and we are able to prove the decidability of the general case of disunification constraints, i.e involving mixed quantification.