Smn theorem

From Wikipedia, the free encyclopedia

The correct title of this article is s_mn theorem. It features superscript or subscript characters that are substituted or omitted because of technical limitations.

In computability theory the s_mn theorem, (also called the translation lemma, parameter theorem, or parameterization theorem) is a basic result about programming languages (and, more generally, Gödel numberings of the computable functions) (Soare 1987, Rogers 1967). It was first proved by Stephen Cole Kleene (Kleene 1943).

In practical terms, the theorem says that for a given programming language and positive integers m and n, there is a particular algorithm that operates on the source code of programs with m+n free variables. This algorithm effectively binds m given values to the first m free variables in the program and leaves the rest free.

1 Details
2 Example
3 See also
4 References

[edit] 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 function f with two arguments, $\varphi_{s(p,x)}(y)$ and $f (x, y)$ are defined for the same combinations of x and y and equal for those combinations. In other words, the following extensional equality of functions holds:

$\varphi_{s(p,x)} = \lambda y.\varphi_p(x,y).\,$

To generalize the theorem, choose a scheme for encoding n numbers as one number, so that the original numbers can be extracted by primitive recursive functions. For example, one might interleave the bits of the numbers. Then for any m,n > 0, there exists a primitive recursive function $s^m_n$ of m+1 arguments that behaves as follows: for every Gödel number p of a function with m+n arguments,

$\varphi_{s^{m}_{n}(p,x_1,\dots,x_m)} = \lambda y_1,\dots,y_n.\varphi_p(x_1,\dots,x_m,y_1,\dots,y_n)\,$

$s^1_1$ is just the function s already described.

[edit] Example

The following Lisp code implements s₁₁ for Lisp.

(defun s11 (f x)
  (list 'lambda '(y) (list f x 'y))

For example, (s11 '(lambda (x y) (+ x y)) 3) evaluates to (lambda (y) ((lambda (x y) (+ x y)) 3 y)).

[edit] See also

[edit] References

Odifreddi, P. (1999). Classical Recursion Theory. North-Holland. ISBN 0-444-87295-7.
Rogers, H. [1967] (1987). The Theory of Recursive Functions and Effective Computability. First MIT press paperback edition. ISBN 0-262-68052-1.
Soare, R. (1987). Recursively enumerable sets and degrees, Perspectives in Mathematical Logic. Springer-Verlag. ISBN 3-540-15299-7.
Kleene, S. C. (1943). "General recursive functions of natural numbers". Mathematische Annalen 53: 727–742.