> I did manage to implement addition (and therefore subtraction) of binary
> numbers.

The sum of two Peano integers:

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

The sum of two binary integers:

ISum{x, y, z}:
   ~co ~t ISum_Dn{x, y, 0, co, t} &
   (
     (co = 0 & z = t) |
     (co = 1 & z = D[1, t])
   )
;

ISum_D1{x, y, ci, co, z}:
   (x = 0 & y = 0 & ci = 0 & co = 0 & z = 0) |
   (x = 0 & y = 0 & ci = 1 & co = 0 & z = 1) |
   (x = 0 & y = 1 & ci = 0 & co = 0 & z = 1) |
   (x = 0 & y = 1 & ci = 1 & co = 1 & z = 0) |
   (x = 1 & y = 0 & ci = 0 & co = 0 & z = 1) |
   (x = 1 & y = 0 & ci = 1 & co = 1 & z = 0) |
   (x = 1 & y = 1 & ci = 0 & co = 1 & z = 0) |
   (x = 1 & y = 1 & ci = 1 & co = 1 & z = 1)
;

ISum_Dn{x, y, ci, co, z}:
   ~headX ~tailX x = D[headX, tailX] &
   ~headY ~tailY y = D[headY, tailY] &
   ~headZ ~tailZ z = D[headZ, tailZ] &
   (
     (
       tailX = D[] &
       tailY = D[] &
       tailZ = D[] &
       ISum_D1{headX, headY, ci, co, headZ}
     ) |
     (
       ~ct ISum_Dn{tailX, tailY, ci, ct, tailZ} &
           ISum_D1{headX, headY, ct, co, headZ}
     )
   )
;

Note also that if we use Peano integers, there is exactly one way to 
write each number. With binary, there are several ways. For example, 11 
and 0011 both denote 3. The ISum{} predicate above works only for 
numbers containing the same number of bits. I haven't even attempted to 
implement binary multiplication yet. (That would probably turn out to be 
drastically faster, however...)

Post a reply to this message