I'd like to understand why the interaction with swipl appears to be inconsistent.
Here's a typical example. Suppose I have consulted a knowledgebase that includes the following definitions:
acc_max([H|T], A, Max) :- H > A, acc_max(T, H, Max).
acc_max([H|T], A, Max) :- H =< A, acc_max(T, A, Max).
acc_max([], A, A).
max([H|T], Max) :- acc_max(T, H, Max).
Below I show what my screen looks like after I type max([0, 1, 2], X). at the prompt, and hit Enter:
?- max([0, 1, 2], X).
X = 2 ▮
(The ▮ indicates the position of the cursor.)
Note, in particular, that the interpreter's next prompt has not yet appeared.
Here's what the screen looks like after I type ;:
?- max([0, 1, 2], X).
X = 2 ;
false.
?- ▮
Now I finally get the interpreter's prompt.
In contrast, below I show what my screen looks like after I type max([2, 0, 1], X). at the prompt, and hit Enter:
?- max([2, 0, 1], X).
X = 2.
?- ▮
Notice that this time I got the interpreter's prompt right away - I did not need to type ;. Also, there's no false.
I've found many other similar inconsistencies (e.g. sometimes the output true. shows up on the screen, but in other similar situations it doesn't).
As a newcomer to Prolog, I find such inconsistencies disconcerting (not to mention discouraging, since they are a constant reminder that I really have no clue of what's going on).
Is there a simple way to rationalize these inconsistencies?
Alternatively, is there some implementation of Prolog that provides a more consistent and predictable interaction than does SWI-Prolog?
So, as @lurker said, this is the result of choice points - cases where there is a rule that has not been evaluated, which may yield more solutions.
Let's go through an even simpler version of your example, max([0,1],X). vs max([1,0],X)..
max([0,1],X).:
This goes to acc_max([1],0,X)., which matches both acc_max([H|T], A, Max) :- rules. We evaluate them in the order that they appear:
First we see that 1 > 0 is true, and call acc_max([],1,X). This matches only acc_max([], A, A)., and we therefore unify X with 1. We have a solution! But we also have a rule that has not been evaluated yet. This is where you see:
X = 1 ▮
So now we type ;, and evaluate the second acc_max([H|T], A, Max) :- rule. We see that 1 =< 0 is not true, so this rule fails. We are now out of rules to try, so it turns out there are no more solutions. Hence:
X = 1 ;
false.
Now we'll look at max([1,0],X).:
This is now acc_max([0],1,X).. Again, we have two rules, evaluated in the order they appear:
First we see that 0 > 1 is not true, so the first rule fails and we evaluate the second.
Now we see that 0 =< 1 is true, and call acc_max([],1,X). This matches only acc_max([], A, A)., and we therefore unify X with 1 (again). We have the solution, and this time we have no unevaluated rules (ie. no unexplored choice points). So now we see:
X = 1.
... as there is no doubt in Prolog's "mind" that there are no other solutions. If you were to invert the order of the rules:
acc_max([], A, A).
acc_max([H|T], A, Max) :- H =< A, acc_max(T, A, Max).
acc_max([H|T], A, Max) :- H > A, acc_max(T, H, Max).
... you would see the behaviour invert as well.
Hopefully this helps to demonstrate that this is a consistent and predictable interaction, and should be one shared by all variants of Prolog.