Prolog arrow operator

Question

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

From what I understand, the result of yes / no tells the user whether the request was successful or not. The query is always executed in the predicate true , and it always fails to false .

• since ;/2 means OR (which is commutative), the first two queries must be equivalent (both succeed)

• in the predictive logic, the formulas (true->false) and false are evaluated as FALSE, so the last two queries should be equivalent

Therefore: the second query seems incompatible with theoretical logic

Is there a mistake in my reasoning? I feel that I do not understand something fundamental.

Answer 1

This is a very good question.

To clarify @larsmans answer, the predicate ->/2 acts as if-then-else in combination with the predicate ;/2 . Actually, this is just if-then .

Looking at the if-then-else , the description in the GNU Prolog manual reads:

->/2 often combined with ;/2 to define if-then-els e as follows: Goal1 -> Goal2 ; Goal3. Goal1 -> Goal2 ; Goal3. Note that Goal1 -> Goal2 is the first argument of (;) / 2 and Goal3 (the else part) is the second argument . Such an if-then-else Control construct first creates a selection point for the else-part (intuitively related to ;/2 ), and then runs Goal1 . If successful [from Goal1 ], all the selection points created by Goal1 together with the selection point for the else-part are deleted and Goal2 is executed. If Goal1 is not running, Goal3 is running.

In this case, we have:

 (true -> false) ; true 

The first true is Goal1 , which succeeds. As soon as this happens, according to the description of the predicate behavior, the selection point that leads you to the second true statement ( Goal3 ) will be deleted. Therefore, when false is encountered, the failure occurs without returning to the second true , and the entire request fails.

If, however, you did something like this:

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

There is a selection point after the first sentence of foo , so you get:

 | ?- foo. yes. 

---

I think the confusion comes from comparing false ; true false ; true with (true -> false) ; true (true -> false) ; true A more similar expression for (true -> false) ; true (true -> false) ; true would be the following:

 (true, !, false) ; true 

which will also be evaluated as false due to how it works ; . ; provides a point of choice in case of rejection of the first offer But if the first sentence has a cut and excludes the choice point, then it will not be fulfilled, and the request will not be fulfilled as a whole.

Answer 2

The arrow in the Prolog does not correspond to material implication in first-order logic. This is a triple if-then-else statement with an optional alternative. Due to how it is implemented in the Prolog syntax,

 (true -> false) ; true 

doesn't mean what you think. It was parsed as true -> false ; true true -> false ; true :

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

therefore, it fails because it means "if true then false else true ", that is false .