## 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.