It seems to me that when the outermost|toplevel function is itself an expression to be evaluated (i.e.: a higher-order function returning the function to be applied at top-level), then normal-order evaluation "gets stuck".

For example $(\lambda x . (\lambda y . (y^x)) 2) (5+1)$ is such that I have to evaluate $\lambda x . (\lambda y . (y^x)) 2$ to $\lambda y . (y^2)$ in order to be able to substitute $(5+1)$ into its body. But then I reduced an expression that is not the outermost, hence it was not normal-order.

Are this and similar expressions not evaluatable in normal-order?

Or can I reduce it to $(\lambda x . ((5+1)^x)) 2$ by substituting into the inner lambda?

Or is the top-level expression simply not considered a redex, because it is not of the form $(\lambda y. e) a$, but of the form $(\lambda x.(\lambda y.e)b) a$, hence the leftmost outermost redex is its left part $\lambda x.(\lambda y.e)b$?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.