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 both terms s and t are given using some kind of compressed representation. In this setting, term representation with dags, but also with the more general formalism of singleton tree grammars, are considered. 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 singleton tree grammars. The special cases of first-order matching and also unification with STGs are shown to be decidable in PTIME.

• Type: Conference
• Year: 2008
• Where: LICS
• Authors: Adria Gascón, Guillem Godoy, Manfred Schmidt-Schauß
• Keywords: Computer Science, Contains Context Variables, Context Variables, LICS 2008, Singleton Tree Grammars