2
$\begingroup$

I have been tasked with reducing the following lambda expression:

(λpq.pqp)(λab.a)(λab.b)

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

Call-by-name

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

Step 1) alpha-equivalence

(λpq.pqp)(λab.a)(λcd.d)

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

(λq.(λab.a)q(λab.a)(λcd.d)

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

(λab.a)(λcd.d)(λab.a)

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

(λb.(λcd.d))(λab.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.

Call-by-value

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

Step 1) alpha-equivalence

(λpq.pqp)(λab.a)(λcd.d)

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

(λpq.pqp)(λd.d)

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

(λpq.pqp)

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

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

(λpq.pqp)((λab.a)(λcd.d))

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

Call-by-name:

(λ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)) ➝
λq.(λd.d)

Call-by-value:

(λ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) ➝
λq.(λd.d)

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

Improve this answer
$\endgroup$
2
  • $\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
    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$
    – Andrej Bauer
    Dec 18, 2018 at 14:33

Your Answer

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

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