En la teoría de la computabilidad, la S m
n El teorema (también llamado lema de traducción , teorema de parámetro 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 probado 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 que un lenguaje de programación determinado y números enteros positivos m y n , existe un determinado algoritmo 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.
Detalles
La forma básica del teorema se aplica a funciones de dos argumentos (Nies 2009, p. 6). Dada una numeración de Gödelde funciones recursivas, hay 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 se definen para las mismas combinaciones de números naturales x y y , y sus valores son iguales para cualquier tal combinación. En otras palabras, la siguiente igualdad extensional de funciones se cumple para cada x :
Más generalmente, para cualquier m , n > 0, existe una función recursiva primitivade 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 1 ,…, x m :
La función de s se ha descrito anteriormente se pueden tomar para ser.
Declaración formal
Aridades dadas y , 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 , tal que
Además, hay una máquina de Turing Eso permite a ser calculado a partir de y ; se denota.
Informalmente encuentra la máquina de Turing que es el resultado de codificar los valores de dentro . El resultado se generaliza a cualquier modelo informático completo de Turing .
Ejemplo
El siguiente código Lisp implementa s 11 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))
Ver también
Referencias
- Kleene, Carolina del Sur (1936). "Funciones recursivas generales de números naturales" . Mathematische Annalen . 112 (1): 727–742. doi : 10.1007 / BF01565439 .
- Kleene, Carolina del Sur (1938). "Sobre notaciones para números ordinales" (PDF) . El diario de la lógica simbólica . 3 : 150-155. (Esta es la referencia que la edición de 1989 de la "Teoría de la recursividad clásica" de Odifreddi da en la p. 131 para el teorema.)
- Nies, A. (2009). Computabilidad y aleatoriedad . Guías lógicas de Oxford. 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 Septentrional. 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.