Appeler par nom vs ordre normal

Question

Je sais que ce sujet a été discuté plusieurs fois, mais il y a quelque chose qui n'est pas clair pour moi. J'ai lu cette question applicative-order/call-by-value and normal-order/call-by-name differences et il y a quelque chose que je voudrais clarifier une fois pour toutes:

appel par nom

Comme ordre normal, mais aucune réduction sont effectuées à l'intérieur des abstractions. Par exemple λx. (Λx.x) x est dans la forme normale selon cette stratégie, bien qu'il contienne le redex (λx.x) x.

En appel par le nom, l'expression λx. (Λx.x) x est dite normale; est-ce parce que "(λx.x) x" est considéré comme le corps (puisque la portée de λ s'étend aussi loin que possible vers la droite)? Et donc de l'autre côté, si j'applique l'ordre normal, quel serait le résultat?

Answer 1

En appel par le nom, l'expression λx. (Λx.x) x est dite normale; est-ce parce que "(λx.x) x" est considéré comme le corps (puisque la portée de λ s'étend aussi loin que possible vers la droite)?

Oui, vous avez raison.

Et ainsi de l'autre côté, si j'applique l'ordre normal, quel serait le résultat?

Vous faites réduction à l'intérieur du corps: (λx.x)x -> x, de sorte que le tout se réduit à la fonction d'identité:

λx.(λx.x)x -> λx.x 

Pour clarifier un peu plus loin, laissez-moi faire une fois de plus, renaming les variables pour se conformer à la Barendregt variable convention: λx.(λx.x)x =α λx.(λy.y)x:

λx.(λy.y)x -> λx.[y := x](y) = λx.x