3
$\begingroup$

Just wondering if something like this...

(λx. y)((λx. (x x))(λx. (x x))) 

Would be considered to be in normal form since it terminates with y if done by normal order but does not terminate if done by applicative order

$\endgroup$
3
  • $\begingroup$ No, it's not in normal form, since it can be reduced under both evaluation strategies. $\endgroup$ Dec 21 '15 at 15:11
  • $\begingroup$ Thanks for confirming Anton. You did mean to say "since it can't be reduced" right? $\endgroup$
    – cpd1
    Dec 21 '15 at 15:13
  • $\begingroup$ It can be reduced, since it's an application. You can find more details here cs.stackexchange.com/a/7704/39226 $\endgroup$ Dec 21 '15 at 15:15
3
$\begingroup$

The expression $(\lambda x.y \ (\lambda x.(x \ \ x) \ \lambda x.(x \ \ x)))$ is not in normal form because it can be further reduced using the β-rule.

Also, as you noted, Applicative Order is not a normalising reduction strategy. For the expression $(\lambda x.y \ (\lambda x.(x \ \ x) \ \lambda x.(x \ \ x)))$ it fails to find the normal form. This is because $(\lambda x.(x \ \ x) \ \lambda x.(x \ \ x))$ is a non-terminating argument, it has no normal form, then it will loop forever.

On the other side, Normal Order is a normalising reduction strategy because it will always find the normal form, if it exists of course. In fact this a practical consequence of the second Church-Rosser theorem. For the expression $(\lambda x.y \ (\lambda x.(x \ \ x) \ \lambda x.(x \ \ x)))$ it finds the normal form. In this case, since $\lambda x. y$ is a constant function, it will ignore its (non-terminating) argument.

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