Search code examples
functional-programmingschemecontinuation-passingfixpoint-combinators

Define fix-point combinator in Continuation Passing Style

  • The fix-point combinators are very useful tools to introduce recursion.
  • The Continuation-Passing style is a style of lambda calculus where functions never return. Instead you pass the rest of your program as a lambda argument into your function and continue through them. It allows you to have better control over the execution flow and more easily define various flow-altering constructs (loops, coroutines, etc...)

However, I am wondering if you can express one in another? All CPS-style languages I have seen have an explicit FIX construct to define recursion.

  • Is it because it is impossible to define a fix-point combinator (or similar) in plain CPS, without FIX? If so, do you know the proof of such thing?
  • Or is it because of typing problems only?
  • Or maybe it is possible, but for some reason impractical?
  • Or I simply didn't find a solution which is out there... ?

I would expect a Y-combinator-like CPS function CPSY to work as this: If I define a Y-ready CPS function, such as:

function Yready(this, return) = 
    return (lambda <args> . <body using 'this' as recursion>);

I would then put it into CPSY to produce a function that recurses into itself:

function CPSY(F, return) = ?????

CPSY(Yready,
    lambda rec . <body where 'rec' names 'lambda <args>' from above, but with the loop closed>
)

The CPSY should be a plain continuation-passing style function without itself relying on any recursion. Y-combinator can be defined in such a way in plain lambda calculus without built-in recursion. Can it exist, in some form, in CPS as well?

To reiterate for clarification: I am looking for a combinator-like function CPSY that:

  • Would enable recursion of CPS functions
  • The definition of it does not rely on recursion
  • The definition of it is given in continuation-passing style (no returning lambdas anywhere within the body of CPSY)
Solution

  • Let's first derive CPS-Y for normal-order evaluation in lambda calculus, and then convert it to applicative-order.

    Wikipedia page defines fixed-point combinator Y by the following equation:

    Y f = f (Y f)

    In CPS form, this equation would look rather like this:

    Y f k = Y f (λh. f h k)

    Now, consider the following non-CPS normal-order definition of Y:

    Y f = (λg. g g) (λg. f (g g))

    Transform it to CPS:

    Y f k = (λg. g g k) (λg.λk. g g (λh. f h k))

    Now, beta-reduce this definition a couple of times to check that it indeed satisfies the “CPS fixed-point” condition above:

    Y f k = (λg. g g k) (λg.λk. g g (λh. f h k))
      = (λg.λk. g g (λh. f h k)) (λg.λk. g g (λh. f h k)) k
      = (λg.λk. g g (λh. f h k)) (λg.λk. g g (λh. f h k)) (λh. f h k)
      = Y f (λh. f h k)

    Voila!

    Now, for applicative-order evaluation, of course, we would need to change this a bit. The reasoning here is the same as in non-CPS case: we need to “thunk” the recursive (g g k) call and proceed only when called for the next time:

    Y f k = (λg. g g k) (λg.λk. f (λx.λk. g g (λF. F x k)) k)

    Here's a direct translation into Racket:

    (define (Y f k)
  ((λ (g) (g g k))
   (λ (g k) (f (λ (x k) (g g (λ (F) (F x k)))) k))))

    We can check that it actually works — for example, here's the recursive triangular number calculation in CPS (except for arithmetic operations, for simplicity):

    (Y (λ (sum k) (k (λ (n k) (if (< n 1)
                              (k 0)
                              (sum (- n 1) (λ (s) (k (+ s n))))))))
   (λ (sum) (sum 9 print)))
;=> 45

    I believe this answers the question.