Understanding Applicative Evaluation Order with the Z-Combinator

I am trying to understand how the Z-combinator (Y-combinator for applicative order languages) definition came about. As Python is applicative I am using Python for this.

So I know Python's evaluation order is applicative. But I seem to be overlooking something in how applicative order works. To compensate for applicative evaluation order I reasoned to build a Y-combinator that does not dive off into infinite recursion it would be sufficient to write it like this:

Y = lambda f : (lambda x : f( lambda z: x(x) (z) )) (lambda x : f(x(x)))

I arrived at this conclusion by first manually deriving Y g like so

Y g =  (lambda f : (lambda x : f(x x)) (lambda x : f(x x))) g      # Definition of Y
    -> (lambda x : g(x x)) (lambda x : g(x x))                   # beta reduction
    -> g((lambda x : g(x x)) (lambda x : g(x x)))                # beta reduction
    -> g((lambda f : (lambda x : f(x x)) (lambda x : f(x x))) g) # lambda abstraction
    =  g(Y g)                                                    # put in Y

And then working my way backwards like this, adding in a lambda abstraction hat would delay the recursion until a value is passed in:

= g(lambda z : Y g z)                                                   
    =  g(lambda z : (lambda f (lambda x : f(x x)) (lambda x : f(x x))) g z) 
    -> g(lambda z : (lambda x : g(x x)) (lambda x : g(x x)) z)         
    -> (lambda x : g(lambda z : x x z)) (lambda x : g(x x))            
Y g =  (lambda f : (lambda x : f( lambda z : x x z)) (lambda x : f(x x))) g

When I manually evaluate factorial 3 where

factorial_ = lambda f : lambda n : 1 if n == 0 else n * f(n-1)

factorial = Y(factorial_)

in applicative order I get

```
factorial 3 = (lambda n : 1 if n == 0 else n * (lambda z : Y factorial_ z)(n-1)) 3
-> 3 * (lambda z : Y factorial_ z)(3-1)
-> 3 * (Y factorial_ 2)

Let's call your proposal X, instead:

X = lambda f : (lambda x : f( lambda z: x(x) (z) )) (lambda x : f(x(x)))

For convenience, we can rewrite it as

M = (lambda x : f(x(x)))    # depends on f
X = lambda f : (lambda x : f( lambda z: x(x) (z) )) M

Now, when we invoke X(f), we get

X(f) =
(lambda x : f( lambda z: x(x) (z) )) M =
f( lambda z: M(M) (z) )

Assume f "recurses", invoking its argument with some value, e.g. 5. Its code might look as

c = M(M)(5)
do something with c
return something

However, M(M) above is exactly the non terminating Y(f). The additional lambda z: disappears after the first recursive call.

In order to prevent that, we need to add lambda z: inside M as well. Hence we get the actual Z combinator:

Z = lambda f : (lambda x : f( lambda z: x(x) (z) )) (lambda x : f(lambda z: x(x) (z)))

StackExchange Computer Science Q#88903, answer score: 2