Algorithm Termination Proofs

Intro to Proofs · Axiom Academy

Will this loop ever finish? Find one quantity that strictly falls and can't go below a floor — and you've proven it must halt. A loop runs while a b , shaving b off a each pass. It could be subtle code — but watch the value of a : it strictly drops every step and can't fall below zero . A quantity like that is a monovariant , and it's the whole proof that the loop terminates. Set a starting value, hit Run, and watch divide(a, 4) subtract 4 again and again. The variant V(a)=a steps down toward the floor — and the instant it drops below b , the loop stops. It can't run forever: there's a bottom. How many steps until it halts? A bounded, strictly-falling variant doesn't just halt — it halts soon , and you can count it. With a = 120 fixed, drag the drop b : each pass removes b , so the loop takes iterations. The bigger the drop, the faster it hits the floor. The floor is what does the work Here's the real point. The baseline drops b = 8 ; drag to drop more each step and watch the iterations fall away. Both descents end — not because of how fast they fall, but because there's a floor . Take the floor away and a strictly-falling variant could descend forever. The bound below is the guarantee.

This is the written version of the interactive lesson above. See the full Intro to Proofs course.