-2
$\begingroup$

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$

$\endgroup$
2
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$

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.