Is an expression in normal form if terminates on normal order but not applicative?

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

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

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.