math.LO — Logic

The Euclidean algorithm is not optimal among uniform processes

Contributed by Jason Davies

Reusing a stored Euclidean prefix, we show that every pair $a\geq b$ has a derivation of $\gcd(a,b)$ from $a,b$ with $O(\log a/\log\log a)$ applications of the remainder function alone; Euclid's algorithm needs order $\log a$ in the worst case. These derivations bound the intrinsic complexity of gcd and coprimeness by the same order, refuting Moschovakis's conjectured logarithmic lower bounds for uniform processes; by his best-uniform-process theorem, a single uniform process attains this bound. The Main Conjecture for algorithms remains open. We also prove an $\Omega(\log\log a)$ lower bound on this complexity for almost all coprime pairs and give, for each $\varepsilon>0$, a nondeterministic register program computing gcd that, on every input $a\geq b\geq1$, has a successful computation using at most $\varepsilon\log a+O(1)$ remainder calls. The upper bound also answers negatively an open problem of van den Dries and Moschovakis on the closure depth of the gcd. The main bounds and the refutations are formalised in Lean 4; the best-uniform-process theorem is cited.