fun fact 0 = 1
| fact n = n * fact (n-1)
(************************************************)
(* Version 1: Continuations as functions *)
fun factcps 0 k = k 1
| factcps n k = factcps (n-1) (fn v => k (n * v))
fun factk n = factcps n (fn v => v)
(************************************************)
(* Version 2: Separate the definition of factcps from the code that
depends on the representation of continuations. *)
(* Code that depends on representation of continuations *)
fun appK k v = k v
fun makeInitK () = (fn x => x)
fun makeRecK k n = (fn v => appK k (n * v))
(* Abstract code for factcps *)
fun abs_factcps 0 k = appK k 1
| abs_factcps n k = abs_factcps (n-1) (makeRecK k n)
fun abs_factk n = abs_factcps n (makeInitK())
(************************************************)
(* Version 3: The abstract code for factcps does not change anymore;
we'll change the code that depends on the representation of
continuations. Any implementation of appK, makeInitK, and makeRecK is
fine as long as it behaves the same as the one above. We can formally
characterize that behavior as follows:
appK (makeInitK()) v
= by definition of makeInitK
appK (fn x => x) v
= by definition of appK
(fn x => x) v
= by beta_v reduction
v
appK (makeRecK k n) v
= by definition of makeRecK
appK (fn v => appK k (n * v)) v
= by definition of appK
(fn v => appK k (n * v)) v
= by beta_v reduction
appK k (n * v)
So in summary any implementation that satisfies the following two
axioms should be fine:
appK (makeInitK()) v = v
appK (makeRecK k n) v = appK k (n * v)
The following are correct:
fun appK k v = k * v
fun makeInitK () = 1
fun makeRecK k n = k * n
Indeed we can verify the axioms as follows:
appK (makeInitK()) v = appK 1 v = 1 * v = v
appK (makeRecK k n) v = appK (k * n) v =
(k * n) * v = k * (n * v) = appK k (n * v)
NOTE that we've used the ASSOCIATIVITY of multiplication here!!!
*)