Bias-Optimal Proof Search (BIOPS)

Given time, the Gödel machine's proof searcher
should systematically generate and test all potentially
relevant proof techniques, to compute alternative
*proof*s and *switchprog*s.
There are many ways of initializing the proof searcher.
Therefore the following details of a particularly fast
example initialization are not really essential for
understanding the basic principles of the Gödel machine.

Let us construct an initial whose proof searcher is optimal in a certain
limited sense to be described below, but *not necessarily optimal*
in the potentially different and more powerful Gödel machine sense
embodied by the given utility function .
We introduce *Bias-Optimal Proof Search* (BIOPS)
which essentially is an application of the recent
*Optimal Ordered Problem Solver*
OOPS [38,40]
to a sequence of proof search tasks.

As long as (which is true at least as long
as no target theorem has been found),
searches a space of *self-delimiting*
[23,6,25,38]
programs written in .
The reader is asked to consult previous work
for details [38,40];
here we just outline the basic procedure:
any currently running proof technique is an
instruction sequence
(whose bitstring-encoded representation
starts somewhere in )
which is read incrementally,
instruction by instruction.
Each instruction is
immediately executed while being read;
this may modify , and may transfer control back to a previously
read instruction (e.g., a loop).
To read and execute a previously unread instruction right
after the end of the
proof technique prefix read so far, first waits until the
execution of the prefix so far *explicitly
requests* such a prolongation, by setting an
appropriate signal in the internal state.
Prefixes may cease to request any further instructions--that's
why they are called self-delimiting.
So the proof techniques form a prefix code, e.g., [25]: no
proof technique that at some point ceases to request a prolongation
of its code can be prefix of another proof technique.

Now to our limited notion of initial optimality.
What is a good way of systematically testing proof techniques?
BIOPS starts with a probability distribution on the
proof techniques written in language .
represents the searcher's initial bias.
could be based on program length,
e.g.,
for binary programs [23,25],
or on a probabilistic version of the
syntax diagram of , where the diagram's edges are labeled
with transition probabilities [38,40].
BIOPS is *near-bias-optimal* in the sense that it will not spend more
time on any proof technique than it deserves,
according to the probabilistic bias,
namely, not more than its probability times the total search time:

The -th proof search task of BIOPS ( ) will be to find a proof of a target theorem applicable to the state of the Gödel machine shortly after the point where the theorem is found. The first such proof may actually provoke a complete Gödel machine rewrite that abolishes BIOPS. So Subsection 2.3.1 will focus just on the very first proof search task. Subsection 2.3.3 will then address the case where the proof searcher has survived the most recent task's solution and wants to profit from earlier solved tasks when possible.

- How the Initial Proof Searcher May Use BIOPS to Solve the First Proof Search Task
- Asymptotic Optimality Despite Online Proof Generation
- How a Surviving Proof Searcher May Use BIOPS to Solve Remaining Proof Search Tasks

Back to Goedel machine home page