How the Initial Proof Searcher May Use BIOPS to Solve the First Proof Search Task

BIOPS first invokes a variant of Levin's universal search
[22]
(Levin attributes similar ideas to Adleman [24]).
Universal search is a simple, asymptotically optimal
[22,24,25,16,50],
near-bias-optimal
[38,40]
way of solving a broad class of problems
whose solutions can be quickly verified.
It was originally described for universal
Turing machines with unlimited storage [22].
In realistic settings, however, we have to introduce
a recursive procedure
[38,40]
for time-optimal backtracking in program space
to perform efficient storage management
on *realistic, limited computers.*

Previous practical variants and extensions of universal
search have been applied
[33,35,47,38,40]
to *offline*
program search tasks where the program inputs are fixed
such that the same program always produces the same results.

This is not the case
in the present *online* setting: the same proof technique
started at different times may yield different proofs,
as it may read parts of (such as the inputs)
that change as the Gödel machine's life proceeds.
Nevertheless, we may apply a variant of universal search
to the space of proof-generating programs
as follows.

For convenience, let us first rename the storage writable by
proof techniques: we place
*switchprog*, *proof*, and all other proof technique-writable
storage cells in a common address space called encoded
somewhere in , with
-th component .
To efficiently undo *temp* changes, we
introduce global Boolean
variables (initially FALSE)
for all .
In the method below we notationally suppress the task dependency
seen in Def. 2.1:

Make an empty stack calledStack. FOR all self-delimiting proof techniques satisfying DO:

- Run until halt or error (such as
division by zero) or steps consumed.
Whenever the execution of changes some
whose FALSE,
set TRUE and
save the previous value
by
pushing the pair
onto
*Stack*. - Pop off all elements of
*Stack*and use the information contained therein to undo the effects of on and to reset all to FALSE. This does not cost significantly more time than executing .^{5}

None of the proof techniques can produce an incorrect *proof*,
due to the nature of the theorem-generating instructions from
Section 2.2.1.
A proof technique can interrupt Method 2.1
only by invoking the instruction *check()* which may transfer
control to *switchprog* (which possibly
will delete or rewrite Method 2.1).

Clearly, since the initial runs on the formalized hardware of the Gödel machine, and since proof techniques tested by can read and other parts of , they can produce proofs concerning the (expected or worst-case) performance of itself.

Back to Goedel machine home page