Lambda Calculus Expression Evaluation

Question

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.

score 1 · Accepted Answer · answered Apr 17 '13 at 00:06

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

answered Apr 17 '13 at 00:06

Abel

7,312

Thanks. The process would be the same whether we do it in normal or applicative order, right? – John Roberts Apr 17 '13 at 00:25
1

Yes, that shouldn't matter. – Abel Apr 17 '13 at 00:26
Could you check this one out too? http://math.stackexchange.com/questions/363890/identifying-all-redexes-in-lambda-expression – John Roberts Apr 17 '13 at 00:39

Lambda Calculus Expression Evaluation

1 Answers1