Search code examples
algorithmlistocamlproof

Compute the highest value with a given list and operators in OCaml


With a given positive integer list and the addition and the multiplication as operators, I want to compute the highest value.

So if my list is [2,3,4], it will be : 2 * 3 * 4 = 24. If there is at least one 1 in the list, it is a little bit more difficult. I found by testing on several examples that to compute the highest value, I have to add 1 to the minimum of the list and etc... until there is no more 1 in the list and compute the product of all integers. For example : [1,2,3,4] would return ( 2 + 1 ) * 3 * 4 = 36; [1,1,2,3,4] would return ( 1 + 1 ) * 2 * 3 * 4 = 48.

My first question is concerning the algorithm part : how to prove properly that my method is correct and will always return the highest value ?

My second concerns the implementation :

I wrote the following code in OCaml to programm it :

(* Return 'list' with the first occurence of 'x' removed *)
let rec remove list x =
match list with
| [] -> []
| hd :: tl -> if hd = x then tl else hd :: remove tl x
;;

(* Return the maximum value which can be computed with the given list*)
let rec test_max list = match list with
  | [] -> 0
  | hd :: [] -> hd
  | hd :: tl ->
    (* If the list contains 1 : remove it from the list, then sort the list to get the min value and add 1 to it *)
    if List.mem 1 list then begin
      let list = List.sort (fun x y -> if (x < y) then 1 else 0) (remove list 1) in
      let test = (List.hd list) + 1 in
      test_max test::(List.tl list);
    end
    else
     List.fold_left ( * ) 1 list;;

And at the instruction

let test = (List.hd list) + 1 in
          test_max test::(List.tl list);

in test_max I get the error :

Error: This expression has type 'a list
       but an expression was expected of type int

Well, I don't really understand why it is expecting an expression of type int in the recursive call ... ?

Thank you in advance :)


Solution

  • Function application has higher precedence than ::. So, your code test_max test::(List.tl list) should indeed be test_max (test::List.tl list).

    Also, you shouldn't use a ; in this place, as it's used to separate unit instructions. Just put nothing and it'll be fine.

    As for some proof hints:

    n + m > n * m
    <=> ( n + m ) / (n * m) > 1
    <=> 1/m + 1/n > 1
    

    As we use positive integers, and as / is decreasing in its second argument. It's easy to see that this is true iff m or n = 1 (equality can be attained when n and m = 2).

    Now, how do we use this +1?

    (n+1) * m > n * (m+1)
    <=> n * m + m > n * m + n
    <=> m > n
    

    So here are your two lemmas. I'll let you search for a full proof.