Search code examples
lambda-calculuscallbynameevaluation-strategy

Call by name vs normal order


I know this topic has been discussed several times, but there is something still unclear to me. I've read this question applicative-order/call-by-value and normal-order/call-by-name differences and there is something I would to clarify once and for all:

Call-by-name

As normal order, but no reductions are performed inside abstractions. For example λx.(λx.x)x is in normal form according to this strategy, although it contains the redex (λx.x)x.

In call by name, the expression λx.(λx.x)x is said to be in normal form; is this because "(λx.x)x" is considered to be the body (since the scope of λ extends as far as possible to the right)? And so on the other side, if I apply the normal order, what would be the result?


Solution

  • In call by name, the expression λx.(λx.x)x is said to be in normal form; is this because "(λx.x)x" is considered to be the body (since the scope of λ extends as far as possible to the right)?

    Yes, you are right.

    And so on the other side, if I apply the normal order, what would be the result?

    You do reduction inside the body: (λx.x)x -> x, so the whole thing reduces to the identity function:

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

    To clarify it a bit further, let me do this one more time, renaming the variables to conform with the Barendregt variable convention: λx.(λx.x)x =α λx.(λy.y)x:

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