歐幾里得 GCD 的正確性證明（Euclid's GCD correctness proof）
/ YOO-klid /
歐幾里得演算法用一條出奇簡單的規則，找出兩數的最大公因數（gcd，即同時整除兩者的最大整數）：把數對 (a, b) 換成 (b, a mod b)，反覆進行，直到第二個數變成 0；此時第一個數就是答案。它有兩千多年歷史，至今仍是標準方法。它的正確性建立在一個乾淨的數論事實加上一個終止度量之上，使它成為「遞迴程序之完整（完全）正確性證明」的絕佳小例子。
關鍵引理：當 b > 0 時，gcd(a, b) = gcd(b, a mod b)。為什麼？寫 a = q*b + r，其中 r = a mod b。任何同時整除 a 與 b 的數，也整除 r = a - q*b；而任何同時整除 b 與 r 的數，也整除 a = q*b + r。所以數對 (a, b) 與數對 (b, r) 擁有完全相同的公因數集合，因而有相同的最大公因數。基底情形是 gcd(a, 0) = a，因為每個數都整除 0，所以 a 與 0 的公因數就只是 a 的因數，其中最大的正是 a 本身。正確性接著由對遞迴呼叫的歸納得出：引理說每一步都保住 gcd，基底情形正確回傳它，所以演算法回傳的值等於原始輸入的 gcd。
終止需要把第二個引數當作良基度量：a mod b 永遠是嚴格小於 b 的非負整數，所以第二個分量每步嚴格遞減，且不會低於 0。一個嚴格遞減的非負整數序列，必在有限步內到達 0，屆時基底情形就觸發。部分正確性（引理＋基底情形）加上終止（遞減度量）一起給出完全正確性。誠實的提醒：這個論證假設 b > 0 才能套用 mod 步驟，且輸入為非負整數；兩個零的 gcd、或負數的 gcd，需要另立慣例。
gcd(252, 105)：252 mod 105 = 42 -> gcd(105, 42)；105 mod 42 = 21 -> gcd(42, 21)；42 mod 21 = 0 -> gcd(21, 0) = 21。引理讓每一步的 gcd 都維持等於 21，而第二個引數 105、42、21、0 嚴格遞減——正確性與終止，兩者都看得見。
引理 gcd(a,b)=gcd(b, a mod b) 讓答案固定不變；遞減的第二個引數逼迫停止。
整個證明的關鍵在於引理：(a,b) 與 (b, a mod b) 共享相同的公因數集合——而不只是 gcd 數值碰巧相同。終止則依賴 a mod b 嚴格小於 b（一個非負整數度量）。