On tree pattern unification problems

Abstract

The problem of many-to-one unification, i.e. a simultaneous unification of a given set of input pattern terms against the set of all subterms of a given input target term, is studied for linear terms. The proposed algorithms generalize either the many-to-one tree pattern matching algorithm based on the path counting principle or the rooted many-to-one tree pattern unification algorithm based on the pattern elimination principle. In both cases, the asymptotical worst-case time complexity of tree pattern unification is quadratic as in the special case of tree pattern matching. However, the expected time complexity of the “pattern-eliminating” algorithm is linear according to the size of input. A possibility of dynamization of the set of input pattern terms is discussed, too. While the “path-counting” algorithm is not adaptable to the dynamic version of the problem, it turns out that the “pattern-eliminating” algorithm is effective enough also in the case when the set of input pattern terms is changed during the computation.