Now, let's see how to exploit Y(f) *f(Y(f)) to express recursive function definitions, which are not primitive in Nuprl. A general form of a one-place recursive function definition would be
f(z) == G(z; x.f(x))
which indicates that in evaluating f(z), not only does the function G(z; x.f(x)) have access to the argument z that was supplied in f(z), but also it may further apply function f(x) to any new arguments at all; thus, recursive calls to f(x) may be made, for various values of x, as part of evaluating f(z).
However, in Nuprl, such recursive definitions are not built-in, they are not primitives. The primitive Operator Definitions of Nuprl must not use the defined operator in its own expansion. So, how do we implement "f(z) == G(z; x.f(x))"?
f(z) == Y((h,z. G(z; x.(h(x)))),z)
Notice that in this definition, the operator f(?) does not occur on the right hand side, so the definition is an ordinary one, rather than a recursive one. The recursive "behavior" is a result of using the Y-combinator, as illustrated below. Note that we're not just looking at Y applied to one argument "h,z. G(z; x.(h(x)))" but its further application to another argument u in order to see how f(u) would be evaluated (recall that "g(x,y)" means "(g(x))(y)"; see Multi-Argument Functions).
Further evaluation depends upon how G(?; x.?) is evaluated. Observe that "Y(h,z. G(z; x.(h(x))))" has been replicated down inside of the instance of G(?; x.?), and that how it gets further applied is up to G(?; x.?).
Returning to our definition of factorial, introduced in Recursive Functions,
is actually an improved representation of the actual content of the definition, which is:
x! == Y((sfa_doc_factorial,x. if x=0 1 else xsfa_doc_factorial(x-1) fi),x)
The recursive form was entered by the user, and this primitive form was automatically generated and stored as the "official" definition. The variable name "sfa_doc_factorial" was selected automatically by the system, using the name assigned to this factorial operator by its creator (sfa).
Note: Although we type applications of Y to functions, as we did for Thm*x:. x! , we don't assign Y itself a function type. For a discussion of how this could be accomplished see Typing Y.
f(Y(f))
h,z. G(z; x.(h(x)))),z)
0
1 else x
(x-1)! fi (recursive)
x:
. x! 
