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