Smn theorem

Smn theorem

In computability theory the smn 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.

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.

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

ee also

*Currying
*Kleene's recursion theorem
*Partial evaluation

References

*
*
*
*

*mathworld|urlname=Kleeness-m-nTheorem|title=Kleene's s-m-n Theorem


Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать курсовую

Look at other dictionaries:

  • Smn-Theorem — Das Theorem ist ein zentrales Resultat der Berechenbarkeitstheorie. Es stellt ein Hilfsmittel dar, mit dem man den Code eines Programms in Abhängigkeit von Parametern berechnen kann. Ein Resultat daraus ist, dass eine Programmiersprache, die zur… …   Deutsch Wikipedia

  • SMN — ist eine Abkürzung für: Stoomvaart Maatschappij „Nederland“, niederländische Reederei Lemhi County Airport, IATA Code des Flughafens von Lemhi County, Idaho, Vereinigte Staaten Servicio Meteorológico Nacional (Argentinien), nationaler… …   Deutsch Wikipedia

  • SMN — may refer to:*Lemhi County Airport, IATA airport code of SMN *Netherland Line or Semper Mare Navigandum *Seri Maharaja Mangku Negara, a Malaysian honour *S m n theorem, a computability theory regarding programming languages *Servicio… …   Wikipedia

  • SMN — puede referirse a: Aeropuerto de Lemhi: código IATA de aeropuerto SMN. Línea Nederlandesa o Semper Mare Navigandum. Galardón honorífico malayo. Teorema de iteración: un teorema de computabilidad teniendo en cuenta lenguajes de programación.… …   Wikipedia Español

  • Utm theorem — In computability theory the utm theorem or universal turing machine theorem is a basic result about Gödel numberings of the set of computable functions. It proves the existence of a computable universal function which is capable of calculating… …   Wikipedia

  • Rogers' equivalence theorem — In computability theory Rogers equivalence theorem characterizes the Gödel numberings, or effective numberings of the set of computable functions. The theorem is named after Hartley Rogers, Jr.Equivalence theoremA numbering of the set of… …   Wikipedia

  • S-m-n-Theorem — Das Theorem ist ein zentrales Resultat der Berechenbarkeitstheorie. Es stellt ein Hilfsmittel dar, mit dem man den Code eines Programms in Abhängigkeit von Parametern berechnen kann. Ein Resultat daraus ist, dass eine Programmiersprache, die zur… …   Deutsch Wikipedia

  • List of mathematics articles (S) — NOTOC S S duality S matrix S plane S transform S unit S.O.S. Mathematics SA subgroup Saccheri quadrilateral Sacks spiral Sacred geometry Saddle node bifurcation Saddle point Saddle surface Sadleirian Professor of Pure Mathematics Safe prime Safe… …   Wikipedia

  • Turing completeness — For the usage of this term in the theory of relative computability by oracle machines, see Turing reduction. In computability theory, a system of data manipulation rules (such as an instruction set, a programming language, or a cellular… …   Wikipedia

  • Kleene's T predicate — In computability theory, the T predicate, first studied by mathematician Stephen Cole Kleene, is a particular set of triples of natural numbers that is used to represent computable functions within formal theories of arithmetic. Informally, the T …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”