2026-10-20 14:14 UTC
@jonmsterling@mathstodon.xyz I don't know your course, but what's the problem with eg the argument used by Dijkstra et al in terms of loop variants? In computing gcd(a,b), either the loop decreases a+b (a natural) via a subtraction, or it halts. Therefore the loop terminates, and the trace is finite.
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-10-20 14:17
@jer_gib@functional.cafe That's the essence of the proof, yes, but one is still relying here on induction in a way that we haven't taught them yet at this point. Which is a self-inflicted problem, I agree ;-)