Context unification with one context variable

Adria Gascón, Guillem Godoy, Manfred Schmidt-Schauß, Ashish Tiwari

Research output: Contribution to journalArticlepeer-review


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.
Original languageEnglish
Pages (from-to)173-193
Number of pages21
JournalJournal of Symbolic Computation
Issue number2
Publication statusPublished - 2010


Dive into the research topics of 'Context unification with one context variable'. Together they form a unique fingerprint.

Cite this