Prolog arrow operator
logic, prolog
Solution
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-els`e 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.
Problem
``` | ?- 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`. since `;/2` means OR (which is commutative) the first two queries should be equivalent(both successful) 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.