Understanding Applicative Evaluation Order with the Z-Combinator

Question

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) 
 = 3 * ((lambda n : 1 if n == 0 else n * (lambda z : Y factorial_ z)(n-1)) 2)
 -> 3 * 2 * ((lambda z : Y factorial_ z)(2-1))
 -> 3 * 2 * (Y factorial_ 1)
 = 3 * 2 * ((lambda n : 1 if n == 0 else n * (lambda z : Y factorial_ z)(n-1)) 1)
 -> 3 * 2 * 1 * ((lambda z : Y factorial_ z)(1-1))
 -> 3 * 2 * 1 * (Y factorial_ 0)
 = 3 * 2 * 1 * ((lambda n : 1 if n == 0 else n * (lambda z : Y factorial_ z)(n-1)) 0)
 -> 3 * 2 * 1 * 1
 -> 6

But when I run

Y = lambda f : (lambda x : f( lambda z: x(x) (z) )) (lambda x : f(x(x)))
factorial_ = lambda f : lambda n : 1 if n == 0 else n * f(n-1)
factorial = Y(factorial_)
print(factorial(3))

I still get the infinite recursion problem:

Y = lambda f : (lambda x : f( lambda z: x(x) (z) )) (lambda x : f(x(x))) [Previous line repeated 994 more times] RecursionError: maximum recursion depth exceeded

So I must not actually have performed correct applicative order on my manual derivation, otherwise I would have gotten infinite recursion like Python gets.

What am I missing here about how applicative order works?

EDIT:

To reiterate:

Let's say I name that version of Y Z':

Let $Z' = \lambda f. \lambda x( f ( \lambda z. x x z)) (\lambda x. f( xx))$

Let $F' = \lambda f. \lambda n. 1 \text{ if } n = 0 \text{ else } n*f(n-1)$ $$ \text{Let } F = Z' F' = (\lambda f . (\lambda x . f( \lambda z . x x z) (\lambda x . f(x x)) F'$$ $$\longrightarrow (\lambda x . F'(\lambda z . x x z)) (\lambda x . F'(x x))$$ $$\longrightarrow F'(\lambda z . (\lambda x . F'(x x)) (\lambda x . F'(x x)) z)$$ Lambda-Abstraction for $F'$
$$= F'(\lambda z . (\lambda f (\lambda x . f(x x)) (\lambda x . f(x x))) F' z)$$ Per definition of $Z'$ $$= F'(\lambda z . Z' F' z)$$

Now applying $F$ to some number:

$$F~ 3 = (\lambda n . 1 \text{ if } n = 0 \text{ else } n * (\lambda z . Z' F' z)(n-1)) 3$$

$$\longrightarrow 3 * (\lambda z . Z' F' z)(3-1) $$

$$\longrightarrow 3 * (Z' F' 2) $$ $$= 3 * ((\lambda n . 1 \text{ if } n = 0 \text{ else } n * (\lambda z . Z' F' z)(n-1)) 2) $$ $$\longrightarrow 3 * 2 * ((\lambda z . Z' F' z)(2-1))$$ $$\longrightarrow 3 * 2 * (Z' F' 1)$$ $$= 3 * 2 * ((\lambda n . 1 \text{ if } n = 0 \text{ else } n * (\lambda z . Z' F' z)(n-1)) 1)$$ $$\longrightarrow 3 * 2 * 1 * ((\lambda z . Z' F' z)(1-1))$$ $$\longrightarrow 3 * 2 * 1 * (Z' F' 0)$$ $$= 3 * 2 * 1 * ((\lambda n . 1 \text{ if } n = 0 \text{ else } n * (\lambda z . Z' F' z)(n-1)) 0)$$ $$\longrightarrow 3 * 2 * 1 * 1$$ $$\longrightarrow 6$$

So, why did this work? It was supposed to go into infinite recursion. What is my mistake?

• chi: Your "Per definition of Z′" step is wrong: that would result in $F′(\lambda z.Y F′ z)$ since you lack a $\lambda z$ to use $Z'$ instead (you'd need another $\lambda z$ in the first $\lambda x.f(xx)$ part, which should be $\lambda x.f(\lambda z. xxz)$). And indeed that's the point! Your $Z'$ "recurses" into $Y$ instead of $Z'$ itself.
• lo tolmencre: Ouh! Yes now I see it. What a silly mistake. Thanks!
• chi: I think it helps noting that both $Y$ and $Z$ manage to achieve recursion using a self-application of the form $MM$ where the first $M$ takes the second one as argument (say $x$), and computes $xx$ which is $MM$ again, hence recursing. If you use $MN$ instead, you end up with $NN$ so you do not start again from the beginning, but from something else. In your case, it happened that $NN$ was, essentially, $Yf$.

Answer 1

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)))

• lo tolmencre: But when we split Y into X and M the f in M won't be the same as the f in X, will it? The free f in M will be alpha-converted so as to not conflict with the bound f in X, will it not?
• lo tolmencre: Why do you write Y(f) = (lambda x : f( lambda z: x(x) (z) )) M? I thought you wanted to use X instead of Y. And even X f would not be (lambda x : f( lambda z: x(x) (z) )) M. Sorry, that part confuses me. Can you add some more explanation to it?
• lo tolmencre: "However, M(M) above is exactly the non terminating Y(f). The additional lambda z: disappears after the first recursive call." I am aware that that is what needs to happen. But I don't see where I made a mistake in my derivation.
• lo tolmencre: I edited my question to with some easier to read math.
• chi: @lotolmencre Actually, it won't be alpha-converted. But anyway, M is not important here: just pretend that the f in M is that one bound in the definition of X. (You are right in that I should have used X(f)! Hopefully I fixed that now)