Smn theorem


In computability theory the ' theorem, is a basic result about programming languages . It was first proved by Stephen Cole Kleene. The name ' comes from the occurrence of an S with subscript n and superscript m in the original formulation of the theorem.
In practical terms, the theorem says that for a given programming language and positive integers m and n, there exists a particular algorithm that accepts as input the source code of a program with m + n free variables, together with m values. This algorithm generates source code that effectively substitutes the values for the first m free variables, leaving the rest of the variables free.

Details

The basic form of the theorem applies to functions of two arguments. Given a Gödel numbering of recursive functions, there is a primitive recursive function s of two arguments with the following property: for every Gödel number p of a partial computable function f with two arguments, the expressions and are defined for the same combinations of natural numbers x and y, and their values are equal for any such combination. In other words, the following extensional equality of functions holds for every x:
More generally, for any m, n > 0, there exists a primitive recursive function of m + 1 arguments that behaves as follows: for every Gödel number p of a partial computable function with m + n arguments, and all values of x1, …, xm:
The function s described above can be taken to be.

Formal statement

Given arities and, for every Turing Machine of arity and for all possible values of inputs, there exists a Turing machine of arity, such that
Furthermore, there is a Turing machine that allows to be calculated from and ; it is denoted.
Informally, finds the Turing Machine that is the result of hardcoding the values of into. The result generalizes to any Turing-complete computing model.

Example

The following Lisp code implements s11 for Lisp.



)))

For example, evaluates to.