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) = λk2.k2(λx.CPS(9)) = λk2.k2(λxk1.k19),
mathend000#
CPS((λx.9)8) = λk4.(λk2.k2(λxk1.k19))(λf.((λk3.k38)(λa.fak4)))
mathend000#
Ü: Normalform von
CPS((λx.9)8)(λz.z)
mathend000#
Johannes Waldmann
2014-03-31