On Non-Termination in DCGs
Manuel Vilares Ferro, David Cabrero, M Pardo · 2007
Non-termination is a crucial problem when encoding unification-based grammar formalisms, although practical systems often diverge from their theoretical definitions. By termination we mean here finiteness of all possible logical derivations starting in the initial goal. Although from a theoretical point of view, we can claim it for decidable problems, often logical problems are confronted with the problem that an apparently correct program may fail to terminate for certain forms of the input. This is, typically, the case of PROLOG programs with left-recursion on local variables.