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
$\begingroup$
$\endgroup$
3
-
$\begingroup$ No, it's not in normal form, since it can be reduced under both evaluation strategies. $\endgroup$– Anton TrunovCommented Dec 21, 2015 at 15:11
-
$\begingroup$ Thanks for confirming Anton. You did mean to say "since it can't be reduced" right? $\endgroup$– cpd1Commented Dec 21, 2015 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$– Anton TrunovCommented Dec 21, 2015 at 15:15
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
