teorema de smn

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

En la teoría de la computabilidad, la S mn
​ 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). Los nombres mn
​ 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 código fuente que efectivamente sustituye los valores de las primeras m variables libres, dejando libres el resto de variables.

El teorema de 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 apropiados. Básicamente, al seleccionar los valores correctos para y , puede hacer que se comporten como para un cálculo específico. En lugar de lidiar con la complejidad de , podemos trabajar con uno 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 extensil 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 ₁ , … , xm _: ${\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 s descrita anteriormente se puede considerar 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 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 xey ; 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 los valores de y en . El resultado se generaliza a cualquier modelo informático completo de Turing . ${\displaystyle {\text{TM}}_{k}}$ ${\displaystyle {\text{TM}}_{x}}$

Esto también se puede extender al total de funciones computables 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 hay 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. Allí, 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, se evalúa como .(s11 '(lambda (x y) (+ x y)) 3)(lambda (g42) ((lambda (x y) (+ x y)) 3 g42))

Ver también

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

Referencias

• Kleene, Carolina del Sur (1936). "Funciones recursivas generales de los números naturales". Annalen Matemáticas . 112 (1): 727–742. doi :10.1007/BF01565439. S2CID  120517999.
• Kleene, SC (1938). "Sobre notaciones para números ordinales" (PDF) . La revista de lógica simbólica . 3 : 150-155. doi :10.2307/2267778. JSTOR  2267778. S2CID  34314018.(Esta es la referencia que da la edición de 1989 de la "Teoría clásica de la recursión" de Odifreddi en la página 131 para el teorema). ${\displaystyle S_{n}^{m}}$
• Nies, A. (2009). Computabilidad y aleatoriedad . Guías de lógica de Oxford. vol. 51. Oxford: Prensa de la Universidad de Oxford. ISBN 978-0-19-923076-1. Zbl  1169.03034.
• Odifreddi, P. (1999). Teoría clásica de la recursividad . Holanda del Norte. ISBN 0-444-87295-7.
• Rogers, H. (1987) [1967]. La teoría de las funciones recursivas y la computabilidad efectiva . Primera edición de bolsillo de prensa del MIT. 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.

enlaces externos

• Weisstein, Eric W. "Teorema smn de Kleene". MundoMatemático .