Luiz
Luiz

Reputation: 99

Predicate order change causes infinite loop

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

Answers (1)

false
false

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

Related Questions