Systematische Übersetzung

Spezifikation:

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

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

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

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

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