I have been tasked with reducing the following lambda expression:


using call-by-name and call-by-value reduction strategies.


strategy: Left-most, outermost redex first but no reduction under lambda.

Step 1) alpha-equivalence


Step 2) Reduction - using the redex (λpq.pqp)(λab.a)


Step 3) - substitute (λcd.d) for q


Step 4) - substitute (λcd.d) for a


Step 5) - substitute (λab.a) for b

(λcd.d) -> (λab.b)

Which gives the same result if you were to use normal order instead.


strategy: Right-most, innermost redex first but no reduction under lambda

Step 1) alpha-equivalence


Step 2) substitute (λab.a) for c


Step 3) substitute (λpq.pqp) for d



1 Answer 1


You misunderstood call-by-value and are doing it backwards, i.e., you are substituting functions into arguments, instead of the other way around. Call-by-value and call-by-name both use the same rules of reduction, but in different places and in a different order.

In your case the call-by-value and call-by-name do not differ, because the arguments are already reduced.

Here is an example, where the difference matters. Reduce


Note that this is different from your examples bacause of the extra parantheses that I put in.


(λpq.pqp)((λab.a)(λcd.d)) ➝
λq.((λab.a)(λcd.d))q((λab.a)(λcd.d)) ➝
λq.((λab.a)(λcd.d))q((λab.a)(λcd.d)) ➝
λq.(λb.(λcd.d))q((λab.a)(λcd.d)) ➝
λq.(λcd.d)((λab.a)(λcd.d)) ➝


(λpq.pqp)((λab.a)(λcd.d)) ➝
(λpq.pqp)(λb.(λcd.d)) ➝
(λpq.pqp)(λb.(λcd.d)) ➝
λq.(λbcd.d)q(λbcd.d) ➝
λq.(λcd.d)(λbcd.d) ➝

The difference is that in call-by-value you normalize the argument before you substitute it for the bound variable.

  • $\begingroup$ Okay, thank you very much I think I have better understanding. I do have another question as I'm not sure if I understand what they mean by no reduction under lambda so let's say we reduced an expression using call-by-value and it reduced to the following: </br> <pre><code> (λb.(λc.v)b)➝ </pre></code> </br> would that be the final result? $\endgroup$
    – Dennis O
    Commented Dec 18, 2018 at 10:21
  • 1
    $\begingroup$ No reduction under $\lambda$ means that we never reduce inside a $\lambda$-abstraction. For example $\lambda x . ((\lambda y . y) x)$ is considered reduced because the only reduction that we can make is inside a $\lambda$-abstraction. $\endgroup$ Commented Dec 18, 2018 at 14:33

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.