Two-layer "Y-style" combinator. Is this common? Does this have an official name?

Question

I've been looking into how languages that forbid use-before-def and don't have mutable cells (no set! or setq) can nonetheless provide recursion. I of course ran across the (famous? infamous?) Y combinator and friends, e.g.:

• http://www.ece.uc.edu/~franco/C511/html/Scheme/ycomb.html
• http://okmij.org/ftp/Computation/fixed-point-combinators.html
• http://www.angelfire.com/tx4/cus/combinator/birds.html
• http://en.wikipedia.org/wiki/Fixed-point_combinator

When I went to implement "letrec" semantics in this style (that is, allow a local variable to be defined such that it can be a recursive function, where under the covers it doesn't ever refer to its own name), the combinator I ended up writing looks like this:

Y_letrec = λf . (λx.x x) (λs . (λa . (f ((λx.x x) s)) a))

Or, factoring out the U combinator:

U = λx.x x
Y_letrec = λf . U (λs . (λa . (f (U s)) a))

Read this as: Y_letrec is a function which takes a to-be-recursed function f. f must be a single-argument function which accepts s, where s is the function that f can call to achieve self-recursion. f is expected to define and return an "inner" function which does the "real" operation. That inner function accepts argument a (or in the general case an argument list, but that can't be expressed in the traditional notation). The result of calling Y_letrec is a result of calling f, and it is presumed to be an "inner" function, ready to be called.

The reason I set things up this way is so that I could use the parse tree form of the to-be-recursed function directly, without modification, merely wrapping an additional function layer around it during transformation when handling letrec. E.g., if the original code is:

(letrec ((foo (lambda (a) (foo (cdr a))))))

then the transformed form would be along the lines of:

(define foo (Y_letrec (lambda (foo) (lambda (a) (foo (cdr a))))))

Note that the inner function body is identical between the two.

My questions are:

• Is my Y_letrec function commonly used?
• Does it have a well-established name?

Note: The first link above refers to a similar function (in "step 5") as the "applicative-order Y combinator", though I'm having trouble finding an authoritative source for that naming.

UPDATE 28-apr-2013:

I realized that Y_letrec as defined above is very close to but not identical to the Z combinator as defined in Wikipedia. Per Wikipedia, the Z combinator and "call-by-value Y combinator" are the same thing, and it looks like that is indeed the thing that may be more commonly called the "applicative-order Y combinator."

So, what I have above is not the same as the applicative-order Y combinator as usually written, but there is almost certainly a sense in which they're related. Here's how I did the comparison:

Starting with:

Y_letrec = λf . (λx.x x) (λs . (λa . (f ((λx.x x) s)) a))

Apply the inner U:

Y_letrec = λf . (λx.x x) (λs . (λa . (f (s s)) a))

Apply the outer U:

Y_letrec = λf . (λs . (λa . (f (s s)) a)) (λs . (λa . (f (s s)) a))

Rename to match Wikipedia's definition of the Z combinator:

Y_letrec = λf . (λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v))

Compare this to Wikipedia's Z combinator:

Z        = λf . (λx . f (λv . ((x x) v))) (λx . f (λv . ((x x) v)))

The salient difference is where the function f is being applied. Does it matter? Are these two functions equivalent despite this difference?

Answer 1

Yes, it is an applicative-order Y combinator. Using U inside it is perfectly OK, I did it too (cf. fixed point combinator in lisp). Whether the usage of U to shorten code has a name or not, I don't think so. It's just an application of a lambda-term, and yes, it makes it clearer IMO too.

What does have a name, is eta-conversion, used in your code to delay evaluation under applicative order, where arguments' values must be known before functional application.

With U applied through and through and eta-reduction performed on your code ( (λa.(f (s s)) a) ==> f (s s) ), it becomes the familiar normal-order Y combinator - i.e. such that works under normal-order evaluation, where arguments' values aren't demanded before functional application, which might end up not needing them (or some of them) after all:

Y = λf . (λs.f (s s)) (λs.f (s s))

BTW the delaying can be applied in slightly different way,

Y_ = λf . (λx.x x) (λs.f (λa.(s s) a)) 

which also works under applicative-order evaluation rules.

What is the difference? let's compare the reduction sequences. Your version,

Y_ = λf . (λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v))

((Y_ f) a) = 
  = ((λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v))) a
  = (λv . (f (x x)) v) a    { x := (λx . (λv . (f (x x)) v)) }
  = (f (x x)) a
  = | ; here (f (x x)) application must be evaluated, so 
    | ; the value of (x x) is first determined
    | (x x) 
    | = ((λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v))) 
    | = (λv . (f (x x)) v)     { x := (λx . (λv . (f (x x)) v)) }

and here f is entered. So here too, the well-behaved function f receives its first argument and it's supposed not to do anything with it. So maybe the two are exactly equivalent after all.

But really, the minutia of lambda-expressions definitions do not matter when it comes to the real implementation, because real implementation language will have pointers and we'll just manipulate them to point properly to the containing expression body, and not to its copy. Lambda calculus is done with pencil and paper after all, as textual copying and replacement. Y combinator in lambda calculus only emulates recursion. True recursion is true self-reference; not receiving copies equal to self, through self-application (however smart that is).

TL;DR: though language being defined can be devoid of such fun stuff as assignment and pointer equality, the language in which we define it will most certainly have those, because we need them for efficiency. At the very least, its implementation will have them, under the hood.

see also: fixed point combinator in lisp , esp. In Scheme, how do you use lambda to create a recursive function?.