Define a path combinator in the continuum walk style

  • Fixed-point combinators are very useful tools for representing recursion.
  • The Continuation-Passing style is a lambda calculus style in which functions are never returned. Instead, you pass the rest of your program as a lambda argument to your function and continue through them. This allows you to better control the flow of execution and easier to define various constructions that change the flow (cycles, coroutines, etc.)

However, I wonder if you can express one in the other? All the CPS-style languages ​​I've seen have an explicit FIX construct for defining recursion.

  • Is it because it is not possible to define a fixed-point combinator (or similar) in plain CPS, without FIX ? If so, do you know the evidence for such a thing?
  • Or is it just because of printing problems?
  • Or maybe it is possible, but for some reason impractical?
  • Or I just did not find the solution that is there ...?

I would expect the CPS function, CPSY Y-combinator, to work as follows: if I define a CPS function, CPSY to Y, such as:

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

Then I would put it in CPSY to create a function that returns to itself:

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

CPSY should be a simple style transfer function, without relying on any recursion. A Y combinator can be defined in this way in simple lambda calculus without built-in recursion. Can it exist in one form or another in CPS?


Repeat for clarification: I'm looking for a combinatorial function CPSY which:

  • Would enable recursion of CPS functions
  • The definition of this is not recursive
  • Its definition is given in the style of passing continuation (in the body of CPSY there is no return of CPSY )
+8
source share
4 answers

TL DR: The same application order Y works for CPS functions written in continuation-curry style.


In combinatorial style, the usual definition of a factorial with Y , of course,

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

Factorial definition of CPS

 fact = \nk -> 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 complemented by an extra contingency argument (I say “contingency” to eliminate ambiguity from true sequels). On the diagram

 (define (mult abk) (k (* ab))) (define (decr ck) (k (- c 1))) (define (equals desf) (if (= de) (s 1) (f 0))) (((lambda (g) ( (lambda (x) (xx)) (lambda (x) (g (lambda (nk) ((xx) nk)))))) (lambda (fact) (lambda (nk) (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, on an automatic karliz, a lazy language (but untyped!) Using eta compression, the above CPS-Y is exactly the same as regular Y itself .

But what if our recursive function has two valid parameters and the continuation of & frasl; Unexpected expenses; third? In a language similar to Schema, we must have a different Y, and inside (lambda (n1 n2 k) ((xx) n1 n2 k)) inside?

We can first switch to the contingency argument and always point in italics (each function has exactly one argument, possibly producing another such function, or the end result after application). And it works :

 (define (mult k) (lambda (xy) (k (* xy)))) (define (decr k) (lambda (x) (k (- x 1)))) (define (equals sf) (lambda (xy) (if (= xy) (s) (f)))) ((((lambda (g) ; THE regular, ( (lambda (x) (xx)) ; applicative-order (lambda (x) (g (lambda (k) ((xx) 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 introduce such a thing if your language is printed. Or, in an untyped language, we could pack all the arguments in a list, perhaps.

+3
source

First, output CPS-Y to evaluate the normal order in the lambda calculus, and then convert it to the applicative order.

The Wikipedia page defines a fixed-point combinator Y with the following equation:

 Y f = f (Y f) 

In CPS form, this equation will look something like this:

 Y fk = Y f (λh. fhk) 

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

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

Convert it to CPS:

 Y fk = (λg. ggk) (λg.λk. gg (λh. fhk)) 

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

 Y fk = (λg. ggk) (λg.λk. gg (λh. fhk)) = (λg.λk. gg (λh. fhk)) (λg.λk. gg (λh. fhk)) k = (λg.λk. gg (λh. fhk)) (λg.λk. gg (λh. fhk)) (λh. fhk) = Y f (λh. fhk) 

Voila!


Now for evaluating the applicative order, of course, we need to change this a bit. The rationale here is the same as in the case other than CPS: we need to “swing” the recursive call (ggk) and act only on the call the next time:

 Y fk = (λg. ggk) (λg.λk. f (λx.λk. gg (λF. F xk)) k) 

Here's a direct translation to Racket:

 (define (Y fk) ((λ (g) (ggk)) (λ (gk) (f (λ (xk) (gg (λ (F) (F xk)))) k)))) 

We can verify that this really works - for example, here is calculating a recursive triangular number in CPS (with the exception of arithmetic operations, for simplicity):

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

I believe this answers the question.

+3
source

Anonymous recursion in the continuation-pass style can be performed as follows (using JS6 as a 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 the label F , we can use the utility function as follows:

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

This allows us to embed 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 go to inline rec3 to make the fact self-preserving:

 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 the 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) } 

This is the fully async part of FizzBuzz I made by https://gist.github.com/Recmo/1a02121d39ee337fb81fc18e735a0d9e

+2
source

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


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

 Prelude> let fixC f = \c -> f (fixC fc) c Prelude> :t fixC fixC :: (t -> t1 -> t) -> t1 -> t Prelude> let facC' = \rec cn -> 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] 

Perhaps providing fixC as a primitive has performance implications, though (if you have extensions that are not just closures), or because the “traditional” lambda calculus doesn't have names for functions that can be used recursively .

(There is probably a more efficient option similar to fix f = let x = fx in x .)

+1
source

All Articles