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

Question

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$?

• Karolis Juodelė: Have you tried evaluating them at all? Is it the first or the second case that's unclear?
• URL87: @KarolisJuodelė: 1st
• mattgately: Shouldn't the lambda expressions be written with parentheses to mark the end of the first lambda expression and the beginning of the argument, e.g.: Let M = (λx.y) ((λx.(x x)) λx.(x x))

Answer 1

$(\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.

Answer 2

The term you are reducing is $(K_y \Omega)$ where $K_y$ is the constant function $\lambda x. y$ (it always returns $y,ドル ignoring its argument) and $\Omega = (\lambda x. (x ,円 x) \: \lambda x. (x ,円 x))$ is a non-terminating term. In some sense $\Omega$ is the ultimate non-terminating term: it beta-reduces to itself, i.e. $\Omega \to \Omega$. (Make sure to work it out on paper at least once in your life.)

Applicative order reduction must reduce the argument of the function to a normal form, before it can evaluate the top-level redex. Since the argument $\Omega$ has no normal form, applicative order reduction loops infinitely. More generally, for any term $M,ドル $M \Omega \to M \Omega,ドル and this is the reduction chosen by the applicative order strategy.

Normal order reduction starts by reducing the top-level redex (because the function $K_y$ is already in normal form). Since $K_y$ ignores its argument, $(K_y \Omega) \to y$ in one step. More generally, $K_y N \to y$ for any term $N,ドル and this is the reduction chosen by the normal order strategy.

This case illustrates a more general phenomenon: applicative order reduction only ever finds a normal form if the term is strongly normalizing, whereas normal order reduction always finds the normal form if there is one. This happens because applicative order always evaluates fully arguments first, and so misses the opportunity for an argument to turn out to be unused; whereas normal order evaluates arguments as late as possible, and so always wins if the argument turns out to be unused.

(The flip side is that applicative order tends to be faster in practice, because it's relatively rare for an argument to be unused; whereas it's common for an argument to be used multiple times, and under applicative order the argument is only evaluated once. Normal order evaluates the argument as often as it's used, be it 0, 1 or many times.)

• Karolis Juodelė: I suppose you made a typo in paragraph 3. $K_y N \to N$ should be $\to y,ドル right? Regardless, +1.