Overview of Hardware and Initial Software / Proof Searcher

The Gödel machine's life consists of discrete cycles or time steps $t=1, 2, \ldots$. Its total lifetime $T$ may or may not be known in advance. In what follows, the value of any time-varying variable $Q$ at time $t$ will be denoted by $Q(t)$; its initial value by $Q(1)$.

During each cycle the Gödel machine hardware (which may be emulated as unchangeable software on a traditional computer) executes an elementary operation which affects its variable state $s \in \cal S \subset B^*$ (without loss of generality we assume $s$ is encoded as a bitstring) and possibly also the variable environmental state $Env \in \cal E$, where the possibly uncountable set $\cal E$ may be unknown or only partially known.

Instead of insisting on a linear relationship between cycles and physical time, we use a hardware-oriented, causal model of time embodied by a hardwired state transition function $F: \cal S \times \cal E \rightarrow \cal S$. For $t > 1$, $s(t)=F(s(t-1), Env(t-1))$ is the state at a point where the hardware operation of cycle $t-1$ is finished, but the one of $t$ has not started yet. $Env(t)$ may depend on $s(t-1)$ and is simultaneously updated or (probabilistically) computed by the possibly reactive environment, whose computational resources may vastly exceed the ones of the Gödel machine.

For example, if the hardware is a Turing machine²(TM) [50], then $s(t)$ is a bitstring that encodes the current contents of all tapes of the TM, the positions of its scanning heads, and the current internal state of the TM's finite state automaton, while $F$ specifies the TM's look-up table which maps any possible combination of internal state and bits above scanning heads to a new internal state and an action such as: replace some head's current bit by 1/0, increment (right shift) or decrement (left shift) some scanning head, read and copy next input bit to cell above input tape's scanning head, etc. Alternatively, if the hardware is given by the abstract model of a modern microprocessor with limited storage, $s(t)$ will encode the current storage contents, register values, instruction pointers etc.

In order to conveniently talk about programs and data, we will often attach names to certain string variables encoded as components or substrings of $s$. Of particular interest are 7 variables called time, x, y, p, proof, switchbit, switchprog, to be explained below. All these variables except for the hardware-written time and x are in principle writable by programs stored within $s$, although at least the initial software or policy $p(1)$ will be set up such that $p$ initially can modify only certain limited parts of $s$, as long as it cannot prove the usefulness of modifying other parts as well.

1. At time $t$, variable $time$ holds a unique binary representation of $t$. We initialize $time(1)=\lq 1\textrm{'}$, the bitstring consisting only of a one. The hardware increments $time$ from one cycle to the next. This requires at most $O(log t)$ and on average only $O(1)$ computational steps.

2. Variable x holds environmental inputs. For $t > 1$, $x(t)$ may differ from $x(t-1)$ only if a program running on the Gödel machine has executed a special input-requesting instruction at time $t-1$. Generally speaking, the delays between successive inputs should be sufficiently large so that programs can perform certain elementary computations on an input, such as copying it into internal storage (a reserved part of $s$) before the next input arrives.

3. $y(t)$ is an output bitstring which may subsequently influence the environment, where $y(1)=\lq 0\textrm{'}$ by default. For example, $y(t)$ could be interpreted as a control signal for an environment-manipulating robot whose actions may have an effect on future inputs.

4. $p(1)$ is the initial software: a program implementing the original policy for interacting with the environment and for proof searching. Certain parts of $s$ may be used by the policy for computing temporary results. Using some sort of process interleaving technique, the initial $p(1)$ is written such that it will allocate a fixed fraction of the time to a subpolicy $e$, which somehow computes outputs $y$ in response to inputs $x$. We may initialize $e$ by any known problem solving algorithm, to exploit from the start whatever initial prior knowledge is available.

   In the remaining time $p$ will execute a proof-searching subroutine that systematically tests proof-generating programs called proof techniques written in a universal programming language $\cal L$ implemented as part of the initial software $p(1)$ running on the Gödel machine's hardware. A special role is played by three global variables (initially) writable only by proof techniques:

   1. switchprog holds a program whose execution may directly modify any part of the Gödel machine except for variables that can be set directly only by the hardware or by the environment, such as $time$ and $x$ (or, in case a TM is used as hardware, the representation of the current internal state of the TM's finite state automaton).

   2. switchbit is a binary variable initialized by `0'. Setting it to `1' starts the unstoppable process of transferring control to the current switchprog.

   3. proof holds a proof incrementally computed by the currently tested proof technique. The proof searcher's goal is to find a proof stating that switchbit should be set, which implies that the current switchprog will be executed. So the decision of whether the Gödel machine should be changed in a particular way (out of many possible ways) will be reduced to the binary decision of whether switchbit should adopt a particular value. The next subsections will describe details; the final Section 4 will summarize everything.

Back to Goedel machine home page