First-order term unification is an essential concept in areas like functional and
logic programming, automated deduction, deductive databases, artificial intelligence,
information retrieval, compiler design, etc. We build upon recent
developments in grammar-based compression mechanisms for terms and investigate
algorithms for first-order unification and matching on compressed
terms.
We prove that the first-order unification of compressed terms is decidable
in polynomial time, and also that a compressed representation of the most
general unifier can be computed in polynomial time. Furthermore, we present
a polynomial time algorithm for first-order matching on compressed terms.
Both algorithms represent an improvement in time complexity over previous
results [GGSS09, GGSS08].
We use several known results on the tree grammars used for compression,
called singleton tree grammars (STG)s, like polynomial time computability
of several subalgorithmms: certain grammar extensions, deciding equality of
represented terms, and generating their preorder traversal. An innovation is
a specialized depth of an STG that shows that unifiers can be represented in
polynomial space
