Lambda-Lifting (Realisierung)

• verwendet Kombinatoren (globale Funktionen)

  I = λx.x, S = λxyz.xz(yz), K = λxy.y mathend000#

• und Transformationsregeln

  lift(FA) = lift(F)lift(A), lift(λx.B) = lift_x(B); mathend000#

• Spezifikation: lift_x(B)x→_β^*B mathend000#
• Implementierung:

  falls x $\notin$FV(B) mathend000#, dann lift_x(B) = KB mathend000#;

  sonst lift_x(x) = I, lift_x(FA) = Slift_x(F)lift_x(A) mathend000#

Beispiel: lift(λx.λy.yx) = lift_x(lift_y(yx)) = lift_x(SI(Kx)) = S(K(SI))(S(KK)I) mathend000#