# Lambda Calculus Reduction

I am a little confused to reduce these lambda calculus expressions. I am instructed to give applicative and normal order reductions for these expressions.

$(a):$ $$(\lambda x. (\,(\lambda y.(* 2 y)\,) (+ x y)\,)\,)\,y$$

$(b):$ $$(\lambda x. \lambda y. (x y)\,) \,(λz. (z y)\,)\,$$

Here are the steps I took in my first attempt at $(a)$:

$$(\lambda x. (* 2 (+ x y)))y$$ $$(\lambda x. (* 2 (+ x z)))y \thinspace$$

(substituting $y$ with $z$) $$(* 2 (+ y z))$$

I'm unsure if I even reduced that correctly and how I would reduce in applicative order. Any help is appreciated, thanks!

• Where did z come from? Only bound variables ever need to be renamed (to avoid capturing free variables in terms that are being substituted in). You nearly had it - the correct answer is just (* 2 (+ y y)). – YellPika Jan 29 '15 at 5:05

1. Applicative order: $(λx.((λy.(∗2y))(+xy)))y$, the leftmost innermost redex is $(λy.(∗2y))(+xy)$. It is reduced first. Then we get $(λx.(∗2(+xy)))y$. Here $y$ is a free variable, renaming is not needed. Then the result is $(∗2(+yy))$.
Normal order: $(λx.((λy.(∗2y))(+xy)))y \rightarrow ((λy.(∗2y))(+yy)) \rightarrow *2(+yy)$.
2. Applicative order: \begin{align*}(λx.λy.(xy))(λz.(zy)) &\rightarrow_\alpha (λx.λw.(xw))(λz.(zy))\\ &\rightarrow_{\phantom{\alpha}} λw.((λz.(zy))w) \\ &\rightarrow_{\phantom{\alpha}} λw.wy\end{align*} The first $y$ is bound, the second $y$ is free. When $x$ is substituted by $(λz.(zy))$, name capture occurs, so the bound y is renamed by $w$.