Beta-Reduktion

Die Hauptoperation beim Konvertieren von Lambda-Ausdrücken wird Beta-Reduktion genannt. Sie kommt bei der Applikation einer Abstraktion auf einen Lambda-Ausdruck zum Tragen.

$% latex2html id marker 962 \fbox{ \parbox{12.5cm}{ {\sc Fundamentalbegriff {\a... ...wird wie folgt dargestellt: \begin{center}$((\lambda x.M) N)$ \end{center} } }$

$% latex2html id marker 968 \fbox{ \parbox{12.5cm}{ {\sc Fundamentalbegriff {\a... ...nter}$((\lambda x . M) N) \rightarrow_\beta M[x \leftarrow N]$ \end{center} } }$

Beispiele:

$((\lambda x.x\hspace{0.25em} x)(\lambda y.y)) \rightarrow_\beta ((\lambda y.y)(\lambda y.y)) \rightarrow_\beta (\lambda y.y)$
$((\lambda x.(\lambda y.x\hspace{0.25em} y)) y) \rightarrow_\beta (\lambda y_0.y\hspace{0.25em} y_0)$

Anmerkung:
Das zweite Beispiel demonstriert die Notwendigkeit einer Alpha-Konvertierung. Das an das $\lambda$ gebundene musste in umbenannt werden, damit das freie nicht durch die Substitution vom $\lambda$ eingefangen würde.

Georg Loczewski 2003-08-07