Really excellent work on this. When I saw the initial version, I went ahead and made a stub for Y combinator, admittedly for humor reasons, but perhaps something about some of the combinators would be nice. :) -- EdwardOConnor
When this article talks about renaming formal arguments:
(λ x. λ y. y x) (λ x. y) to λ z. z (λ x. y)
It doesn't make sense to me.
- It's an information loss, because we don't know what z is.
- It conflicts with the discussion about normal forms, since then any expression can be transformed to another one just by calling it λ z. z.
But it is a very interesting topic, and I'm certainly learning from this page. -- forgotten gentleman
Maybe there should be a note that this is the untyped lambda calculus, and that there are also several typed lambda calculi.