Loop checks for logic programs with functions

Two complete loop checking mechanisms have been presented in the literature for logic programs with functions: OS-check and EVA-check. OS-check is com putationally efficient but quite unreliable in that it often mis-identifies infinite loops, whereas EVA-check is reliable for a majority of cases but quite expensive. In this paper, we develop a series of new complete loop ch ecking mechanisms, called VAF-checks. The key technique we introduce is the notion of expanded variants, which captures a key structural characteristi c of infinite loops. We show that our approach is superior to both OS-check and EVA-check in that it is as efficient as OS-check and as reliable as EV A-check. (C) 2001 Elsevier Science B.V. All rights reserved.