cps_and_continuation_operators.mdwn

   1 ;; call-by-value CPS
   2 ; see Dancy and Filinski, "Representing control: a study of the CPS transformation" (1992)
   3 ; and Sabry, "Note on axiomatizing the semantics of control operators" (1996)
   4
   5 ; [x] = var x
   6 let var = \x (\k. k x) in
   7 ; [\x. body] = lam (\x. [body])
   8 let lam = \x_body (\k. k (\x. x_body x)) in
   9 ; [M N] = app [M] [N]
  10 let app = \m n. (\k. m (\m. n (\n. m n k))) in
  11
  12 ; helpers
  13 let app3 = \a b c. app (app a b) c in
  14 let app4 = \a b c d. app (app (app a b) c) d in
  15 ; [succ] = op1 succ
  16 let op1 = \op. \u. u (\a k. k (op a)) in
  17 ; [plus] = op2 plus
  18 let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in
  19 let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in
  20
  21 ;; continuation operators
  22 ; [let/cc k M] = letcc (\k. [M])
  23 let callcc = \k. k (\f u. (\j. f j u) (\y w. u y)) in
  24 let letcc = \x_body. app callcc (lam x_body) in
  25 let letcc = \k_body. \k. (\j. (k_body j) k) (\y w. k y) in
  26
  27 ; [abort M] = abort [M]
  28 let abort = \body. \k. body (\m m) in
  29 ; [prompt M] = prompt [M]
  30 let prompt = \body. \k. k (body (\m m)) in
  31 ; [shift k M] = shift (\k. [M])
  32 let shift = \k_body. \k. (\j. (k_body j) (\m m)) (\y w. w (k y)) in
  33
  34 ;; examples
  35 ; (+ 100 (let/cc k (+ 10 1))) ~~> 111
  36 ; app3 (op2 plus) (var hundred) (letcc (\k. app3 (op2 plus) (var ten) (var one)))
  37
  38 ; (+ 100 (let/cc k (+ 10 (k 1)))) ~~> 101
  39 ; app3 (op2 plus) (var hundred) (letcc (\k. app3 (op2 plus) (var ten) (app (var k) (var one))))
  40
  41 ; (+ 100 (+ 10 (abort 1))) ~~> 1
  42 ; app3 (op2 plus) (var hundred) (app3 (op2 plus) (var ten) (abort (var one)))
  43
  44 ; (+ 100 (prompt (+ 10 (abort 1)))) ~~> 101
  45 ; app3 (op2 plus) (var hundred) (prompt (app3 (op2 plus) (var ten) (abort (var one))))
  46
  47 ; (+ 1000 (prompt (+ 100 (shift k (+ 10 1))))) ~~> 1011
  48 ; app3 (op2 plus) (var thousand) (prompt (app3 (op2 plus) (var hundred) (shift (\k. ((op2 plus) (var ten) (var one))))))
  49
  50 ; (+ 1000 (prompt (+ 100 (shift k (k (+ 10 1)))))) ~~> 1111
  51 ; app3 (op2 plus) (var thousand) (prompt (app3 (op2 plus) (var hundred) (shift (\k. (app (var k) ((op2 plus) (var ten) (var one)))))))
  52
  53 ; (+ 1000 (prompt (+ 100 (shift k (+ 10 (k 1)))))) ~~> 1111 but added differently
  54 ; app3 (op2 plus) (var thousand) (prompt (app3 (op2 plus) (var hundred) (shift (\k. ((op2 plus) (var ten) (app (var k) (var one)))))))
  55
  56 ; (+ 100 ((prompt (+ 10 (shift k k))) 1)) ~~> 111
  57 ; app3 (op2 plus) (var hundred) (app (prompt (app3 (op2 plus) (var ten) (shift (\k. (var k))))) (var one))
  58
  59 ; (+ 100 (prompt (+ 10 (shift k (k (k 1)))))) ~~> 121
  60 ; app3 (op2 plus) (var hundred) (prompt (app3 (op2 plus) (var ten) (shift (\k. app (var k) (app (var k) (var one))))))
  61