recursion theorem (idea)

In Computation Theory, the Recursion Theorem allows a turing machine T to obtain its own description <T>. So given T, we would like to construct R such that R(w) = T(<R>, w). We need some intermediate functions to do this construction. I will use a lambda calculus notation:

P = \w. \x. w
Q = \w. P w
B = \m. m (Q m)

Then,

R = \w. T (B (P T(B) w), w)
R w = T (B (P T(B) w), w)
    = T (B (T (B)), w)
    = T (T (B (Q T(B))), w)
    = T (\w. T (B (P T(B) w)), w)
    = T (R, w)

For example, if we wanted a function to recursively compute 2^n, we'd let

E = \f. \x. (if x = 0 then 1 else 2 * f(x-1))
R = \w. E (B (P E(B) w), w)

perhaps using a polymorphic representation of if-then-else statements. So anyway, to do the computation, we'd do

R 2 = E(R, 2)
    = if 2 = 0 then 1 else 2 * R(2-1)
    = 2 * R(1)
    = 2 * E(R, 1)
    = 2 * (if 1 = 0 then 1 else 2 * R(1-1))
    = 2 * 2 * R(0)
    = 2 * 2 * E(R, 0)
    = 2 * 2 * (if 0 = 0 then 1 else 2 * R(0-1))
    = 2 * 2 * 1
    = 4