Understanding the Y combinator
Lambda calculus (λ-calculus) is a mathematical system for computation based on function abstraction and application, using variable binding and substitution.1
A lambda term is just a valid expression in the lambda calculus system. Well, what makes an expression valid? The following 3 rules are used to determine if a lambda expression is valid:
There is also eta reduction (η-reduction), which expresses the idea of extensionality,2 which applied to this context establishes that two functions are the same if and only if they give the same result for all arguments.
Later we will also mention the opposite of the beta reduction, the beta abstraction, which instead of simplifying an expression, it adds an extra function call that might be useful (e.g. in Lisps) for delaying the evaluation of the arguments.
Some of these look a bit confusing to me, specially when embedding expressions in text, so I will try to make each expression as readable as possible.
