Page 79 - Textos de Matemática Vol. 38

ORDINALS, COMPUTATIONS, AND MODELS OF SET THEORY 71
the program will call itself with non-empty stacks α = α0, α1, . . . , αn−1 and compute the value F(αn−1). During the main loop of the program the bounded quantifier ∃ν < α ranges over all ν < α. The subloop evaluates the kernel H(α,ν,F(ν)) = 1 of the quantifier and returns the result for the further calcu- lation.
value:=2
MainLoop:
nu:=last(stack) alpha:=llast(stack) if nu = alpha then
%% set value to undefined
1: do remove_last_element_of(stack)
value:=0
goto SubLoop
end_do
else 2: do
stack:=stack + 1 goto MainLoop end_do
SubLoop:
nu:=last(stack) alpha:=llast(stack)
if alpha = UNDEFINED then STOP else
do
if H(alpha,nu,value)=1 then 3: do
%% set value equal to 0
%% push the ordinal 0 onto the stack
remove_last_element_of(stack) value:=1
goto SubLoop
end_do
else 4: do
stack:=stack + 2*(3**y) value:=2
goto MainLoop
end_do
end_do
%% push y+1
%% set value to undefined