Def x! == ifx=0 1 elsex(x-1)! fi (recursive)

Observe that the operator *n*!"

The computational basis of Nuprl's semantics is an untyped calculus, which includes the *x*.*b*(*x*)"*f*(*a*)"

Thus, we can build the computational fixed-point "combinator"

Def Y( f) == (x.f(x(x)))(x.f(x(x)))

Now, observe how *x*.*f*(*x*(*x*)))(*x*.*f*(*x*(*x*)))

( x.f(x(x)))(x.f(x(x))) *f((x.f(x(x)))(x.f(x(x))))

One step of computation stuffs the whole original term into the argument place of an application of *f**f**x*.*f*(*x*(*x*)))(*x*.*f*(*x*(*x*)))*f**f*.(*x*.*f*(*x*(*x*)))(*x*.*f*(*x*(*x*)))

Y == f.(x.f(x(x)))(x.f(x(x)))

Normally, we display such definitions using applications to the variable on the lefthand side instead of using the abstraction operator on the right hand side, which comports better with standard mathematical practice: *f*) == (*x*.*f*(*x*(*x*)))(*x*.*f*(*x*(*x*)))

With this definition in place, we can rewrite *f*)

Y( f) * (x.f(x(x)))(x.f(x(x))) *f((x.f(x(x)))(x.f(x(x)))) *f(Y(f))

Eliding intermediate steps pointedly demonstrates the fixed-pointedness *f*) * *f*(Y(*f*))

About: