Semantik für CPS

Semantik von Ausdruck x in Umgebung E mathend000#

ist Funktion von Continuation nach Wert (Action)

value(E, label L B) = \ k -> 
  value (E[L/k], B) k
value (E, jump L B) = \ k -> 
  value (E, L) $ \ k' ->
  value (E, B) k'

Beispiel 1:

value (E, label x x) 
  = \ k -> value (E[x/k], x) k
  = \ k -> k k

Beispiel 2

value (E, jump (label x x)(label y y)) 
= \ k ->
  value (E, label x x) $ \ k' -> 
  value (E, label y y) k'
= \ k -> 
  value (E, label y y) (value (E, label x x))
= \ k -> ( \ k0 -> k0 k0 ) ( \ k1 -> k1 k1 )