Prolog: why is true == not(not(true)) -> false?

1
votes

Obviously true = not(not(true)) has to be false, because = tries to unify the atom true with the term not(not(true)) (without evaluating the term), which is false, since the terms are not identical.

However, I thought == really compares whatever is evaluated. Thus, I thought true == not(not(true)) should evaluate to true == true, just like (for arithmetic operators) 4 =:= 2 + 2 would evaluate to 4 =:= 4 and return true.

...but this is what I get in SWI-Prolog:

?- true == not(not(true)).
false.

What am I getting wrong?

1
prologlogical-operators
You used not(not(false)) in one place and not(not(true)) in others. Was that deliberate? – user2357112 supports Monica
No, a typo. Sry. Fixed it. – daniel451

1 Answers

1
votes

(==)/2 does not compare whatever is evaluated. It does not evaluate its arguments. It only succeeds if the arguments are already instantiated to matching terms.

In prolog, not(not(true)) is a compound term, which is the term not/1 with a single argument, not(true), itself being a term not/1 of one argument consisting of the term true/0 which has no arguments. It doesn't have a value. It doesn't even get "executed" except in certain contexts. In Prolog, the predicate not/1 succeeds if it's argument fails, and it fails if its argument succeeds. This isn't the value or functional result, but a behavior. This is assuming that it appears in a context such as the following:

not(not(true)),
write('This will be written out because not(not(true)) succeeded'), nl.

The expression true == not(not(true)) in Prolog is a compound term, equivalent to:

'=='(true, not(not(true)))

In this context, not(not(true)) is not evaluated. Prolog will first exercise the (==)/2 equivalence operator, which succeeds if its arguments are instantiated to the same term. Are the terms true and not(not(true)) in Prolog the same (or equivalent)? No they are not. One is simple term with no arguments (true/0). The other is a compound term: a term with one argument that is itself a term with one argument. Thus the (==)/2 fails here.

Note that (=:=)/2 is quite different. It is an operator that compares results of arithmetic expressions. The arguments must be evaluable arithmetic expressions and (=:=)/2 will succeed if they evaluate to the same result, and it will fail if they do not.