Note that with the standard representation of natural numbers in lambda calculus, the Church numerals [1], you don't even need the Y combinator to implement factorial:
fac = λn.λf.n(λf.λn.n(f(λf.λx.n f(f x))))(λx.f)(λx.x)
For example, applied to Church numeral 3 this gives (with F=(λf.λn.n(f(λf.λx.n f(f x))))):
Hey tromp, do you have any recommendations for grokking Lambda calculus properly?
I've read a few tutorials and introductions, and I understand the notions of alpha- and beta-reductions, abstractions vs application, but I still have issues with practical examples like the above.
Am I missing something here or should I just go back to the basics?
Have you tried actually implementing things with it? You're obviously not going to implement a web browser, but basic math, some sort of basic strings, lots of other things with a focus on "basic" because even with functions you're working at an awfully low level here?
You can read definitions and commentary on those definitions until the cows come home but until you actually use it you're not going to get it. Like most math.
> I still have issues with practical examples like the above.
What issues would those be? Do you see that λf.λx.n f(f x)) is the Church numeral n+1 ?
I think there's few better ways to grok lambda calculus than working through examples like these step-by-step.
[1] https://en.wikipedia.org/wiki/Church_encoding