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 $s$ (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 $temp$ encoded somewhere in $s$, with $k$-th component $temp_k$. To efficiently undo temp changes, we introduce global Boolean variables $mark_k$ (initially FALSE) for all $temp_k$. In the method below we notationally suppress the task dependency seen in Def. 2.1:

Method 2.1   In the $i$-th phase $(i=1,2,3, ldots)$ DO:

Make an empty stack called Stack. FOR all self-delimiting proof techniques $w in cal L$ satisfying $P(w) geq 2^{-i}$ DO:

1. Run $w$ until halt or error (such as division by zero) or $2^iP(w)$ steps consumed. Whenever the execution of $w$ changes some $temp_k$ whose $mark_k=$ FALSE, set $mark_k :=$ TRUE and save the previous value $overline{temp}_k$ by pushing the pair $(k, overline{temp}_k)$ onto Stack.

2. Pop off all elements of Stack and use the information contained therein to undo the effects of $w$ on $temp$ and to reset all $mark_k$ to FALSE. This does not cost significantly more time than executing $w$.⁵

Method 2.1 is conceptually very simple: it essentially just time-shares all program tests such that each program gets at most a constant fraction of the total search time. Note that certain long proofs producible by short programs (with repetitive loops etc.) are tested early by this method. This is one major difference between BIOPS and more traditional brute force proof searchers that systematically order proofs by their sizes, instead of the sizes (or probabilities) of their proof-computing proof techniques.

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 $w$ 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 $p$ runs on the formalized hardware of the Gödel machine, and since proof techniques tested by $p$ can read $p$ and other parts of $s$, they can produce proofs concerning the (expected or worst-case) performance of $p$ itself.

Back to Goedel machine home page