Lambda-Kalkül Reduktionsregeln

Aus ProgrammingWiki

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))