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