CPS-Transf. f. Abstraktion, Applikation

vgl. Sect. 6 in: Gordon Plotkin: Call-by-name, call-by-value and the λ mathend000#-calculus, Th. Comp. Sci. 1(2) 1975, 125-159 http://dx.doi.org/10.1016/0304-3975(75)90017-1 , http://homepages.inf.ed.ac.uk/gdp/

• CPS(v) = λk.kv mathend000#
• CPS(FA) = λk.(CPS(F)(λf.CPS(A)(λa.fak))) mathend000#
• CPS(λx.B) = λk.k(λx.CPS(B)) mathend000#

dabei sind k, f, a mathend000# frische Namen.

Bsp. CPS(λx.9) = λk₂.k₂(λx.CPS(9)) = λk₂.k₂(λxk₁.k₁9), mathend000#

CPS((λx.9)8) = λk₄.(λk₂.k₂(λxk₁.k₁9))(λf.((λk₃.k₃8)(λa.fak₄))) mathend000#

Ü: Normalform von CPS((λx.9)8)(λz.z) mathend000#