On the Y-Combinator in Lambda Calculus

Question

I am trying to follow this explanation on the Y-combinator

Fairly at the beginning the author shows this function definition and claims that stepper(stepper(stepper(stepper(stepper()))) (5) were equal to factorial(5).

stepper = function(next_step)
             return function(n)
                       if n == 0 then
                          return 1
                       else
                          return n * next_step(n-1)
                       end
                    end
          end

I have translated this into (enriched) lambda syntax to the best of my understanding as follows: $\renewcommand{\l}{\lambda} \renewcommand{\t}{\text}$

for $2!$

$((\l f. \l n.\ (\t{zero})\ \overline{n}\ \overline{1}\ \overline{n} \times f\ (\overline{n} - 1))\ (\l f. \l n.\ (\t{zero})\ \overline{n}\ \overline{1}\ \overline{n} \times f\ (\overline{n} - 1)))\ \overline{2}$ $\longrightarrow (\l n.\ (\t{zero})\ \overline{n}\ \overline{1}\ \overline{n} \times (\l f. \l n.\ (\t{zero})\ \overline{n}\ \overline{1}\ \overline{n} \times f\ (\overline{n} - \overline{1}))\ (\overline{n} - 1))\ \overline{2}\ $ $\longrightarrow (\t{zero})\ \overline{2}\ \overline{1}\ \overline{n} \times (\l f. \l n.\ (\t{zero})\ n\ \overline{1}\ \overline{n} \times f\ (\overline{n} - 1))\ (\overline{2} - \overline{1}) $ $\longrightarrow \overline{n} \times (\l f. \l n.\ (\t{zero})\ \overline{n}\ \overline{1}\ \overline{n} \times f\ (\overline{n} - \overline{1}))\ (\overline{2} - \overline{1}) $

Here is the problem now. If I apply $(\overline{2} - \overline{1})$ now it gets inserted into $f$, which makes no sense. So, should the call

stepper(stepper(stepper(stepper(stepper()))) (5)

not also have an initial argument for the innermost stepper()-call? The author claims the code to work correctly, so what am I missing here, please?

Answer 1

Well, assuming that $n$ will reach $0$ while we get to the innermost stepper function, that would allow us to input anything as next_step is not used then. (Probably nil is passed this way to the function.)

Now stepper() is a function that basically expects the input 0 and returns 1.

The next step is stepper(stepper()) which inputs n and returns n * stepper()(n-1), i.e. if n happens to be 1 now, it returns 1.

Following this logic, the given 5-fold stepper function seems to expect the input 4, so there is a mistake in any case. Maybe if n==1 was rather meant, or just missed one more stepper.

Indeed, it would be clearer if e.g. this innermost input would be something like $\lambda x.1$.