Space-unconstructable function in the proof of Savitch's theorem

Question

I'm learning about the Savitch's theorem, and while the construction proof is straightforward, I still don't understand one part about it.

The proof I'm talking about is the same as is currently on Wikipedia. It starts by describing a function - let's call it CAN_YIELD(start, end, limit) for now.

It is then said that the non-deterministic Turing Machine can be simulated by a deterministic Turing Machine by calling CAN_YIELD(start_state, end_state, f(n)).

The proof then continues by describing that the function takes O(f(n)) space for one configuration and O(f(n)) for the recursion of the function. This nicely results in O(f(n)^2) which is the result we want.

The issue is that if the f(n) is not space-constructible, we don't know what limit number we should input into the CAN_YIELD function. I've seen some proofs saying that we can add something like a 'size' parameter and check if it is large enough - but again, we don't know the actual f(n) value, so I don't understand how this works.

One example of such proof can be found here. Another instance is this answer that states that we can replace the space-constructability requirement of the function by using a fixed space bound, which we increase after every iteration. Same issue as before, I don't see how that might work without knowing when to stop.

I'd be happy for any insight into this issue, or any corrections made to my statements!

Answer 1

Starting Point: ​ ​ ​ ​ ​ ​ ​ For inputs x, if ​ ​ ​ [there is no sequence of choices
which makes the non-deterministic machine accept x] ​ and
[for all positive integers S, there is a sequence of non-deterministic choices that,
when made for input x, will cause the non-deterministic machine to use more than S space]
then on input x, the deterministic machine is allowed
to run forever with no bound on its space usage.

Otherwise, such simulation would suffice for solving the halting problem:
Run the simulator until it halts or loops, then output accordingly.


With that in mind, the simulation works as follows:

S = 1
while True:
    run CAN_YIELD with space-bound S
    if that accepts then accept
    increase S by 1
    for end_state in configurations_at_which_the_nondeterministic_machine_might_have_just_used_more_than_space_(S):
        run CAN_YIELD with space-bound S and end_state
        if that accepts then break out of the for loop
    if the for loop ended without a break then REJECT