1

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?

user3578468
  • 1,371
  • The main things to "understand" about Y combinator is that there is a lambda expression $Y$ such that for every lambda expression $F$, that $YF$ is a fixed point of $F$, that is $F(YF) = YF$. There are several lambda expressions $Y$ that have this property, it is usually easier to express them in terms of combinators. It can be pretty complicated when you try to follow reasoning on how to find a $Y$ expression, but once you've found it, the important thing is to be able to verify the fixed point property, which is just a straightforward evaluation of $F(YF)$. – DanielV May 16 '16 at 01:28

1 Answers1

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$.

Berci
  • 90,745