Does it make sense to speak of algorithms that take an infinite amount of time to terminate?
In particular, suppose we have a loop with a bound function that is initially positive and is decreased by the loop body each time. Furthermore, suppose that termination of the loop implies that bound function is non-positive. (Ie almost all assumptions of The Invariance Theorem are satisfied.)
Here's the rub, initially the value of the bound function is the cardinality of the natural numbers.
What can be said in such situations?
Any help or direction is most welcome; thank you!
bf
such that before the loop we have, usually,bf > 0
and after the loop we havebf <= 0
. That is, it is an integer-valued expression that depends on the program variables, such that it is decreased by each iteration of the loop body and is guaranteed to be non-positive if/when the loop terminates. $\endgroup$