CODEWITHSUNDEEP
algorithmfunctional-programmingocaml
qiubit
qiubit

Reputation: 4816

How to prove correctness of the following code?

I've got a following problem:

Write a function, that, given a list l and an int c, returns min(|c+x1+x2|), where x1 and x2 are some values from the list. [It's also possible that x1=x2]

And I've got a code that apparently solves this problem:

let bestSum l c =
  let rec f l lr res =
    match (l,lr) with
    | ([],lr) -> res
    | (l,[]) -> res
    | (h1::t1, h2::t2) -> if (h1+h2+c)>0 then f l t2 (min res (h1+h2+c)) else
                            f t1 lr (min res (-(h1+h2+c))) in
  f l (rev l) (abs (2* (hd l) + c));;

Intuitively, I kind of know how and why it works, but I'm not sure it will work for every possible case. So how to prove it, kinda formally?

EDIT: Yeah, I forgot to add, the list is sorted, sorry.

Upvotes: 0

Views: 106

Answers (1)

arghbleargh
arghbleargh

Reputation: 3170

I'm going to assume your list is sorted, because otherwise it doesn't work. Here is a description of your algorithm that should make it clear why your program works. Suppose your numbers are x[0], x[1], ... , x[n]. The goal is to find two numbers x[i] and x[j] such that their sum is as close to -c as possible. Let's plot the values x[i] + x[j] + c in a (n + 1) by (n + 1) grid, labeling the positive values with + and negative values with - (see below for an example). The goal is to find the cell with minimum absolute value.

Example where c = 0, x = [-3, -2, 1, 4].

       x[0] x[1] x[2] x[3]

x[0]     -    -    -   (+)
x[1]     -    -   (-)  (+)
x[2]    (-)  (-)  (+)   + 
x[3]    (+)   +    +    +

You'll notice that the -'s and +'s are divided into two regions, and indeed this has to be the case because each cell's value is smaller than the cell directly below or to the right of it. Based on that observation, the only cells that can be optimal are the ones at the boundary between - and +.

Your algorithm basically follows this boundary (cells considered by your algorithm are marked in parentheses). Let's walk through a few steps:

First, consider x[3] + x[0]. We see that it's +, so x[3] + x[1] can't possibly be better, try x[2] + x[0] next.

       x[0] x[1] x[2] x[3]

x[0]     ?    ?    ?    ?
x[1]     ?    ?    ?    ?
x[2]     *    ?    ?    ? 
x[3]    (+)   X    X    X 

* = thing to try next
X = ruled out

x[2] + x[0] is negative, so x[1] + x[0] can't possibly be better. Try x[2] + x[1] next.

       x[0] x[1] x[2] x[3]

x[0]     X    ?    ?    ?
x[1]     X    ?    ?    ?
x[2]    (-)   *    ?    ? 
x[3]    (+)   X    X    X

x[2] + x[1] is negative, so x[1] + x[1] can't be better. Try x[2] + x[2] next.

       x[0] x[1] x[2] x[3]

x[0]     X    X    ?    ?
x[1]     X    X    ?    ?
x[2]    (-)  (-)   *    ? 
x[3]    (+)   X    X    X

... and so on.

Upvotes: 1

Related Questions