1
$\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)

$\endgroup$
3
$\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.

$\endgroup$
  • $\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 '18 at 10:21
  • $\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 '18 at 14:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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