Systematische Übersetzung

Spezifikation:

• Eingabe: geschlossener Lambda-Ausdruck P
• Ausgabe: äquivalenter Kombinator-Ausdruck [P]

  (Applikationen mit S, K, I; sonst keine Variablen und Lambdas)

benutzt [λx.A] = lift_x(A) mit Spezifikation: lift_x(A)x→^*A

• lift_x(y) = falls x = y dann I sonst Ky
• lift_x(AB) = Slift_x(A)lift_x(B)
• lift_x(λy.A) = lift_x(lift_y(A))

Beispiele: λx.xx, λxy.y, λxy.yx -- Vereinfachungen?