拡張GCDについて

スナネコです。拡張GCDについての質問に答えます。

問題:
以下のように実装された extgcdがある。
整数 a,b(a,b)\neq(0,0) を満たし、extgcd(a, b) の返り値を (x,y) としたとき、 \max(|x|,|y|)\leq \max(|a|,|b|) が成り立つことを示せ。

def extgcd(a, b):
  # ax+by=gcd(x,y) を満たす (x,y) を返す
  if b == 0: return (1, 0)
  X, Y = extgcd(b, a % b)
  x = Y
  y = X - a // b * Y
  return (x, y)


extgcd(a, b) が「|ax+by|=\gcd(a,b) を満たす整数 x,y を返すこと」の証明は省略します。

最初に補題を示しておきます。
補題★:
0 でない整数 a,b と整数 x,y,g について、|ax+by|=g かつ |g|< |b| かつ |x|\leq|b| が成り立つならば、|y|\leq |a| である。
証明:
ax+by=\pm g を変形すると、|by|=|\pm g-ax|\leq|g|+|ax| となり、この両辺を |b| で割ると |y|\leq|g/b|+|ax/b| となります。
ここで |x|\leq |b| の仮定から |x/b|\leq 1 なので |ax/b|\leq |a| であり |y|\leq |g/b|+|ax/b|\leq |g/b|+|a| です。
仮定から |a|,|y| は整数で |g/b|<1 なので、小数部分を無視してよく |y|\leq |a| が成り立つことがわかりました。

もとの問題の証明をします。
証明:
a=0 または b=0 のとき、extgcd(a,b) の返り値は (1,0)(0,1) になることが実際にアルゴリズムの挙動を追うことでわかるのでOKです。
a\neq 0 かつ b\neq 0 のときを考えます。
|x|\leq |b| かつ |y|\leq |a| が成り立つことを示します。このことが示せれば |x|\leq |b|\leq \max(|a|,|b|) かつ |y|\leq |a|\leq \max(|a|,|b|) となって \max(|x|,|y|)\leq \max(|a|,|b|) が成り立つことが言えます。
再帰の深さに関する帰納法で証明します。
まず再帰の深さが1回で終わるケース、つまり a\%b=0 のときを考えます。
このときは実際にアルゴリズムの挙動を追うことで (0,1) が返されることがわかるのでOKです。
次に再帰の深さが2回以上になるケース、つまり a\%b\neq 0 のときを考えます。
このとき、帰納法の仮定を使いつつ示すべきことをまとめると
|bX+(a\%b)Y|=\gcd(a,b) かつ |X|\leq |a\%b| かつ |Y|\leq |b| を満たす整数 X,Y が与えられる。x=Yy= X - \left\lfloor\frac{a}{b}\right\rfloor * Y としたとき、|x|\leq |b| かつ |y|\leq |a| となることを示せ」です。
x=Y なので |x|=|Y|\leq |b| は明らかです。
a\%b\neq 0 なので |\gcd(a,b)|<|b| になることに注意すると、「a,b\neq 0 かつ |ax+by|=\gcd(a,b) かつ |\gcd(a,b)|< |b| かつ |x|\leq |b|」が成り立っているので補題★を使うことができて、|y|\leq |a| が成り立つことがわかります。
よって帰納法により証明できました。