User:IssaRice/Computability and logic/Rogers fixed point theorem using Sipser's notation

From Machinelearning

Sipser's textbook presents the recursion theorem, but not the fixed point theorem. Here is one way to state the fixed point theorem using Sipser's notation.

Theorem (Fixed point theorem). Let be a Turing machine which computes a function . Then there exists a Turing machine which computes a function , and a Turing machine which computes a function , such that and for all .

Remark. This is basically a "curried" version of the recursion theorem. Instead of , we have (with abuse of notation) . This is the difference between and .

Proof. The proof is pretty similar to the one in Sipser's book. We build in three parts, , where:

  • is
  • is the Turing machine that, on input :
    • computes
    • combines the result with to make a complete Turing machine
    • prints along with the description of this Turing machine and halts, i.e. outputs
  • is an "eval" Turing machine that, on input :
    • changes the tape contents to
    • runs , and stores the result as
    • changes the tape contents to
    • runs

While depends on a description of and , note that neither nor requires a description of (or of each other), so there is no circularity.

Given input , what does do? First runs, and prints after the input. After runs, the tape contains . Next, runs. computes and combines this with . Thus, after finishes, the tape contains . Finally runs. It first runs with input , and stores . Then it runs on , which results in being left on the tape at the end. Since this is the final output of given the input , we have .

Even though the statement of the proof makes it seem like we have to find R and T separately, this is actually not the case. Once we specify R, the description of T is given by .

See also