Define fix-point combinator in Continuation Passing Style
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.
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.
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