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.

Solution 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.

---

false ; true

(true -> false) ; true

(true -> false) ; true

(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.

Solution 2

The arrow in Prolog does not correspond to material implication in first-order logic. It's a ternary "if-then-else" operator with an optional alternative. Because of the way it's implemented in Prolog syntax,

(true -> false) ; true

does not mean what you think it does. It's parsed as true -> false ; true:

?- ((true -> false) ; true) =.. Expr.
Expr = [;, (true->false), true].

?- (true -> false ; true) =.. Expr.
Expr = [;, (true->false), true].

so it fails, because it means "if true then false else true", i.e. false.

Comments

[bsky]

Do you mean to say "if true then false else true" ?

[Fred Foo]

@octavian: eh, yes. Fixed that.

[bsky]

Can't the expression be seen as ;(->(true, false), true)? In this case, how is "choice-points [...] for the else-part are removed" possible, as '->/2' is an argument to ';/2', so it shouldn't be able to change its definition?

[lurker]

@octavian, actually it is consistent if you take the analogous example of ;((true,!,false),false). That query will come back false because, even though the first expression is false, the choice point has been eliminated with a cut. I added further explanation to my answer.

[Will Ness]

a rare - good and interesting - question indeed. :) I'll just add that it is natural to omit the false alternative ( (true -> false; false) ; true. ) and this Q shows that in Prolog we should be really careful about it.

[lurker]

@octavian is my answer satisfactory?