I am looking at the following lambda calculus expression: (λx.(λy.(x(λx.xy))))y. Could somebody help me to evaluate it? I am guessing that the first step would be to pass the outermost y into the outer most function λx, but I am unsure where to go from there.


1 Answer 1


First we have to rename the bound $y$ to $z$ to avoid capture: $$(\lambda x.(\lambda z. (x(\lambda x.xz))))y$$ Then we may substitute $y$ for any bound occurence of $x$: $$(\lambda z. (y(\lambda x.xz)))$$

  • $\begingroup$ Thanks. The process would be the same whether we do it in normal or applicative order, right? $\endgroup$ Apr 17, 2013 at 0:25
  • 1
    $\begingroup$ Yes, that shouldn't matter. $\endgroup$
    – Abel
    Apr 17, 2013 at 0:26
  • $\begingroup$ Could you check this one out too? math.stackexchange.com/questions/363890/… $\endgroup$ Apr 17, 2013 at 0:39

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .