Search code examples
lambda-calculus

Reduce this lambda Expression

(λy.λy.yy)(yy) Guys, I am unable to solve this expression. I would appreciate it if someone helps me solve this lambda expression with stepwise reduction

Solution 
  • (λy.λy.yy)(yy)

    The first lambda never "gets to use" its variable because it's named the same as the inner lambda. Nevertheless, if this isn't a transcription error, the reduction is straightforward.

    Before you reduce an expression where there could be a name conflict, rename the bound variables. The expression becomes:

    (λx.λz.zz)(yy)

    Next, substitute. Since variable x from the first lambda doesn't have any bound instance to replace, anything you apply to it gets discarded.

    λz.zz

    Since this expression cannot be reduced more, this is the normal form.