„Kolejność aplikacji” i „Normalna kolejność” w rachunku lambda

Kolejność aplikacji: Zawsze w pełni oceniaj argumenty funkcji przed oceną samej funkcji, na przykład -

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

Normalna kolejność: wyrażenie zostanie zmniejszone z zewnątrz, na przykład -

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

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

Dlaczego w takiej kolejności nieskończona pętla, ale w normalnej kolejności M → y ?$M \rightarrow$
$M \rightarrow y$

$(\lambda x.y \ (\lambda x.(x \ \ x) \ \lambda x.(x \ \ x)))$

Termin, który redukujesz to $(K_y \Omega)$ gdzie $K_y$ jest funkcją stałą $\lambda x. y$ (zawsze wraca $y$ignorując jego argument) i $\Omega = (\lambda x. (x \, x) \: \lambda x. (x \, x))$jest terminem nieokreślającym. W pewnym sensie$\Omega$ jest ostatecznym terminem nie kończącym: zmniejsza się do siebie, tj $\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.)