Define fix-point combinator in Continuation Passing Style

9
votes
  • 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)
4
functional-programmingschemecontinuation-passingfixpoint-combinators
"... IOW, without using letrec in any form, only let (in Scheme terms)." I believe that's what you mean. Interesting question... – Will Ness

4 Answers

3
votes

TL;DR: same applictive-order Y works for CPS functions written in continuation-curried style.

In combinatory style, the usual definition of factorial with Y is, of course,

_Y (\r -> \n -> { n==0 -> 1 ; n * r (n-1) })     , where
                               ___^______
_Y = \g -> (\x-> x x) (\x-> g (\n-> x x n))  -- for applicative and normal order

CPS factorial definition is

fact = \n k -> equals n 0         -- a conditional must expect two contingencies
                 (\True -> k 1) 
                 (\False -> decr n 
                                 (\n1-> fact n1          -- *** recursive reference
                                             (\f1-> mult n f1 k)))

CPS-Y is augmented for the extra contingency argument (I'm saying "contingency" to disambiguate from true continuations). In Scheme,

(define (mult a b k)     (k (* a b)))
(define (decr c   k)     (k (- c 1)))
(define (equals d e s f) (if (= d e) (s 1) (f 0)))

(((lambda (g) 
     ( (lambda (x) (x x))
       (lambda (x) (g (lambda (n k) ((x x) n k))))))

  (lambda (fact)
    (lambda (n k)
      (equals n 0 (lambda (_) (k 1))
                  (lambda (_) (decr n 
                                (lambda (n1) (fact n1
                                               (lambda (f1) (mult n f1 k))))))))))

  5 (lambda (x) (display x)) )

This returns 120.

Of course in an auto-currying lazy language (but untyped!) by eta-contraction the above CPS-Y is exactly the same as the regular Y itself.

But what if our recursive function has two actual parameters, and continuation ⁄ contingency — the third? In Scheme-like language, would we have to have another Y then, with the (lambda (n1 n2 k) ((x x) n1 n2 k)) inside?

We can switch to always having the contingency argument first, and always code in the curried manner (each function has exactly one argument, possibly producing another such function, or a final result after all are applied). And it works, too:

(define (mult   k)   (lambda (x y) (k (* x y))))
(define (decr   k)   (lambda (x)   (k (- x 1))))
(define (equals s f) (lambda (x y) (if (= x y) (s) (f))))

((((lambda (g)                                ; THE regular,
     ( (lambda (x) (x x))                        ; applicative-order
       (lambda (x) (g (lambda (k) ((x x) k))))))   ; Y-combinator

   (lambda (fact)
    (lambda (k)
      (lambda (n)
        ((equals  (lambda () (k 1))
                  (lambda () ((decr (lambda (n1) 
                                        ((fact 
                                            (lambda (f1) ((mult k) n f1)))
                                         n1)))
                               n)))
          n 0)))))

   (lambda (x) (display x))) 
  5)

There are ways to type such a thing, too, if your language is typed. Or, in an untyped language, we could pack all arguments in a list maybe.

3
votes

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.

2
votes

Anonymous recursion in continuation-passing-style can be done as following (using JS6 as language):

// CPS wrappers
const dec = (n, callback)=>{
    callback(n - 1)
}
const mul = (a, b, callback)=>{
    callback(a * b)
}
const if_equal = (a, b, then, else_)=>{
    (a == b ? then : else_)()
}

// Factorial
const F = (rec, n, a, callback)=>{
    if_equal(n, 0,
        ()=>{callback(a)},
        ()=>{dec(n, (rn)=>{
            mul(a, n, (ra)=>{
                rec(rec, rn, ra, callback)
            })
        })
    })
}

const fact = (n, callback)=>{
    F(F, n, 1, callback)
}

// Demo
fact(5, console.log)

To get rid of the double use of label F, we can use a utility function like so:

const rec3 = (f, a, b, c)=>{
    f(f, a, b, c)
}
const fact = (n, callback)=>{
    rec3(F, n, 1, callback)
}

This allows us to inline F:

const fact = (n, callback)=>{
    rec3((rec, n, a, callback)=>{
        if_equal(n, 0,
            ()=>{callback(a)},
            ()=>{dec(n, (rn)=>{
                mul(a, n, (ra)=>{
                    rec(rec, rn, ra, callback)
                })
            })
        })
    }, n, 1, callback)
}

We can proceed to inline rec3 to make fact selfcontained:

const fact = (n, callback)=>{
    ((f, a, b, c)=>{
        f(f, a, b, c)
    })((rec, n, a, callback)=>{
        if_equal(n, 0,
            ()=>{callback(a)},
            ()=>{dec(n, (rn)=>{
                mul(a, n, (ra)=>{
                    rec(rec, rn, ra, callback)
                })
            })
        })
    }, n, 1, callback)
}

The following JavaScript uses the same approach to implement a for loop.

const for_ = (start, end, func, callback)=>{
    ((rec, n, end, func, callback)=>{
        rec(rec, n, end, func, callback)
    })((rec, n, end, func, callback)=>{
        func(n, ()=>{
            if_equal(n, end, callback, ()=>{
                S(n, (sn)=>{
                    rec(rec, sn, end, func, callback)
                })
            })
        })
    }, start, end, func, callback)
}

It's part of the fully async FizzBuzz I made https://gist.github.com/Recmo/1a02121d39ee337fb81fc18e735a0d9e

1
votes

This is the "trivial solution", not the non-recursive one the OP wanted -- it is left for comparison.

If you have a language providing recursive bindings, you can define fix for CPS functions (here using Haskell):

Prelude> let fixC f = \c -> f (fixC f c) c
Prelude> :t fixC
fixC :: (t -> t1 -> t) -> t1 -> t
Prelude> let facC' = \rec c n -> if n == 0 then c 1 else c (n * rec (n-1))
Prelude> let facC = fixC facC'
Prelude> take 10 $ map (facC id) [1..10]
[1,2,6,24,120,720,5040,40320,362880,3628800]

Maybe providing fixC as a primitive has performance implications, though (if you have continuations represented not simply as closures), or is due to the fact that "traditional" lambda calculus does not have names for functions which can be used recursively.

(Probably there is also a more efficient variant analogous to fix f = let x = f x in x.)