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!

  • 2
    $\begingroup$ 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)). $\endgroup$
    – YellPika
    Jan 29, 2015 at 5:05

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.