«Ordre applicable» et «Ordre normal» dans le lambda-calcul

Ordre d'application: Évaluez toujours complètement les arguments d'une fonction avant d'évaluer la fonction elle-même, comme -

$(\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$

Ordre normal: l'expression serait réduite de l'extérieur vers, comme -

$(\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$

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

Pourquoi est-ce que dans l'ordre d'application, boucle infinie, mais dans l'ordre normal, M → y ?$M \rightarrow$
$M \rightarrow y$

est une boucle infinie car λ x . ( x x ) λ x . ( x x ) → λ x . ( x x ) λ x . ( x x ) Notez 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$

$\Omega$$M$$M \Omega \to M \Omega$

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

Ce cas illustre un phénomène plus général: la réduction d'ordre applicatif ne trouve une forme normale que si le terme est fortement normalisant, tandis que la réduction d'ordre normal trouve toujours la forme normale s'il y en a une. Cela se produit parce que l'ordre applicatif évalue toujours entièrement les arguments en premier, et manque ainsi l'opportunité pour un argument de se révéler inutilisé; tandis que l'ordre normal évalue les arguments le plus tard possible et gagne donc toujours si l'argument s'avère inutilisé.

(Le revers est que l'ordre d'application a tendance à être plus rapide dans la pratique, car il est relativement rare qu'un argument ne soit pas utilisé; alors qu'il est courant qu'un argument soit utilisé plusieurs fois, et dans l'ordre d'application, l'argument n'est évalué qu'une seule fois. Normal order évalue l'argument aussi souvent qu'il est utilisé, que ce soit 0, 1 ou plusieurs fois.)