Theory of Computation

2.6 THE ITERATION THEOREM OF KLEENE

Suppose that i codes a URM program, M, that acts on input variables x and y to compute a function λxy. f(x, y). It is certainly trivial to modify program M to compute λx. f(x, a) instead. In computer programming terms, we replace an instruction such as “read y” by one that says “y ← a”.

In URM terms, since the input variables X11, X111, … are initialized before the computation starts, the way to implement the suggested “decommissioning” of y as an input variable—opting rather to initialize it with the number a explicitly, first thing during the computation—is to do the following, assuming x and y of f are mapped to X11 and X111 of M:

(1) Remove X111 from the input variables list, X11, X111, and

(2) Modify M into M′ by adding the instruction X111 ← a as the very first instruction.

From the original code, i, a new code (depending on i and a) can be easily calculated. This is the intuition of Kleene’s iteration or “S-m-n” theorem below.          

The mathematical details are as follows.

2.6.0.31 Definition. (Code Concatenation)

2.6.0.32 Remark. Clearly, ...