Page 80 - Textos de Matemática Vol. 38

72 PETER KOEPKE
The correctness of the program with respect to the above intention is established by
Theorem 8.3. The above program P has the following properties
a) If P is in state MainLoop at time s with stack contents ⟨α0, α1, . . . , αn−1⟩ where n 1 then it will get into state SubLoop at a later time t with the same stack contents ⟨α0, α1, α2, . . . , αn−1⟩ and the register value holding the value F (αn−1 ). Moreover in the time interval [s, t) the contents of stack will always be at least as big as ⟨α0, α1, . . . , αn−1⟩.
b) Let P be in state MainLoop at time s with stack contents α0 > α1 > α2 > · · · > αn−1 where n 1. Define α¯ =the minimal ordinal ν < αn−1 such that H(αn−1,ν,F(ν)) = 1 if this exists and α¯ = αn−1 else. Then there is a strictly increasing sequence (ti|i α¯) of times ti > t such that P is in state MainLoop
at time ti with stack contents ⟨α0, α1, α2, . . . , αn−1, i⟩, and in every time interval τ ∈ [ti, ti+1) the stack contents are ⟨α0, α1, α2, . . . , αn−1, i⟩.
c) If P is in state MainLoop with stack contents α then it will later stop with stack content α and the register value holding the value F (α). Hence the function F is ordinal register computable.
Proof. a) and b) are proved simultaneously by induction over the last element αn−1 of the stack. Assume that P is in state MainLoop at time s with stack contents ⟨α0,α1,α2,...,αn−1⟩ where n 1 and that a) and b) hold for all stack contents ⟨β0, β1, . . . , βm−1⟩ with βm−1 < αn−1. Define α¯ as in b).
We first prove b) by defining an appropriate sequence (ti|i α¯) by recur- sion over i α¯.
i = 0: inspection of P shows that the computation will move to state 2 and obtain stack contents ⟨α0, α1, α2, . . . , αn−1, 0⟩ before immediately returning to MainLoop.
i=j+1wherej<α¯.Byrecursion,P isinstateMainLoopattimetj with stack contents ⟨α0, α1, α2, . . . , αn−1, j⟩. j < α¯ αn−1 so that by the simultane- ous induction a) holds for ⟨α0, α1, α2, . . . , αn−1, j⟩. So there will be a later time when P is in stateSubLoopwith stack contents ⟨α0,α1,α2,...,αn−1,j⟩ and value= F(j). Also during that computation the stack contents will always be ⟨α0, α1, α2, . . . , αn−1, j⟩. Inspection of the program shows that it will further compute H(αn−1, j, F (j)). This value will be ̸= 1 by definition of α¯. So the com- putation will move on to state 4 with stack contents ⟨α0, α1, α2, . . . , αn−1, j + 1⟩. At the subsequent time ti = tj+1 P is in state MainLoop with stack contents ⟨α0,α1,α2,...,αn−1,i⟩.
i is a limit ordinal. Then by the limit behaviour of the machine and in partic- ular by the above proposition, at time{tj|j < i} the machine will be in state MainLoop with stack contents.
Now we prove a).
Case 1: α¯ < αn−1. Then F(α¯) = 1. By b) P will get to state MainLoop