Is there an easier way to show why this query is always equivalent to bitor?

Question

This works, and I can't see right off the bat why:

CREATE OR REPLACE FUNCTION bitor ( x bigint, y bigint ) RETURNS bigint AS $body$
BEGIN
     RETURN x + y - bitand(x,y);
END;
$body$
LANGUAGE PLPGSQL
;

I have posted a couple things around SE for a more mathematical explanation, so I understand why it works logically now (at least in circuitry) but I was curious to post it here as it ultimately started as a query problem. Or maybe, the linked post is already the clearest way to show this?

I hope you don't use this in pl/pgsql. Postgres has built-in bit operators. — ypercubeᵀᴹ, Jun 27 '16 at 19:02
It's more of a curiosity than something for production, of course — galois, Jun 27 '16 at 20:00

score 4 · Answer 1 · answered Jun 27 '16 at 18:40

In short, you want to prove that:

bitand(x,y) + bitor(x,y) = x + y

Split the x and y numbers into the respective bits. Now, lets prove first that the same stands for bits a and b (a and b can only have the values 0and 1):

bitand(a,b) + bitor(a,b) = a + b

But for bits these are trivial:

bitand(a,b) = least(a,b)
bitor(a,b) = greatest(a,b)

Therefore (assuming a <=b without any loss of generality):

bitand(a,b) + bitor(a,b) = least(a,b) + greatest(a,b) = a + b

So, back to x and y and splitting them:

x = a0 * 1  +  a1 * 2  +  a2 * 4  + ... +  an * 2^n
y = b0 * 1  +  b1 * 2  +  b2 * 4  + ... +  bn * 2^n

x + y = (a0+b0) * 1  +  (a1+b1) * 2  +  ... +  (an+bn) * 2^n

But we can do the same for bitand and bitor:

bitand(x,y) = c0 * 1  +  c1 * 2  +  c2 * 4  + ... +  cn * 2^n
bitor(x,y)  = d0 * 1  +  d1 * 2  +  d2 * 4  + ... +  dn * 2^n

bitand(x,y) + bitor(x,y) = (c0+d0) * 1  +  (c1+d1) * 2  +  ... +  (cn+dn) * 2^n

Considering also that:

bitand(ai,bi) = ci
bitor(ai,bi) = di

we apply our previous results to find:

x + y = (c0+d0) * 1  +  (c1+d1) * 2  +  ... +  (cn+dn) * 2^n

and we have a proof.

What I'm worried is possible overflows. It's probably wiser to use (x - bitand(x,y)) + y to avoid them. — ypercubeᵀᴹ, Jun 27 '16 at 18:51

Is there an easier way to show why this query is always equivalent to bitor?

1 Answers1