A nice way to think about eta-reduction is that it asserts something about the types of expressions in lambda calculus, namely that every expression is in fact a function.
If an expression M can appear in the left position of the function application operation, this implies that M is a function.
By way of analogy, if I have a formula x == x+0, this implies that x is a number.
Or, s == s + '' would imply that s is a string.
So, if M == lambda x. M(x), this is saying that M is a function.
If an expression M can appear in the left position of the function application operation, this implies that M is a function.
By way of analogy, if I have a formula x == x+0, this implies that x is a number.
Or, s == s + '' would imply that s is a string.
So, if M == lambda x. M(x), this is saying that M is a function.