Asymptotic Optimality Despite Online Proof Generation

Online proof techniques whose outputs depend on ephemeral events such as inputs should be viewed as a potentially extremely useful asset, not as an unwanted burden. Their advantages become particularly obvious when the original axioms state that parts of certain appropriately marked inputs may be taken as teacher-given theorems without further proof. Such external online help may be dangerous but can greatly speed up the proof search, since there will be short/probable (and therefore frequently tested) programs exploiting the helpful information by simply appending copies of teacher-given theorems to proof. Similarly, the outcome of online experiments may severely restrict the possible futures of the environment. This in turn could be used by the Gödel machine to greatly reduce the search space of relevant proof techniques and of candidates for useful behavior.

As already mentioned above, however, online proof techniques will in general produce different outputs at different times. Is this worrisome when it comes to ensuring the property of bias-optimality? Not really: since proof techniques are general programs, some of them may compensate `just in the right way' for online Gödel machine state changes that are caused by time-varying inputs and various processes running on the Gödel machine. In particular, some proof techniques may produce appropriate target theorems no matter what's the precise time at which they are started, e.g., by appropriately computing useful values for switchprog and $t_1$ in formula (2) in response to the current $time$, or by waiting for a certain type of repetitive, informative input until it reappears, etc.

No matter how proof techniques compute proofs, Method 2.1 has the optimal order of computational complexity in the following sense. If independently of $time$ 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 by the Gödel machine), then Method 2.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$. So the method is asymptotically as fast as the fastest (unknown) such proof technique. (Of course, this assumes that the Gödel machine's lifetime will be sufficient to absorb the constant factor.)

In general, however, no method can generate more than a small fraction of the possible proofs, not even Method 2.1, despite its limited optimality properties. For example, each single cycle in principle could already give rise to a whole variety of distinct theorems producible through instruction state2theorem (Item 4 in Section 2.2.1). Most of them will never be generated though, since the instruction itself will typically already consume several cycles.

We observe that BIOPS searches for a provably good switchprog in a near-bias-optimal and asymptotically optimal way, exploiting the fact that proof verification is a simple and fast business. But here the expression `provably good' refers to a typically different and more powerful sense of optimality depending on the Gödel machine's utility function! (BTW, note that the total utility of a Gödel machine may be hard to verify--the evaluation may consume its entire lifetime).

Back to Goedel machine home page