Yeah, zero is probably not the best thing to return if left == right; same with an all red interval. Wasn't thinking carefully enough when generalizing it, but I will fix.
def binary_search(left, right, is_green):
left -= 1
while left + 1 < right:
middle = (left + right) // 2
if is_green(middle):
left = middle
else:
right = middle
return right
# Usage.
binary_search(0, len(array), lambda i: array[i] < 6)
*Equivalent except for the rounding in the division.
For signed search ranges, if you modify my implementation above to compute the midpoint as (lo + hi) // 2 and (lo + hi) < 0 and the language rounds integer division toward zero, you gain a rounding-related bug. In this sort of circumstance, your approach does not gain that bug because it doesn't care which way division is rounded. Python doesn't have overflow and rounds down, so ~all of the errors we can make on that line won't happen anyway :)
If the range is unsigned, lo-1 is likely to be MAX_VALUE, but it seems like it still does the right thing.
1. The entire range isn't red, so at some point [proof needed] we will move left to a green element. From that point on we can continue analysis like normal. (I can't think of an easy way to prove such a claim without messing with floor division and induction, etc... but it seems intuitively true.)
2. The entire range is red, so green will never be moved, so right will point to the first element and green will point to one before the first. This returns the correct value.
I'll have to come up with a way to easily prove statement 1 above to be convinced that it is better. But I can include this version in the follow up.
(A less sneaky version is to explicitly define new predicates: `is_green2(i) := (i == left - 1) || is_green(i)` and `is_red2(i) := (i == right) || is_red(i)`, where `left` and `right` refer to the function's original parameters (inclusive-exclusive). These predicates can be used as the invariants, and are sufficient for showing that at the end of the loop the result is either the first red, or one-past-the-end if everything is green.)
An alternative is to tweak the invariants:
Let `left` and `right` be the function's original parameters (inclusive-exclusive), and let `l` (that's a lowercase L) and `r` be the variables used in the loop (exclusive-exclusive).
The original invariants are `is_green(l)` and `is_red(r)`, which require sneaky definitions when `l = left - 1` and `r = right`.
The tweaked invariants are `is_green(i) for all i where left <= i <= l` and `is_red(i) for all i where r <= i < right`. In other words, everything up to and including `l` is green, and everything from `r` onward is red.
These invariants are vacuously true when `l = left - 1` and `r = right`, so they hold before the loop (without having to define `left - 1` to be green and `right` to be red).