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

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.

StackExchange Computer Science Q#51003, answer score: 3