Reputation: 99
So I've got a predicate that works for uninstantiated variables nat_cset(N,Cs)
that relates a natural number with the counting set Sn = {1,2,...,N}
.
nat_cset_(0,Acc,Acc).
nat_cset_(N,Acc,Cs) :- N #> 0, N_1 #= N - 1, nat_cset_(N_1, [N|Acc], Cs).
nat_cset(N,Cs) :- nat_cset_(N,[],Cs).
One thing I've noticed is that is the following query nat_cset(N,Cs), N = 6.
enters an infinite loop while N = 6, nat_cset(N,Cs).
does not:
?- nat_cset(N,Cs), N = 6, false.
...
?- N = 6, nat_cset(N,Cs), false.
false
This happens because in the second query, prolog it should only look for solutions for N = 6 while in the first query, prolog will search for infinite solutions such that N = 6.
My question is, is this 'adequate' behaviour for nat_cset/2
or is this a unwanted behaviour? I've read somewhere that the order of predicates changing the solutions makes it not monotonic and removes its purity, but at the same time I can't think of a way to make nat_cset/2
any different.
Sorry for the noob question, a lot of the concepts are new to me and I'm still trying to process it all.
Upvotes: 2
Views: 150
Reputation: 10122
The query
?- nat_cset(N,Cs), N = 6, false.
has exactly the same termination property as
?- nat_cset(N,Cs), false,N = 6.
So the goal N = 6
has in this case no influence on termination whatsoever,1. Only if you add it in front can it influence termination.
As already said, rather start with programs using successor-arithmetics and not clpfd
/clpz
. They are much simpler and still expose the relevant properties needed to understand failure slicing.
1 This assumes that N = 6
is always terminating, as it does with clpz
in Scryer and clpfd
in SWI. With general coroutining this is not necessarily the case. Think of freeze(N, inf), N = 6
.
Upvotes: 7