The -theorem is a central result of the computability theory . It represents a tool in computer science with which the code of a program can be calculated depending on parameters, and was first proven by Stephen C. Kleene (see recursion theorem ). A result of this is that a programming language that can execute code generated at runtime can support currying .
${\ displaystyle s_ {n} ^ {m}}$

Assuming that the corresponding function is of the type for a fixed index , there is a total and computable function with
${\ displaystyle i}$${\ displaystyle \ varphi _ {i} \ colon \ mathbb {N} ^ {m + n} \ to \ mathbb {N}}$${\ displaystyle s_ {n} ^ {m} \ colon \ mathbb {N} ^ {m + 1} \ to \ mathbb {N}}$

The property says that there is a code that is executed (or can be executed) with the parameters and , a transformation program that outputs , and a program that calculates the same on input as it does on input from and .
${\ displaystyle s_ {n} ^ {m}}$${\ displaystyle w}$${\ displaystyle x}$${\ displaystyle v}$${\ displaystyle U}$${\ displaystyle w}$${\ displaystyle x}$${\ displaystyle v}$${\ displaystyle w_ {x}}$${\ displaystyle v}$${\ displaystyle w}$${\ displaystyle x}$${\ displaystyle v}$

Examples

The -theorem is a possibility to construct new functions from functions whose predictability is already known.
${\ displaystyle s_ {n} ^ {m}}$

For example, let to show that a total and computable function exists, so for the following applies: .
${\ displaystyle g \ colon \ mathbb {N} ^ {2} \ to \ mathbb {N}}$${\ displaystyle i, j, x \ in \ mathbb {N}}$${\ displaystyle \ varphi _ {g (i, j)} (x) = \ varphi _ {i} (x) + \ varphi _ {j} (x)}$

To do this, define . The function can be calculated, so there is an index , such that: . From the -Theorem the existence of a total computable function now follows with for all . Now we define , is then obviously also totally calculable and the following applies:
${\ displaystyle \ psi (i, j, x) = \ varphi _ {i} (x) + \ varphi _ {j} (x)}$${\ displaystyle \ psi}$${\ displaystyle k \ in \ mathbb {N}}$${\ displaystyle \ psi = \ varphi _ {k}}$${\ displaystyle s_ {n} ^ {m}}$${\ displaystyle s_ {1} ^ {2} \ colon \ mathbb {N} ^ {3} \ to \ mathbb {N}}$${\ displaystyle \ varphi _ {s_ {1} ^ {2} (k, i, j)} (x) = \ varphi _ {k} (i, j, x) = \ psi (i, j, x) }$${\ displaystyle i, j, x \ in \ mathbb {N}}$${\ displaystyle g (i, j): = s_ {1} ^ {2} (k, i, j)}$${\ displaystyle g}$

In particular, the theorem is often used to construct reduction functions :
${\ displaystyle s_ {n} ^ {m}}$

As an example, the general holding problem should be reduced to the epsilon holding problem . More precisely, so the existence of a total computable function to show, so for all true .
${\ displaystyle H = \ {(i, x) \ in \ mathbb {N} ^ {2} \ mid \ varphi _ {i} (x) {\ downarrow} \}}$${\ displaystyle H_ {0} = \ {e \ in \ mathbb {N} \ mid \ varphi _ {e} (0) {\ downarrow} \}}$${\ displaystyle f \ colon \ mathbb {N} ^ {2} \ to \ mathbb {N}}$${\ displaystyle i, x \ in \ mathbb {N}}$${\ displaystyle \ varphi _ {i} (x) {\ downarrow} \ Leftrightarrow \ varphi _ {f (i, x)} (0) {\ downarrow}}$

Analogous to the above one defines that the function is obviously calculable and its value does not depend on . So let it be an index so that . The -theorem now yields the existence of a totally computable function , so that . If you sit down and choose , it results
${\ displaystyle \ psi (i, x, y) = \ varphi _ {i} (x)}$${\ displaystyle \ psi}$${\ displaystyle y}$${\ displaystyle k}$${\ displaystyle \ psi = \ varphi _ {k}}$${\ displaystyle s_ {n} ^ {m}}$${\ displaystyle s_ {1} ^ {2}}$${\ displaystyle \ varphi _ {s_ {1} ^ {2} (k, i, x)} (y) = \ varphi _ {k} (i, x, y)}$${\ displaystyle f (i, x) = s_ {1} ^ {2} (k, i, x)}$${\ displaystyle y = 0}$