Teoría de la realizabilidad: diferencia de poder entre el cálculo Lambda y las máquinas de Turing

48

Tengo tres preguntas secundarias relacionadas, que se destacan con viñetas a continuación (no, no se pueden dividir, si se lo pregunta). Andrej Bauer escribió, aquí , que algunas funciones son realizables a través de una máquina de Turing, pero no a través del cálculo lambda. Un paso clave de su razonamiento es:

Sin embargo, si usamos el cálculo lambda, entonces [el programa] c debe calcular un número que representa una máquina de Turing a partir de un término lambda que representa una función f. Esto no se puede hacer (puedo explicar por qué, si lo hace como una pregunta por separado).

  • Me gustaría ver una explicación / prueba informal.

No veo cómo aplicar el teorema de Rice aquí; se aplicaría al problema "¿son esta máquina de Turing T y este término lambda L equivalente?", porque la aplicación de este predicado a términos equivalentes da el mismo resultado. Sin embargo, la función requerida podría calcular TM diferentes pero equivalentes para términos lambda diferentes pero equivalentes.

  • Además, si el problema es con la introspección de un término lambda, creo que pasar una codificación Gödel de un término lambda también sería aceptable, ¿no?

Por un lado, dado que su ejemplo implica calcular, en el cálculo lambda, el número de pasos que necesita una máquina de Turing para completar una tarea determinada, no estoy muy sorprendido.

  • Pero como aquí el cálculo lambda no puede resolver un problema relacionado con la máquina de Turing, me pregunto si se puede definir un problema similar para el cálculo lambda y demostrar que no se puede resolver para las máquinas de Turing, o si existe una diferencia de poder a favor de Máquinas de Turing (lo que me sorprendería).
Blaisorblade
fuente

Respuestas:

56

John Longley tiene un artículo de encuesta muy extenso que discute los temas involucrados, "Nociones de computabilidad en tipos superiores" .

La idea básica es que la tesis de Church-Turing solo se trata de funciones de , ¡y hay más en la computación que eso! En particular, cuando escribimos programas, hacemos uso de funciones de tipo superior (como ( NN ) N ).NN(NN)N

Para definir completamente un modelo de cómputo de tipo superior, necesitamos especificar la convención de llamada para las funciones, para permitir que una función llame a otra función que recibe como argumento. En el cálculo lambda, la convención de llamada estándar es que representamos funciones mediante términos lambda, y lo único que puede hacer con un lambda en el cálculo lambda es aplicarlo. En codificaciones típicas con máquinas de Turing, pasamos funciones como argumentos arreglando una codificación particular de Godel, y luego cadenas que representan el índice de la máquina que desea pasar como argumento.

La diferencia en la codificación significa que puede analizar la sintaxis del argumento con una codificación de estilo TM, y no puede hacerlo con una representación estándar de cálculo lambda. Por lo tanto, si recibe un término lambda para una función de tipo , solo puede probar su comportamiento pasándole n particulares ; no puede analizar la estructura del término de ninguna manera. Esto no es suficiente información para descubrir el código del término lambda.NNn

Una cosa que vale la pena señalar es que con los tipos superiores, si un lenguaje es menos expresivo en un orden, es más expresivo un orden hacia arriba, porque las funciones son contravariantes. De manera similar, hay funciones que puede escribir en LC que no puede con una codificación de estilo TM (porque se basan en el hecho de que puede pasar argumentos funcionales y saber que el receptor no puede mirar dentro de la función que le asigna) .

EDITAR: Aquí hay un ejemplo de una función definible en PCF, pero no en las codificaciones TM + Goedel. Declararé la isAlwaysTruefunción

 isAlwaysTrue : ((unit → bool) → bool) → bool

que debe devolver verdadero si su argumento ignora su argumento y siempre devuelve verdadero, debe devolver falso si su argumento devuelve falso en cualquier entrada y entra en un ciclo si su argumento entra en un ciclo en cualquier entrada. Podemos definir esta función con bastante facilidad, de la siguiente manera:

isAlwaysTrue p = p (λ(). true) ∧ p (λ(). false) ∧ p (λ(). ⊥)

donde es el cálculo de bucle y es el operador y en booleanos. Esto funciona porque solo hay tres habitantes unit → boolen PCF, por lo que podemos enumerarlos exhaustivamente. Sin embargo, en un modelo de estilo de codificación TM + Goedel, ppodría probar cuánto tiempo tarda su argumento en devolver una respuesta y devolver diferentes respuestas en función de eso. Por lo tanto, la implementación de isAlwaysTruecon TM no cumpliría con las especificaciones.

Neel Krishnaswami
fuente
1
Esta es una excelente encuesta. Gracias por el enlace !
Suresh Venkat
Me di cuenta de que había olvidado aceptar una respuesta, aunque tenía la intención de aceptar la suya. ¡Lo siento!
Blaisorblade
"La diferencia en la codificación significa que puede analizar la sintaxis del argumento con una codificación de estilo TM, y no puede hacerlo con una representación estándar de cálculo lambda". ¿Pero si tiene representaciones para la composición de funciones? Además, lo que dices parece sugerir que HOL es más que una teoría de un cálculo lambda tipificado, ¿es más que eso?
Hibou57
Además, ¿qué pasa con esto: cs.virginia.edu/~evans/cs150/classes/class39/lecture39.pdf . ¿Esto está mal de alguna manera?
Hibou57
Estimado Neel, ¿tiene un ejemplo para una función que se pueda realizar en el modelo de cálculo lambda pero no en el modelo de Turing?
Ingo Blechschmidt
29

Lo que dijo Neel, y también lo siguiente.

NNλλλ

λNN


λNNλ

NNλappn¯f:NNf(k)appn¯k¯n¯nappλ

Xf:X×NNλtf~:X(NN)λsXNNλff~NNλλNNλ

XNNλXX

Andrej Bauer
fuente
2
Todavía estoy esperando ese mejor ejemplo ...
Jacques Carette
1
λ
No entiendo cómo el curry puede volverse incuestionable. Debería poder reutilizar el teorema smn, ya que su prueba construye una función en datos de primer orden (naturales). Según la tesis de Church-Turing, este comportamiento en los naturales puede implementarse como un término lambda (que utiliza funciones nativas internamente, pero no veo cómo eso está prohibido). De manera similar, se puede probar el teorema de utm, por lo que, según su publicación , deberíamos haber terminado. ¿Qué me estoy perdiendo?
Blaisorblade
1
En la respuesta, expliqué lo que significa que el curry se vuelve incontestable, a saber, que el objeto sugerido no es exponencial en la categoría de conjuntos representados.
Andrej Bauer
¡Gracias por la explicación! Lamentablemente no puedo votar de nuevo. Puedo seguir la mayoría de los detalles técnicos; No estoy familiarizado con los modelos topológicos, pero de todos modos estoy familiarizado con "no se pueden inspeccionar funciones en programación funcional / cálculo λ". Su último párrafo también explica por qué no puedo pasar por smn, porque el currículum dado por smn produce nuevamente códigos Gödel, no funciones estándar como usted requiere. Meditaré sobre ese párrafo.
Blaisorblade