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, privacy policy and cookie policy