4 ms·

I like this version: low = -1 high = arr.length while(high - low > 1){ mid = (high + low)/2 if(arr[mid] <= x) low = mid else high = mid } Thi

• karakot 8y ago
  and it's also a broken version.
  • jules 8y ago
    How so? Are you talking about (high + low)/2? Whether that is correct depends on the language. With 64 bit arithmetic it's correct in practice, and with arbitrary size arithmetic it's correct in practice and in theory. It only really causes problems if you're using 32 bit arithmetic on a 64 bit machine.
    • ncmncm 8y ago
      Just keep telling yourself that. Or, look up the right answer.
      • jules 8y ago
        Perhaps instead of being mean, you could be helpful and post a link to said answer.
        • raymond_goo 8y ago
          With 64 bit variables it probably works. But for less here is the correct implementation: https://ai.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html https://ai.googleblog.com/2006/06/extra-extra-read-all-about...
          • jules 8y ago
            This implementation: mid = ((unsigned int)low + (unsigned int)high)) >> 1; essentially extends the bit width from 31 bit to 32 bit by going from signed to unsigned, and is thus correct up to array lengths of order 2^31 rather than 2^30. Using an even larger bit width should classify as at least as correct as this. In summary, (low + high)/2 or (low + high) >> 1 is correct up to 2^30 for 32 bit signed and up to 2^62 for 64 bit signed, up to 2^31 for 32 bit unsigned, and up to 2^63 for 64 bit unsigned.
  • wizeman 8y ago
    Actually, I can definitely say that this version is not broken, i.e. I've formally proven it to be mathematically correct assuming that: 1. high and low are bigints (such as when using Python, for example) 2. the input array is sorted (needed for any binary search algorithm) 3. this missing code at the bottom is added: if (0 <= low && low < arr.length) { if (arr[low] == x) { return low; } } return -1; // (or "raise Not_found" or whatever you use to indicate that 'x' was not found). You can find the formal proof in WhyML below. This includes proofs that: 1. all array accesses are in bounds [checked automatically] 2. there is no undefined behavior (such as division by zero) [checked automatically] 3. the function always terminates [enforced automatically, proven with the help of the 'variant' clause] 4. there are no overflows [checked automatically, not possible since we're using bigints] 5. if an index is returned, the array has an element with value equal to x at that index [the 'ensures' clause] 6. if instead the function returns "not found", the array does not have any element with a value equal to x [the 'raises' clause] ... all this assuming that the input array is sorted [the 'requires' clause] Code + proof here (it makes more sense if you can read OCaml syntax): https://clbin.com/jbTk8 https://clbin.com/jbTk8
    • jules 8y ago
      Awesome! Interesting that it can prove that given only the loop invariant. The inner loop could be factored to a subroutine with the following contract: let P be a predicate on the integers such that (i <= j) => (P(i) => P(j)), and let low be such that P(low) = false and high such that P(high) = true. The subroutine returns i such that P(i) = false and P(i+1) = true. The subroutine further promises to only call P(k) on low < k < high. This may be applied to the predicate P(k) = (x <= arr[k]) on the range (low,high) = (-1,arr.length) to find the point at which the predicate flips from false to true (we're essentially pretending to know that there is a small value at arr[-1] and a large value at arr[arr.length], and the subroutine promises to only call P(k) on values strictly between -1 and arr.length). Is it possible to do this with WhyML?
      • wizeman 8y ago
        Actually, my loop invariant was unnecessarily confusing (I was sleep deprived), here's a better version: https://clbin.com/OhyJ3 https://clbin.com/OhyJ3 Your question is very interesting and I think the answer is 'yes'. I will try to implement it and report back.