Online Universal Search in Proof Space

BIOPS starts with a probability distribution $P$ (the initial bias) on the proof techniques $w$ that one can write in $\cal L$, e.g., $P(w)=K^{-l(w)}$ for programs composed from $K$ possible instructions [26]. BIOPS is near-bias-optimal [47] in the sense that it will not spend much more time on any proof technique than it deserves, according to its probabilistic bias, namely, not much more than its probability times the total search time:

Definition 5.1 (Bias-Optimal Searchers [47])   Let $\cal R$ be a problem class, $\cal C$ be a search space of solution candidates (where any problem $r \in \cal R$ should have a solution in $\cal C$), $P(q \mid r)$ be a task-dependent bias in the form of conditional probability distributions on the candidates $q \in \cal C$. Suppose that we also have a predefined procedure that creates and tests any given $q$ on any $r \in \cal R$ within time $t(q,r)$ (typically unknown in advance). Then a searcher is $n$-bias-optimal ($n \geq 1$) if for any maximal total search time $T_{total} > 0$ it is guaranteed to solve any problem $r \in \cal R$ if it has a solution $p \in \cal C$ satisfying $t(p,r) \leq P(p \mid r)~T_{total}/n$. It is bias-optimal if $n=1$.

Method 5.1 (BIOPS)   In phase $(i=1,2,3, \ldots)$ DO: FOR all self-delimiting [26] 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.
2. Undo effects of $w$ on $s^p$ (does not cost significantly more time than executing $w$).

A proof technique $w$ can interrupt Method 5.1 only by invoking instruction check() (Item 5), which may transfer control to switchprog (which possibly even will delete or rewrite Method 5.1). Since the initial $p$ runs on the formalized hardware, and since proof techniques tested by $p$ can read $p$ and other parts of $s$, they can produce proofs concerning the (expected) performance of $p$ and BIOPS itself. Method 5.1 at least has the optimal order of computational complexity in the following sense.

Theorem 5.1   If independently of variable time(s) some unknown fast proof technique $w$ would require at most $f(k)$ steps to produce a proof of difficulty measure $k$ (an integer depending on the nature of the task to be solved), then Method 5.1 will need at most $O(f(k))$ steps.

Proof. It is easy to see that Method 5.1 will need at most $O(f(k)/P(w)) = O(f(k))$ steps--the constant factor $1/P(w)$ does not depend on $k$. Q.E.D.

Note again, however, that the proofs themselves may concern quite different, arbitrary formalizable notions of optimality (stronger than those expressible in the $O()$-notation) embodied by the given, problem-specific, formalized utility function $u$. This may provoke useful, constant-affecting rewrites of the initial proof searcher despite its limited (yet popular and widely used) notion of $O()$-optimality.