Why/when do we ever need transfinite loop variants?

Question

I do not understand why one would ever need a transfinite loop variant.

Why do natural-number-valued variants not suffice? My simple (but perhaps too naive) argument is: if a loop $L$ terminates from any initial state then there should be a trivial variant function $V$ which simply maps every state $s$ to the number of iterations needed for $L$ to terminate on $s$. Naturally, $V$ would be decreased by 1 with every iteration of $L$.

Can anyone provide an example of a simple deterministic while loop (no recursion, no reading of additional user provided input during runtime of the loop, no nondeterministic choices, etc.) that terminates on every initial state it is started from and yet requires a transfinite loop variant to prove its termination?

Answer 1

You are correct when you observe that for any particular terminating loop $L$ we may simply define the invariant "we're getting one step closer to termination". But proving that this is indeed a valid invariant may require transfinite induction!

For instance, we could write a loop that computes the Goodstein sequence. This is particular sequence of numbers which starts with any given number $n$ and it eventually terminates, but proving that it terminates for every $n$ requires transfinite induction to the ordinal $\epsilon_0$ (which is the limit of ordinals $\omega$, $\omega^\omega$, $\omega^{\omega^\omega}$, ...)! So, in order to show that a loop computing the Goodstein sequence terminates for every inital term $n$ we need an appeal to transfinite induction.

At this point we have two choices:

1. Use transfinite induciton to show the loop terminates, then "forget" that you used transfinite induction to show that the silly invariant "we're one step closer to the end" does the job.

2. Use a loop invariant which requires ordinal numbers but is informative because it is an obviously decreasing sequence that dominates the Goodstein sequence.

Take your pick.

In summary, it's not just about whether we can avoid ordinal numbers (we cannot avoid them completely), it's also whether we want to. Avoiding them might just complicate your life and lead to convoluted proofs of termination. Why would we do that?

Answer 2

I would like to add the following to Andrej's response (not enough rep for a comment).

Indeed, we cannot avoid ordinals but we may hide them. One approach is to use some modal logic that takes essentially care of "we're one step closer to the end" without mentioning ordinals explicitly. This approach has been used successfully by Nakano and other people to handle termination, but also in domain theoretic proofs. In fact, Solovay showed that a certain modal logic characterises well-founded induction. This allows proving, for example, termination in a way that looks as if we are reasoning about one step, while in reality we progress by well-founded induction.

Answer 3

If I may add something, too, I'd suggest that some of the ways ordinals are presented tend to make them sound more 'suspicious' than they actually are. At least, I think there are other ways of presenting them that make them seem less suspicious.

For instance, I think it's pretty common for people to say or imply that using transfinite ordinals involves doing some steps in a process 'more than' infinitely many times. Like, if we have universes indexed by ordinals, we might talk about the step of constructing a universe containing some sets, and if one of those sets was itself a universe, the 'new' one would be indexed by the successor of the 'old' one. And for indexes of ω and above people might say that we have 'iterated the universe construction' more than finitely many times. That sounds wrong from a perspective where you can only "do" finitely many things.

Instead, I think it's good to think of limit ordinals as being more flexible than e.g. natural numbers. They allow you to describe inductive processes where you are able to make local choices about how big your induction needed to be, whereas to do the same with naturals, you essentially have to figure out all the choices that will be made ahead of time, and construct a corresponding natual number that is big enough for all those choices.

Or, in the universe example, one way in which the universe $U_ω$ is flexible is that for any $U_n$ below it, there are other universes $U_{n+k+1}$ above it, but still below $U_ω$. This is not (necessarily) because we have "done" infinitely many universe constructions, though, but because we have defined $U_ω$ in a way that we can talk about however many finite lower universes as we need, when we need to. We will only ever require finitely many in practice.

Perhaps for any particular example we wish to examine, we could construct exactly the finite structure we want ahead of time (like, you must step from $U_{n+5}$ to $U_n$ because I need that much extra room). But it is much easier to construct a flexible structure that is still used in a finite way.