Kombinator-Reduktion
Die Kombinator-Reduktion ist, neben dem Lambda-Kalkül, ein weiteres Auswertungsverfahren für Lambda-Ausdrücke (siehe Lambda-Ausdruck).
Unter einem Kombinator versteht man einen Lambda-Ausdruck ohne freie Variable. Beispiele für Kombinatoren sind:
• die Identität I mit I e = e,
• der "cancelator" K mit K e f = e und
• der "distributor" S mit S e f g = e g (f g).
Von links nach rechts gelesen stellen die oben genannten Gleichungen für I, K und S Reduktionsregeln dar. Wenn ein Lambda-Ausdruck in einen semantisch gleichwertigen Kombinator-Ausdruck überführt wird, kann der Ausdruck anhand dieser Regeln ausgewertet werden.
Den zu einem Lambda-Ausdruck korrespondierenden Kombinator-Ausdruck erhält man mittels der Funktion comb. Es gilt:
comb(c) = c, für alle Konstanten c,
comb(id) = id, für alle Variablenbezeichner id,
comb(e1, e2) = comb(e1) comb(e2) und
comb(λ x.e) = abstr(x, comb(e))
Die Funktion abstr ist eine Hilfsfunktion mit der Eigenschaft (abstr(x, e)) x = e:
abstr(x, c) = K c, für alle Konstanten c,
abstr(x, x) = I, für alle Variablenbezeichner x,
abstr(x, id) = K id, für alle ungleichnen Variablenbezeichner x und id und
abstr(x, (e1, e2)) = (S abstr(x, e1) abstr(x, e2)).
Unter einem Kombinator versteht man einen Lambda-Ausdruck ohne freie Variable. Beispiele für Kombinatoren sind:
• die Identität I mit I e = e,
• der "cancelator" K mit K e f = e und
• der "distributor" S mit S e f g = e g (f g).
Von links nach rechts gelesen stellen die oben genannten Gleichungen für I, K und S Reduktionsregeln dar. Wenn ein Lambda-Ausdruck in einen semantisch gleichwertigen Kombinator-Ausdruck überführt wird, kann der Ausdruck anhand dieser Regeln ausgewertet werden.
Den zu einem Lambda-Ausdruck korrespondierenden Kombinator-Ausdruck erhält man mittels der Funktion comb. Es gilt:
comb(c) = c, für alle Konstanten c,
comb(id) = id, für alle Variablenbezeichner id,
comb(e1, e2) = comb(e1) comb(e2) und
comb(λ x.e) = abstr(x, comb(e))
Die Funktion abstr ist eine Hilfsfunktion mit der Eigenschaft (abstr(x, e)) x = e:
abstr(x, c) = K c, für alle Konstanten c,
abstr(x, x) = I, für alle Variablenbezeichner x,
abstr(x, id) = K id, für alle ungleichnen Variablenbezeichner x und id und
abstr(x, (e1, e2)) = (S abstr(x, e1) abstr(x, e2)).