BuK/IIm21/Lambda-Kalkül Reduktionsregeln

Wiki-Quelltext dieser Seite.

Beta-Regel:

((λx. E) M) ⇒ E[M/x]


Bedingungen:

- E und M sind λ-Ausdrücke

- M ist nicht in E gebunden

- x ist eine Variable


Vorgehen:

- ersetze alle in in E vorkommenden x durch M


Beispiel:

((λx. (x x)) y) = (λx. (y y))



Alpha-Regel:

(λx. E) ←→ (λx′. E[x′/x])



Bedingungen:

- x' komm nicht frei in E vor


Vorgehen:

- Ersetze jedes x durch x'


Beispiel:

- (λx.(λy.(λz. (x (y z))))) ←→ (λa.(λb.(λc. (a (b c)))))


Motivation:

- λ-Ausdruck für Anwendung anderer Reduktionsregeln aufbereiten

((λx. (λy . (x y)))(y w )) ←→ (gebundenes y durch ungebundenes z ersetzen)
((λx. (λz. (x z)))(y w)) ⇒ (y jetzt frei, Betta-Regel nutzbar)
(λz. ((y w) z))


Eta-Regel:

(λz. ((λx. E ) z)) ⇒ (λx. E) und (λx. (E x)) ⇒ E

Vorgehensweise:

- Abstraktion und zugehörige Variable fallen weg


Beispiel:

(λz. ((λx. (y x)) z)) ⇒ (λx. (y x))