Lambda Calculus - Call-by-name AND call-by-value reduction

Question

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)

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

(λ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.