"Anwendbare Ordnung" und "Normale Ordnung" in der Lambda-Rechnung

Anwendbare Reihenfolge: Bewerten Sie die Argumente einer Funktion immer vollständig, bevor Sie die Funktion selbst bewerten, wie z.

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

Normale Reihenfolge: Der Ausdruck würde von außen nach innen reduziert, wie -

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

Warum ist es so, dass in der anwendbaren Reihenfolge Endlosschleife, aber in der normalen Reihenfolge M → y ?$M \rightarrow$
$M \rightarrow y$

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

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.

Dieser Fall zeigt ein allgemeineres Phänomen: Die anwendbare Ordnungsreduktion findet immer nur dann eine Normalform, wenn der Term stark normalisiert, wohingegen die normale Ordnungsreduktion immer die Normalform findet, wenn es eine gibt. Dies liegt daran, dass die anwendbare Reihenfolge immer zuerst die vollständigen Argumente bewertet und somit die Gelegenheit verpasst, dass sich herausstellt, dass ein Argument nicht verwendet wird. Die normale Reihenfolge wertet Argumente so spät wie möglich aus und gewinnt immer, wenn sich herausstellt, dass das Argument nicht verwendet wird.

(Die Kehrseite ist, dass die anwendbare Reihenfolge in der Praxis in der Regel schneller ist, da ein Argument relativ selten nicht verwendet wird; wohingegen ein Argument häufig mehrfach verwendet wird und bei anwendbarer Reihenfolge das Argument nur einmal ausgewertet wird. Normal order wertet das Argument so oft aus, wie es verwendet wird, sei es 0, 1 oder mehrmals.)