Context Matching for Compressed Terms

This paper is an investigation of the matching problem for term equations s = t where s contains context variables and first-order variables, and both terms s and t are given using some kind of compressed representation. The main result is a polynomial time algorithm for context matching with dags, when the number of different context variables is fixed for the problem. NP-completeness is obtained when the terms are represented using the more general formalism of singleton tree grammars. As an ingredient of this proof, we also show that the special case of first-order matching with singleton tree grammars is decidable in polynomial time.