>> 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.

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

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

One might think about implementing some kind of primitive which allows 
you to add and subtract real integers. Actually, this turns out to be 
less helpful than you might imagine.

Using Peano arithmetic, we can write things such as

   x = S[y]

this denotes the fact that x = y+1, without specifying which actual 
integer y contains. We can work that out later. By contrast, if you 
wanted to implement some primitive which works in definite integers, you 
would have to somehow augment the solution language to support 
constraints like "x is one greater than y". Using Peano arithmetic, you 
get that for free.

Perhaps the only primitive I ought to be adding is one to convert 
between real integers and Peano integers...

I did manage to implement addition (and therefore subtraction) of binary 
numbers. On the one hand, that makes numbers much shorter to write. (The 
amount of characters required to represent N is now O(log N) rather than 
O(N).) On the other hand, the predicates become quite a lot more 
complicated, so it's dubious whether it actually runs any /faster/. It's 
also much harder to debug if it doesn't work properly.

Post a reply to this message