Unification and Matching of Compressed Terms

Manfred Schmidt-Schauss (Johann Wolfgang Goethe Universität Frankfurt am Main)

Unification of first-order terms requires exponential time without compression, but can be computed in O(n log(n)) time using a dag representation. A general device for compression and studying variants of algorithms on compressed terms are singleton tree grammars (SLP) that generalize straight line programs (SLPs). In the best case these allow for an exponential compression factor of the size of strings and terms, and also for the depth of terms. Plandowski's theorem shows that the equality test of two SLP-compressed words can be done in polynomial time in the size of the SLPs, which also holds in the more general case of STG-compressed terms.

Different variants of unification and matching algorithms for STG-compressed terms have been developed and analyzed. First-order unification can be performed in polynomial time on the size of the compressed terms. The best currently known upper bound is O(|V|(m+|V|)^3), (m: size of the compression, n: depth of the grammar, |V|: number of variables) using an efficient algorithm for compressed string matching of Y. Lifshits. First-order matching requires O((m+|V|)^3) time, using the same ideas. Context matching can be shown to remain in NP if the input terms are STG-compressed ground terms instead of usual first-order terms.