Complejidad computacional implícita

Jones ^{[ 7 ] [ 12 ]} definió un lenguaje de programación que puede resolver problemas de decisión donde la entrada es una cadena binaria, y demostró que un problema puede resolverse en este lenguaje si y solo si está en P. El lenguaje puede describirse brevemente de la siguiente manera. Recibe la entrada como una lista de bits. Tiene variables que pueden apuntar a la lista y cambiar mediante la aplicación de la operación "tail" para que puedan avanzar en la lista. Puede definir funciones recursivas , pero no tiene funciones de orden superior . Fundamentalmente, no tiene constructores de tipos de datos (de ahí el nombre cons-free ): la lista de entrada es la única estructura de datos en todo el programa. La ausencia de constructores limita el poder expresivo, impidiendo la construcción de estructuras de datos auxiliares cuyo tamaño podría aumentar durante el cálculo. Cabe destacar que esta restricción no reduce la clase de problemas decidibles a un subconjunto propio de P: todo problema en P puede resolverse dentro del lenguaje. Además, los programas en este lenguaje pueden ejecutarse en tiempo exponencial, pero solo resuelven problemas de tiempo polinomial, por lo que la caracterización implícita es independiente del tiempo de ejecución real de cada programa. Jones también ha demostrado que si se añade no determinismo al lenguaje (como en una máquina de Turing no determinista ), la clase de problemas que se pueden aceptar sigue siendo P. ^{[ 12 ]}

Bellantoni y Cook ^{[ 6 ]} demostraron que cierta clase de funciones coincide con la programación funcional (PF). Estas son funciones que se definen, al igual que las funciones recursivas primitivas , mediante un conjunto de funciones base y operadores para construir nuevas funciones a partir de las existentes. Se utiliza un esquema de recursión especial en lugar del esquema de recursión primitivo, como se verá más adelante, y además, las funciones tienen sus argumentos divididos en dos "tipos". Esto se indica separando los argumentos con un punto y coma:${\displaystyle f(x_{1},\dots ,x_{k};x_{k+1},\dots ,x_{k+n})}$Los argumentos que siguen al punto y coma se denominan seguros (un nombre más intuitivo podría ser "protegidos"). Cuando se pasa un valor en una posición segura, no se permite que crezca demasiado; observe la diferencia entre las cláusulas (3) y (4) a continuación. Otra diferencia importante con respecto a la definición de funciones recursivas primitivas es que aquí los argumentos se consideran cadenas binarias y podemos incrementar un valor añadiendo un bit ( x 0 o x 1) en contraste con la función sucesora numérica ( x' ).

Aquí está la lista de funciones básicas:

Podemos combinar funciones para formar otras nuevas utilizando un esquema de composición y un esquema de recursión. Dado${\displaystyle g,{\vec {r}},{\vec {s}}}$, su composición predicativa ,${\displaystyle f=g\circ ({\vec {r}};{\vec {s}})}$se define por$${\displaystyle f({\vec {x}};{\vec {y}})=g({\vec {r}}({\vec {x}};);{\vec {s}}({\vec {x}};{\vec {y}})).}$$ Dado${\displaystyle g,h_{0},h_{1}}$, la recursión predicativa en el esquema de notación define una función${\displaystyle f}$por $${\displaystyle {\begin{aligned}f(\varepsilon ,{\vec {x}};{\vec {y}})&=g({\vec {x}};{\vec {y}}),\\f(zi,{\vec {x}};{\vec {y}})&=h_{i}(z,{\vec {x}};{\vec {y}},f(z,{\vec {x}};{\vec {y}})).\end{aligned}}}$$ Se denomina "recursión en notación" porque en cada llamada recursiva eliminamos un poco del argumento de recursión, a diferencia de la recursión "en valor", que va de z a z -1.

Ejemplo. Definimos una función${\displaystyle r(x)}$que recibe una cadena binaria x y devuelve una cadena de 0 de la misma longitud que x . Para mayor legibilidad, omitimos las invocaciones de las funciones de proyección que son técnicamente necesarias para recuperar el argumento de la función, por ejemplo,${\displaystyle \pi _{1}^{1}(x)}$para obtener x en la función${\displaystyle g(x)}$. $${\displaystyle {\begin{aligned}g(x)&=f(x,x),{\text{where}}\\f(\varepsilon ,x;)&=\varepsilon ,\\f(zi,x;)&=S_{0}(x;f(z,x;)).\end{aligned}}}$$ Nótese cómo necesitamos mantener inicialmente una copia de x para poder aplicar el operador de sucesor binario acotado en la recursión.

Leivant ^{[ 10 ]} desarrolló un enfoque alternativo basado en la estratificación de datos: los números naturales (u otros datos) se clasifican en niveles, y la recursión solo se permite respetando el orden de los niveles. Las funciones definibles mediante recursión limitada por niveles coinciden con funciones computables en tiempo polinomial. El marco de Leivant es sintácticamente más flexible que el álgebra de Bellantoni-Cook y se extiende naturalmente a lenguajes imperativos.

Girard, Scedrov y Scott ^{[ 4 ]} introdujeron la lógica lineal acotada , una variante de la lógica lineal en la que el uso de la regla de contracción está limitado por términos polinomiales. Las demostraciones en este sistema corresponden, a través de la correspondencia de Curry-Howard , a funciones computables en tiempo polinomial. El trabajo posterior sobre lógica lineal ligera de Girard ^{[ 13 ]} y su desarrollo en teoría de tipos por Baillot y Terui ^{[ 14 ]} , y la lógica lineal suave de Lafont ^{[ 15 ]} dieron lugar a sistemas relacionados con una teoría de demostración más limpia , que caracterizan la computación en tiempo polinomial mediante restricciones estructurales en la modalidad exponencial.