Context unification with one context variable

The context unification problem is a generalization of standard term unification. It consists of finding a unifier for a set of term equations containing first-order variables and context variables. In this paper we analyze the special case of context unification where the use of at most one context variable is allowed and show that it is in NP. The motivation for investigating this subcase of context unification is interprocedural program analysis for programs described using arbitrary terms, generalizing the case where terms were restricted to using unary function symbols. Our results imply that the redundancy problem is in coNP, and that the finite redundancy property holds in this case. We also exhibit particular cases where one context unification is polynomial.