reversal query from DCG chapter loops

[jasonhemann]

When I try to follow the reversal example from the DCG chapter, the example query loops on my system. More generally, the query phrase(reversal([a], Ls) loops under either scryer or swipl using the following file.

%% reversal.pl
%% :- use_module(library(dcg/basics)). %% For swipl
%% :- use_module(library(dcgs)). %% For scryer

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

Can you verify that your system actually produces the below answer from the book's sample query? If so, can you imagine what I might be doing wrong?

?- phrase(reversal("abcd"), Ls).
   Ls = "dcba".

I am currently using the following versions:

$ swipl --version
SWI-Prolog version 8.4.2 for x86_64-darwin
$  scryer-prolog --version
"v0.9.0-63-gc490d818"

[mthom]

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].

[triska]

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.

[jasonhemann]

Ah. Quite so. Thank you.