"Orden de aplicación" y "Orden normal" en cálculo lambda

Orden de aplicación: siempre evalúe completamente los argumentos de una función antes de evaluar la función en sí, como -

$(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow (\lambda x. x^2(2+1))\rightarrow \ (\lambda x. x^2(3)) \rightarrow \ 3^2 \ \rightarrow \ 9$

Orden normal: la expresión se reduciría desde afuera hacia adentro, como -

$(\lambda x.x^2 (\lambda x.(x+1) \ 2)) \rightarrow \ (\lambda x.(x+1) \ \ \ 2)^ 2 \rightarrow\ (2+1)^2 \ \rightarrow 3^2 \ \rightarrow \ 9$

Sea $M = (\lambda x.y \ (\lambda x.(x \ \ x) \ \lambda x.(x \ \ x)))$

¿Por qué es que en orden aplicativo, bucle infinito, pero en orden normal, M → y ?$M \rightarrow$
$M \rightarrow y$

es un bucle infinito porque λ x . ( x x ) λ x . ( x x ) → λ x . ( x x ) λ x . ( x x ) Observe que λ x . ( $(\lambda x.y \ (\lambda x.(x \ \ x) \ \lambda x.(x \ \ x)))$

$(K_y \Omega)$$K_y$$\lambda x. y$$y$$\Omega = (\lambda x. (x \, x) \: \lambda x. (x \, x))$$\Omega$$\Omega \to \Omega$

La reducción de orden aplicable debe reducir el argumento de la función a una forma normal, antes de que pueda evaluar la redex de nivel superior. Desde el argumento$\Omega$$M$$M \Omega \to M \Omega$

$K_y$$K_y$$(K_y \Omega) \to y$$K_y N \to y$$N$

Este caso ilustra un fenómeno más general: la reducción de orden aplicativo solo encuentra una forma normal si el término se normaliza fuertemente, mientras que la reducción de orden normal siempre encuentra la forma normal si la hay. Esto sucede porque el orden aplicativo siempre evalúa completamente los argumentos primero y, por lo tanto, pierde la oportunidad de que un argumento no se utilice; mientras que el orden normal evalúa los argumentos lo más tarde posible, por lo que siempre gana si el argumento no se utiliza.

(La otra cara es que el orden aplicativo tiende a ser más rápido en la práctica, porque es relativamente raro que un argumento no se use; mientras que es común que un argumento se use varias veces, y bajo orden aplicativo el argumento solo se evalúa una vez. Normal El orden evalúa el argumento con la frecuencia que se usa, ya sea 0, 1 o muchas veces).