0
$\begingroup$

I want to prove that the basic multiplication algorithm is correct when applied to binary numbers. I try to follow the steps described here and here but didn't succeed.

The basic implementation algorithm is the multiply function defined below, the other functions are given by completeness (this is F# but it reads as pseudo code):

let toBitsArray (x : int) =
    let bitArray = System.Collections.BitArray(System.BitConverter.GetBytes(x))
    let bits = Array.zeroCreate<bool> bitArray.Count
    bitArray.CopyTo(bits, 0)
    bits

(* Gives an array of bits (bool: 1 or 0) in little endian representation 
   for example 5 = 00000000000000000000000000000101 (32 bits)
   the function will give this array:
   [|true; false; true; false; false; false; false; false; false; false; 
     false; false; false; false; false; false; false; false; false;
     false; false; false; false; false; false; false; false; false;
     false; false; false; false|] 
   which represents 10100000000000000000000000000000 (32 bits) *)
let toLittleEndianBitsArray (x : int) = 
    let bits = toBitsArray x
    if System.BitConverter.IsLittleEndian
    then bits
    else Array.rev bits

let multiply (x : int) (y : int) =
    let by = toLittleEndianBitsArray y
    let rec loop (x : int64) (y : bool list) =
        if List.isEmpty y 
        then 0L
        else 
            let h = List.head y        
            let t = List.tail y
            if h
            then x + (loop (x <<< 1) t)
            else loop (x <<< 1) t

    loop (int64 x) (List.ofArray by)
$\endgroup$
  • 2
    $\begingroup$ Is there a specific step in the proofs you linked that is tripping you up? $\endgroup$ – Aaron Rotenberg Nov 26 '19 at 22:01
  • $\begingroup$ well, I'm not being able of coming with an induction step that eases the proof, in the examples I linked there is P(m) = x+y=m+1, m >= 2 and x, y >= 1 then it proves the recursion with multiplication(x-1,y) but I have to prove it with multiplication( leftshift x, y)... I do not see how to proceed $\endgroup$ – sabotero Nov 26 '19 at 22:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.