Lambda-Kalkül
Der Lambda-Kalkül beschreibt die Auswertung von Lambda-Ausdrücken (siehe Lambda-Ausdruck). Der Kalkül formt Lambda-Ausdrücke anhand von drei verschiedenen Umformungsregeln um:
• die α-Konversion, mit der gebundene Variable beliebig unbenannt werden können,
• die β-Reduktion löst eine Applikation auf, ((λ x.E1) E2) wird zu E1[x/E2],
• die δ-Reduktion wertet Ausdrücke aus, die aus Konstanten des Basisbereichs gebildet werden.
Man beginnt die Auswertung eines Lambda-Ausdrucks mit α-Konversionen, die solange durchgeführt werden, bis alle Variablen unterschiedliche Namen haben. Das verhindert Probleme bei den nachfolgenden Anwendungen der β-Reduktion (name clash).
Ein Lambda-Ausdruck, der nicht mehr β-Reduzierbar ist, heisst Normalform. Aus dem Church-Rosser-Theorem folgt, dass wenn eine Normalform existiert, diese auch eindeutig ist.
Das Church-Rosser-Theorem besagt, dass die Relation R, mit E1 R E2 g.d.w. E2 durch β-Reduktion aus E1 entstanden ist, die Rauten-Eigenschaft besitzt:
für alle x gilt: aus x R* y und x R* z folgt,
es existiert w mit: y R* w und z R* w.
Die Eindeutigkeit der Normalform folgt aus der Tatsache, dass wenn y und z Normalformen sind, diese gleich sein müssen.
Nicht jeder Lambda-Ausdruck hat eine Normalform:
((λ x . (x x)) (λ x . (x x)))
bleibt bei der β-Reduktion unverändert.
Ein Teilausdruck eines Lambda-Ausdrucks, auf den eine β-Reduktion angewendet werden kann, heisst Redex (reducibe expression). Lambda-Ausdrücke können mehrere Redexe haben.
Man nennt einen Redex outermost, wenn er in keinem anderen Redex enthalten ist. Ein Redex heisst innermost, wenn er keinen weiteren Redex enthält. Leftmost wird ein Redex genannt, wenn sein lambda-Symbol links von den lambda-Symbolen aller anderen Redexe steht. Analoges gilt für Redexe, die rightmost sind.
Wird bei der Auswertung eines Lambda-Ausdrucks stets der leftmost, outermost Redex gewählt, spricht man von einer normal order reduction (NOR). Wenn eine Normalform des Ausdrucks existiert, dann kann sie durch eine NOR berechnet werden.
Wird immer der leftmost, innermost Redex gewählt, nennt man die Auswertung eine applicative order reduction (AOR).
Lambda-Ausdrücke können auch ausgewertet werden durch:
• die SECD-Maschine,
• Kombinator-Reduktion und
• Graphen-Reduktion.
• die α-Konversion, mit der gebundene Variable beliebig unbenannt werden können,
• die β-Reduktion löst eine Applikation auf, ((λ x.E1) E2) wird zu E1[x/E2],
• die δ-Reduktion wertet Ausdrücke aus, die aus Konstanten des Basisbereichs gebildet werden.
Man beginnt die Auswertung eines Lambda-Ausdrucks mit α-Konversionen, die solange durchgeführt werden, bis alle Variablen unterschiedliche Namen haben. Das verhindert Probleme bei den nachfolgenden Anwendungen der β-Reduktion (name clash).
Ein Lambda-Ausdruck, der nicht mehr β-Reduzierbar ist, heisst Normalform. Aus dem Church-Rosser-Theorem folgt, dass wenn eine Normalform existiert, diese auch eindeutig ist.
Das Church-Rosser-Theorem besagt, dass die Relation R, mit E1 R E2 g.d.w. E2 durch β-Reduktion aus E1 entstanden ist, die Rauten-Eigenschaft besitzt:
für alle x gilt: aus x R* y und x R* z folgt,
es existiert w mit: y R* w und z R* w.
Die Eindeutigkeit der Normalform folgt aus der Tatsache, dass wenn y und z Normalformen sind, diese gleich sein müssen.
Nicht jeder Lambda-Ausdruck hat eine Normalform:
((λ x . (x x)) (λ x . (x x)))
bleibt bei der β-Reduktion unverändert.
Ein Teilausdruck eines Lambda-Ausdrucks, auf den eine β-Reduktion angewendet werden kann, heisst Redex (reducibe expression). Lambda-Ausdrücke können mehrere Redexe haben.
Man nennt einen Redex outermost, wenn er in keinem anderen Redex enthalten ist. Ein Redex heisst innermost, wenn er keinen weiteren Redex enthält. Leftmost wird ein Redex genannt, wenn sein lambda-Symbol links von den lambda-Symbolen aller anderen Redexe steht. Analoges gilt für Redexe, die rightmost sind.
Wird bei der Auswertung eines Lambda-Ausdrucks stets der leftmost, outermost Redex gewählt, spricht man von einer normal order reduction (NOR). Wenn eine Normalform des Ausdrucks existiert, dann kann sie durch eine NOR berechnet werden.
Wird immer der leftmost, innermost Redex gewählt, nennt man die Auswertung eine applicative order reduction (AOR).
Lambda-Ausdrücke können auch ausgewertet werden durch:
• die SECD-Maschine,
• Kombinator-Reduktion und
• Graphen-Reduktion.