(self self) call inside the let statement, in strict language

Question

I am currently, going through this article on Y-combinator by Mike Vanier.
Along the way of Y-combinator derivation, this code:

(define (part-factorial self)
  (lambda (n)
    (if (= n 0)

      1
      (* n ((self self) (- n 1))))))

((part-factorial part-factorial) 5) ==> 120
(define factorial (part-factorial part-factorial))
(factorial 5) ==> 120

is worked out to:

(define (part-factorial self)
  (let ((f (self self)))
    (lambda (n)
      (if (= n 0)
        1
        (* n (f (- n 1)))))))

(define factorial (part-factorial part-factorial))
(factorial 5) ==> 120

After that, article states:

This will work fine in a lazy language. In a strict language, the (self self) call in the let statement will send us into an infinite loop, because in order to calculate (part-factorial part-factorial) (in the definition of factorial) you will first have to calculate (part-factorial part-factorial) (in the let expression).

and then reader is challenged:

For fun: figure out why this wasn't a problem with the previous definition.

It seems to me I've figured out why, though I would like to confirm that:

1. I am correct in my understanding.
2. I don't miss any critical points, in my understanding.

My understanding is: in the first code snippet (self self) call won't result into infinite loop, because it is contained (wrapped) into lambda as a part-factorial function, and thus evaluated to lambda (n) until the call to (self self) is actually made, which happens only for n > 0. Thus, after (= n 0) evaluates to #t, there is no need in calling (self self).

Answer 1

Yes, that's the right answer. And indeed this trick (wrapping something that would otherwise recurse in a lambda) is critical when defining Y for applicative-order languages, which I think his article talks about (it's a good article by the way).

Answer 2

Yes, the "let-over-lambda" in the second definition

(define (part-factorial self)
  (let ((f (self self)))        ; let above the
    (lambda (n)                    ; lambda
      (if (= n 0)
        1
        (* n (f (- n 1)))))))

causes the application (self self) to be triggered before the (lambda (n) ...) can be returned.

This suggests another way to avoid the looping: put the problematic self-application itself behind its own lambda:

(define (part-factorial self)
  (let ((f (lambda (a) ((self self) a))))
    (lambda (n)
      (if (= n 0)
        1
        (* n (f (- n 1)))))))

and now this works, too. It is known as "eta-expansion" (or "eta-conversion" in general, as its dual is "eta-contraction").

This way is what's actually used in the usual "applicative-order Y-combinator" definition.

In the first definition the (self self) application is only triggered when its result is actually needed — but the cost to it is that we had to write it in a somewhat "unnatural" style, which is in any case different from what we'd like to write, i.e. just use f to refer to the function which is somehow made recursive for us behind the scenes.

With the explicit self-application the burden is on us, and we humans are known to err. To err is human, after all, as to forgive — Divine; but our computers are not at that all-forgiving stage quite yet.

So, this is the why of Y. To let us write it straight, without worries, with the details factored out and abstracted safely away.

And the burden of explicit self-application shall be mentioned no more.