X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=cps.mdwn;fp=cps.mdwn;h=0000000000000000000000000000000000000000;hp=605e86a5fc4f038b00dc9cf9444f0fbfe4d52ead;hb=347bc26072eb5d6c69943f72306768b28161f1ab;hpb=172783a2998a2d2d6a0e1cbda2e4f68710099fe3 diff --git a/cps.mdwn b/cps.mdwn deleted file mode 100644 index 605e86a5..00000000 --- a/cps.mdwn +++ /dev/null @@ -1,61 +0,0 @@ -;; call-by-value CPS -; see Dancy and Filinski, "Representing control: a study of the CPS transformation" (1992) -; and Sabry, "Note on axiomatizing the semantics of control operators" (1996) - -; [x] = var x -let var = \x (\k. k x) in -; [\x. body] = lam (\x. [body]) -let lam = \x_body (\k. k (\x. x_body x)) in -; [M N] = app [M] [N] -let app = \m n. (\k. m (\m. n (\n. m n k))) in - -; helpers -let app3 = \a b c. app (app a b) c in -let app4 = \a b c d. app (app (app a b) c) d in -; [succ] = op1 succ -let op1 = \op. \u. u (\a k. k (op a)) in -; [plus] = op2 plus -let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in -let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in - -;; continuation operators -; [let/cc k M] = letcc (\k. [M]) -let callcc = \k. k (\f u. (\j. f j u) (\y w. u y)) in -let letcc = \x_body. app callcc (lam x_body) in -let letcc = \k_body. \k. (\j. (k_body j) k) (\y w. k y) in - -; [abort M] = abort [M] -let abort = \body. \k. body (\m m) in -; [prompt M] = prompt [M] -let prompt = \body. \k. k (body (\m m)) in -; [shift k M] = shift (\k. [M]) -let shift = \k_body. \k. (\j. (k_body j) (\m m)) (\y w. w (k y)) in - -;; examples -; (+ 100 (let/cc k (+ 10 1))) ~~> 111 -; app3 (op2 plus) (var hundred) (letcc (\k. app3 (op2 plus) (var ten) (var one))) - -; (+ 100 (let/cc k (+ 10 (k 1)))) ~~> 101 -; app3 (op2 plus) (var hundred) (letcc (\k. app3 (op2 plus) (var ten) (app (var k) (var one)))) - -; (+ 100 (+ 10 (abort 1))) ~~> 1 -; app3 (op2 plus) (var hundred) (app3 (op2 plus) (var ten) (abort (var one))) - -; (+ 100 (prompt (+ 10 (abort 1)))) ~~> 101 -; app3 (op2 plus) (var hundred) (prompt (app3 (op2 plus) (var ten) (abort (var one)))) - -; (+ 1000 (prompt (+ 100 (shift k (+ 10 1))))) ~~> 1011 -; app3 (op2 plus) (var thousand) (prompt (app3 (op2 plus) (var hundred) (shift (\k. ((op2 plus) (var ten) (var one)))))) - -; (+ 1000 (prompt (+ 100 (shift k (k (+ 10 1)))))) ~~> 1111 -; app3 (op2 plus) (var thousand) (prompt (app3 (op2 plus) (var hundred) (shift (\k. (app (var k) ((op2 plus) (var ten) (var one))))))) - -; (+ 1000 (prompt (+ 100 (shift k (+ 10 (k 1)))))) ~~> 1111 but added differently -; app3 (op2 plus) (var thousand) (prompt (app3 (op2 plus) (var hundred) (shift (\k. ((op2 plus) (var ten) (app (var k) (var one))))))) - -; (+ 100 ((prompt (+ 10 (shift k k))) 1)) ~~> 111 -; app3 (op2 plus) (var hundred) (app (prompt (app3 (op2 plus) (var ten) (shift (\k. (var k))))) (var one)) - -; (+ 100 (prompt (+ 10 (shift k (k (k 1)))))) ~~> 121 -; app3 (op2 plus) (var hundred) (prompt (app3 (op2 plus) (var ten) (shift (\k. app (var k) (app (var k) (var one)))))) -