Spezifikation

(lambda) lifting:

• Eingabe: Programm P mathend000#, bei dem alle Abstraktionen geschlossen sind
• Ausgabe: äquivalentes Programm P' mathend000#,
  bei dem alle Abstraktionen (geschlossen und) global sind

Motivation: in Maschinencode gibt es nur globale Sprungziele

(CPS-Transformation: Unterprogramme kehren nie zurück ⇒ mathend000# globale Sprünge)