An integer division identity

Here’s an interesting question that came up on StackOverflow the other day: we know in “real” algebra that the equation (a / b) / c = a / (b * c) is an “identity”; it is true for any values of a, b, and c.[1. Assuming of course that both sides have a well-defined value.] Does this identity hold for integer arithmetic in C#?

In general, no, because of overflow. In a checked context the right side can overflow and produce an exception but the left side cannot. In an unchecked context two large positive values for b and c can overflow to a negative number on the right hand side, thereby producing a different result than the left hand side.

Moreover, commenter “Peter” points out that if b is -1 then (a/b) can overflow too; I hadn’t thought about that case, so good catch.

But what about the specific case where a, b, and c are positive numbers and there are no overflows in either expression? Can we rely on this identity under those circumstances?

Let’s find out!

We begin by going back to the definition of integer division; as I’ve described before, there are two operators: the division operator and the remainder operator. Suppose we have (again supposing that x and y are positive integers):

r = x % y
q = x / y

The relationship between those values is:

x = q * y + r

where 0 <= r < y

Let’s break our suspected identity apart into left and right sides. Let’s say that the first division on the left side is:

qab = a / b
rab = a % b
b * qab + rab = a
0 <= rab < b

So our left hand side is qab / c. The quotient and remainder of that are:

qleft = qab / c
rleft = qab % c
c * qleft + rleft = qab
0 <= rleft < c

We can eliminate qab through substitution to get the equation:

b * c * qleft + b * rleft + rab = a

OK, that will do for the left hand side. For the right hand side we have just one division:

qright = a / (b * c)
rright = a % (b * c)
b * c * qright + rright = a
0 <= rright < b * c

We now have two equations that equal the same thing, a, so let’s set them equal to each other:

b * c * qleft + b * rleft + rab = b * c * qright + rright

We know that qleft and qright are both integers. Therefore there is an integer d, their difference, such that qleft + d = qright. Let's eliminate qright from our equation:

b * c * qleft + b * rleft + rab = b * c * qleft + b * c * d + rright

And solve for d:

d = (b * rleft + rab - rright) / (b * c)

d is an integer. Is possibly positive? Let’s make some inequalities. We know that rright is non-negative, so the numerator of that fraction:

b * rleft + rab - rright <= b * rleft + rab

We know that rleft < c and c > 0 so

b * rleft + rab <= b * (c - 1) + rab

We know that rab < b, so:

b * (c - 1) + rab < b * (c - 1) + b

But that’s b * c. Therefore the numerator of this fraction is strictly less than its denominator, and therefore the fraction must be strictly less than one. Since the fraction is an integer, d must be zero or negative; it cannot be positive.

The proof that d also cannot be negative and therefore must be zero is similar and is left as an exercise.

Since d is zero, qleft = qright, which establishes the identity — again, provided that all the operands are positive numbers and the multiplication does not overflow.

Proving that the identity works for negative a, b and c is also left as an exercise.

Advertisements

22 thoughts on “An integer division identity

    • I was thinking the same. But luckily for me my news reader kept a copy, so I’m pretty sure we are not going insane!

    • He mentioned on Twitter that he was cancelling the series on tail recursion.

  1. Your tail recursion article was both interesting and useful. I hope you decide to repost it and to finish the series. You shouldn’t let internet hostility dictate what you write about.

      • Maybe I’m simply thinner-skinned, but I certainly felt some hostility-by-proxy for you from that chain of Twitter posts.

        In any case I’m sorry you canceled the series; I was looking forward to it. It’s always frustrating when a small group gets up in arms because their pet interest isn’t mentioned during discussion of a wider topic.

        Thank you for the time and effort you put into this site.

      • I also would like to see you revive the tail recursion series, which promised to be interesting and informative, as usual. Twitter is a poor medium for nuanced communication, so I hope you won’t let a few tweets deter you (though I agree with those who’d like to see more references to F#!).

  2. I think it’s a shame too. Probably proof that Twitter is not an appropriate medium for nuanced communication. As it stands, the F#-gurus’ reactions do come across as being a bit peevish.

    I personally think that it would be refreshing and interesting to hear about tail calls from the perspective of someone who ISN’T neck-deep in F#. A simple “Tail calls exist in F#, but that’s not the topic of this series” would suffice, in my opinion.

    But as you say, it’s your blog, and your call.

  3. I stand by my belief that Twitter has overall not been an improvement as far as author-audience participation goes. I think a bit of enforced distance improves things for everyone. Blog feedback takes a little more time, and that can be a good thing. Twitter is actually worse than the peanut gallery, since there are no snacks.

    In the interest of constructive discussion I will not voice my opinion on the actual tweets here.

  4. Pingback: The Morning Brew - Chris Alcock » The Morning Brew #1370

  5. What is with a=Int32.MinValue and b=c=-1? Then
    1) b*c = 1, i.e. does not overflow
    2) a/(b*c) = Int32.MinValue
    3) a/b is not representable as Int32 and so (a/b)/c should throw an exception or return garbage

    Peter

  6. For even more fun
    (a * b) / c = a * (b / c) can overflow on the left or underflow on the right. But could it underflow and overflow?

  7. Yeah, sorry to perpetuate the hijack, but the tail recursion piece had some really interesting and useful info for C# programmers (the main audience of this blog), such as “The 64 bit jitter may do a tail optimization, but the 32 bit jitter doesn’t. And this may affect the stack trace.”

    I don’t see how the existence of F#, which supports tail recursion better, is an argument against talking about it from a C# perspective. That’s like saying “You should never talk about how one might do class-based inheritance in JScript (as opposed to prototype-based inheritance), because there are other languages like C# which are class based.”

    Obviously it’s your blog and you can talk about whatever you want, but it seems a shame to go so far as deleting the post, which had taught me some interesting things I didn’t know about C#.

  8. Forgive me but C# brought me here! I have no interest (time) in learning F# at the moment and would like to know more about tail recursions in C#. Please reconsider your tail recursion series. 😦

  9. I have to agree with everyone’s comments about the tail recursion series. It’s a good article. It doesn’t mean that if you talk about how hot water+vinegar can easily clean stains, you SHOULD mention that bleach detergent HAS this feature. You’re discussing stain removal but you didn’t made a reference to bleach. Does it sound incomplete? No. Those people on twitter are a bunch of egotists.

  10. I don’t understand what’s wrong about describing tail calls from C# perspective. And I don’t agree that “F# is pretty much required knowledge if you’re going to blog about .NET and tailcalls”. Tail calls are not exclusive to F# – it’s general CS knowledge. Also how “F# does it” is irrelevant from the point of view of CLR which is supposed to be language-agnostic.

    This blog has this thing called “Comments” so why Don Syme or Richard Broida didn’t just write a comment filling any holes they see in the article instead of jumping on you on Twitter for not mentioning F#. It left a very bad taste in my mouth.

    • I don’t think that’s completely accurate – the IL instruction set used by the CLR has a “tail.” prefix for tail calls, but of all the common .NET languages only F# ever emits it. So an accounting of tail calls only in C# won’t cover the full .NET story. I can’t speak for Don or Richard but I would guess that their tweets have been taken more negatively than was intended (as 140 character statements can sometimes be). I don’t think it’s outrageous to have hoped for a footnote mentioning F#, for instance, though obviously Eric is free to write posts as he pleases, and as he noted we’d only seen part 1 of the series.

      • I agree that it’s good reason to mention F#. But not mentioning it doesn’t make the blog post invalid. I still think that they should leave a comment here if they felt that something was missing. Especially given that this is mainly C# blog and tail recursion in F# was already discussed on F# team blog.

        And is F# a required knowledge when you describe tail calls in .NET? Well, I could argue with that. But of course Eric has a lot better overview of the situation knowing what was coming up in subsequent parts.

        Anyway let’s hope that Eric will return with “kosher” version on tail recursion series. 😉 I’m looking forward to it.

  11. I’m returning to FAIC after a somewhat lengthy hiatus that started shortly before the tail recursion post was posted and removed. I have to add my voice to those seeking the revival of the series. FAIC has taught me many valuable lessons, many of which improved my F# skills — most notably those on two core functional programming concepts: persistent immutable data structures and monads.

    For example, I read all the documentation on F# computation expressions without understanding them. Then I read Eric’s series on monads, and all was clear.

    In general, considering CS concepts in the specific C# context, even if the concepts are not practical for writing idiomatic C# (e.g., continuation passing style) gives C# programmers tools that can make their transition to other languages that much easier. The F# evangelists seem to underestimate the contribution that this blog makes to their cause, even if it never mentions the language by name.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s