CODEWITHSUNDEEP
lambdalambda-calculusreduction
Peter111
Peter111

Reputation: 823

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?

Upvotes: 0

Views: 58

Answers (1)

melpomene
melpomene

Reputation: 85877

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).

Upvotes: 4

Related Questions