How to get from factorial to a y-combinator?

In one of his conference talks Jim Weirich derives the applicative form of the y-combinator by refactoring a partial definition of factorial. The starting point in his talk is different than what follows here but the ideas are all the same.

# partial definition of factorial
f = \g -> \x -> x == 1 ? 1 : x * g(g)(x - 1)
# factorial = f(f)

Notice that we never name something simultaneously on the LHS and the RHS, i.e. there is no recursion. With the above starting point getting to a y-combinator is pretty simple

# first factor out g(g)(x - 1)
\g -> (\h -> \x -> x == 1 ? 1 : x * h(x - 1))(\y -> g(g)(y))
# next factor out \h -> \x -> ...
(\f -> \g -> f(\y -> g(g)(y)))(\h -> \x -> x == 1 ? 1 : x * h(x - 1))

Now if you look at the function that is being applied to the partial definition of factorial

\f -> \g -> f(\y -> g(g)(y))

we just need to apply it to itself after applying it to a partial definition of factorial to get the full factorial. Spelling that out with lambdas gives us

y = \p -> (\h -> h(h))((\f -> \g -> f(\y -> g(g)(y))(p))

It is still pretty incomprehensible standing on its own but deriving it from the partial definition of factorial makes sense to me. One problem I have with it though is that you somehow have to guess the expression g(g) and it is not at all clear why. Let's say we start with the recursive definition of factorial

factorial = \x -> x == 1 ? 1 : x * factorial(x - 1)

The obvious thing to do if you can't refer to the name of the function within the body of the function is to try to abstract it

factorial = (\g -> \x -> x == 1 ? 1 : x * g(x - 1))(factorial)

The problem is that this is a dead end. I don't see how you can guess that the right thing to do is to factor g(x - 1) into g(g)(x - 1) and start the chain of reasoning at the top of this post. In his talk Jim Weirich does the equivalent of what I did by basically pulling g(g) out of a hat.

So the question is does anyone know a motivating reason for why the proper placeholder in the partial definition of factorial is g(g)(x - 1)?

• – Petr Pudlák Nov 2 '14 at 16:07
• @PetrPudlák Thanks, that's a really good answer and gives a pretty good heuristic for how g(g) comes about from informal reasoning about the recursive definitions. – davidk01 Nov 2 '14 at 21:57