Proof techniques written in are composed of instructions that allow any part of to be read, such as inputs , or the code of . The instructions of `higher-level' language are actually implemented as subroutines running on the Gödel machine hardware. They may write on , a part of reserved for their temporary results. The output of any tested proof technique is an incrementally growing proof placed in the string variable proof stored somewhere in . proof and are reset to the empty string at the beginning of each new proof technique test. Apart from standard arithmetic and function-defining instructions [38,40] that modify , the programming language includes special instructions for prolonging the current proof by correct theorems, for deleting previously proven theorems from proof to free storage, for setting switchprog, and for checking whether a provably optimal Gödel machine-modifying program was found and should be executed now. Below we list all six special instructions for modifying proof, switchbit, switchprog (there are no others). Two of them form a non-traditional interface between syntax and semantics (Items 4 and 5; marked by `'), relating the search in the space of abstract symbol strings representing proofs to the actual, continually changing Gödel machine state and goal. The nature of the six proof-modifying instructions below makes it impossible to insert an incorrect theorem into proof, thus trivializing proof verification:
Note: It is no problem to fully encode both the hardware description and the initial hardware-describing software within the software itself. To see this, observe that some software may include a program that can print the software.
Since many theorems about the Gödel machine's behavior will typically be provable even in the absence of precise initialization information, however, we do not necessarily insist that the initial state is fully axiomatized, just as we do not insist that the rules governing the environment's behavior are precisely known in advance.
Item 4 will describe an instruction that permits the online creation of theorems closely related to the initialization axioms above, through subroutines that can read parts of the current Gödel machine state and subsequently transform the observations into theorems.
Alternative utility functions would favor improvement of worst case instead of expected future performance, or higher reward intake per time interval etc. See also examples in Section 3.2.
This non-traditional online interface between syntax and semantics requires special care though. We must avoid inconsistent results through parts of that change while being read. For example, the present value of a quickly changing instruction pointer IP (continually updated by the hardware) may be essentially unreadable in the sense that the execution of the reading subroutine itself will already modify IP many times. For convenience, the (typically limited) hardware could be set up such that it stores the contents of fast hardware variables every cycles in a reserved part of , such that an appropriate variant of state2theorem() could at least translate certain recent values of fast variables into theorems. This, however, will not abolish all problems associated with self-observations. For example, the to be read might also contain the reading procedure's own, temporary, constantly changing string pointer variables, etc.^{3}To address such problems on computers with limited memory, state2theorem first uses some fixed protocol to check whether the current is readable at all or whether it might change if it were read by the remaining code of state2theorem. If so, or if are not in the proper range, then the instruction has no further effect. Otherwise it appends an observed theorem of the form to proof. For example, if the current time is 7770000, then the invocation of state2theorem(6,9) might return the theorem , where reflects the time needed by state2theorem to perform the initial check and to read leading bits off the continually increasing (reading also costs time) such that it can be sure that is a recent proper time label following the start of state2theorem.
The purpose of introducing is to deal with hardware-specific temporal delays that may be involved in checking and switching--it may take a significant amount of time to match abstract symbol strings found during proof search to the Gödel machine's real current state. If a target theorem has been found, check() uses a simple prewired subroutine to check whether there is enough time left to set switchbit (originally 0) to 1 before the continually increasing will equal . If this subroutine returns a negative result, check() exits. Otherwise it sets switchbit (there is no other way of changing switchbit). Then it repeatedly tests until , to make sure the condition of formula (2) was fulfilled at . Then it transfers control to switchprog (there is no other way of calling switchprog). The switchprog may subsequently rewrite all parts of , excluding hardware-reserved parts such as and , but including .
With the typical example of formula (1)
the utility of switching to switchprog at a certain time
depends on the remaining expected lifetime.
So the set of possible target theorems (2)
and the expected utility of self-changes may vary over time as
more and more of the lifetime is consumed.
Given the possibly limited axiomatized knowledge about how the
environment will evolve,
proof techniques may reason about the code of check()
described above. They can prove a goal
theorem of the form (2) from
the current, unmodified axioms only if
the potential upcoming
transfer of control to the current switchprog provably yields
higher expected cumulative reward
within the resulting expected
remaining lifetime than ignoring switchprog and continuing
the proof search (thus eventually creating and evaluating many
alternative switchprogs). Of course,
this fully takes into account the time needed to
complete the switch to switchprog and to execute switchprog,
which will consume part of the remaining life.
One way a proof technique could start to
infer target theorem (2)
would be to first prove a prediction about parts of at some
time in the near future,
such as
Note that a proof technique does not necessarily have to compute the true expected utilities of switching and not switching--it just needs to determine which is higher. For example, it may be easy to prove that speeding up a subroutine of the proof searcher by a factor of 2 will certainly be worth the negligible (compared to lifetime ) time needed to execute the subroutine-changing algorithm, no matter what's the precise utility of the switch.