DCGs: A declarative/logical way to describe pushback lists?

[jeshan]

I see that you explained this concept in the procedural sense but not the logical one (or did I miss it?). A logical explanation would explain the concept better.

Here, you write:

the-power-of-prolog/prolog/dcg.html

Lines 505 to 518 in d69a239

	Head, <b>[T<sub>1</sub>,...,T<sub>n</sub>]</b> --&gt; Body.
	</pre>
	can be read operationally as: parse the list
	using&nbsp;<tt>Body</tt>, then prepend the
	terms&nbsp;<tt>T<sub>1</sub>,&nbsp;...,&nbsp;T<sub>n</sub></tt> to the remaining list.
	For example:
	<pre>
	nt1, <b>[b]</b> --&gt; [a].
	nt2 --&gt; [b].
	</pre>
	The body of <tt>nt1//0</tt> describes a list whose single element

Head, [T1,...,Tn] --> Body.

can be read operationally as: parse the list using Body, then prepend the terms T1, ..., Tn to the remaining list...

Would it be accurate to say that:

Head describes the list difference Body minus [T1, ..., Tn] ?

I was expecting you to write something like that.

Continuing the above:

nt1, [b] --> [a].

The body of nt1//0 describes a list whose single element is the atom a. Operationally, after nt1//0 has consumed the atom a in a list that is being parsed, it inserts the atom b in front of the remaining list.

If my statement above is correct, then I suppose that a more concise version of the previous sentence could be:

nt1 describes the list difference [a] - [b]

which is proven by the output:

?- phrase(nt1, A, B), list_diff(A, B) = list_diff([a], [b]).
A = [a],
B = [b].

Side note: We could add that using phrases like "X is the list difference Y - Z" would make it obvious to the newbie why phrase/3 is needed instead of phrase/2.

If I think of nt1 in this way, it helped me to understand the section about passing implicit states. E.g you write:

state(S0, S), [S] --> [S0].

The nonterminal state(S0, S) can be read as: "The current state is S0, and henceforth it is S".

That left me scratch my head! Instead, I was expecting something like:

state(S0, S) describes the list difference [S0] - [S] where the current state is S0 followed by the state S

I practised and learnt that we can make the list track all state changes by making a simple change:

% keep the S to maintain a history
state(S0, S), [S] --> [S0, S].

I understood that this works because it describes the list difference [S0, S] - [S] equalling [S0], describing only the expected current state S0.

What do you think of my logical description of pushback lists?