0

Binary GCD algorithm is described in the following link: https://en.wikipedia.org/wiki/Binary_GCD_algorithm

I wonder if there exists any mathematics proof of the finiteness of this algorithm,that is,how to prove that the GCD can be achieved within finite times of iterations with this algorithm? 

while n != 0 and m != 0 do
    if n is even and m is even then
        ans ← ans × 2
        n ← n/2
        m ← m/2
    else if n is even and m is odd then
        n ← n/2
    else if n is odd and m is even then
        m ← m/2
    end if
    if n > m then
        swap(n, m)
    end if
    m ← (m − n)
end while
return n × ans

My partial solution:

set a>=b
case 1:a%2=0 and b%2=0 a=a/2-b/2;b=b/2;
case 2:a%2=0 and b%2=1 
    if a/2>=b a=a/2-b;b=b;
    else a=b b=b-a/2
case 3:a%2=1 and b%2=0 a=a-b/2;b=b/2;
case 4:a%2=1 and b%2=1 a=a-b;b=b

Since in every iteration,if a!=b,the larger one will strictly decrease.The ways to terminate the loop is that a=2b or a=b,both ways will let the larger one to turn zero.So the larger one will eventually the turn zero in finite times,and the loop stops.Can anybody give me advice on my proof?

novahow
  • 1
  • What have you tried? – saulspatz Mar 18 '20 at 12:36
  • @saulspatz I tried setting a=(2^s)m ,b=(2^t)n,and the result will decline through each iteration,but i can't figure out how to prove that a and b will eventually be the same. – novahow Mar 18 '20 at 13:28
  • What are $a,b,s,t,m,n$? Please edit the question body to show the algorithm and your attempt at proof. I can't help you if I don't know what you've done. – saulspatz Mar 18 '20 at 14:03
  • @saulspatz I've given a poor proof for this,I'll be glad if you can give me some advice or pinpoint the flaw of the proof. – novahow Mar 18 '20 at 14:37
  • Well, if the larger one is zero, so is the smaller one, because neither is ever negative. But the loop stops as soon as one of the is zero. Bur why are you using different letters in the algorithm and the proof? That doesn't make sense. – saulspatz Mar 18 '20 at 16:14

0 Answers0