Technical Report: DCC-2005-01

Avoiding Infinite Loops in the Solving of Equations Involving Sequence Variables and Terms with Flexible Arity Function Symbols

Jorge Coelho and Mário Florido

DCC-FC & LIACC, Universidade do Porto
R. do Campo Alegre 823, 4150-180 Porto, Portugal
Phone: 351 22 6078830, Fax: 351 22 6003654
E-mail: {jcoelho,amf}
February 2005


Solving equations involving terms with variables that can be instantiated to sequences of terms (sequence variables) and terms with function symbols of arbitrary arity may lead to infinite loops. This is particularly relevant when the implementations traverse the solution tree using a depth-first strategy, because some solutions become unreachable when they appear after a branch that loops. In this paper we present a simple method for checking if a branch will lead to a loop. This makes it possible to go on with the unification algorithm without trying to explore those branches. The technique we use is based on an abstraction of the original unification by a Diophantine equation on the sizes of the terms involved. We present this abstraction and show that it is correct with respect to the original unification.