`reversal` query from DCG chapter loops about the-power-of-prolog HOT 3 CLOSED

There's a slight error in the transcription of the first call of the second clause. After correcting, we get:

reversal([]) --> [].
reversal([L|Ls]) --> reversal(Ls), [L].

from the-power-of-prolog.

Adding to this, we can use failure slicing to produce explanations for non-termination. For example, I can insert {false} at any point of a grammar rule, like this:

reversal([]) --> { false }, [].
reversal([L|Ls]) --> reversal([Ls]), { false }, [L].

This means that we are effectively considering now the following fragment:

reversal([L|Ls]) --> reversal([Ls]).

With which we still get (universal) non-termination:

?- phrase(reversal("abcd"), Ls), false.
   loops.

As long as this fragment does not terminate, the original program also does not terminate. Hence, if you want to improve termination properties of your grammar, you must change this specific fragment in the original program.

The ability to selectively remove portions of the code and still be able to make interesting statements about the original program by reasoning about only the remainder is one of the greatest attractions of logic programming.

from the-power-of-prolog.

Ah. Quite so. Thank you.

from the-power-of-prolog.