Maybe there should be a note that this is the untyped lambda calculus, and that there are also several typed lambda calculi. |
(λ 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