** Next:** How a Surviving Proof
** Up:** Bias-Optimal Proof Search (BIOPS)
** Previous:** How the Initial Proof

###

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
in formula (2)
in response to the current , 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 some unknown, fast proof technique
would require at most steps to produce
a proof of difficulty measure (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
steps--the constant
factor does not depend on .
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).

** Next:** How a Surviving Proof
** Up:** Bias-Optimal Proof Search (BIOPS)
** Previous:** How the Initial Proof
Juergen Schmidhuber
2003-10-28

Back to Goedel Machine Home Page