Solving a simple equation in Prolog goes wrong

Question

I've written a Prolog program an during the iteration it unifies variables and want to solve the following equation. But it says "false"?!

?- 0.4 =< 4 - 3.6.
false.

Even this is "false":

?- 0.4 = 4 - 3.6.

Why?? Do you know the solution how to fix this?

In my program, it has to be true.. And I think, mathematically both equation are true.

Thanks for your help!!

Answer 1

You are running into problems inherent to floating point representation. Try this C program:

#include <stdio.h>

main()
{
    if (0.4 <= 4 - 3.6) printf("OK\n");
    else printf("NO!\n");

    printf("%.25f\n", 0.4 - (4-3.6));
}

to see what happens. Keep in mind that SWI-Prolog uses double precision arithmetic implemented in C for floating point numbers.

One way to work around this is to use the rational numbers provided by SWI-Prolog:

?- X is rationalize(3.6).
X = 18 rdiv 5.

?- X is rationalize(0.4).
X = 2 rdiv 5.

?- rationalize(0.4) =< 4-rationalize(3.6).
true.

Answer 2

In Prolog, - is not an operator that subtracts two numbers. It only creates a term with binary functor -.

Try:

?- X = 4 - 1.
X = 4-1 ?
yes
?- X = -(4,1).
X = 4-1 ?
yes

This expression needs to be simplified to a number before comparison. To do that, you can use the is operator. Comparison via >= and =< also first evaluates both sides and compares the numbers. Another useful operator is =:=, which is equality comparison in conventional sense.

However, with floating point numbers you should not use comparison directly, since 4 - 3.6 is actually 0.3999999999999999 due to the internal storage format that is unable to preserve arbitrary precision. Is is better to check whether the difference between the two numbers is reasonably small.

It also might make sense to use == instead of = as the former only does the comparison and should a free variable get into this predicate, it will not be bound by it.

(At least that is how it works in SICStus Prolog. EDIT: just tested with SWI Prolog and it works pretty much the same.)