prolog cut off in method

I have a question I would like to ask you something about a code snippet:

insert_pq(State, [], [State]) :- !.
insert_pq(State, [H|Tail], [State, H|Tail]) :-
    precedes(State, H).
insert_pq(State, [H|T], [H|Tnew]) :-
    insert_pq(State, T, Tnew).
precedes(X, Y) :- X < Y.  % < needs to be defined depending on problem

the function quite clearly adds an item to a priority queue. The problem I have is the cut off operator in the first line. Presumably whenever the call reaches this line of code this is the only开发者_如何学运维 possible solution to the query, and the function calls would simply unwind (or is it wind up?), there would be no need to back track and search for another solution to the query.

So this cut off here is superfluous. Am I correct in my deduction?

Yes, any half-decent Prolog compiler will notice that there is no other clause where the second argument is an empty list.

It would be more useful at the end of the second clause, though I'd rather combine the second and the third clause and use a local cut (precedes(...) -> ... ; ...).

The particular technique that the compiler users to eliminate candidate predicates for matching is called argument indexing. Different prolog implementations could potentially index different numbers of arguments by default.

So if you're worried about whether an argument is being indexed or not, you should check how many arguments the prolog you're using indexes. According to the SWI reference manual it only indexes the first argument by default. So in your case the cut is actually not redundant. You can however explicitly stipulate which arguments should be indexed using the predicates index/1 and hash/1 which are linked to in the above link.

Or you could just reorder the arguments, or you could just keep the cut.

Yes, you are correct. Even if the compiler isn't half-decent (which SWI Prolog certainly is), the worst it can do is match the second and third clauses, which will fail immediately.

However, if the second clause matches, the third does as well. Is this the intended behaviour?