Not equal seems to always fail

[AKEOPLUS-boris-bocquet]

SWI-Prolog (threaded, 64 bits, version 9.1.10) % *** clpBNR v0.11.1 ***.

Dear Rick, a friend told gave me this small problem to implement : can prolog check if a given function is a "norm" or not. To be a norm, the function has to respect a couple of properties. The only one I started to implement is norm(a*X) = a * norm(X).
I know that Prolog is not the best language for theorem / math proving. Still, I though this could help him to find quickly counter-examples.

Saddly, I could not succeed. It looks like the not equal always fail.

Here is the code :

norm1(X, Y, N):- 
    X::real,
    Y::real,
    N::real,
    { N == abs(X - Y)}.

normNok(X, Y, N):-
    X::real,
    Y::real,
    N::real,
    {N == exp(X-Y)}.

my_norm_under_test(X, Y, N):- norm1(X, Y, N).
%my_norm_under_test(X, Y, N):- normNok(X, Y, N).

is_a_norm_test1(A, X, Y, N1, N2) :- 
    [A, X, Y, N1, N2]::real,
    {AX == A * X, AY == A*Y},
    my_norm_under_test(AX, AY, N1),
    my_norm_under_test(X, Y, N2),
    {AN2 == A*N2},
    format("N1 = "), write(N1), format("~nN2 = "), write(N2), format("~nA*N2 = "), write(AN2), format("~n"),
    {N1 == AN2}.

is_not_a_norm_test1(A, X, Y, N1, N2) :- 
    [A, X, Y, N1, N2]::real,
    {AX == A * X, AY == A*Y},
    my_norm_under_test(AX, AY, N1),
    my_norm_under_test(X, Y, N2),
    {AN2 == A*N2},
    format("N1 = "), write(N1), format("~nN2 = "), write(N2), format("~nA*N2 = "), write(AN2), format("~n"),
    {N1 <> AN2}.

norm1 is a function that respect the property. Whereas normNok does not.
I can switch the norm to be tested by commenting / uncommenting the lines with my_norm_under_test.

When I test norm1, I have these outputs for these queries :

2 ?- is_a_norm_test1(0.5, 2.0, 3.0, N1, N2).
N1 = _12784{real(0.4999999999999989,0.5000000000000009)}
N2 = _12866{real(0.9999999999999991,1.0000000000000007)}
A*N2 = _18840{real(0.4999999999999995,0.5000000000000006)}
N1:: 0.50000000000000...,
N2:: 1.00000000000000... .

3 ?- is_not_a_norm_test1(0.5, 2.0, 3.0, N1, N2).
N1 = _24146{real(0.4999999999999989,0.5000000000000009)}
N2 = _24228{real(0.9999999999999991,1.0000000000000007)}
A*N2 = _29954{real(0.4999999999999995,0.5000000000000006)}
false.

It looks OK for me.

Now I switch to normNok and here are the results I got from the queries :

5 ?- is_a_norm_test1(0.5, 2.0, 3.0, N1, N2).
N1 = _792{real(0.6065306597126328,0.6065306597126342)}
N2 = _874{real(0.367879441171442,0.3678794411714427)}
A*N2 = _6516{real(0.18393972058572097,0.18393972058572142)}
false.

6 ?- is_not_a_norm_test1(0.5, 2.0, 3.0, N1, N2).
N1 = _2876{real(0.6065306597126328,0.6065306597126342)}
N2 = _2958{real(0.367879441171442,0.3678794411714427)}
A*N2 = _8600{real(0.18393972058572097,0.18393972058572142)}
false.

Query number 5 fails. Which is fine because N1 <> A*N2, so I cannot meet the constrain N1 == A*N2.

So if query 5 fails, why query 6 also fails ?? Even in the console output, the intervals of N1 and A*N2 are really far away, so I cannot see why not equal fails.

I tried other NOK norms (e.g. log and cos). Similar behaviour. I tried to restrains reals to be within -1e3, 1e3 : same behaviour.

Can you help ?
This is not an urgent matter at all.
Thanks in advance

[AKEOPLUS-boris-bocquet]

Even trying without the implementation of my norms, I got similar weird results :

8 ?- {N1 == 0.6065, A == 0.5, N2== 0.3678, AN2 == A * N2}.           
N1:: 0.606500000000000...,  
A:: 0.500000000000000...,   
N2:: 0.367800000000000...,  
AN2:: 0.183900000000000... .

9 ?- {N1 == 0.6065, A == 0.5, N2== 0.3678, AN2 == A * N2}, {N1 <> AN2}.
false.
      
10 ?- {N1 == 0.6065, A == 0.5, N2== 0.3678, AN2 == A * N2}, {N1 =\= AN2}. 
false.
      
11 ?- {N1 == 0.6065, A == 0.5, N2== 0.3678, AN2 == A * N2}, {N1 == AN2}.  
false.

Queries 9 and 10 are wrong.

[ridgeworks]

<> and =\= are only supported for integers, the reason being that these operations are unsound over reals. The set of reals is continuous so X <> Y can't be finitely expressed. Of course you can express <> over finite domains like integers and floats. In clpBNR using <> automatically constrains the values to be integers:

?- {N1 <> N2}.
N1::integer(-1.0Inf, 1.0Inf),
N2::integer(-1.0Inf, 1.0Inf).

< and > have a similar issue (unsound over reals), but the restriction is relaxed in clpBNR. In these cases X<Y means the upper bound of X is less than the lower bound of Y by 1 floating point value which can be useful for some branch-and-bound search algorithms

[ridgeworks]

In these cases X<Y means the upper bound of X is less than the lower bound of Y by 1 floating point value which can be useful for some branch-and-bound search algorithms

Sorry, I meant "at least 1 floating point value".