I am looking for an example of continuation passing style which does not involve any examples from programming languages; in particular, an example which involves a reduction sequence from the lambda calculus would be very useful.
If I search for "continuation passing style" on the internet, all I can find are examples from programming languages, which make little sense to me. How can the technique be illustrated by something from the lambda calculus?
I am trying to read Phillip Wadler's "Monads and composable continuations", and having at least some preliminary understanding of what continuation passing would be in the lambda calculus would be useful.
If we to add two numbers we could use the expression $$ \lambda n,m. n+m. $$ If we switch this to continuation passing style we need add another parameter, the continuation function, $k$. Then we have $$ \lambda n,m,k. k(n+m) $$ The only difference is that, instead of returning a value, we pass the return value to the continuation. It's not any different in $\lambda$ calculus than in any other programming language.
Things are a little more interesting when we have a function defined by recursion; in this case it can easier to change the continuation to an anonymous function that calls the original continuation. The example at "The definition of the factorial using continuations in the Lambda calculus " demonstrates how to do this.
In the context of addition, a recursive definition might be $$ Y \lambda f \lambda n,m. \text{if } n = 0 \text{ then } m \text{ else } 1 + f(n-1,m). $$ To switch this to continuation passing style we could use something like this: $$ Y \lambda f \lambda n,m\lambda k. \text{if } n = 0 \text{ then } k(m) \text{ else } f(n-1, m, \lambda v. k(v+1)). $$ Of course, in the end, the second one still ends up calling $k(n+m)$ once all the intermediate anonymous functions are evaluated.