Why can't my rule solve for X in a simple algebraic equation?

Question

I'm new to Prolog, so please be gentle.

This is my rule:

solve(X) :- A = B, A is (7 * (X - 2)), B is (3 * (X + 4)).

Obviously, the correct answer here is 6.5. If I give that to Prolog, it confirms:

| ?- solve(6.5).

yes

However, if I ask Prolog to do the dirty work, it throws an error:

| ?- solve(X).
uncaught exception: error(instantiation_error,(is)/2)

I fully concede that whatever is going on here is due to my misunderstanding of Prolog. Can someone explain to me how I might get this to work or why it won't work?

Answer 1

In Prolog, is is an arithmetic evaluation operator. It calculates the result of an expression on its right side, and assigns it to a variable on its left side.

The expression to be evaluated must contain only numbers and arithmetic operators/functions. In other words, to evaluate an expression, is must already know all the numbers in it.

Another way of saying this is that is is "unidirectional", unlike the = which is bi-directional. Which is what you expected. And that is the meaning of the error that you got.

Solving such equations - constraints - is a job for a constraint solver.

Answer 2

You can use a library for this, available in SWI-Prolog at least: library(clpr) and library(clpq).

Here from the top level for Reals:

?- use_module(library(clpr)).
true.

?- {7 * (X - 2) = 3 * (X + 4)}.
X = 6.5 ;
false.

Or, if you use Rationals:

?- use_module(library(clpq)).
true.

?- {7 * (X - 2) = 3 * (X + 4)}, R is float(X).
X = 13 rdiv 2,
R = 6.5.

If you want to do it yourself, it will be of course much more work. You would have to write code like

...,
(   ground(X)
->  7 * (X - 2) =:= 3 * (X + 4)
;   X is (3*4 + 2*7) / (7 - 3)
),
...

By the way, what you are doing: A = B, A is ..., B is .... This is a bit dangerous, for example:

?- A = B, A is 3 - 2, B is sin(pi/2).
false.

?- 3 - 2 =:=  sin(pi/2).
true.

3 - 2 evaluates to the integer 1; then, sin(pi/2) evaluates to the floating point number 1.0, and this does not unify with the integer 1. So, the first query fails!

?- 1 = 1.0.
false.