Prolog arrow operator

Question

| ?- true ; (true->false)
yes
| ?- (true->false) ; true.
no
| ?- false ; true.
yes

From what I understand the 'yes'/'no' result tells the user whether the query was successful or not. The query is always successful on the predicate true and it always fails on false.

1. since ;/2 means OR (which is commutative) the first two queries should be equivalent(both successful)

2. in predicative logic the formulas (true->false) and false evaluate to FALSE, so the last two queries should be equivalent

Therefore: the second query appears to be inconsistent with theoretical logic

Is there a mistake in my reasoning? I feel I'm not understanding something fundamental.

Answer 1

This is a very good question.

Just to elaborate on @larsmans's answer, the ->/2 predicate acts as an if-then-else when combined with the ;/2 predicate. On it's own, it's just if-then.

Looking at the if-then-else construct, the description given in the GNU Prolog manual says:

->/2 is often combined with ;/2 to define an if-then-else as follows: Goal1 -> Goal2 ; Goal3. Note that Goal1 -> Goal2 is the first argument of the (;)/2 and Goal3 (the else part) is the second argument. Such an if-then-else control construct first creates a choice-point for the else-part (intuitively associated with ;/2) and then executes Goal1. In case of success [of Goal1], all choice-points created by Goal1 together with the choice-point for the else-part are removed and Goal2 is executed. If Goal1 fails then Goal3 is executed.

In this case we have:

(true -> false) ; true

The first true is Goal1, which succeeds. As soon as that happens, according to the description of the behavior of the predicate, the choice point that would lead you to the second true statement (Goal3) is REMOVED. So when the false is encountered, failure occurs with no backtracking to the second true and the entire query fails.

If, however, you did something like this:

foo :-
    true -> false.
foo :-
    true

There's a choice point after the first foo clause fails, so you get:

| ?- foo.
yes.

---

I think the confusion stems from comparing false ; true with (true -> false) ; true. A more analogous expression to (true -> false) ; true would be:

(true, !, false) ; true

Which will also evaluate to false because of how ; works. The ; provides a choice point in the event of failure of the first clause. But if the first clause has a cut and eliminates the choice point, then it won't be taken and the query fails overall.