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