Teorema de Smn

Sobre la transformación de un programa mediante la sustitución de constantes por variables libres

En la teoría de la computabilidad, la S m
-n El teorema , escrito también como " teorema smn " o " teorema smn " (también llamado lema de traducción , teorema de parámetros y teorema de parametrización ) es un resultado básico sobre los lenguajes de programación (y, más generalmente, las numeraciones de Gödel de las funciones computables ) (Soare 1987, Rogers 1967). Fue demostrado por primera vez por Stephen Cole Kleene (1943). El nombre S m
-n proviene de la aparición de una S con subíndice n y superíndice m en la formulación original del teorema (ver más abajo).

En términos prácticos, el teorema dice que para un lenguaje de programación dado y números enteros positivos m y n , existe un algoritmo particular que acepta como entrada el código fuente de un programa con m + n variables libres , junto con m valores. Este algoritmo genera un código fuente que efectivamente sustituye los valores de las primeras m variables libres, dejando libres el resto de las variables.

El teorema smn establece que dada una función de dos argumentos que es computable , existe una función total y computable tal que básicamente "arregla" el primer argumento de . Es como aplicar parcialmente un argumento a una función. Esto se generaliza sobre tuplas para . En otras palabras, aborda la idea de "parametrización" o "indexación" de funciones computables. Es como crear una versión simplificada de una función que toma un parámetro adicional (índice) para imitar el comportamiento de una función más compleja. ${\displaystyle g(x,y)}$ ${\displaystyle \phi _{s}(x)(y)=g(x,y)}$ ${\displaystyle g}$ ${\displaystyle m,n}$ ${\displaystyle x,y}$

La función está diseñada para imitar el comportamiento de cuando se le dan los parámetros adecuados. Básicamente, al seleccionar los valores correctos para y , puede hacer que se comporte como para un cálculo específico. En lugar de lidiar con la complejidad de , podemos trabajar con una función más simple que capture la esencia del cálculo. ${\displaystyle s_{m}^{n}}$ ${\displaystyle \phi (x,y)}$ ${\displaystyle m}$ ${\displaystyle n}$ ${\displaystyle s}$ ${\displaystyle \phi (x,y)}$ ${\displaystyle s_{m}^{n}}$

Detalles

La forma básica del teorema se aplica a funciones de dos argumentos (Nies 2009, p. 6). Dada una numeración de Gödel de funciones recursivas, existe una función recursiva primitiva s de dos argumentos con la siguiente propiedad: para cada número de Gödel p de una función computable parcial f con dos argumentos, las expresiones y están definidas para las mismas combinaciones de números naturales x e 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 x : ${\displaystyle \varphi }$ ${\displaystyle \varphi _{s(p,x)}(y)}$ ${\displaystyle f(x,y)}$

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

De manera más general, para cualquier m , n > 0 , existe una función recursiva primitiva de m + 1 argumentos que se comporta de la siguiente manera: para cada número de Gödel p de una función computable parcial con m + n argumentos, y todos los valores de x ₁ , …, x _m : ${\displaystyle S_{n}^{m}}$

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

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

Declaración formal

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

${\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 S que permite calcular k a partir de x e y ; se denota . ${\displaystyle k=S_{n}^{m}(x,y_{1},\dots ,y_{m})}$

De manera informal, S encuentra la máquina de Turing que es el resultado de codificar de forma rígida los valores de y en . El resultado se generaliza a cualquier modelo computacional de Turing completo . ${\displaystyle {\text{TM}}_{k}}$ ${\displaystyle {\text{TM}}_{x}}$

Esto también puede extenderse a funciones computables totales de la siguiente manera:

Dada una función computable total y tal que , : ${\displaystyle s_{m,n}:\mathbb {N} ^{m+1}\rightarrow \mathbb {N} }$ ${\displaystyle m,n\geq 1}$ ${\displaystyle \forall {\vec {x}}\in \mathbb {N} ^{m},\forall {\vec {y}}\in \mathbb {N} ^{n}}$ ${\displaystyle \forall e\in \mathbb {N} }$

${\displaystyle \phi _{e}^{m+n}({\vec {x}},{\vec {y}})=\phi _{s_{m,n}{(e,{\vec {x}})}}^{n}({\vec {y}})}$

También existe una versión simplificada del mismo teorema (definido de hecho como " teorema smn simplificado ", que básicamente utiliza una función computable total como índice de la siguiente manera:

Sea una función computable. En este caso, existe una función computable total tal que , : ${\displaystyle f:\mathbb {N} ^{n+m}\rightarrow \mathbb {N} }$ ${\displaystyle s:\mathbb {N} ^{m}\rightarrow \mathbb {N} }$ ${\displaystyle \forall x\in \mathbb {N} ^{m}}$ ${\displaystyle {\vec {y}}\in \mathbb {N} ^{n}}$

${\displaystyle f({\vec {x}},{\vec {y}})=\phi _{S({\vec {x}})}^{(n)}({\vec {y}})}$

Ejemplo

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

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

Por ejemplo, evalúa a .(s11 '(lambda (x y) (+ x y)) 3)(lambda (g42) ((lambda (x y) (+ x y)) 3 g42))

Véase también

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

Referencias

• 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 : 150–155. doi :10.2307/2267778. JSTOR  2267778. S2CID  34314018.(Ésta es la referencia que la edición de 1989 de la "Teoría de la recursión clásica" de Odifreddi da en la pág. 131 para el teorema.) ${\displaystyle S_{n}^{m}}$
• 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 de la recursión clásica . Holanda del Norte. ISBN 0-444-87295-7.
• Rogers, H. (1987) [1967]. La teoría de funciones recursivas y computabilidad efectiva . Primera edición de bolsillo de la editorial MIT. ISBN 0-262-68052-1.
• Soare, R. (1987). Conjuntos y grados enumerables recursivamente . Perspectivas en lógica matemática. Springer-Verlag. ISBN 3-540-15299-7.

Enlaces externos

• Weisstein, Eric W. "Teorema smn de Kleene". MathWorld .