The definition of the factorial using continuations in the Lambda calculus

382 Views Asked by At

I am trying to understand why the definition below of the factorial given here is an example of a continuation:

https://www.seas.harvard.edu/courses/cs152/2010sp/lectures/lec11.pdf

$$FACT_{cps} = Y \hspace{0.2cm} λf. λn, k.\hspace{0.2cm} \text{if} \hspace{0.2cm} n = 0 \hspace{0.2cm} \text{then} \hspace{0.2cm} k1 \hspace{0.2cm} \text{else} \hspace{0.2cm} f (n − 1) (λv. k (n ∗ v))$$

If $n = 0$, we get $k1$, which is $1!$. If $n = 1$, we get $k(1 * f(0)) = 1 * 0! = 1$. If $n = 2$, we get $k(2 * f(1)) = 2* 1! = 2$.

I presume this is how the formula works above.

But why is it an example of a continuation? Also, is the $Y$ an error in the handout?

The authors of the handout describe the use of continuations as follows:

Using continuations, functions can be transformed into "functions that don’t return”—functions that take, besides the usual arguments, an additional argument representing a continuation. When the function finishes, it invokes the continuation on its result, instead of returning the result to its caller. Writing functions in this way is usually referred to as Continuation-Passing Style, or CPS for short.

Could someone illustrate what they mean with reference to $FACT_{cps}$ as defined above?

1

There are 1 best solutions below

0
On

$Y$ is Haskell Curry's Y-combinator, which is used here to express the recursive factorial function as a closed lambda expression, rather than as a non-closed lambda expression that contains a symbol that represents a self-reference. But this has no relevance for continuation passing, it's just a standard trick when dealing formally with recursion.

$k$ is a continuation function which is supplied as an extra argument. Instead of reducing to $n!$ as a straight-forward factorial function would, this function reduces to $k(n!)$. So instead of returning the result $n!$ to where the function was applied, the continuation function $k$ controls what happens next with the result. It could for example use the result in some further computation which invokes yet another continuation function, and so on.