2026-10-20 11:01 UTC
Oh my god, I'm teaching the kids stuff that relies on thinking about the "trace" of Euclid's algorithm, before having taught them induction... Very sketchy :-(.
If I were starting from scratch, I'd teach them inductive definitions from the start, and then derive Euclid's algorithm from such an inductive definition.
Replies (2)
-
@ohad@mathstodon.xyz 2026-10-20 12:04
@jonmsterling@mathstodon.xyz I don't remember that. We were using the UMP of gcd
-
@jer_gib@functional.cafe 2026-10-20 14:14
@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.