Teorema S m n

En la teoría de la computabilidad, el teorema S m n   , también escrito como " teorema smn " o " teorema smn " (también llamado lema de traslación , teorema del parámetro y teorema de parametrización ), es un resultado fundamental sobre lenguajes de programación (y, más generalmente, numeraciones de Gödel de las funciones computables parciales ) (Soare 1987, Rogers 1967). Fue demostrado por primera vez por Stephen Cole Kleene (1943). El nombre${\displaystyle S_{m}^{n}}$proviene de la ocurrencia de un${\displaystyle S}$con subíndice${\displaystyle n}$y superíndice${\displaystyle m}$en la formulación original del teorema (véase más abajo).

En términos prácticos, el teorema dice que para un lenguaje de programación dado y enteros positivos${\displaystyle m}$y${\displaystyle n}$, existe un algoritmo particular que acepta como entrada el código fuente de un programa con${\displaystyle m+n}$variables libres , junto con${\displaystyle m}$valores. Este algoritmo genera código fuente que, en esencia, sustituye los valores por los primeros.${\displaystyle m}$variables libres, dejando el resto de las variables libres.

La forma básica del teorema se aplica a funciones de dos argumentos (Nies 2009, p.  6). Dado un número de Gödel${\displaystyle \varphi }$de funciones computables parciales, hay una función recursiva primitiva${\displaystyle s}$de dos argumentos con la siguiente propiedad: para cada número de Gödel${\displaystyle e}$de una función computable parcial${\displaystyle f}$con dos argumentos, las expresiones${\displaystyle \varphi _{s(e,x)}(y)}$y${\displaystyle f(x,y)}$se definen para las mismas combinaciones de números naturales${\displaystyle x}$y${\displaystyle y}$y sus valores son iguales para cualquier combinación de este tipo. En otras palabras, la siguiente igualdad extensional de funciones se cumple para cada${\displaystyle x}$:

${\displaystyle \varphi _{s(e,x)}\simeq \lambda y.\varphi _{e}(x,y).}$

En términos más generales, para cualquier${\displaystyle m,n>0}$, existe una función recursiva primitiva${\displaystyle S_{n}^{m}}$de${\displaystyle m+1}$argumentos que se comportan de la siguiente manera: para cada número de Gödel${\displaystyle e}$de una función computable parcial con${\displaystyle m+n}$argumentos y todos los valores de${\displaystyle x_{1},x_{2},...,x_{m}}$:

${\displaystyle \varphi _{S_{n}^{m}(e,x_{1},\dots ,x_{m})}\simeq \lambda y_{1},\dots ,y_{n}.\varphi _{e}(x_{1},\dots ,x_{m},y_{1},\dots ,y_{n}).}$

La función${\displaystyle s}$descrito anteriormente puede tomarse como${\displaystyle S_{1}^{1}}$.

Dadas las aridades${\displaystyle m}$y${\displaystyle n}$, para cada máquina de Turing${\displaystyle {\text{TM}}_{x}}$de aridad${\displaystyle m+n}$y para todos los posibles valores de entrada${\displaystyle y_{1},\dots,y_{m}}$Existe una máquina de Turing${\displaystyle {\text{TM}}_{k}}$de aridad${\displaystyle n}$, de tal manera que

${\displaystyle \forall z_{1},\dots ,z_{n}:{\text{TM}}_{x}(y_{1},\dots ,y_{m},z_{1},\dots ,z_{n})={\text{TM}}_{k}(z_{1},\dots ,z_{n}).}$

Además, existe una máquina de Turing.${\displaystyle S}$que permite${\displaystyle k}$a calcular desde${\displaystyle x}$y${\displaystyle y}$; se denota${\displaystyle k=S_{n}^{m}(x,y_{1},\dots ,y_{m})}$.

De manera informal,${\displaystyle S}$encuentra la máquina de Turing${\displaystyle {\text{TM}}_{k}}$ese es el resultado de codificar los valores de${\displaystyle y}$en${\displaystyle {\text{TM}}_{x}}$El resultado se generaliza a cualquier modelo de computación Turing-completo .

El siguiente código Lisp implementa s ₁₁ para Lisp.

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

Por ejemplo, se evalúa como , donde es un símbolo "nuevo".(s11'(lambda(xy)(+xy))3)(lambda(g42)((lambda(xy)(+xy))3g42))g42

• Zurra
• Teorema de recursión de Kleene
• Evaluación parcial

• Kleene, SC (1936). "Funciones recursivas generales de números naturales" . Mathematische Annalen . 112 (1): 727– 742. doi : 10.1007/BF01565439 . S2CID 120517999 . 
• Kleene, SC (1938). " Sobre notaciones para números ordinales" (PDF) . The Journal of Symbolic Logic . 3 (4): 150– 155. doi : 10.2307/2267778 . JSTOR 2267778. S2CID 34314018 .  (Esta es la referencia que la edición de 1989 de "Classical Recursion Theory" de Odifreddi da en la página  131 para la${\displaystyle S_{n}^{m}}$teorema.)
• Nies, A. (2009). Computabilidad y aleatoriedad . Oxford Logic Guides. Vol.  51. Oxford: Oxford University Press. ISBN 978-0-19-923076-1. Zbl 1169.03034 . 
• Odifreddi, P. (1999). Teoría clásica de la recursión . North-Holland. ISBN 0-444-87295-7.
• Rogers, H. (1987) [1967]. La teoría de las funciones recursivas y la computabilidad efectiva . Primera edición en rústica de MIT Press. ISBN 0-262-68052-1.
• Soare, R. (1987). Conjuntos y grados recursivamente enumerables . Perspectivas en lógica matemática. Springer-Verlag. ISBN 3-540-15299-7.

• Weisstein, Eric W. "Teorema s - m - n de Kleene " . MathWorld .