Solving a Unification Problem under Constrained Substitutions Using Tree Automata

A unification problem under constrained substitutions, a generalization of the usual unification problems, is a useful formalization of a practical problem in which there are some constraints on operations and objects that we can use. In this paper, a procedure to solve the problem under some linearity conditions is introduced. Since the problem is undecidable in general, the procedure falls into an infinite loop for some instances. We clarify a decidable sufficient condition under which our procedure terminates, and review known classes of term rewriting systems that satisfy the condition. The procedure uses tree automata to solve the problem, which is quite a new and promising approach to unification problems.