How a Surviving Proof Searcher May Use BIOPS to Solve Remaining Proof Search Tasks

In what follows we assume that the execution of the switchprog corresponding to the first found target theorem has not rewritten the code of $p$ itself--the current $p$ is still equal to $p(1)$--and has reset switchbit and returned control to $p$ such that it can continue where it was interrupted. In that case the BIOPS subroutine of $p(1)$ can use OOPS [38,40] to accelerate the search for the $n$-th target theorem ($n>1$) by reusing proof techniques for earlier found target theorems where possible. The basic ideas are as follows (details in [38,40]):

Whenever a target theorem has been proven, $p(1)$ freezes the corresponding proof technique: its code becomes non-writable by proof techniques to be tested in later proof search tasks. But it remains readable, such that it can be copy-edited and/or invoked as a subprogram by future proof techniques. We also allow prefixes of proof techniques to temporarily rewrite the probability distribution on their suffixes [40,38], thus essentially rewriting the probability-based search procedure (an incremental extension of Method 2.1) based on previous experience. As a side-effect we metasearch for faster search procedures, which can greatly accelerate the learning of new tasks [40,38].

Given a new proof search task, BIOPS performs OOPS [40,38] by spending half the total search time on a variant of Method 2.1 that searches only among self-delimiting [23,6] proof techniques starting with the most recently frozen proof technique. The rest of the time is spent on fresh proof techniques with arbitrary prefixes (which may reuse previously frozen proof techniques though) [38,40]. (We could also search for a generalizing proof technique solving all proof search tasks so far. In the first half of the search we would not have to test proof techniques on tasks other than the most recent one, since we already know that their prefixes solve the previous tasks [38,40].)

It can be shown that OOPS is essentially 8-bias-optimal (see Def. 2.1), given either the initial bias or intermediate biases due to frozen solutions to previous tasks [38,40]. This result immediately carries over to BIOPS. To summarize, BIOPS essentially allocates part of the total search time for a new task to proof techniques that exploit previous successful proof techniques in computable ways. If the new task can be solved faster by copy-editing / invoking previously frozen proof techniques than by solving the new proof search task from scratch, then BIOPS will discover this and profit thereof. If not, then at least it will not be significantly slowed down by the previous solutions-- BIOPS will remain 8-bias-optimal.

Back to Goedel Machine Home Page