Define fix-point combinator in Continuation Passing Style

Asked 10/3, 2016 at 13:45 Answered 3/5, 2017 at 6:55

Solved functional-programming scheme continuation-passing fixpoint-combinators

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)

Seneschal answered 10/3, 2016 at 13:45 Comment(1)

"... IOW, without using letrec in any form, only let (in Scheme terms)." I believe that's what you mean. Interesting question... – Finned 10/3, 2016 at 22:27

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.

Trailblazer answered 3/5, 2017 at 6:55 Comment(0)

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.

Finned answered 11/3, 2016 at 1:14 Comment(7)

Correct me if I am wrong, but I think you talk about using Y-combinator for CPS function. I am asking for a combinator itself defined in CPS. \g -> (\x-> x x) (\x-> g (\n k -> (x x) n k)) is not a CPS function. – Seneschal 11/3, 2016 at 12:27

yes, I was thinking about that too. but, what's to stop us defining (CPSY k) f = k (Y f)? – Finned 11/3, 2016 at 12:35

I mean, does your hypothetical language allow for lambdas at all? A lambda function returns its result directly, not through a continuation. Or is your language forbidding lambdas? I think more specifics are needed here; as asked your question is a bit vague in that regard. You speak of "CPS languages". I am not familiar with even one such language; I'm familiar with a CPS programming technique, a CPS programming discipline... AFAIK any function can be converted mechanically to CPS; so Y can too, it seems. – Finned 11/3, 2016 at 12:41

Consider this a theoretical question not tied to any particular programming language (that's why I didn't originally put the 'scheme' tag for example). You have: CPS-lambdas only, constants, primitive operators (such as mult or decr as you defined above), and exit to terminate the program. I explicitly said "The CPSY should be a plain continuation-passing style function". Using full lambda makes the problem a bit simple: as you found it yourself, a regular Y can be used for CPS functions. After all, CPS functions are a just a special case of a normal function. – Seneschal 11/3, 2016 at 12:50

why wouldn't the mechanical conversion work for Y too? Will check it out later... – Finned 11/3, 2016 at 12:55

Added further clarification in the question. CPSY should be built purely from CPS lambdas. So, only CPS in the body fo CPSY. Unless CPS version of {Y} is given, I cannot accept (CPSY k) f = k ({Y} f). – Seneschal 11/3, 2016 at 12:59

yes, figured that out too myself, by now. :) what's left is just to perform the conversion. theory says, it should always be possible... – Finned 11/3, 2016 at 12:59

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!

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.

Trailblazer answered 3/5, 2017 at 6:55 Comment(0)

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

Petry answered 1/2, 2017 at 9:2 Comment(0)

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.)

Fagaceous answered 10/3, 2016 at 19:11 Comment(3)

A recursive binding acts as a built-in fix combinator. Some languages hide it, some are more explicit about it (e.g. let vs letrec). However, I am looking for a solution that does not rely of a built-in FIX in any form. Y-combinator can be defined with the means of plain lambda calculus, as well as actual languages that model the calculus. But can it be done in CPS? – Seneschal 10/3, 2016 at 20:50

Edited the question to make myself a bit more clear :) – Seneschal 10/3, 2016 at 20:54

@Seneschal Ah, now I know what you're after. That's certainly more interesting. I'll leave the answer, though. – Fagaceous 11/3, 2016 at 8:36

Hot tags

Godot Unity Godot Help Programming Godot 4.X GUI GDScript 3D 2D Physics CSharp Godot 3.X VR XR Projects C++

Recommended topics

Hot tags