On 31/05/2012 11:47 AM, scott wrote:

> Also how hard would it be to add support for arithmetic operators? Then
> you would have an equation solver, which arguably would be more useful.

Peano arithmetic. Basically, you use Z[] to represent 0, and S[x] to 
represent x+1. In this way, 3 is represented by S[S[S[Z[]]]]. (In other 
words, 3 lots of S[].)

It's then quite easy to write sum and product predicates:

ISum{x, y, z}:
   (x = Z[] & y = z) |
   (~px ~pz
     x = S[px] &
     z = S[pz] &
     ISum{px, y, pz}
   )
;

IProduct{x, y, z}:
   (x = Z[] & z = Z[]) |
   (~px ~t
     x = S[px] &
     IProduct{px, y, t} &
     ISum{t, y, z}
   )
;

Using this, I was able to solve the following system of simultaneous 
equations:

   x + y = 9
   2x = y

The first equation can be represented by

   ISum{x, y, nine}

where nine is S[S[S[S[S[S[S[S[S[Z[]]]]]]]]]]. The second equation can be 
written

   IProduct{two, x, y}

where, again, two is S[S[Z[]]].

It takes several thousand steps, but Logic Box finds exactly one solutions:

   x := S[S[S[Z[]]]];
   y := S[S[S[S[S[S[Z[]]]]]]];

In other words, x=3 and y=6, which does solve the given equations.

Notice that the ISum{} predicate on its own gives the solution set

   x := 0; y := 9;
   x := 1; y := 8;
   x := 2; y := 7;
   x := 3; y := 6;
   ...
   x := 8; y := 1;
   x := 9; y := 0;

Note also that the ISum{} predicate needs to come first, since it has a 
finite solution set. The IProduct{} predicate has the infinite solution set

   x := 0; y := 0;
   x := 1; y := 2;
   x := 2; y := 4;
   x := 3; y := 6;
   ...

Either way, the correct solution is located. But if IProduct{} comes 
first, the solver never terminates, fruitlessly searching the infinite 
search space for non-existent further solutions. If ISum{} comes first, 
the search terminates eventually.

Either way, it's pretty damned slow. It's basically searching for all 
possible combinations of numbers having the requested properties.

It shouldn't be too hard to add an IExponent{} predicate too, and ask 
the solver to solve some polynomial equations. Remember, though, that at 
this point it handles only integers.

More generally, I'm going to see whether I can implement some more 
efficient type of arithmetic. (E.g., binary arithmetic.)

Post a reply to this message