Linear pattern matching of compressed terms and polynomial rewriting

摘要

We consider term rewriting under sharing in the form of compression by singleton tree grammars (STG), which is more general than the term dags. Algorithms for the subtasks of rewriting are analysed: finding a redex for rewriting by locating a position for a match, performing a rewrite step by constructing the compressed result and executing a sequence of rewrite steps. The first main result is that locating a match of a linear term s in another term t can be performed in polynomial time if s, t are both STG-compressed. This generalizes results on matching of STG-compressed terms, matching of straight-line-programcompressed strings with character-variables, where every variable occurs at most once, and on fully compressed matching of strings. Also, for the case where s is directed-acyclic-graph (DAG)-compressed, it is shown that submatching can be performed in polynomial time. The general case of compressed submatching can be computed in non-deterministic polynomial time, and an algorithm is described that may be exponential in the worst case, its complexity is nO(k), where k is the number of variables with double occurrences in s and n is the size of the input. The second main result is that in case there is an oracle for the redex position, a sequence of m parallel or single-step rewriting steps under STG-compression can be performed in polynomial time. This generalizes results on DAG-compressed rewriting sequences. Combining these results implies that for an STG-compressed term rewrite system with left-linear rules, m parallel or single-step term rewrite steps can be performed in polynomial time in the input size n and m.