Naturaleza de lo incompleto
Se dice que un sistema computacional es completo de Turing si el sistema puede utilizarse para simular una máquina de Turing arbitraria en una cadena de entrada arbitraria. Dado que $\lambda^{\rightarrow}$ es fuertemente normalizador, se garantiza que todo programa bien tipificado se reduce a una forma normal irreducible (es decir, todo programa se detiene). Por lo tanto, no podríamos escribir un $\lambda^{\rightarrow}$ programa para simular una máquina de Turing en una entrada para la cual la máquina nunca se detiene; todo $\lambda^{\rightarrow}$ programas se detienen y tal máquina de Turing en tal entrada, trivialmente, no lo hace.
De manera menos formal, simular máquinas de Turing arbitrarias con entradas arbitrarias significa que se necesita alguna forma de elección condicional (para emular la capacidad de la cabeza de la cinta para moverse a lo largo de la misma), y algún medio para almacenar y manipular un número arbitrario de posiciones de memoria (para emular la cinta). Para $\lambda^{\rightarrow}$ Las reglas de tipificación son suficientes para encapsular la noción de elección, pero no podemos operar sobre cantidades arbitrarias de memoria porque los tipos no pueden recurrir.
Contraejemplos de tipicidad
En cuanto a las cosas que no se pueden expresar con $\lambda^{\rightarrow}$ Un ejemplo clásico sería operadores de punto fijo . Considere por ejemplo Combinador Y que se define como $f.(x. f(xx))(x. f(xx))$ . Obsérvese que dentro de $(xx)$ no podemos asignar un tipo único a las dos apariciones de $x$ .
Un respuesta a una pregunta similar en el sitio de CSTheory sugiere un ejemplo más inteligente: la función que toma un argumento de función computable y devuelve su número de Gödel. También en este caso, la autorreferencia desempeña un papel central y utilizando un argumento diagonal se puede demostrar que no puede existir un término de tipo simple para dicha función.
