





Technical Report: DCC200501Avoiding Infinite Loops in the Solving of Equations Involving Sequence Variables and Terms with Flexible Arity Function SymbolsJorge Coelho and Mário FloridoR. do Campo Alegre 823, 4150180 Porto, Portugal Phone: 351 22 6078830, Fax: 351 22 6003654 Email: {jcoelho,amf}@ncc.up.pt AbstractSolving 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 depthfirst 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. 

