Lambda Expression Reduction

Question

I am unable to solve the following lambda expression using both normal order (Call-by-name) and applicative order (Call-by-value) reduction. I keep getting different answers for both. This is the lambda expression that has to be reduced using both techniques:

$(\lambda f\ x\ldotp f\ (f\ x))\ (\lambda f\ x\ldotp f\ (f\ x))\ f\ x$

Answer 1

I keep getting different answers for both.

You should get the same result for both orders. Please show your work so that the community can help you find your mistake.

My guess is you have mistakenly substituted $f$ instead of $x$ towards the end, when $f$ is in fact free.

The correct reduction procedure is shown below.

---

$(\lambda f\ x\ldotp f\ (f\ x))\ (\lambda f\ x\ldotp f\ (f\ x))\ f\ x$

There is no difference between normal order and applicative order at the first step.

$(\lambda f\ x\ldotp f\ (f\ x))\ ((\lambda f\ x\ldotp f\ (f\ x))\ f)\ x$

---

At this step there is a difference, because the value being applied to, $((\lambda f\ x\ldotp f\ (f\ x))\ f)$ is not in beta normal form. Let's ignore it and use normal order first.

Normal Order

$((\lambda f\ x\ldotp f\ (f\ x))\ f)\ (((\lambda f\ x\ldotp f\ (f\ x))\ f)\ x)$

$(\lambda x\ldotp\ f\ (f\ x))\ (((\lambda f\ x\ldotp f\ (f\ x))\ f)\ x)$

$f\ (f\ (((\lambda f\ x\ldotp f\ (f\ x))\ f)\ x))$

$f\ (f\ (f\ (f\ x)))$

---

Let's go back to the first step.

$(\lambda f\ x\ldotp f\ (f\ x))\ ((\lambda f\ x\ldotp f\ (f\ x))\ f)\ x$

---

This time let's use applicative order

Applicative Order

$(\lambda f\ x\ldotp f\ (f\ x))\ (\lambda x\ldotp f\ (f\ x))\ x$

$(\lambda x\ldotp f\ (f\ x))\ ((\lambda x\ldotp f\ (f\ x))\ x)$

$(\lambda x\ldotp f\ (f\ x))\ (f\ (f\ x))$

$f\ (f\ (f\ (f\ x)))$

---

With normal order we reduced the expression to:

$f\ (f\ (f\ (f\ x)))$

With applicative order we reduced the expression to:

$f\ (f\ (f\ (f\ x)))$

The results are the same.