Instructions/Subroutines for Making & Verifying Axioms & Theorems and for Initiating Online Self-Improvements

Proof techniques written in $\cal L$ are composed of instructions that allow any part of $s$ to be read, such as inputs $x$, or the code of $p(1)$. The instructions of `higher-level' language $\cal L$ are actually implemented as subroutines running on the Gödel machine hardware. They may write on $s^p$, a part of $s$ 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 $s$. proof and $s^p$ 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 $s^p$, the programming language $\cal L$ 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 `$\spadesuit$'), 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:

1. get-axiom(n) takes as argument an integer $k$ (computed by a prefix of the currently tested proof technique with the help of arithmetic instructions such as those used in previous work [38,40]). Then it generates the $k$-th axiom (if it exists, according to the axiom scheme outlined below) and appends the axiom as a theorem to the current theorem sequence in proof. The initial axiom scheme encodes:
   1. Hardware axioms: A compact axiomatic description of the finite computer hardware (or the unchangeable software in case the Gödel machine hardware is emulated by software), formally specifying how certain components of $s$ (other than the environmental inputs $x$) may change from one cycle to the next. For example, the following axiom could describe how some 64-bit hardware's instruction pointer stored in $s_{1:64}$ is continually increased by 64 as long as there is no overflow and the value of $s_{65}$ does not indicate that a jump to some other address should take place:
      
      $$(\forall t \forall n : [(n < 2^{58}) \wedge (n > 0) \wedge (t > 1) \wedge (t < T) \wedge (string2num(s_{1:64}(t))=n)$$
      
      
      
      
      $$\wedge (s_{65}(t)=\lq 0\textrm{'}) ] \rightarrow (string2num(s_{1:64}(t+1))=n+64))$$
      
      
      Here the semantics of used symbols such as `(' (open parenthesis) and `$>$' (greater than) and `$\rightarrow$' (implies) are the traditional and obvious ones, while `$string2num$' symbolizes a function translating bitstrings into numbers.

   2. Reward axioms: Axioms defining the computational costs of any hardware instruction, and physical costs of output actions (if any, e.g., when the $y(t)$ are interpreted as robot control signals). Related axioms assign values to certain input events $x$ which may encode rewards for desired behavior, or punishment (e.g., when a Gödel machine-controlled robot bumps into an obstacle). Additional axioms define the total value of the Gödel machine's life as a scalar-valued function of all rewards (e.g., their sum) and costs experienced between cycles $1$ and $T$, etc. Example axiom (unexplained symbols carry the obvious meaning):
      
      $$(\forall t_1 \forall t_2: [(t_1 < t_2) \wedge (t_1 \geq 1) \... ... \leq T) ] \rightarrow [R(t_1,t_2)= r(t_1) + R(t_1+1,t_2)]),$$
      
      
      where $r(t)$ is interpreted as the real-valued reward at time $t$, and $R(t_1,t_2)$ as the cumulative reward between times $t_1$ and $t_2$.

   3. Environment axioms: Axioms embodying limited knowledge about the environment, in particular, axioms restricting the way the environment will produce new inputs $x$ in reaction to sequences of outputs $y$. For example, it may be known in advance that the environment is sampled from an unknown probability distribution that is computable, given the previous history [46,47,15], or at least limit-computable [36,37]. Or, more restrictively, the environment may be some unknown but deterministic computer program [51,34] sampled from the Speed Prior [39] which assigns low probability to environments that are hard to compute by any method. Or the interface to the environment is Markovian [30], that is, the current input always uniquely identifies the environmental state--a lot of work has been done on this special case [28,2,49]. Even more restrictively, the environment may evolve in completely predictable fashion known in advance. All such prior assumptions are perfectly formalizable.

   4. Uncertainty axioms: Standard axioms for arithmetics and calculus and probability theory [19] and statistics and string manipulation that (in conjunction with the environment axioms) allow for constructing proofs concerning (possibly uncertain) properties of $s$ as well as bounds on expected remaining lifetime / costs / rewards, given some time $\tau$ and certain hypothetical values for components of $s(\tau)$ etc. An example theorem saying something about expected properties of future inputs might look like this:
      
      $$(\forall t_1: [(1 \leq t_1) \wedge (t_1 + 15597 < T) \wedge ... ... \lq 01011\textrm{'}) \wedge (x_{40:44}(t_1)=\lq 00000\textrm{'}) ]$$
      
      
      
      
      $$\rightarrow (\exists t: [(t_1 < t < t_1 + 15597) \wedge (P_... ...2}(t) = \lq 011011\textrm{'}\mid s(t_1)) > \frac{998}{1000} )])),$$
      
      
      where $P_{\mu}(. \mid . )$ represents a conditional probability with respect to an axiomatized prior distribution $\mu$ encoded in the environment axioms (Item 1c).

   5. Initial state axioms: Information about how to reconstruct the initial state $s(1)$ or parts thereof, such that the proof searcher can build proofs including axioms of the type
      
      $$(s_{{\bf m}:{\bf n}}(1)={\bf z}),  e.g.:  (s_{7:9}(1)=\lq 010\textrm{'}).$$
      
      
      Here and in the remainder of the paper we use bold font in formulas to indicate syntactic place holders (such as m,n,z) for symbol strings representing variables (such as m,n,z) whose semantics are explained in the text (in the present context $z$ is the bitstring $s_{m:n}(1)$).

      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.

   6. Utility axioms: An axiomatic description of the Gödel machine's overall goal in the form of a utility function. A typical `value to go' utility function (to be maximized) is of the form $u(s, Env): \cal S \times \cal E \rightarrow R$, where $\cal R$ the set of real numbers:
      

      $$u(s, Env) = E_{\mu} \left [ \sum_{\tau=time}^{E_{\mu}(T \mid s, Env)} r(\tau) \mid s, Env \right ],$$ (1)

      
      
      where $E_{\mu}(. \mid . )$ denotes the conditional expectation operator with respect to some axiomatized prior distribution $\mu$ encoded in the environment axioms (Item 1c). Note that $time$ is a function of $s$ and uniquely identifies the current cycle, and that we take into account the possibility of extending the expected lifespan $E_{\mu}(T \mid s, Env)$ through appropriate actions leading to `good' values of $s$.

      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.

2. apply-rule(k, m, n) takes as arguments the index $k$ (if it exists) of an inference rule (e.g., [9]) such as modus ponens (stored in a list of possible inference rules encoded within $p(1)$) and the indices $m, n$ of two previously proven theorems (numbered in order of their creation) in the current proof. If applicable, the corresponding inference rule is applied to the addressed theorems and the resulting theorem appended to proof. Otherwise the currently tested proof technique is interrupted. This ensures that proof is never fed with invalid proofs.

3. set-switchprog(m,n) replaces switchprog by $s^p_{m:n}$, provided that $s^p_{m:n}$ is indeed a non-empty substring of $s^p$, the storage writable by proof techniques.

4. $\spadesuit$ state2theorem(m, n) translates semantics into syntax. It takes two integer arguments $m, n$ and tries to transform the current contents of $s_{m:n}$ into a theorem of the form
   
   $$(s_{{\bf m}:{\bf n}}({\bf t_1})={\bf z}),  e.g.:  (s_{6:9}(7775555)=\lq 1001\textrm{'}),$$
   
   
   where $t_1$ represents a time measured (by checking time) shortly after state2theorem was invoked, and $z$ the bistring $s_{m:n}(t_1)$ (recall the special case $t_1=1$ of Item 1e). That is, we are willing to accept the time-labeled current observable contents of any part of $s$ as a theorem that does not have to be proven in an alternative way from, say, the initial state $s(1)$, because the computation so far has already demonstrated that the theorem is true. Thus we may exploit information conveyed by environmental inputs, and the fact that sometimes (but not always) the fastest way to determine the output of a program is to run it.

   This non-traditional online interface between syntax and semantics requires special care though. We must avoid inconsistent results through parts of $s$ 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 $c$ cycles in a reserved part of $s$, 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 $s_{m:n}$ to be read might also contain the reading procedure's own, temporary, constantly changing string pointer variables, etc.³To address such problems on computers with limited memory, state2theorem first uses some fixed protocol to check whether the current $s_{m:n}$ is readable at all or whether it might change if it were read by the remaining code of state2theorem. If so, or if $m,n,$ are not in the proper range, then the instruction has no further effect. Otherwise it appends an observed theorem of the form $(s_{{\bf m}:{\bf n}}({\bf t_1})={\bf z})$ to proof. For example, if the current time is 7770000, then the invocation of state2theorem(6,9) might return the theorem $(s_{6:9}(7775555)=\lq 1001\textrm{'})$, where $7775555-7770000=5555$ reflects the time needed by state2theorem to perform the initial check and to read leading bits off the continually increasing $time$ (reading $time$ also costs time) such that it can be sure that $7775555$ is a recent proper time label following the start of state2theorem.

5. $\spadesuit$ check() translates syntax into semantics. It verifies whether the goal of the proof search has been reached. First it tests whether the last theorem (if any) in $proof$ has the form of a target theorem. A target theorem states that given the current axiomatized utility function $u$ (Item 1f), the utility of a switch from $p$ to the current switchprog would be higher than the utility of continuing the execution of $p$ (which would keep searching for alternative switchprogs). Target theorems are bit-encoded symbol strings of the (decoded) form
   
   $$( [ ((switchbit({\bf t_1})=\lq 1\textrm{'}) \rightarrow (u(s({\bf t_1}), Env({\bf t_1}))=Q^1)) \wedge$$
   
   
   
   

   $$((switchbit({\bf t_1})=\lq 0\textrm{'}) \rightarrow (u(s({\bf t_1}), Env({\bf t_1}))=Q^2)) ] \rightarrow (Q^1>Q^2) )$$ (2)

   
   
   where the variable $t_1$ (represented by syntactic place holder ${\bf t_1}$) stands for a time step, while all other symbols belong to the alphabet of the theorem-proving calculus, that is, the set of possible target theorems is parameterized only by $t_1$. ($Q^1,Q^2$ are just logic variables useful for `temporary assignments' as above, to facilitate the formulation of theorems that compare values conditioned on various alternative hypothetical properties of $s(t_1)$.)

   The purpose of introducing $t_1$ 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 $time$ will equal $t_1$. If this subroutine returns a negative result, check() exits. Otherwise it sets switchbit $:=1$ (there is no other way of changing switchbit). Then it repeatedly tests $time$ until $time > t_1$, to make sure the condition of formula (2) was fulfilled at $t_1$. Then it transfers control to switchprog (there is no other way of calling switchprog). The switchprog may subsequently rewrite all parts of $s$, excluding hardware-reserved parts such as $time$ and $x$, but including $p$.

   With the typical example $u$ 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 $s$ at some time $t_1 > time$ in the near future, such as
   

   $$((switchprog({\bf t_1})=\lq 011010\textrm{'}) \wedge (p({\bf t_1})=p(1)) \wedge \ldots),$$ (3)

   
   
   without predicting the value of switchbit$(t_1)$ yet, and a related theorem about effects of alternative values of switchbit$(t_1)$, such as
   

   $$% latex2html id marker 313( [(switchprog({\bf t_1})=\lq 01101... ...wedge \ldots] \rightarrow {\bf (target theorem (\ref{goal}))})$$ (4)

   
   
   Now (2) can be derived from (3) and (4) in the obvious way.

   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 $T$) time needed to execute the subroutine-changing algorithm, no matter what's the precise utility of the switch.

6. delete-theorem(m) deletes the $m$-th theorem in the currently stored proof, thus freeing storage such that proof-storing parts of $s$ can be reused and the maximal proof size is not necessarily limited by storage constraints. Theorems deleted from proof, however, cannot be addressed any more by apply-rule to produce further prolongations of proof.

Back to Goedel machine home page