¿Por qué la estrategia de evaluación de llamada por valor no se Turing completa?

Question

Estoy leyendo un artículo sobre diferentes href="http://en.wikipedia.org/wiki/Evaluation_strategy" (I vinculadas artículo en la wiki, pero yo estoy leyendo otra no en Inglés). Y dice que a diferencia de las estrategias y call-by-name call-by-need, la estrategia call-by-value es no Turing completa .

¿Alguien puede explicar, por favor, ¿por qué es así? Si es posible, añada un ejemplo pls.

Answer 1

disputo la reclamación en el artículo que está leyendo. (No me pagan por esto, así que voy a dar un argumento sugerente, no una prueba.)

Es bien sabido que, al menos en la reducción de orden normal (también conocido como llamar por su nombre), el cálculo lambda puro es Turing completo. Pero si nos fijamos en el papel seminal de John Reynolds de definición Intérpretes de orden superior Lenguajes de Programación , podemos ver que Reynolds analiza en profundidad la diferencia entre la llamada por su nombre y llamada por valor. Una parte crítica del argumento es que con el fin de hacer una distinción apropiada, podemos transformar un programa en de continuación pasando estilo . Los CPS transforman es diferente para la llamada por la necesidad y la llamada por valor, pero los términos transformadas resultantes se pueden evaluar en cualquier estilo.

Así que aquí viene el argumento: escribir un programa de cálculo lambda que simula una máquina de Turing, entonces CPS transformarla usando la transformada de CBN, y se puede evaluar el código resultante utilizando una estrategia de reducción de VSC. ¡Explosión! Turing completo.

En la práctica, seguro que puede escribir un programa CBV para emular una máquina de Turing; es probable que sea suficiente para recoger un combinador de punto fijo adecuado, como por ejemplo T. (El más famoso combinator Y funciona sólo bajo una estrategia de reducción de llamada por nombre, es decir, la reducción normal de orden.)

Renuncia: No he estudiado cálculo lambda en mucho tiempo, y estoy seguro de que hay varios detalles equivocadas en el argumento anterior. Pero estoy seguro de la sustancia. No sería la primera vez que vi algo descaradamente mal en los recursos en línea acerca de la teoría del lenguaje de programación.

Answer 2

Su pregunta no tiene mucho sentido sin referencia a un lenguaje específico, pero voy a tratar mi mejor esfuerzo para responder con respecto al cálculo lambda sin tipo.

La existencia de un punto fijo valor de llamada por combinador (es decir, "combinator Y") para el cálculo lambda sin tipo parece refutar la afirmación básica (ver: Punto fijo Combinator ). La existencia de tales rompe un combinador de normalización fuerte, lo que sugiere que hay por lo menos una lengua que se Turing completo que utiliza una estrategia de evaluación de llamada por valor.

Mucho más probabilidades de afectar a la integridad de Turing de una lengua es la existencia (o falta de) un sistema de tipos. Por ejemplo, el cálculo lambda mecanografiado simplemente-no puede codificar un combinador de punto fijo, y está fuertemente normalizar (es decir, todos los términos así mecanografiadas-reducen a un valor), sin embargo, esto es cierto independientemente de la estrategia de evaluación empleado. Más bien, es una consecuencia del sistema tipo.