Lambda Calculus Reduction

Question

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!

Answer 1

Applicative order: The leftmost, innermost redex is always reduced first.

Normal order: The leftmost, outermost redex is always reduced first.

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

   Normal order reduction is same as the applicative order.