I am now reading Types and Programming Languages, and I’ve been trying to wrap my head around the Y combinator and why it works. This is how I explained it to myself:
We want to define a recursive function, which means the function should be able to refer to itself. Unfortunately, Lambda calculus does not give us this option, so we define a function of the form:
Where is some reduced version of . In order for this thing to be a recursion, we need to find a parameter for which:
We notice that is a fixed point of by definition, hence the name fixed point combinators. We also notice that it must be a function of (otherwise it’s a constant and we can show trivially that it doesn’t work, duh), so we can write:
Cool. Now we are looking for such that:
Hmmm… Ok. Let’s try to name and pass it as a parameter to , will that work?
This sucks. After our change we no longer need to pass to , but :
Fortunately, can easily express using our bound variable as ! So if we write:
We can see that the Y combinator as we defined it is a fixed point of the function , just like we wanted.
Great success :)
I ignored reduction rules for the sake of simplicity, but it’s interesting to note that the book talks about another type of fixed point combinator, which should be used under different reduction rules:
I wonder how many fixed points has under each set of reduction rules.