<p>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!</p>

<p>For instance, we could write a loop that computes the <a href="https://en.wikipedia.org/wiki/Goodstein%27s_theorem#Goodstein_sequences" rel="noreferrer">Goodstein sequence</a>. 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.</p>

<p>At this point we have two choices:</p>

<ol>
<li><p>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.</p></li>
<li><p>Use a loop invariant which requires ordinal numbers but is <em>informative</em> because it is an obviously decreasing sequence that dominates the Goodstein sequence.</p></li>
</ol>

<p>Take your pick.</p>

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

CC BY-SA 4.0
2018-09-17T07:09:52.887Z
2018-09-17T07:56:07.507Z
2018-09-17T07:56:07.507Z
Andrej Bauer
<p>I would like to add the following to Andrej's response (not enough rep for a comment).</p>

<p>Indeed, we cannot avoid ordinals but we may <em>hide</em> 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 <a href="https://dx.doi.org/10.1109/LICS.2000.855774" rel="noreferrer">Nakano</a> and <a href="https://doi.org/10.1145/1190216.1190235" rel="noreferrer">other people</a> to handle termination, but also in <a href="https://doi.org/10.1109/LICS.2013.27" rel="noreferrer">domain theoretic proofs</a>. In fact, <a href="https://doi.org/10.1007/BF02757006" rel="noreferrer">Solovay</a> 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.</p>

CC BY-SA 4.0
2018-09-17T13:58:04.960Z
2018-09-17T13:58:04.960Z
Henning Basold
<p>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.</p>

<p>For instance, I <em>think</em> 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.</p>

<p>Instead, I think it's good to think of limit ordinals as being more <em>flexible</em> than e.g. natural numbers. They allow you to describe inductive processes where you are able to make <em>local</em> 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 <em>will</em> be made ahead of time, and construct a corresponding natual number that is big enough for all those choices.</p>

<p>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 <em>will</em> only ever require finitely many in practice.</p>

<p>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.</p>

CC BY-SA 4.0
2018-09-17T23:22:52.727Z
2018-09-17T23:22:52.727Z
Dan Doel
<p>I do not understand why one would ever need a transfinite loop variant. </p>

<p>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$. </p>

<p>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? </p>

CC BY-SA 4.0
2018-09-17T03:00:31.417Z
Would you like to provide some context? For instance what is a transfinite loop?
Łukasz Lew
CC BY-SA 4.0
2018-09-27T09:03:10.320Z
Sorry for the confusion! It should read transfinite (loop variant), not (transfinite loop) variant.
blk
<lo.logic><computability><pl.programming-languages><program-verification>
Why/when do we ever need transfinite loop variants?
blk
# Why/when do we ever need transfinite loop variants?

(Asked by: username_0 on 2018-09-16)

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?

**Tags:** lo.logic, computability, pl.programming-languages, program-verification
> **Comments:**
> **username_1**: Would you like to provide some context? For instance what is a transfinite loop?  
> **username_0**: Sorry for the confusion! It should read transfinite (loop variant), not (transfinite loop) variant.  

---

## 3 answers

### Answer by username_2 on 2018-09-17. Score: 13

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](https://en.wikipedia.org/wiki/Goodstein%27s_theorem#Goodstein_sequences). 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 by username_3 on 2018-09-17. Score: 9

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](https://dx.doi.org/10.1109/LICS.2000.855774) and [other people](https://doi.org/10.1145/1190216.1190235) to handle termination, but also in [domain theoretic proofs](https://doi.org/10.1109/LICS.2013.27). In fact, [Solovay](https://doi.org/10.1007/BF02757006) 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 by username_4 on 2018-09-17. Score: 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.


---

