|
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}@ncc.up.pt
February 2005
Abstract
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.
|