Search code examples
lambda-calculus

Beta reduction in lambda calculus: Order of evaluation important?

Given the following lambda expression, where \ resembles lambda:

(\kf.f(\c.co)km)(\x.dox)(\le.le)

Is it wrong if I convert (\c.co)k into ko? I did that and apparently, it was wrong. The right way to go would have been to evaluate the outer function first, meaning (\f.f(\c.co)(\x.dox)m)(\le.le) would have been the desired solution.

Is that true, because I can't find any rule that could indicate that in our lecture notes? If yes, why can't I evaluate inner functions first? I've done it like this and my solution was correct, nonetheless.

Regards.

Solution

  • I asked my TA, he said that application is left associative, meaning

    (\kf.f(\c.co)km)(\x.dox)(\le.le)

    is equivalent to

    ( [\kf.( [ f(\c.co) ]k )m ][\x.dox] )[ \le.le ]

    That explains why k can't be applied to (\c.co).:/

    Brackets/parentheses are used only to make it more readable.

    Regards.