Reading this question got me thinking: For a given function f, how can we know that a loop of this form:

while (x > 2)
   x = f(x)

will stop for any value x? Is there some simple criterion?

(The fact that f(x) < x for x > 2 doesn't seem to help since the series may converge).

Specifically, can we prove this for sqrt and for log?

+6  A: 

For these functions, a proof that ceil(f(x))<x for x > 2 would suffice. You could do one iteration -- to arrive at an integer number, and then proceed by simple induction.

For the general case, probably the best idea is to use well-founded induction to prove this property. However, as Moron pointed out in the comments, this could be impossible in the general case and the right ordering is, in many cases, quite hard to find.

Edit, in reply to Amnon's comment:

If you wanted to use well-founded induction, you would have to define another strict order, that would be well-founded. In case of the functions you mentioned this is not hard: you can take x << y if and only if ceil(x) < ceil(y), where << is a symbol for this new order. This order is of course well-founded on numbers greater then 2, and both sqrt and log are decreasing with respect to it -- so you can apply well-founded induction.

Of course, in general case such an order is much more difficult to find. This is also related, in some way, to total correctness assertions in Hoare logic, where you need to guarantee similar obligations on each loop construct.

How can we do this? "Smaller than" doesn't appear to be a well founded relation on a real interval, since any open subset doesn't have a minimal element.
Edited to provide the details of using wf induction.
@finrod: Are you claiming that given a function f, such an ordering is always possible to find (assuming termination for every x)? Maybe you should rephrase: 'could try' instead of 'would have".
@Moron, I believe that the ordering should encode *why* the function stops. It doesn't have to be linear, so basically if you understand why the function terminates, you should be able to construct the proof that its argument gets "smaller" in each subsequent call. Of course we aren't able to do this right now for the function in Collatz sequence: but that is because we don't know *why* (or even, in this case, if) the function terminates. I don't have the proof, but I'll think on it in spare time.Besides, in order to prove this by wf induction, you have to define the order ;)
@finrod: I am not so sure that an ordering will always exist given an f, which will allow you to prove loop termination. Your post comes off as saying there will. Existence of an ordering is just a sufficient condition for loop termination (and is a very useful technique), but it is not a necessary one. So I suggest you edit your post to only talk about sufficiency, not necessity. Btw, you don't need to define an order to prove existence. E.g: Well Ordering Theorem proof using Zorn's Lemma doesn't give you one :-)
@Moron, I believe there is a connection to a lemma from Term Rewriting I've seen some time ago. I will check this -- and if I cannot give a proof it exists, I will edit the answer.
@finrod: +1 :-).
+2  A: 

(The fact that f(x) < x for x > 2 doesn't seem to help since the series may converge).

If we're talking about floats here, that's not true. If for all x > n f(x) is strictly less than x, it will reach n at some point (because there's only a limited number of floating point values between any two numbers).

Of course this means you need to prove that f(x) is actually less than x using floating point arithmetic (i.e. proving it is less than x mathematically does not suffice, because then f(x) = x may still be true with floats when the difference is not enough).

Yeah, I kind of forgotten about floats. Then again, there are occasions sometimes, when one would need arbitrary precision numbers -- and then this would not suffice.Also, the floating point arithmetic has its quirks when very small numbers are considered, and it might be hard to establish the proof.
@sepp2k: that's a good point! But I'm assuming x is a real number.
+2  A: 

There is no general algorithm to determine whether a function f and a variable x will end or not in that loop. The Halting problem is reducible to that problem.

For sqrt and log, we could safely do that because we happen to know the mathematical properties of those functions. Say, sqrt approaches 1, log eventually goes negative. So the condition x < 2 has to be false at some point.

Hope that helps.

The question wasn't about an algorithmic way to do this. In fact, you could find it hard to encode the function `f` and the real number `x` as an input.
+3  A: 

There's a general theorem for when then sequence of iterations will converge. (A convergent sequence may not stop in a finite number of steps, but it is getting closer to a target. You can get as close to the target as you like by going far enough out in the sequence.)

The sequence x, f(x), f(f(x)), ... will converge if f is a contraction mapping. That is, there exists a positive constant k < 1 such that for all x and y, |f(x) - f(y)| <= k |x-y|.

John D. Cook
k must be less than 1
Thanks. Yes, k must be less than 1. I updated my answer.
John D. Cook
+1  A: 
+1  A: 

Sure. For all positive numbers x, the following inequality holds:

 log(x) <= x - 1

(this is a pretty basic result from real analysis; it suffices to observe that the second derivative of log is always negative for all positive x, so the function is concave down, and that x-1 is tangent to the function at x = 1). From this it follows essentially immediately that your while loop must terminate within the first ceil(x) - 2 steps -- though in actuality it terminates much, much faster than that.

A similar argument will establish your result for f(x) = sqrt(x); specifically, you can use the fact that:

sqrt(x) <= x/(2 sqrt(2)) + 1/sqrt(2)

for all positive x.

If you're asking whether this result holds for actual programs, instead of mathematically, the answer is a little bit more nuanced, but not much. Basically, many languages don't actually have hard accuracy requirements for the log function, so if your particular language implementation had an absolutely terrible math library this property might fail to hold. That said, it would need to be a really, really terrible library; this property will hold for any reasonable implementation of log.

Stephen Canon

I suggest reading this wikipedia entry which provides useful pointers. Without additional knowledge about f, nothing can be said.

Alexandre C.