Remove leading s(s(0)) in list

问题:

(This is a followup to that question).

How to write lead1(Xs,Ys) which is true, iff Ys is a suffix of Xs with all leading s(s(0)) terms removed. Thus instead of removing leading 0s this question is now about removing leading s(s(0))s.

^{Compared to the original question, the difficulty lies here in handling cases of s(X) and s(s(X)) properly.}

回答1:

Here's a version with if_/3 and =/3:

list_suffix([],[]).
list_suffix([X|Xs],S) :-
   if_(X=s(s(0)), list_suffix(Xs,S), S=[X|Xs]).

Queries with a ground first argument succeed deterministically:

?- list_suffix([s(0)],S).
S = [s(0)].

?- list_suffix([s(0),s(s(0))],S).
S = [s(0), s(s(0))].

?- list_suffix([s(s(0)),s(0),s(s(0))],S).
S = [s(0), s(s(0))].

?- list_suffix([s(s(0)), s(s(0)),s(0),s(s(0))],S).
S = [s(0), s(s(0))].

If the list consists of a term different from s/1, say f(_) the second list is identical to the first:

?- list_suffix([f(_)],S).
S = [f(_G201)].

?- list_suffix([f(_)],[]).
false.

Partially instantiated lists work as well:

?- list_suffix([X, s(s(0)),s(0),s(s(0))],S).
X = s(s(0)),
S = [s(0), s(s(0))] ;
S = [X, s(s(0)), s(0), s(s(0))],
dif(X, s(s(0))).

The most general query works as well but is listing the answer in an unfair manner:

?- list_suffix(X,Y).
X = Y, Y = [] ;
X = [s(s(0))],
Y = [] ;
X = [s(s(0)), s(s(0))],
Y = [] ;
X = [s(s(0)), s(s(0)), s(s(0))],
Y = [] ;
.
.
.

However, this can be remedied by prefixing a goal length/2:

?- length(X,_), list_suffix(X,Y).
X = Y, Y = [] ;
X = [s(s(0))],
Y = [] ;
X = Y, Y = [_G155],
dif(_G155, s(s(0))) ;
X = [s(s(0)), s(s(0))],
Y = [] ;
X = [s(s(0)), _G79],
Y = [_G79],
dif(_G79, s(s(0))) ;
X = Y, Y = [_G155, _G158],
dif(_G155, s(s(0))) ;
X = [s(s(0)), s(s(0)), s(s(0))],
Y = [] ;
.
.
.

回答2:

Hiere is an adaptation of my answer of the previous question. It shows the use of when/2 instead of freeze/2. freeze/2 only follows a nonvar/1 condition on the first argument. when/2 can follow more complex conditions.

lead(X, Y) :- var(X), !, freeze(X, lead(X,Y)).
lead([X|Y], Z) :- \+ ground(X), !, when(ground(X), lead([X|Y],Z)).
lead([s(s(0))|X], Y) :- !, lead(X, Y).
lead(X, X).

Here are some example runs, I am picking similar examples as in my answer I gave to the previous answer. We see how when/2 adapts its own condition when the list argument gets gradually instantiated:

?- lead([s(0),s(s(0)),s(s(0)),s(0)],Y).
Y = [s(0), s(s(0)), s(s(0)), s(0)].

?- lead([s(s(0)),s(s(0)),s(s(0)),s(0)],Y).
Y = [s(0)].

?- lead([X,s(s(0)),s(s(0)),s(0)],Y), X=s(_).
X = s(_G3686),
when(ground(_G3686), lead([s(_G3686), s(s(0)), s(s(0)), s(0)], Y)).

?- lead([X,s(s(0)),s(s(0)),s(0)],Y), X=s(0).
X = s(0),
Y = [s(0), s(s(0)), s(s(0)), s(0)].

?- lead([X,s(s(0)),s(s(0)),s(0)],Y), X=s(s(_)).
X = s(s(_G3713)),
when(ground(_G3713), lead([s(s(_G3713)), s(s(0)), s(s(0)), s(0)], Y)).

?- lead([X,s(s(0)),s(s(0)),s(0)],Y), X=s(s(0)).
X = s(s(0)),
Y = [s(0)].

freeze/2 and when/2 are corouting primitives. Their pureness is well documented in the literature. According to this source the first Prolog system with corouting was Prolog-II with its geler/2 primitive. The source also mentions the importance of corouting to bootstrap constraint solvers.

Assume pureness is tested with commutativity, here is a sample test:

?- lead([X,s(s(0)),s(s(0)),s(0)],Y), X=s(s(0)).
X = s(s(0)),
Y = [s(0)].

?- X=s(s(0)), lead([X,s(s(0)),s(s(0)),s(0)],Y).
X = s(s(0)),
Y = [s(0)].

But freeze/2 and when/2 not necesserely guarantee completeness, as I already wrote in my first answer we might need to do something 'at the end'. Means after a query we might have a set of floundering goals. In constraint programming we would then start labeling.

Also freeze/2 and when/2 cannot find early fails by combining goals, as constraint solvers can do.

The above eexample runs with SWI-Prolog without some import, and in Jekejeke Prolog use the Minlog Extension and import library(term/suspend).