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?

Cassatt

As I recall, applicative order is constrasted with normal order. In applicative order languages such as Scheme arguments are evaluated right away, before the function gets to see them. This makes defining a Y-combinator complicated. In normal order, as in traditional lambda calculus, parameters are passed around and only evaluated when there is no other option. Y-combinators are simpler in normal order e.g. Hindley and Seldin p. 34. – Witter

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

Humfrid

Thanks very much. Is there a reason to prefer one form over the other? I ended up at mine after a lot of exploration and tinkering, and I was surprised when I figured out it wasn't truly identical. – Cassatt

there's one small difference in the reduction sequence. Your version is actually better I think, it ensures the reduction stops; the usual will proceed one step further and stop if f behaves as expected. – Humfrid

the additions to 2nd version in history have relevant derivation. (although, there's still the error about U being a delaying device - it isn't; only eta-expansion is). I can dig it out and add to the answer here. – Humfrid

ah, I know what I meant - when calculating (Y_ f), (not ((Y_ f) a)), your version stops sooner by one reduction step, and it stops by itself, without going into f. The standard def will end up applying (λs.f (λa.(s s) a)) (λs.f (λa.(s s) a)) == f (λa.(s s) a) { s := (λs.f (λa.(s s) a)) } and it enters into f definition. So the standard def is too eager; yours is properly lazy. Congrats! – Humfrid