"Applicative order" and "Normal order" in lambda-calculus

Answered By : Karolis Juodelė

$(\lambda x.y \ (\lambda x.(x \ \ x) \ \lambda x.(x \ \ x)))$ is an infinite loop because $$\lambda x.(x \ \ x) \ \lambda x.(x \ \ x) \to \lambda x.(x \ \ x) \ \lambda x.(x \ \ x)$$ Notice that $\lambda x.(x \ \ x)$ just writes it's argument twice.

Problem Detail: 

Applicative order: Always fully evaluate the arguments of a function before evaluating the function itself , like -

$(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow (\lambda x. x^2(2+1))\rightarrow \ (\lambda x. x^2(3)) \rightarrow \ 3^2 \ \rightarrow \ 9$

Normal order: The expression would be reduced from the outside in , like -

$(\lambda x.x^2 (\lambda x.(x+1) \ 2)) \rightarrow \ (\lambda x.(x+1) \ \ \ 2)^ 2 \rightarrow\ (2+1)^2 \ \rightarrow 3^2 \ \rightarrow \ 9 $

Let $M = (\lambda x.y \ (\lambda x.(x \ \ x) \ \lambda x.(x \ \ x)))$

Why is it that under applicative order, $M \rightarrow$ infinite loop,
but under normal order, $M \rightarrow y$?

Asked By : URL87

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/7702