Prolog is and =. Why don't they work the same way as the logical constraints?

I'm still very new to prolog, and am trying to wrap my head around why math constraints don't seem to work the same way logical ones do.

It seems like there's enough information to solve this:

f(A, B) :- A = (B xor 2).

But when I try f(C, 3), I get back C = 3 xor 2. which isn't very helpful. Even less useful is the fact that it simply can't find a solution if the inputs are reversed. Using is instead of = makes the example input return the correct answer, but the reverse refuses to even attempt anything.

From my earlier experimentation, it seems that I cou开发者_运维知识库ld write a function that did this logically using the binary without trouble, and it would in fact go both ways. What makes the math different?

For reference, my first attempt at solving my problem looks like this:

f(Input, Output) :- 
    A is Input xor (Input >> 11),
    B is A xor ((A >> 7) /\ 2636928640),
    C is B xor ((B << 15) /\ 4022730752),
    Output is C xor (C >> 18).

This works fine going from input to output, but not the other way around. If I switch the is to =, it produces a long logical sequence with values substituted but can't find a numerical solution.

I'm using swi-prolog which has xor built in, but it could just as easily be defined. I was hoping to be able to use prolog to work this function in both directions, and really don't want to have to implement the logical behaviors by hand. Any suggestions about how I might reformulate the problem are welcome.

Pure Prolog is not supposed to handle math. The basic algorithm that drives Prolog - Unify and backtrack on failure - Doesn't mention arithmetic operators. Most Prolog implementations add arithmetics as an ugly hack into their bytecode.

The reason for this is that arithmetic functions do not act the same way as functors. They cannot be unified in the same way. Not every function is guaranteed to work for each combination of ground and unground arguments. For example, the algorithm for raising X to the power of Y is not symmetric to finding the Yth root of X. If all arithmetic functions were symmetric, encryption and cryptography wouldn't work!

That said, here are the missing facts about Prolog operators:

First, '=' is not "equals" in Prolog, but "unify". The goal X = Y op Z where op is an operator, unifies X with the functor 'op'(Y,Z). It has nothing to do with arithmetic equality or assignment.

Second, is, the ugly math hack, is not guaranteed to be reversible. The goal X is Expr, where Expr is an arithmetic expression, first evaluates the expression and then tries to assign it to X. It won't always work for each combination of numbers and variables - Check your Prolog library documentation.

To summarize:

• Writing reversible mathematical functions requires the mathematical knowledge and algorithm to make the function reversible. Prolog won't do the magic for you in this case.
• If you're looking for smart equation solving, you might want to check Prolog constraint-solving libraries for finite and contiguous domains. Not the same thing as reversible math, but somewhat smarter than Prolog's naive arithmetic operators.

If you want to compare the result of evaluating expression, you should use the operator (=:=)/2, or when checking for apartness the operator (=/=)/2.

The operator works also for bitwise operations, since bitwise operations work on integeres, and integers are numbers. The operator is part of the ISO core standard. For the following clause:

f(A, B) :- A =:= (B xor 2).

I get the following runs, in SWI-Prolog, Jekejeke Prolog etc..:

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.31)
Copyright (c) 1990-2016 University of Amsterdam, VU Amsterdam

?- f(100, 102).
true.

?- f(102, 100).
true.

?- f(100, 101).
false.

If you want a more declarative way of handling bits, you can use a SAT solver integrated into Prolog. A good SAT solver should also support limited or unlimited bit vectors, but I cant currenty tell whats available here and what the restrictions would be.

See for example this question here: Prolog SAT Solver