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

Question

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?

Lachlan

Of course you can always just do it for every representable integer. That's a proof, but not a very interesting or illuminating one. – Inotropic

twos compliment, threes a crowd bada bing – Diller

Answer 1

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.

Viscounty

A really elegant proof. I like it! – Sinistral

This proof applies to unsigned integers. For the C language, you cannot prove the result for signed integers because it's not necessarily true. – Sunroom

Answer 2

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

Slobber

I'm voting this one up. There's no requirement in the C standard to use 2's complement at all. It's just one of the encoding schemes allowed. – Gondolier

That's a good point. The question may be edited to make this clear. – Juxtaposition

@paxdiablo: if the integer type is unsigned, twos complement is irrelevant and it's provable for the C language. – Sunroom

@R, I don't think that's right. If the implementation is using ones complement, then -x is exactly the same as ~x. If you then add one to the latter (~x + 1), they are not equal. For example, the eight bit ones comlpement for 3 is 0000-0011, ~3 is 1111-1100, ~3 + 1 is 1111-1101 which is -2. – Gondolier

Answer 3

~x+1 is equivalent to 2's complement + 1 (i.e. negative number) representations of -x, ~(x-1) also represents the same (consider the case where last bit is 1, ~(x-1) = ~(b1b2.b(n-1)1 - 0) = b1'b2'...b(n-1)'1 = b1'b2'...b(n-1)'0 + 1 = ~x+1. Similar case hold for last bit is 0. ~(x-1) = ~(b1b2..bi100..00 - 1) = ~b1b2..bi011..11 = b1'b2'..bi'100..00 = b1'b2'..bi'011..11 + 1 = ~x + 1.

Pint

I don't see how referring to the somewhat arbitrary definition of twos complement in any way represents a proof of an algebraic statement of the two's complement identities. Isn't that just the definition? It's like "proving" that #ff0000 is red because it's an RGB color value... – Slobber

i don't see how being rude is helping, just down vote and move on? – Diller

While this post isn't entirely clear, mainly due to formatting, it is entierly correct, and DigitalRoss's complaint isn't valid, I think. – Donitadonjon

actually, this is a very good try, using "general" odd and even integers and proving that both expressions are equivalent, and equal to negation. So, the property holds for all integers, since any integer is either odd or even. – Juxtaposition

how both expressions are equal to negation needs more clarification. – Juxtaposition

I didn't intend to be rude, and I did not do any downvoting. What's wrong with suggesting, quite accurately btw, that since we have simply defined negated numbers to be represented in 2's-complement, that we cannot therefore prove it .. because it's an axiom. One proves statements in terms of axioms. I suppose ultimately a proof can be anything that reduces to an axiom but this seemed rather close to simply restating one. – Slobber

Making a point or asking a serious question isn't being rude. – Lili

Answer 4

I'll try to present an intuitive explaination that everybody should find handy. If you insist we may try a more formal approach.

In two's complement representation, in order to have a unique representation of the zero element, we sacrifice one positive element. As a result, there is an extra negative number that has no positive mirror.

So, given 2 bits, we get: {+1, 0, -1, -2} which would be represented in binary as:

-2    10
-1    11
 0    00
+1    01

So, we may think of the zero as a mirror. Now, given an integer x, if we want to invert its sign, we can start by inverting all bits. This would have been enough if there was no zero between the positives and negatives. But since the zero makes a shift, in positives, we have compensate for that.

The two expressions mentioned in the question make this compensation before ~(x-1) and after ~x+1 inverting the bits. You can easily verify that using +1 and -1 in our 2-bit example.

Juxtaposition

Answer 5

In general this is not true, as the C standard doesn't require the use of twos complement to represent negative numbers.

In particular, the result of applying ~ to a signed type is not defined.

However, as far as I know all modern machines use twos complement for integers.

Aspasia

+1 I agree with the "all modern machines use..." part, but you have to be aware that the compiler may also optimize some signed expression based the assumption that it does not overflow, because if the expression did, the behavior would be undefined so the compiler doesn't have to care. There is an example in lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/… – Unsuspecting

It may be true that all modern machines use twos complement, but some DSPs (like Motorola 56xxx) also allow saturation arithmetic so that there is no overflow/underflow. 0x7fffff + 1 == 0x7fffff, 0x800000 - 1 == 0x800000. – Monograph

@Pascal Cuoq That's remarkable. I see it happening in gcc 4.3.2 with -O2 or greater. I also put Frama-C on my list of things to look at. – Aspasia

The objections and counterexamples only apply to signed integers. The behavior for unsigned integers, including the interaction between bitwise and arithmetic operators, is completely defined by the C language. – Sunroom