Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to prove that the C statement -x, ~x+1, and ~(x-1) yield the same results?

I want to know the logic behind this statement, the proof. The C expression -x, ~x+1, and ~(x-1) all yield the same results for any x. I can show this is true for specific examples. I think the way to prove this has something to do with the properties of two's complement. Any ideas?

like image 598
Ben Fossen Avatar asked Feb 17 '10 05:02

Ben Fossen


2 Answers

Consider what you get when you add a number to its bitwise complement. The bitwise complement of an n-bit integer x has a 1 everywhere x has a 0, and vice versa. So it's clear to see:

x + ~x = 0b11...11 (n-bit value of all ones)

Regardless of the number of bits in x. Further, note that adding one to an n-bit number filled with all ones will make it wrap to zero. Thus we see:

x + ~x + 1 = 0b11...11 + 1 = 0 and ~x + 1 = -x.

Similarly, note (x - 1) + ~(x - 1) = 0b11...11. Then (x - 1) + ~(x - 1) + 1 = 0, and ~(x - 1) = -x.

like image 98
Julian Panetta Avatar answered Sep 18 '22 15:09

Julian Panetta


I'm not certain you can prove this from any sort of useful axiom other than the rather trivial reduction back to the fact that we have defined negative numbers in modern integer ALUs to be in twos complement.

Computers don't have to be implemented with twos complement binary hardware, it's just that there are various attractive properties and almost everything is built that way these days. (But not floating point! Those are one's complement!)

So we build a machine that happens to represent negative numbers in 2's complement. Expressions that show negative numbers to be represented in two's complement are accurate, but only because we defined them that way. That's the axiomatic basis for negative integer numbers in modern machines.

Since we define negation in terms of two's complement, you are essentially referring to the axioms, although I suppose that's what all proofs ultimately do.

Maybe this is why I'm not really a theory guy. :-)

like image 21
DigitalRoss Avatar answered Sep 19 '22 15:09

DigitalRoss