Loop Invariants as Tautologies

Question

Would it be correct to characterize loop invariants as a type of tautology? I ask since the invariant must basically always be true, before the loop starts, before each iteration and after the loop terminates. I realize that there is the possibility that the invariant could become false during the body of the loop. But since inside the loop "doesn't count" is it fair to characterize the invariant as a tautology?

Answer 1

A Tautology is a formula (in a certain logic) that is true under every model of that logic. That is, it is equivalent to the formula "$True$".

A loop invariant, however, is a certain claim that is usually true under some models, and false under others (a model in this case is an algorithm). Then, you prove that the invariant is true under your specific model.

If you add axioms to your logic that forces then only model to be the one of your specific program, then indeed this would be a tautology. But such a process (adding axioms and proving that something is a tautology), is what is more commonly known as "proof". (For clarification: even if you add enough axioms, you may not be able to prove your claim, even if it's a tautology, in case of incomplete systems).

For example, consider a loop that increases a variable $i$ by $1$. An invariant of the loop may be that if before the loop $i>0$, then after the loop $i>0$. Indeed, this loop satisfies it. But it is not a tautology, since we can come up with other loops that do not satisfy it.

Answer 2

The word tautology is a technical word. The following is a tautology of classical propositional logic.

$\vdash p \lor \neg p$

When interpreted over the natural numbers, the following is a theorem.

$ (\mathbb{N},<)\vdash \forall x. \exists y. x < y$

But we do not say it is a tautology in the strict logical sense of the word because there are structures where this is not true.

Considering $S = \{a,b\}$, $<$ defined as $\{(a,b)\}$, we have $(S,<) \not \vdash \forall x. \exists y. x < y$

Similarly, if you think of a loop $P$ as implicitly defining the axioms of a theory, then a loop invariant $I$ as satisfying

$P \vdash \text{Every execution satisfies } I $

Thus, in exactly the same way as the existence of successors is a theorem of arithmetic, a loop invariant is a theorem of a logical theory defined by the program. A loop invariant is not a tautology in the standard mathematical sense of the word tautology. A tautology in this context would satisfy

$ \vdash \text{Every execution satisfies } I $

From which we can conclude that every tautology is a loop invariant, but not every loop invariant is a tautology.

Answer 3

I am guessing that, by "tautology," you mean a property that is true in all states. (I have seen some Lecturers use the term in that way, e.g., $x > 1 \Longrightarrow x > 0$, which is true in all states no matter what $x$ is, might be called a "tautology". The technical definition of "tautology" in logic is more narrow, but I will continue to use your terminology.)

A loop invariant is only true at a particular program point in the loop. It is true for every state encountered at that point, but it might be false for states encountered at other program points (inside the loop as well as outside the loop). So, clearly, it is not a "tautology" in the sense I stated above.

However, there is an interesting proof rule formulated in Reynolds's extension of Hoare Logic. If, in a particular piece of code, there are no operations that affect the truth/falsity of an assertion, and we know that the assertion is true at the beginning of the code, then we can pretend that the assertion is a "tautology" in the middle of that code.

A good example of this is a binary search procedure for an array $A$. Before the procedure starts, the pre-condition states that the array is sorted. Inside the binary search procedure, we don't do anything to modify the array. So, it will continue to be sorted throughout the procedure. Reynolds's rule says that, for the duration of the procedure, we can pretend that "$A$ is sorted" is a "tautology". This is a useful trick to use. Without it we would need to add "$A$ is sorted" in every assertion in the middle of the procedure, and we can see that it is quite pointless to keep repeating this silly condition because we are never modifying the array. Reynolds's rule allows to avoid the silliness.

For interesting applications of this rule, see the Chapter 5 of Reynolds's Craft of Programming.