2
$\begingroup$

I know that the general strategy to do the correction of an algorithm is as follow :

  • if the algorithm is recursive then prove the correctness using induction
  • if the algorithm is iterative (using a for loop for example) then find an invariant

Finding an invariant is sometimes hard while induction is easy. So since every iterative algorithm can be transformed into a recursive one, why do we bother finding clever invariant while we could do :

find the recursive equivalent algorithm -> use induction

Maybe the part : "transform the iterative program into a recursive one" is hard, but for simple programs it's definitely worth it. I mean sometimes it is (at least for me) very hard to find invariant, but when doing induction everything is "easy".

So I guess I am missunderstanding something ?

Thank you !

$\endgroup$
  • $\begingroup$ Using a loop invariant is also a proof by induction. The main difference is that a recursive procedure often comes with a "loop invariant", since its semantics are known. $\endgroup$ – Yuval Filmus Feb 22 at 19:15
  • $\begingroup$ @user100779 yes, you misunderstand, basically. $\endgroup$ – Apass.Jack Feb 22 at 20:06
4
$\begingroup$

A proof using a loop invariant is also a proof by induction – you prove that the invariant is indeed an invariant by induction. The reason that finding the inductive hypothesis is easier for recursive procedures is that we usually state the semantics of the recursive function – what it is supposed to compute – and this is the "loop invariant" we use to prove its correctness.

Let's consider the following two procedures for summing an array $A[1],\ldots,A[n]$:

Iterative:

  1. $sum \gets 0$
  2. $i \gets 1$
  3. While $i \leq n$:
    • $sum \gets sum + A[i]$
    • $i \gets i + 1$
  4. Return $sum$

Recursive:

$Sum(A[1],\ldots,A[n])$

  1. If $n = 0$, Return $0$
  2. If $n > 0$, Return $Sum(A[1],\ldots,A[n-1]) + A[n]$

The loop invariant for the iterative algorithm is $sum = A[1] + \cdots + A[i-1]$. This is something we have to come up with. We prove that it holds by induction, and conclude that the function returns $A[1] + \cdots + A[n]$.

In contrast, it is clear what $Sum$ is supposed to compute: the sum of its input. We still need to argue inductively that $Sum$ works correctly, but the inductive hypothesis $$Sum(A[1],\ldots,A[i]) = A[1] + \cdots + A[i]$$ corresponds to the semantics of $Sum$.

We often attach a meaning to recursive procedures, but not so often to loops. If we did attach a semantic meaning to the $i$'th iteration, it would become easy to formulate the loop invariant. An example is the Floyd–Warshall algorithm (or rather, some of its implementations), where the $i$'th iteration computes the shortest path of length at most $i$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.