As far as I see, what computer scientists refer to as loop invariant proofs are exact replicas of induction proof. Is it true? Can I state that loop invariant proof implies an induction? Is there a theoretical difference?
$\begingroup$
$\endgroup$
$\begingroup$
$\endgroup$
Good question. I think yes, a loop invariant proof implies induction. However, it also deals with the termination step which is outside of the scope of induction. So a loop invariant contains an induction proof, but goes beyond that, and so an induction proof does not do all that a loop invariant proof does.
(1) Here, showing that the invariant holds before the first iteration is like the base case, and showing that the invariant holds from iteration to iteration is like the inductive step.
