481–490 of 507 posts
Binary search. Very simple, incredibly powerful; can search on data or math function. It's the basis for other CS concepts. JS implementation: https://gist.github.com/netgusto/90c8e0e7019a832cbf95eac58e1...
The complexity is O(log log n), under the assumption of a uniform distribution of the data.
Earlier quoted context omitted.
There's no matching process at the beginning of medical school, but there is for assigning med school graduates to residencies. This variant of the problem is NP-hard, so there's no exact solution, but matching still works pretty well. https://web.stanford.edu/~alroth/papers/rothperansonaer.PDF has all the details.
When you are referring to this "variant", are you referring to maximal matching, or bipartite matching when the number of people and schools don't equal?
Earlier quoted context omitted.
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 You can find the formal proof in WhyML below. This includes proofs that: 1. all array accesse…
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 (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 Th…
It seems that the answer is definitely "yes", it can be done with WhyML.
There are a few minor caveats:
1. I had to change the function with the while loop to return an option instead of raising the Not_found exception, which makes the code a bit uglier. This is because I ran into the following bug in Why3 (it's already fixed in the master branch, but not in the most recent release): https://gitlab.inria.fr/why3/why3/issues/214
2. It turns out that the value of "high" is not statically known at compile time, because it depends on the size of the array. So I changed "high" to be a function of the array rather than a constant (I did the same to "low" for consistency).
3. Similarly and consequently, the predicate P(i) is not only a function of "i". It's also a function of the value being searched for ("x"), i.e. if P(i) is true or not depends on which value you're searching for. This also means that P() is also a function of the specific array being searched for (because some arrays may have "x" but others not).
4. You said that "we're pretending to know that there is a small value at arr[-1] and a large value at arr[arr.length]", but unless I misunderstood something, we can't actually pretend that, this must be written in the code somewhere, otherwise it won't work. For simplicity, I have chosen to implement those rules in the predicate itself. However, this is also enforced by the function with the while loop, i.e., it always makes sure that whatever predicate you have chosen, it has to implement those rules. I am sure that this could be changed, but I think it would complicate the proofs.
The result is that in module "GenericBinarySearch", like the name says, we have a neat generic binary search function which works with any predicate P (called "pred" in the code), any function "low", any function "high" and for any type.
And in module "ArrayBinarySearch" we have an instantiation of "GenericBinarySearch" which works for sorted arrays!
Also note that the axiom in the code is only an axiom in the generic module (it specifies what must be true of P()), but when the generic module is instantiated, Why3 verifies that the axiom is actually true for the specific instance of the predicate (so there is no cheating).
You can find the code in the link below. Enjoy!
Earlier quoted context omitted.
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 (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 Th…
Ok, so this proved to be more difficult than I anticipated and it took me a while, but fortunately I really enjoyed the challenge! It seems that the answer is definitely "yes", it can be done with WhyML. There are a few minor caveats: 1. I had to change the function with the while loop to return an option instead of raising the Not_found exception, which makes the code a bit uglier. This is because I ran into the fol…
I had something like this in mind:
let binary_search (pred: int -> bool) (low: int) (high: int): int
requires { pred low = False }
requires { pred high = True }
requires { forall i j. (i (pred i -> pred j)}
ensures { pred result = False /\ pred (result+1) = True }
=
let cur_low = ref low in
let cur_high = ref high in
while !cur_high - !cur_low > 1 do
variant { !cur_high - !cur_low }
invariant { pred !cur_low = False /\ pred !cur_high = True }
let mid = div (!cur_high + !cur_low) 2 in
if not (pred mid) then
cur_low := mid
else
cur_high := mid
done;
!cur_low
let predicate pred (i: int) (x: t) (k: int)
= if i = high x then true else
k My first programming project was a tic-tac-toe game with a computer opponent. I painstakingly copy-pasted about a hundred nested `if` statements to check for a winner & decide the computer’s next move. Several years later I saw a Matlab demo that did this by indexing the grid using values from a 3x3 magic square[1]. In a magic square, every row, column, and diagonal has the same sum. So checking for a winner was just…
Fast inverse square root, sometimes referred to as Fast InvSqrt() or by the hexadecimal constant 0x5F3759DF, is an algorithm that estimates 1/√x, the reciprocal (or multiplicative inverse) of the square root of a 32-bit floating-point number x in IEEE 754 floating-point format. https://en.m.wikipedia.org/wiki/Fast_inverse_square_root I especially love the story around it.
Union-find data structure: https://en.wikipedia.org/wiki/Disjoint-set_data_structure
After hearing the word "memoization" go through my head (part of "Hacking the Coding Interview." which I recommend at least for the wealth of example questions for practice), I basically walked my way through making a disjoint-set data structure using the words as keys and the set number as values. I'm prettyy sure that making that up on the spot is what got me the job.
Earlier quoted context omitted.
Ok, so this proved to be more difficult than I anticipated and it took me a while, but fortunately I really enjoyed the challenge! It seems that the answer is definitely "yes", it can be done with WhyML. There are a few minor caveats: 1. I had to change the function with the while loop to return an option instead of raising the Not_found exception, which makes the code a bit uglier. This is because I ran into the fol…
Very nice. I don't quite understand why you need the option in GenericBinarySearch. Doesn't the function always return Some? I had something like this in mind: let binary_search (pred: int -> bool) (low: int) (high: int): int requires { pred low = False } requires { pred high = True } requires { forall i j. (i (pred i -> pred j)} ensures { pred result = False /\ pred (result+1) = True } = let cur_low = ref low in let…
Yes, indeed! Your version is not only a lot more simple and elegant than mine, but your proof code was enough for Z3 to automatically figure out that everything works.
Therefore, I hereby declare that you are ready to use and learn more about Why3/WhyML.
Here's a working complete implementation of your version: https://clbin.com/cwvKY
There's only a minor caveat with your version: there's no formal guarantee that `binary_search` won't call `pred` below `low` or above `high`, because (as far as I know) we can't encode those requirements if we pass the function as an argument. Maybe there's a way to do that, but I don't know WhyML that deeply.
> Those tests are only necessary for the proofs, right?
I think so. We can probably separate `pred` into a logical version and a run-time version, making sure that the result of the logical `pred` matches the result of the run-time `pred` when `-1 I think this should be very easy to do with WhyML, I will try and figure out if I can do it.
Earlier quoted context omitted.
Very nice. I don't quite understand why you need the option in GenericBinarySearch. Doesn't the function always return Some? I had something like this in mind: let binary_search (pred: int -> bool) (low: int) (high: int): int requires { pred low = False } requires { pred high = True } requires { forall i j. (i (pred i -> pred j)} ensures { pred result = False /\ pred (result+1) = True } = let cur_low = ref low in let…
> Can something like that work? Yes, indeed! Your version is not only a lot more simple and elegant than mine, but your proof code was enough for Z3 to automatically figure out that everything works. Therefore, I hereby declare that you are ready to use and learn more about Why3/WhyML. Here's a working complete implementation of your version: https://clbin.com/cwvKY There's only a minor caveat with your version: ther…
What happens if you remove requires { forall i j. (i (pred i -> pred j)}? I think it should still check, actually. That property ensures that the answer will be unique, but the algorithm will find a point pred i = False /\ pred (i+1) = True even if the predicate does not satisfy that property.
If you add the uniqueness to the ensures, does Z3 still automatically prove it correct?
ensures { forall j. pred j = False /\ pred (j+1) = True -> j == result) }Earlier quoted context omitted.
> Can something like that work? Yes, indeed! Your version is not only a lot more simple and elegant than mine, but your proof code was enough for Z3 to automatically figure out that everything works. Therefore, I hereby declare that you are ready to use and learn more about Why3/WhyML. Here's a working complete implementation of your version: https://clbin.com/cwvKY There's only a minor caveat with your version: ther…
That would be nice, then the run time predicate can be fast while the logical version remains elegant. What happens if you remove requires { forall i j. (i (pred i -> pred j)}? I think it should still check, actually. That property ensures that the answer will be unique, but the algorithm will find a point pred i = False /\ pred (i+1) = True even if the predicate does not satisfy that property. If you add the uniquen…
If I simply remove that 'requires', then Why3 cannot prove the postcondition of `binary_search` automatically anymore (using the Z3, CVC4 and Eprover automatic provers that I have installed).
Specifically, Why3 tries to split the postcondition into the 2 parts: `pred result = False`, which gets verified correctly, and `pred (result+1) = True`, which cannot be verified automatically.
I think this is because nothing stops `high` from actually being lower than `low`. If someone passes those 2 arguments reversed (high as low and low as high), then probably the algorithm wouldn't work, right? At least, Why3 is not convinced that it would work.
However, if I add this loop invariant: `!cur_low Diff here: https://clbin.com/wVkhO And full code here: https://clbin.com/2gBfJ
I tried separating `pred` into logical and run-time versions (one with the ifs and the other only with the comparison), and it all seems to work fine, except for one problem:
The run-time version of `pred` is a partial function (it only works for valid array indices), so it needs a precondition. However, when I pass `pred` as an argument to `binary_search`, I can't / don't know how to specify that the argument needs the precondition.
Therefore, Why3 complains that the precondition of `pred` may not be respected (all other verification conditions are proven to be valid).
I could do what I did before (making `low` and `high` functions, etc) but that greatly complicates the code...
Maybe there is some way to do that, but currently I don't know how.