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^{[citation needed]}.

In practical terms, the theorem says that, given any programming language and integers m, n > 0, there is an algorithm with the following property: given the source code for a function f with m + n arguments and values a₁,...,a_m for the first m as input, the algorithm outputs source code for a function g such that

g(x₁,...,x_n)=f(a₁,...,a_m, x₁,...,x_n).

A corollary of the theorem is that any programming language capable of executing code generated at runtime can be made to support currying.

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 with two arguments, $\varphi_{s(p,x)}(y)$ and $p (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_mn of m+1 arguments that behaves as follows: for every Gödel number p of a function with m+n arguments,

$\varphi_{s_{mn}(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₁₁ 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

Kleene's recursion theorem

[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.