the Lambda Calculus is often taught or presented in ways that are kind of weird and mysterious, with things like the Y combinator as some magical "look at this weird magic! i'm a wizard!" kind of thing
so i want to demystify the Y combinator
Replies:
9
lets start by looking at the problem. lets suppose we have some flavor of lambda calculus. im going to use something that looks like haskell. and we define factorial like so:
fac = \n -> if n == 0 then 1 else n * fac (n - 1)
this is a perfectly fine definition of factorial, but it relies on having a primitive notion of named functions. what if we want to avoid that. can we some how come up with a mechanism for getting the same effect?
maybe!
but only maybe. we have to do some calculations
lets observe, first, that we can factor out the recursive occurrence like so:
fac = (\r -> \n -> if n == 0 then 1 else n * r (n - 1)) fac
and now let's abbreviate like so:
F := \r -> \n -> if n == 0 then 1 else n * r (n - 1)
this is just an abbreviation for us while writing, it's not a part of the program
so we have an equivalence here now that looks like this:
fac ~ F fac
im writing ~ because i don't actually want to define it to be _equal_, since that definitional equality requires recursion which we're trying to avoid
we just want the equivalence to hold
so we want these two things to be equal, and we want somehow achieve this using only the non-recursive components available to us
how can things be equal in the lambda calculus?
either 1) they're syntactically just the same, modulo choices of bound variables...
or 2) they both reduce in 0 or more steps to (1)
for simplicity, lets ignore reductions of non-lambda terms, because lambdas are the only meaningfully interesting computation here
so what does this actually mean?
it means the definition of fac, whatever we end up with, has to lambda-beta-reduce zero or more times to produce the same thing that F fac reduces to
so let's make a guess
this is whole game is about making guesses with our options so lets make a guess
lets guess that `fac` reduces to `F fac`, rather than both reducing to some common thing by different means
if so, the `fac` has to be of the form `M N` for some lambda M and some expression N of whatever form
that is to say, M := \x -> M' for some M'
