S-m-n theorem
From Wikipedia, the free encyclopedia
- The correct title of this article is smn theorem. It features superscript or subscript characters that are substituted or omitted because of technical limitations.
In computability theory the smn theorem, (also called the translation lemma or parameter theorem) is a basic result about programming languages, abstractly called Gödel numberings, first given by Stephen Cole Kleene.
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 with m+n arguments and values for the first m as input, it outputs the source code for a function that effectively hardcodes the first m arguments to those values.
A corollary of the theorem is that any programming language capable of executing code generated at runtime can be made to support currying.
Contents |
[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, <math>\varphi_{s(p,x)}(y)</math> and <math>p(x,y)</math> 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:
- <math>\varphi_{s(p,x)} = \lambda y.\varphi_p(x,y)</math>
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 smn of m+1 arguments that behaves as follows: for every Gödel number p of a function with m+n arguments,
- <math>\varphi_{s_{mn}(p,x_1,...,x_m)} = \lambda y_1,...,y_n.\varphi_p(x_1,...,x_m,y_1,...,y_n)</math>
s11 is just the function s already described.
[edit] Example
The following Lisp code implements s11 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)).
