Search code examples
lambdalambda-calculusreduction

Why do we stop after reaching this term? Lambda Calculus

I'm calculating the normal form of a lambda Term. I also have the solution so I know that my steps until the "end" were right. The given term is

(\a.\b.(\x.a b x)(\y. b y x) a) (\f. f f)g

and the normalform of that is 

    g g (\y. g y x)(\f. f f)

I also got this but then I continued and I do not understand why this is the final term. I continued with 

g g g (\f. f f) x

and then 

g g g x x

But apparently I went too far, do you know why you are supposed to stop earlier?

Solution

  • It's not a matter of stopping earlier. You're misinterpreting the syntax of lambda calculus.

    By convention, when we write A B C, we mean (A B) C, not A (B C); that is, function application is left associative.

    Therefore

    g g (\y. g y x)(\f. f f)

    parses as

    ((g g) (\y. (g y) x)) (\f. f f)

    In particular, (g g) is applied to (\y. g y x), whereas (\y. g y x) is not applied to (\f. f f).